-
- 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);
-
+ bool isBooleanVarUsed(){return booleanVarUsed;}
+ void printConstraint(BooleanEdge boolean);
+ void printConstraints();
+
+ Vector<Order *> *getOrders() { return &allOrders;}
+ HashsetOrder *getActiveOrders() { return &activeOrders;}
+
+ Tuner *getTuner() { return tuner; }
+
+ SetIteratorBooleanEdge *getConstraints() { return constraints.iterator(); }
+
+ SATEncoder *getSATEncoder() {return satEncoder;}
+
+ void replaceBooleanWithTrue(BooleanEdge bexpr);
+ void replaceBooleanWithTrueNoRemove(BooleanEdge bexpr);
+ void replaceBooleanWithFalseNoRemove(BooleanEdge bexpr);
+ void replaceBooleanWithFalse(BooleanEdge bexpr);
+ void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
+ CSolver *clone();
+ void serialize();
+ static CSolver *deserialize(const char *file, InterpreterType itype = SATUNE);
+ void autoTune(uint budget);
+ void inferFixedOrders();
+ void inferFixedOrder(Order *order);
+ void setInterpreter(InterpreterType type);
+ bool useInterpreter() {return interpreter != NULL;}
+ void setTuner(Tuner *_tuner) { tuner = _tuner; }
+ long long getElapsedTime() { return elapsedTime; }
+ long long getEncodeTime();
+ long long getSolveTime();
+ long getSatSolverTimeout() { return satsolverTimeout;}
+
+ CMEMALLOC;
+
+private:
+ void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child);
+ void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child);
+ void handleFunction(ElementFunction *ef, 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);