Interface should be bool, not happenedbefore

[satune.git] / src / csolver.h

diff --git a/src/csolver.h b/src/csolver.h
index 00abc666d7eb3f0df4a33906ecd917103816b10b..8f5d6975b5062bbc5245cf0186d1b1bc955937f5 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -4,6 +4,7 @@
 #include "ops.h"
 #include "corestructs.h"
 #include "asthash.h"
+#include "solver_interface.h"
 
 class CSolver {
 public:
@@ -18,7 +19,7 @@ public:
        Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
 
        Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
-               
+
        /** This function creates a mutable set. */
 
        MutableSet *createMutableSet(VarType type);
@@ -43,7 +44,7 @@ public:
        Boolean *getBooleanTrue();
 
        Boolean *getBooleanFalse();
-       
+
        /** This function creates a boolean variable. */
 
        Boolean *getBooleanVar(VarType type);
@@ -86,6 +87,14 @@ public:
 
        Boolean *applyLogicalOperation(LogicOp op, Boolean **array, uint asize);
 
+       /** This function applies a logical operation to the Booleans in its input. */
+
+       Boolean *applyLogicalOperation(LogicOp op, Boolean *arg1, Boolean *arg2);
+
+       /** This function applies a logical operation to the Booleans in its input. */
+
+       Boolean *applyLogicalOperation(LogicOp op, Boolean *arg);
+
        /** This function adds a boolean constraint to the set of constraints
            to be satisfied */
 
@@ -98,7 +107,7 @@ public:
        Boolean *orderConstraint(Order *order, uint64_t first, uint64_t second);
 
        /** When everything is done, the client calls this function and then csolver starts to encode*/
-       int startEncoding();
+       int solve();
 
        /** After getting the solution from the SAT solver, client can get the value of an element via this function*/
        uint64_t getElementValue(Element *element);
@@ -106,19 +115,20 @@ public:
        /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
        bool getBooleanValue(Boolean *boolean);
 
-       HappenedBefore getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
+       bool getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
 
        bool isTrue(Boolean *b);
        bool isFalse(Boolean *b);
-       
+
        void setUnSAT() { unsat = true; }
 
        bool isUnSAT() { return unsat; }
 
        Vector<Order *> *getOrders() { return &allOrders;}
+       HashsetOrder * getActiveOrders() { return &activeOrders;}
 
        Tuner *getTuner() { return tuner; }
-       
+
        SetIteratorBoolean *getConstraints() { return constraints.iterator(); }
 
        SATEncoder *getSATEncoder() {return satEncoder;}
@@ -129,11 +139,11 @@ public:
        CSolver *clone();
        void autoTune(uint budget);
 
-       void setTuner(Tuner * _tuner) { tuner = _tuner; }
+       void setTuner(Tuner *_tuner) { tuner = _tuner; }
        long long getElapsedTime() { return elapsedTime; }
        long long getEncodeTime();
        long long getSolveTime();
-       
+
        CMEMALLOC;
 
 private:
@@ -164,20 +174,21 @@ private:
        /** This is a vector of all order structs that we have allocated. */
        Vector<Order *> allOrders;
 
+       HashsetOrder activeOrders;
+       
        /** This is a vector of all function structs that we have allocated. */
        Vector<Function *> allFunctions;
 
-       Boolean * boolTrue;
-       Boolean * boolFalse;
-       
+       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