updated master to a working state

Author: jweede

include/config.h

@@ -53,6 +53,15 @@ int dX_printf (int , const char* , ...);
 #endif
  * ----------------- */
 
+#define D_E(x) { x }
+#define D_0(x) { x }
+
+#if _DEBUG_LVL_COMPILE >= 1
+# define D_1(x) { if ((DEBUG_LVL&15) >= 1) { x; } }
+#else
+# define D_1(x) {}
+#endif
+
 #if _DEBUG_LVL_COMPILE >= 2
 # define D_2(x) if ((DEBUG_LVL&15) >= 2) { x }
 # define D_2E(x) if ((DEBUG_LVL&15) == 2) { x }
@@ -63,6 +72,24 @@ int dX_printf (int , const char* , ...);
 # define DM_2(x) {}
 #endif
 
+#if _DEBUG_LVL_COMPILE >= 6
+# define D_6(x) if ((DEBUG_LVL&15) >= 6) { x }
+#else
+# define D_6(x) {}
+#endif
+
+#if _DEBUG_LVL_COMPILE >= 7
+# define D_7(x) if ((DEBUG_LVL&15) >= 7) { x }
+#else
+# define D_7(x) {}
+#endif
+
+#if _DEBUG_LVL_COMPILE >= 8
+# define D_8(x) if ((DEBUG_LVL&15) >= 8) { x }
+#else
+# define D_8(x) {}
+#endif
+
 #if _DEBUG_LVL_COMPILE >= 9
 # define D_9(x) if ((DEBUG_LVL&15) >= 9) { x }
 # define TB_9(x) D_9(if(ite_counters[NUM_BACKTRACKS]>=TRACE_START) { x }) 
@@ -77,11 +104,26 @@ int dX_printf (int , const char* , ...);
 # define D_C(x) {}
 #endif
 
+#define dE_printf1(x)        D_E(fprintf(stddbg, x);)
+#define dE_printf2(x1,x2)    D_E(fprintf(stddbg, x1, x2);)
+#define dE_printf3(x1,x2,x3) D_E(fprintf(stddbg, x1, x2, x3);)
+#define dE_printf4(x1,x2,x3,x4) D_E(fprintf(stddbg, x1, x2, x3,x4);)
+
 #define dC_printf1(x)        D_C(printf(x);)
 #define dC_printf2(x1,x2)    D_C(printf(x1, x2);)
 #define dC_printf3(x1,x2,x3) D_C(printf(x1, x2, x3);)
 #define dC_printf4(x1,x2,x3,x4) D_C(printf(x1, x2, x3,x4);)
 
+#define d0_printf1(x)        D_0(fprintf(stddbg, x);)
+#define d0_printf2(x1,x2)    D_0(fprintf(stddbg, x1, x2);)
+#define d0_printf3(x1,x2,x3) D_0(fprintf(stddbg, x1, x2, x3);)
+#define d0_printf4(x1,x2,x3,x4) D_0(fprintf(stddbg, x1, x2, x3,x4);)
+
+#define d1_printf1(x)        D_1(fprintf(stddbg, x);)
+#define d1_printf2(x1,x2)    D_1(fprintf(stddbg, x1, x2);)
+#define d1_printf3(x1,x2,x3) D_1(fprintf(stddbg, x1, x2, x3);)
+#define d1_printf4(x1,x2,x3,x4) D_1(fprintf(stddbg, x1, x2, x3,x4);)
+
 #define d2_printf1(x)        D_2(fprintf(stddbg, x);)
 #define d2_printf2(x1,x2)    D_2(fprintf(stddbg, x1, x2);)
 #define d2_printf3(x1,x2,x3) D_2(fprintf(stddbg, x1, x2, x3);)
@@ -100,6 +142,36 @@ int dX_printf (int , const char* , ...);
 
 #define dm2_printf2(x1,x2)    DM_2(fprintf(stddbg, x1, x2);)
 
