5 #include "corestructs.h"
7 #include "solver_interface.h"
14 /** This function creates a set containing the elements passed in the array. */
15 Set *createSet(VarType type, uint64_t *elements, uint num);
17 /** This function creates a set from lowrange to highrange (inclusive). */
19 Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
21 VarType getSetVarType(Set *set);
23 Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
25 /** This function creates a mutable set. */
27 MutableSet *createMutableSet(VarType type);
29 /** This function adds a new item to a set. */
31 //Deprecating this unless we need it...
32 void addItem(MutableSet *set, uint64_t element);
34 /** This function adds a new unique item to the set and returns it.
35 This function cannot be used in conjunction with manually adding
38 uint64_t createUniqueItem(MutableSet *set);
41 * Freeze and finalize the mutableSet ...
43 void finalizeMutableSet(MutableSet* set);
45 /** This function creates an element variable over a set. */
47 Element *getElementVar(Set *set);
49 /** This function creates an element constrant. */
50 Element *getElementConst(VarType type, uint64_t value);
52 Set* getElementRange (Element* element);
54 BooleanEdge getBooleanTrue();
56 BooleanEdge getBooleanFalse();
58 /** This function creates a boolean variable. */
60 BooleanEdge getBooleanVar(VarType type);
62 /** This function creates a function operator. */
64 Function *createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,
65 OverFlowBehavior overflowbehavior);
67 /** This function creates a predicate operator. */
69 Predicate *createPredicateOperator(CompOp op, Set **domain, uint numDomain);
71 Predicate *createPredicateTable(Table *table, UndefinedBehavior behavior);
73 /** This function creates an empty instance table.*/
75 Table *createTable(Set **domains, uint numDomain, Set *range);
77 Table *createTableForPredicate(Set **domains, uint numDomain);
78 /** This function adds an input output relation to a table. */
80 void addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result);
82 /** This function converts a completed table into a function. */
84 Function *completeTable(Table *, UndefinedBehavior behavior);
86 /** This function applies a function to the Elements in its input. */
88 Element *applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus);
90 /** This function applies a predicate to the Elements in its input. */
92 BooleanEdge applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus);
94 BooleanEdge applyPredicate(Predicate *predicate, Element **inputs, uint numInputs);
96 /** This function applies a logical operation to the Booleans in its input. */
98 BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);
100 /** This function applies a logical operation to the Booleans in its input. */
102 BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2);
104 /** This function applies a logical operation to the Booleans in its input. */
106 BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge arg);
108 /** This function adds a boolean constraint to the set of constraints
111 void addConstraint(BooleanEdge constraint);
113 /** This function instantiates an order of type type over the set set. */
114 Order *createOrder(OrderType type, Set *set);
116 /** This function instantiates a boolean on two items in an order. */
117 BooleanEdge orderConstraint(Order *order, uint64_t first, uint64_t second);
119 /** When everything is done, the client calls this function and then csolver starts to encode*/
122 /** After getting the solution from the SAT solver, client can get the value of an element via this function*/
123 uint64_t getElementValue(Element *element);
125 /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
126 bool getBooleanValue(BooleanEdge boolean);
128 bool getOrderConstraintValue(Order *order, uint64_t first, uint64_t second);
130 bool isTrue(BooleanEdge b);
131 bool isFalse(BooleanEdge b);
133 void setUnSAT() { unsat = true; }
135 bool isUnSAT() { return unsat; }
137 Vector<Order *> *getOrders() { return &allOrders;}
138 HashsetOrder * getActiveOrders() { return &activeOrders;}
140 Tuner *getTuner() { return tuner; }
142 SetIteratorBooleanEdge * getConstraints() { return constraints.iterator(); }
144 SATEncoder *getSATEncoder() {return satEncoder;}
146 void replaceBooleanWithTrue(BooleanEdge bexpr);
147 void replaceBooleanWithTrueNoRemove(BooleanEdge bexpr);
148 void replaceBooleanWithFalse(BooleanEdge bexpr);
149 void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
152 void autoTune(uint budget);
154 void setTuner(Tuner *_tuner) { tuner = _tuner; }
155 long long getElapsedTime() { return elapsedTime; }
156 long long getEncodeTime();
157 long long getSolveTime();
162 void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child);
163 void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child);
165 //These two functions are helpers if the client has a pointer to a
166 //Boolean object that we have since replaced
167 BooleanEdge rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);
168 BooleanEdge doRewrite(BooleanEdge b);
169 /** This is a vector of constraints that must be satisfied. */
170 HashsetBooleanEdge constraints;
172 /** This is a vector of all boolean structs that we have allocated. */
173 Vector<Boolean *> allBooleans;
175 /** This is a vector of all set structs that we have allocated. */
176 Vector<Set *> allSets;
178 /** This is a vector of all element structs that we have allocated. */
179 Vector<Element *> allElements;
181 /** This is a vector of all predicate structs that we have allocated. */
182 Vector<Predicate *> allPredicates;
184 /** This is a vector of all table structs that we have allocated. */
185 Vector<Table *> allTables;
187 /** This is a vector of all order structs that we have allocated. */
188 Vector<Order *> allOrders;
190 HashsetOrder activeOrders;
192 /** This is a vector of all function structs that we have allocated. */
193 Vector<Function *> allFunctions;
195 BooleanEdge boolTrue;
196 BooleanEdge boolFalse;
198 /** These two tables are used for deduplicating entries. */
199 BooleanMatchMap boolMap;
200 ElementMatchMap elemMap;
202 SATEncoder *satEncoder;
205 long long elapsedTime;