Renaming

[satune.git] / src / csolver.h

diff --git a/src/csolver.h b/src/csolver.h
index 7939ee516f7fae5ea24c73311929e7c635b7e8bd..a37434cf3e86bc39d3c209aeda7f99a5f6d6fb1c 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -1,8 +1,9 @@
 #ifndef CSOLVER_H
 #define CSOLVER_H
-#include "classlist.h"
+#include "classes.h"
 #include "ops.h"
-#include "structs.h"
+#include "corestructs.h"
+#include "asthash.h"
 
 class CSolver {
 public:
@@ -37,6 +38,10 @@ public:
        /** This function creates an element constrant. */
        Element *getElementConst(VarType type, uint64_t value);
 
+       Boolean *getBooleanTrue();
+
+       Boolean *getBooleanFalse();
+       
        /** This function creates a boolean variable. */
 
        Boolean *getBooleanVar(VarType type);
@@ -109,7 +114,7 @@ public:
 
        Tuner *getTuner() { return tuner; }
        
-       HSIteratorBoolean *getConstraints() { return constraints.iterator(); }
+       SetIteratorBoolean *getConstraints() { return constraints.iterator(); }
 
        SATEncoder *getSATEncoder() {return satEncoder;}
 
@@ -117,14 +122,14 @@ public:
        void replaceBooleanWithFalse(Boolean *bexpr);
        void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb);
        CSolver *clone();
-       void autoTune();
+       void autoTune(uint budget);
 
        void setTuner(Tuner * _tuner) { tuner = _tuner; }
        long long getElapsedTime() { return elapsedTime; }
        long long getEncodeTime();
        long long getSolveTime();
        
-       MEMALLOC;
+       CMEMALLOC;
 
 private:
        void handleXORFalse(BooleanLogic *bexpr, Boolean *child);
@@ -157,10 +162,17 @@ private:
        /** This is a vector of all function structs that we have allocated. */
        Vector<Function *> allFunctions;
 
+       Boolean * boolTrue;
+       Boolean * boolFalse;
+       
+       /** These two tables are used for deduplicating entries. */
+       BooleanMatchMap boolMap;
+       ElementMatchMap elemMap;
+       
        SATEncoder *satEncoder;
        bool unsat;
        Tuner *tuner;
-
+       
        long long elapsedTime;
 };
 #endif