+ SetIteratorBooleanEdge *getConstraints() { return constraints.iterator(); }
+
+ SATEncoder *getSATEncoder() {return satEncoder;}
+
+ void replaceBooleanWithTrue(BooleanEdge bexpr);
+ void replaceBooleanWithTrueNoRemove(BooleanEdge bexpr);
+ void replaceBooleanWithFalse(BooleanEdge bexpr);
+ void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
+ CSolver *clone();
+ void serialize();
+ static CSolver* deserialize(const char * file);
+ void autoTune(uint budget);
+
+ void setTuner(Tuner *_tuner) { tuner = _tuner; }
+ long long getElapsedTime() { return elapsedTime; }
+ long long getEncodeTime();
+ long long getSolveTime();
+
+ CMEMALLOC;
+
+private:
+ void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child);
+ void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child);
+
+ //These two functions are helpers if the client has a pointer to a
+ //Boolean object that we have since replaced
+ BooleanEdge rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);
+ BooleanEdge doRewrite(BooleanEdge b);
+ /** This is a vector of constraints that must be satisfied. */
+ HashsetBooleanEdge 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;
+
+ HashsetOrder activeOrders;
+
+ /** This is a vector of all function structs that we have allocated. */
+ Vector<Function *> allFunctions;
+
+ BooleanEdge boolTrue;
+ BooleanEdge boolFalse;
+
+ /** These two tables are used for deduplicating entries. */
+ BooleanMatchMap boolMap;
+ ElementMatchMap elemMap;
+
+ SATEncoder *satEncoder;
+ bool unsat;
+ Tuner *tuner;
+ long long elapsedTime;
+};