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);
/** This function creates an element constrant. */
Element *getElementConst(VarType type, uint64_t value);
- Boolean *getBooleanTrue();
+ BooleanEdge getBooleanTrue();
+
+ BooleanEdge getBooleanFalse();
- Boolean *getBooleanFalse();
-
/** This function creates a boolean variable. */
- Boolean *getBooleanVar(VarType type);
+ BooleanEdge getBooleanVar(VarType type);
/** This function creates a function operator. */
/** This function applies a function to the Elements in its input. */
- Element *applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus);
+ Element *applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus);
/** This function applies a predicate to the Elements in its input. */
- Boolean *applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus);
+ BooleanEdge applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus);
- Boolean *applyPredicate(Predicate *predicate, Element **inputs, uint numInputs);
+ BooleanEdge applyPredicate(Predicate *predicate, Element **inputs, uint numInputs);
/** This function applies a logical operation to the Booleans in its input. */
- Boolean *applyLogicalOperation(LogicOp op, Boolean **array, uint asize);
+ BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);
- /** This function applies a logical operation to the Booleans in its input. */
+ /** This function applies a logical operation to the Booleans in its input. */
- Boolean *applyLogicalOperation(LogicOp op, Boolean * arg1, Boolean * arg2);
+ BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2);
/** This function applies a logical operation to the Booleans in its input. */
- Boolean *applyLogicalOperation(LogicOp op, Boolean *arg);
+ BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge arg);
/** This function adds a boolean constraint to the set of constraints
to be satisfied */
- void addConstraint(Boolean *constraint);
+ void addConstraint(BooleanEdge constraint);
/** This function instantiates an order of type type over the set set. */
Order *createOrder(OrderType type, Set *set);
/** This function instantiates a boolean on two items in an order. */
- Boolean *orderConstraint(Order *order, uint64_t first, uint64_t second);
+ BooleanEdge 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 solve();
uint64_t getElementValue(Element *element);
/** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
- bool getBooleanValue(Boolean *boolean);
+ bool getBooleanValue(BooleanEdge boolean);
- HappenedBefore getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
+ bool getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
+
+ bool isTrue(BooleanEdge b);
+ bool isFalse(BooleanEdge b);
- 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; }
- Transformer* getTransformer() {return transformer;}
-
- SetIteratorBoolean *getConstraints() { return constraints.iterator(); }
+
+ SetIteratorBooleanEdge * getConstraints() { return constraints.iterator(); }
SATEncoder *getSATEncoder() {return satEncoder;}
- void replaceBooleanWithTrue(Boolean *bexpr);
- void replaceBooleanWithFalse(Boolean *bexpr);
- void replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb);
+ void replaceBooleanWithTrue(BooleanEdge bexpr);
+ void replaceBooleanWithTrueNoRemove(BooleanEdge bexpr);
+ void replaceBooleanWithFalse(BooleanEdge bexpr);
+ void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
CSolver *clone();
+ void serialize();
void autoTune(uint budget);
- void setTransformer(Transformer * _transformer) { transformer = _transformer; }
- 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:
- 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);
+ 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. */
- HashsetBoolean constraints;
+ HashsetBooleanEdge constraints;
/** This is a vector of all boolean structs that we have allocated. */
Vector<Boolean *> allBooleans;
/** 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;
-
+ BooleanEdge boolTrue;
+ BooleanEdge boolFalse;
+
/** These two tables are used for deduplicating entries. */
BooleanMatchMap boolMap;
ElementMatchMap elemMap;
-
+
SATEncoder *satEncoder;
bool unsat;
Tuner *tuner;
- Transformer* transformer;
long long elapsedTime;
};
#endif