3 #include "mutableset.h"
10 #include "satencoder.h"
11 #include "sattranslator.h"
13 CSolver *allocCSolver() {
14 CSolver *This = (CSolver *) ourmalloc(sizeof(CSolver));
16 This->constraints = allocDefHashSetBoolean();
17 This->allBooleans = allocDefVectorBoolean();
18 This->allSets = allocDefVectorSet();
19 This->allElements = allocDefVectorElement();
20 This->allPredicates = allocDefVectorPredicate();
21 This->allTables = allocDefVectorTable();
22 This->allOrders = allocDefVectorOrder();
23 This->allFunctions = allocDefVectorFunction();
24 This->satEncoder = allocSATEncoder();
28 /** This function tears down the solver and the entire AST */
30 void deleteSolver(CSolver *This) {
31 deleteHashSetBoolean(This->constraints);
33 uint size = getSizeVectorBoolean(This->allBooleans);
34 for (uint i = 0; i < size; i++) {
35 deleteBoolean(getVectorBoolean(This->allBooleans, i));
37 deleteVectorBoolean(This->allBooleans);
39 size = getSizeVectorSet(This->allSets);
40 for (uint i = 0; i < size; i++) {
41 deleteSet(getVectorSet(This->allSets, i));
43 deleteVectorSet(This->allSets);
45 size = getSizeVectorElement(This->allElements);
46 for (uint i = 0; i < size; i++) {
47 deleteElement(getVectorElement(This->allElements, i));
49 deleteVectorElement(This->allElements);
51 size = getSizeVectorTable(This->allTables);
52 for (uint i = 0; i < size; i++) {
53 deleteTable(getVectorTable(This->allTables, i));
55 deleteVectorTable(This->allTables);
57 size = getSizeVectorPredicate(This->allPredicates);
58 for (uint i = 0; i < size; i++) {
59 deletePredicate(getVectorPredicate(This->allPredicates, i));
61 deleteVectorPredicate(This->allPredicates);
63 size = getSizeVectorOrder(This->allOrders);
64 for (uint i = 0; i < size; i++) {
65 deleteOrder(getVectorOrder(This->allOrders, i));
67 deleteVectorOrder(This->allOrders);
69 size = getSizeVectorFunction(This->allFunctions);
70 for (uint i = 0; i < size; i++) {
71 deleteFunction(getVectorFunction(This->allFunctions, i));
73 deleteVectorFunction(This->allFunctions);
74 deleteSATEncoder(This->satEncoder);
78 Set *createSet(CSolver *This, VarType type, uint64_t *elements, uint numelements) {
79 Set *set = allocSet(type, elements, numelements);
80 pushVectorSet(This->allSets, set);
84 Set *createRangeSet(CSolver *This, VarType type, uint64_t lowrange, uint64_t highrange) {
85 Set *set = allocSetRange(type, lowrange, highrange);
86 pushVectorSet(This->allSets, set);
90 MutableSet *createMutableSet(CSolver *This, VarType type) {
91 MutableSet *set = allocMutableSet(type);
92 pushVectorSet(This->allSets, set);
96 void addItem(CSolver *This, MutableSet *set, uint64_t element) {
97 addElementMSet(set, element);
100 uint64_t createUniqueItem(CSolver *This, MutableSet *set) {
101 uint64_t element = set->low++;
102 addElementMSet(set, element);
106 Element *getElementVar(CSolver *This, Set *set) {
107 Element *element = allocElementSet(set);
108 pushVectorElement(This->allElements, element);
112 Element *getElementConst(CSolver *This, VarType type, uint64_t value) {
113 Element *element = allocElementConst(value, type);
114 pushVectorElement(This->allElements, element);
118 Boolean *getBooleanVar(CSolver *This, VarType type) {
119 Boolean *boolean = allocBooleanVar(type);
120 pushVectorBoolean(This->allBooleans, boolean);
124 Function *createFunctionOperator(CSolver *This, ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
125 Function *function = allocFunctionOperator(op, domain, numDomain, range, overflowbehavior);
126 pushVectorFunction(This->allFunctions, function);
130 Predicate *createPredicateOperator(CSolver *This, CompOp op, Set **domain, uint numDomain) {
131 Predicate *predicate = allocPredicateOperator(op, domain,numDomain);
132 pushVectorPredicate(This->allPredicates, predicate);
136 Predicate *createPredicateTable(CSolver *This, Table *table, UndefinedBehavior behavior) {
137 Predicate *predicate = allocPredicateTable(table, behavior);
138 pushVectorPredicate(This->allPredicates, predicate);
142 Table *createTable(CSolver *This, Set **domains, uint numDomain, Set *range) {
143 Table *table = allocTable(domains,numDomain,range);
144 pushVectorTable(This->allTables, table);
148 Table *createTableForPredicate(CSolver *solver, Set **domains, uint numDomain) {
149 return createTable(solver, domains, numDomain, NULL);
152 void addTableEntry(CSolver *This, Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
153 addNewTableEntry(table,inputs, inputSize,result);
156 Function *completeTable(CSolver *This, Table *table, UndefinedBehavior behavior) {
157 Function *function = allocFunctionTable(table, behavior);
158 pushVectorFunction(This->allFunctions,function);
162 Element *applyFunction(CSolver *This, Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
163 Element *element = allocElementFunction(function,array,numArrays,overflowstatus);
164 pushVectorElement(This->allElements, element);
168 Boolean *applyPredicate(CSolver *This, Predicate *predicate, Element **inputs, uint numInputs) {
169 return applyPredicateTable(This, predicate, inputs, numInputs, NULL);
171 Boolean *applyPredicateTable(CSolver *This, Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
172 Boolean *boolean = allocBooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
173 pushVectorBoolean(This->allBooleans, boolean);
177 Boolean *applyLogicalOperation(CSolver *This, LogicOp op, Boolean **array, uint asize) {
178 return allocBooleanLogicArray(This, op, array, asize);
181 void addConstraint(CSolver *This, Boolean *constraint) {
182 addHashSetBoolean(This->constraints, constraint);
185 Order *createOrder(CSolver *This, OrderType type, Set *set) {
186 Order *order = allocOrder(type, set);
187 pushVectorOrder(This->allOrders, order);
191 Boolean *orderConstraint(CSolver *This, Order *order, uint64_t first, uint64_t second) {
192 Boolean *constraint = allocBooleanOrder(order, first, second);
193 pushVectorBoolean(This->allBooleans,constraint);
197 int startEncoding(CSolver *This) {
198 naiveEncodingDecision(This);
199 SATEncoder *satEncoder = This->satEncoder;
200 encodeAllSATEncoder(This, satEncoder);
201 int result = solveCNF(satEncoder->cnf);
202 model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);
203 for (uint i = 1; i <= satEncoder->cnf->solver->solutionsize; i++) {
204 model_print("%d, ", satEncoder->cnf->solver->solution[i]);
210 uint64_t getElementValue(CSolver *This, Element *element) {
211 switch (GETELEMENTTYPE(element)) {
215 return getElementValueSATTranslator(This, element);
222 bool getBooleanValue( CSolver *This, Boolean *boolean) {
223 switch (GETBOOLEANTYPE(boolean)) {
225 return getBooleanVariableValueSATTranslator(This, boolean);
232 HappenedBefore getOrderConstraintValue(CSolver *This, Order *order, uint64_t first, uint64_t second) {
233 return getOrderConstraintValueSATTranslator(This, order, first, second);