3 #include "mutableset.h"
10 #include "satencoder.h"
11 #include "sattranslator.h"
13 CSolver *allocCSolver() {
14 CSolver *This = (CSolver *) ourmalloc(sizeof(CSolver));
15 This->constraints = allocDefVectorBoolean();
16 This->allBooleans = allocDefVectorBoolean();
17 This->allSets = allocDefVectorSet();
18 This->allElements = allocDefVectorElement();
19 This->allPredicates = allocDefVectorPredicate();
20 This->allTables = allocDefVectorTable();
21 This->allOrders = allocDefVectorOrder();
22 This->allFunctions = allocDefVectorFunction();
23 This->satEncoder = allocSATEncoder();
27 /** This function tears down the solver and the entire AST */
29 void deleteSolver(CSolver *This) {
30 deleteVectorBoolean(This->constraints);
32 uint size = getSizeVectorBoolean(This->allBooleans);
33 for (uint i = 0; i < size; i++) {
34 deleteBoolean(getVectorBoolean(This->allBooleans, i));
36 deleteVectorBoolean(This->allBooleans);
38 size = getSizeVectorSet(This->allSets);
39 for (uint i = 0; i < size; i++) {
40 deleteSet(getVectorSet(This->allSets, i));
42 deleteVectorSet(This->allSets);
44 size = getSizeVectorElement(This->allElements);
45 for (uint i = 0; i < size; i++) {
46 deleteElement(getVectorElement(This->allElements, i));
48 deleteVectorElement(This->allElements);
50 size = getSizeVectorTable(This->allTables);
51 for (uint i = 0; i < size; i++) {
52 deleteTable(getVectorTable(This->allTables, i));
54 deleteVectorTable(This->allTables);
56 size = getSizeVectorPredicate(This->allPredicates);
57 for (uint i = 0; i < size; i++) {
58 deletePredicate(getVectorPredicate(This->allPredicates, i));
60 deleteVectorPredicate(This->allPredicates);
62 size = getSizeVectorOrder(This->allOrders);
63 for (uint i = 0; i < size; i++) {
64 deleteOrder(getVectorOrder(This->allOrders, i));
66 deleteVectorOrder(This->allOrders);
68 size = getSizeVectorFunction(This->allFunctions);
69 for (uint i = 0; i < size; i++) {
70 deleteFunction(getVectorFunction(This->allFunctions, i));
72 deleteVectorFunction(This->allFunctions);
73 deleteSATEncoder(This->satEncoder);
77 Set *createSet(CSolver *This, VarType type, uint64_t *elements, uint numelements) {
78 Set *set = allocSet(type, elements, numelements);
79 pushVectorSet(This->allSets, set);
83 Set *createRangeSet(CSolver *This, VarType type, uint64_t lowrange, uint64_t highrange) {
84 Set *set = allocSetRange(type, lowrange, highrange);
85 pushVectorSet(This->allSets, set);
89 MutableSet *createMutableSet(CSolver *This, VarType type) {
90 MutableSet *set = allocMutableSet(type);
91 pushVectorSet(This->allSets, set);
95 void addItem(CSolver *This, MutableSet *set, uint64_t element) {
96 addElementMSet(set, element);
99 uint64_t createUniqueItem(CSolver *This, MutableSet *set) {
100 uint64_t element = set->low++;
101 addElementMSet(set, element);
105 Element *getElementVar(CSolver *This, Set *set) {
106 Element *element = allocElementSet(set);
107 pushVectorElement(This->allElements, element);
111 Element *getElementConst(CSolver *This, VarType type, uint64_t value) {
112 Element *element = allocElementConst(value, type);
113 pushVectorElement(This->allElements, element);
117 Boolean *getBooleanVar(CSolver *This, VarType type) {
118 Boolean *boolean = allocBooleanVar(type);
119 pushVectorBoolean(This->allBooleans, boolean);
123 Function *createFunctionOperator(CSolver *This, ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
124 Function *function = allocFunctionOperator(op, domain, numDomain, range, overflowbehavior);
125 pushVectorFunction(This->allFunctions, function);
129 Predicate *createPredicateOperator(CSolver *This, CompOp op, Set **domain, uint numDomain) {
130 Predicate *predicate = allocPredicateOperator(op, domain,numDomain);
131 pushVectorPredicate(This->allPredicates, predicate);
135 Predicate *createPredicateTable(CSolver *This, Table *table, UndefinedBehavior behavior) {
136 Predicate *predicate = allocPredicateTable(table, behavior);
137 pushVectorPredicate(This->allPredicates, predicate);
141 Table *createTable(CSolver *This, Set **domains, uint numDomain, Set *range) {
142 Table *table = allocTable(domains,numDomain,range);
143 pushVectorTable(This->allTables, table);
147 Table *createTableForPredicate(CSolver *solver, Set **domains, uint numDomain) {
148 return createTable(solver, domains, numDomain, NULL);
151 void addTableEntry(CSolver *This, Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
152 addNewTableEntry(table,inputs, inputSize,result);
155 Function *completeTable(CSolver *This, Table *table, UndefinedBehavior behavior) {
156 Function *function = allocFunctionTable(table, behavior);
157 pushVectorFunction(This->allFunctions,function);
161 Element *applyFunction(CSolver *This, Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
162 Element *element = allocElementFunction(function,array,numArrays,overflowstatus);
163 pushVectorElement(This->allElements, element);
167 Boolean *applyPredicate(CSolver *This, Predicate *predicate, Element **inputs, uint numInputs) {
168 return applyPredicateTable(This, predicate, inputs, numInputs, NULL);
170 Boolean *applyPredicateTable(CSolver *This, Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
171 Boolean *boolean = allocBooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
172 pushVectorBoolean(This->allBooleans, boolean);
176 Boolean *applyLogicalOperation(CSolver *This, LogicOp op, Boolean **array, uint asize) {
177 return allocBooleanLogicArray(This, op, array, asize);
180 void addConstraint(CSolver *This, Boolean *constraint) {
181 pushVectorBoolean(This->constraints, constraint);
184 Order *createOrder(CSolver *This, OrderType type, Set *set) {
185 Order *order = allocOrder(type, set);
186 pushVectorOrder(This->allOrders, order);
190 Boolean *orderConstraint(CSolver *This, Order *order, uint64_t first, uint64_t second) {
191 Boolean *constraint = allocBooleanOrder(order, first, second);
192 pushVectorBoolean(This->allBooleans,constraint);
196 int startEncoding(CSolver *This) {
197 naiveEncodingDecision(This);
198 SATEncoder *satEncoder = This->satEncoder;
199 encodeAllSATEncoder(This, satEncoder);
200 int result = solveCNF(satEncoder->cnf);
201 model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);
202 for (uint i = 1; i <= satEncoder->cnf->solver->solutionsize; i++) {
203 model_print("%d, ", satEncoder->cnf->solver->solution[i]);
209 uint64_t getElementValue(CSolver *This, Element *element) {
210 switch (GETELEMENTTYPE(element)) {
214 return getElementValueSATTranslator(This, element);
221 bool getBooleanValue( CSolver *This, Boolean *boolean) {
222 switch (GETBOOLEANTYPE(boolean)) {
224 return getBooleanVariableValueSATTranslator(This, boolean);
231 HappenedBefore getOrderConstraintValue(CSolver *This, Order *order, uint64_t first, uint64_t second) {
232 return getOrderConstraintValueSATTranslator(This, order, first, second);