Try to fix encapsulation

[satune.git] / src / csolver.h

diff --git a/src/csolver.h b/src/csolver.h
index d611e1d894faeab1947668350c710655ba1d3a90..aaf3b3064f744bd7b49c7441af83da9fe8b67984 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -9,36 +9,7 @@ class CSolver {
        CSolver();
        ~CSolver();
        
-       SATEncoder *satEncoder;
-       bool unsat;
-       Tuner *tuner;
-       
-       /** This is a vector of constraints that must be satisfied. */
-       HashSetBoolean constraints;
-
-       /** This is a vector of all boolean structs that we have allocated. */
-       Vector<Boolean *> allBooleans;
-
-       /** This is a vector of all set structs that we have allocated. */
-       Vector<Set *> allSets;
-
-       /** This is a vector of all element structs that we have allocated. */
-       Vector<Element *> allElements;
-
-       /** This is a vector of all predicate structs that we have allocated. */
-       Vector<Predicate *> allPredicates;
-
-       /** This is a vector of all table structs that we have allocated. */
-       Vector<Table *> allTables;
-
-       /** This is a vector of all order structs that we have allocated. */
-       Vector<Order *> allOrders;
-
-       /** This is a vector of all function structs that we have allocated. */
-       Vector<Function *> allFunctions;
-
        /** This function creates a set containing the elements passed in the array. */
-
        Set *createSet(VarType type, uint64_t *elements, uint num);
 
        /** This function creates a set from lowrange to highrange (inclusive). */
@@ -130,7 +101,58 @@ class CSolver {
 
        HappenedBefore getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
 
+       void setUnSAT() { unsat = true; }
+
+       bool isUnSAT() { return unsat; }
+
+       Vector<Order *> * getOrders() { return & allOrders;}
+
+       Tuner * getTuner() { return tuner; }
+
+       HSIteratorBoolean * getConstraints() { return constraints.iterator(); }
+
+       SATEncoder * getSATEncoder() {return satEncoder;}
+
+       void replaceBooleanWithTrue(Boolean *bexpr);
+       void replaceBooleanWithFalse(Boolean *bexpr);
+       void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb);
+
+       
        MEMALLOC;
-};
 
+ private:
+       void handleXORFalse(BooleanLogic *bexpr, Boolean *child);
+       void handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child);
+       void handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child);
+       void handleANDTrue(BooleanLogic *bexpr, Boolean *child);
+       void handleORFalse(BooleanLogic *bexpr, Boolean *child);
+
+       /** This is a vector of constraints that must be satisfied. */
+       HashSetBoolean constraints;
+
+       /** This is a vector of all boolean structs that we have allocated. */
+       Vector<Boolean *> allBooleans;
+
+       /** This is a vector of all set structs that we have allocated. */
+       Vector<Set *> allSets;
+
+       /** This is a vector of all element structs that we have allocated. */
+       Vector<Element *> allElements;
+
+       /** This is a vector of all predicate structs that we have allocated. */
+       Vector<Predicate *> allPredicates;
+
+       /** This is a vector of all table structs that we have allocated. */
+       Vector<Table *> allTables;
+
+       /** This is a vector of all order structs that we have allocated. */
+       Vector<Order *> allOrders;
+
+       /** This is a vector of all function structs that we have allocated. */
+       Vector<Function *> allFunctions;
+
+       SATEncoder *satEncoder;
+       bool unsat;
+       Tuner *tuner;
+};
 #endif