+#define d6_printf1(x)        D_6(fprintf(stddbg, x);)
+#define d6_printf2(x1,x2)    D_6(fprintf(stddbg, x1, x2);)
+#define d6_printf3(x1,x2,x3) D_6(fprintf(stddbg, x1, x2, x3);)
+#define d6_printf4(x1,x2,x3,x4) D_6(fprintf(stddbg, x1, x2, x3,x4);)
+#define d6_printf5(x1,x2,x3,x4,x5) D_6(fprintf(stddbg, x1, x2, x3,x4,x5);)
+#define d6_printf6(x1,x2,x3,x4,x5,x6) D_6(fprintf(stddbg, x1, x2, x3,x4,x5,x6);)
+#define d6_printf7(x1,x2,x3,x4,x5,x6,x7) D_6(fprintf(stddbg, x1, x2, x3,x4,x5,x6,x7);)
+#define d6_printf8(x1,x2,x3,x4,x5,x6,x7,x8) D_6(fprintf(stddbg, x1, x2, x3,x4,x5,x6,x7,x8);)
+#define d6_printf9(x1,x2,x3,x4,x5,x6,x7,x8,x9) D_6(fprintf(stddbg, x1, x2, x3,x4,x5,x6,x7,x8,x9);)
+
+#define d7_printf1(x)        D_7(fprintf(stddbg, x);)
+#define d7_printf2(x1,x2)    D_7(fprintf(stddbg, x1, x2);)
+#define d7_printf3(x1,x2,x3) D_7(fprintf(stddbg, x1, x2, x3);)
+#define d7_printf4(x1,x2,x3,x4) D_7(fprintf(stddbg, x1, x2, x3,x4);)
+#define d7_printf5(x1,x2,x3,x4,x5) D_7(fprintf(stddbg, x1, x2, x3,x4,x5);)
+#define d7_printf6(x1,x2,x3,x4,x5,x6) D_7(fprintf(stddbg, x1, x2, x3,x4,x5,x6);)
+#define d7_printf7(x1,x2,x3,x4,x5,x6,x7) D_7(fprintf(stddbg, x1, x2, x3,x4,x5,x6,x7);)
+#define d7_printf8(x1,x2,x3,x4,x5,x6,x7,x8) D_7(fprintf(stddbg, x1, x2, x3,x4,x5,x6,x7,x8);)
+#define d7_printf9(x1,x2,x3,x4,x5,x6,x7,x8,x9) D_7(fprintf(stddbg, x1, x2, x3,x4,x5,x6,x7,x8,x9);)
+
+#define d8_printf1(x)        D_8(fprintf(stddbg, x);)
+#define d8_printf2(x1,x2)    D_8(fprintf(stddbg, x1, x2);)
+#define d8_printf3(x1,x2,x3) D_8(fprintf(stddbg, x1, x2, x3);)
+#define d8_printf4(x1,x2,x3,x4) D_8(fprintf(stddbg, x1, x2, x3,x4);)
+#define d8_printf5(x1,x2,x3,x4,x5) D_8(fprintf(stddbg, x1, x2, x3,x4,x5);)
+#define d8_printf6(x1,x2,x3,x4,x5,x6) D_8(fprintf(stddbg, x1, x2, x3,x4,x5,x6);)
+#define d8_printf7(x1,x2,x3,x4,x5,x6,x7) D_8(fprintf(stddbg, x1, x2, x3,x4,x5,x6,x7);)
+#define d8_printf8(x1,x2,x3,x4,x5,x6,x7,x8) D_8(fprintf(stddbg, x1, x2, x3,x4,x5,x6,x7,x8);)
+#define d8_printf9(x1,x2,x3,x4,x5,x6,x7,x8,x9) D_8(fprintf(stddbg, x1, x2, x3,x4,x5,x6,x7,x8,x9);)
+
 #define d9_printf1(x)        D_9(fprintf(stddbg, x);)
 #define d9_printf2(x1,x2)    D_9(fprintf(stddbg, x1, x2);)
 #define d9_printf3(x1,x2,x3) D_9(fprintf(stddbg, x1, x2, x3);)

include/log.h

@@ -46,7 +46,6 @@
 #include <sys/types.h>
 #include <sys/stat.h>
 #include <unistd.h>
-#include <signal.h>
 
 /* 
  * parameter types 

include/params.h

@@ -37,11 +37,7 @@
 
 #ifndef PROTOTYPES_H
 #define PROTOTYPES_H
-// this include and using stmt should be removed once move to scons is
-// complete.
-#include <sstream>
-#include <vector>
-using namespace std;
+
 
 double get_runtime();
 long get_memusage();
@@ -67,14 +63,6 @@ int splitXors();
 void countSingleXors(BDDNode *, int *, int *);
 int are_oppos(BDDNode *, BDDNode *);
 
-int build_algebraic_func(BDDNode* xdd, stringstream& ss);
-int GBReduceXors();
-vector<BDDNode*> build_BDDs_from_sage(stringstream& ss);
-BDDNode* parseXOR(string andstr);
-BDDNode* parseAND(string andstr);
-string strip_whitespace(string str);
-string strip_char(string str, char c);
-
 void SAT_to_CNF();
 void Smurfs_to_BDD();
 void Do_Lemmas();