3 #include "mutableset.h"
10 #include "satencoder.h"
11 #include "sattranslator.h"
14 CSolver *allocCSolver() {
15 CSolver *This = (CSolver *) ourmalloc(sizeof(CSolver));
17 This->constraints = allocDefHashSetBoolean();
18 This->allBooleans = allocDefVectorBoolean();
19 This->allSets = allocDefVectorSet();
20 This->allElements = allocDefVectorElement();
21 This->allPredicates = allocDefVectorPredicate();
22 This->allTables = allocDefVectorTable();
23 This->allOrders = allocDefVectorOrder();
24 This->allFunctions = allocDefVectorFunction();
25 This->satEncoder = allocSATEncoder();
26 This->tuner = allocTuner();
30 /** This function tears down the solver and the entire AST */
32 void deleteSolver(CSolver *This) {
33 deleteHashSetBoolean(This->constraints);
35 uint size = getSizeVectorBoolean(This->allBooleans);
36 for (uint i = 0; i < size; i++) {
37 deleteBoolean(getVectorBoolean(This->allBooleans, i));
39 deleteVectorBoolean(This->allBooleans);
41 size = getSizeVectorSet(This->allSets);
42 for (uint i = 0; i < size; i++) {
43 deleteSet(getVectorSet(This->allSets, i));
45 deleteVectorSet(This->allSets);
47 size = getSizeVectorElement(This->allElements);
48 for (uint i = 0; i < size; i++) {
49 deleteElement(getVectorElement(This->allElements, i));
51 deleteVectorElement(This->allElements);
53 size = getSizeVectorTable(This->allTables);
54 for (uint i = 0; i < size; i++) {
55 deleteTable(getVectorTable(This->allTables, i));
57 deleteVectorTable(This->allTables);
59 size = getSizeVectorPredicate(This->allPredicates);
60 for (uint i = 0; i < size; i++) {
61 deletePredicate(getVectorPredicate(This->allPredicates, i));
63 deleteVectorPredicate(This->allPredicates);
65 size = getSizeVectorOrder(This->allOrders);
66 for (uint i = 0; i < size; i++) {
67 deleteOrder(getVectorOrder(This->allOrders, i));
69 deleteVectorOrder(This->allOrders);
71 size = getSizeVectorFunction(This->allFunctions);
72 for (uint i = 0; i < size; i++) {
73 deleteFunction(getVectorFunction(This->allFunctions, i));
75 deleteVectorFunction(This->allFunctions);
76 deleteSATEncoder(This->satEncoder);
77 deleteTuner(This->tuner);
81 Set *createSet(CSolver *This, VarType type, uint64_t *elements, uint numelements) {
82 Set *set = allocSet(type, elements, numelements);
83 pushVectorSet(This->allSets, set);
87 Set *createRangeSet(CSolver *This, VarType type, uint64_t lowrange, uint64_t highrange) {
88 Set *set = allocSetRange(type, lowrange, highrange);
89 pushVectorSet(This->allSets, set);
93 MutableSet *createMutableSet(CSolver *This, VarType type) {
94 MutableSet *set = allocMutableSet(type);
95 pushVectorSet(This->allSets, set);
99 void addItem(CSolver *This, MutableSet *set, uint64_t element) {
100 addElementMSet(set, element);
103 uint64_t createUniqueItem(CSolver *This, MutableSet *set) {
104 uint64_t element = set->low++;
105 addElementMSet(set, element);
109 Element *getElementVar(CSolver *This, Set *set) {
110 Element *element = allocElementSet(set);
111 pushVectorElement(This->allElements, element);
115 Element *getElementConst(CSolver *This, VarType type, uint64_t value) {
116 Element *element = allocElementConst(value, type);
117 pushVectorElement(This->allElements, element);
121 Boolean *getBooleanVar(CSolver *This, VarType type) {
122 Boolean *boolean = allocBooleanVar(type);
123 pushVectorBoolean(This->allBooleans, boolean);
127 Function *createFunctionOperator(CSolver *This, ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
128 Function *function = allocFunctionOperator(op, domain, numDomain, range, overflowbehavior);
129 pushVectorFunction(This->allFunctions, function);
133 Predicate *createPredicateOperator(CSolver *This, CompOp op, Set **domain, uint numDomain) {
134 Predicate *predicate = allocPredicateOperator(op, domain,numDomain);
135 pushVectorPredicate(This->allPredicates, predicate);
139 Predicate *createPredicateTable(CSolver *This, Table *table, UndefinedBehavior behavior) {
140 Predicate *predicate = allocPredicateTable(table, behavior);
141 pushVectorPredicate(This->allPredicates, predicate);
145 Table *createTable(CSolver *This, Set **domains, uint numDomain, Set *range) {
146 Table *table = allocTable(domains,numDomain,range);
147 pushVectorTable(This->allTables, table);
151 Table *createTableForPredicate(CSolver *solver, Set **domains, uint numDomain) {
152 return createTable(solver, domains, numDomain, NULL);
155 void addTableEntry(CSolver *This, Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
156 addNewTableEntry(table,inputs, inputSize,result);
159 Function *completeTable(CSolver *This, Table *table, UndefinedBehavior behavior) {
160 Function *function = allocFunctionTable(table, behavior);
161 pushVectorFunction(This->allFunctions,function);
165 Element *applyFunction(CSolver *This, Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
166 Element *element = allocElementFunction(function,array,numArrays,overflowstatus);
167 pushVectorElement(This->allElements, element);
171 Boolean *applyPredicate(CSolver *This, Predicate *predicate, Element **inputs, uint numInputs) {
172 return applyPredicateTable(This, predicate, inputs, numInputs, NULL);
174 Boolean *applyPredicateTable(CSolver *This, Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
175 Boolean *boolean = allocBooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
176 pushVectorBoolean(This->allBooleans, boolean);
180 Boolean *applyLogicalOperation(CSolver *This, LogicOp op, Boolean **array, uint asize) {
181 return allocBooleanLogicArray(This, op, array, asize);
184 void addConstraint(CSolver *This, Boolean *constraint) {
185 addHashSetBoolean(This->constraints, constraint);
188 Order *createOrder(CSolver *This, OrderType type, Set *set) {
189 Order *order = allocOrder(type, set);
190 pushVectorOrder(This->allOrders, order);
194 Boolean *orderConstraint(CSolver *This, Order *order, uint64_t first, uint64_t second) {
195 Boolean *constraint = allocBooleanOrder(order, first, second);
196 pushVectorBoolean(This->allBooleans,constraint);
200 int startEncoding(CSolver *This) {
201 naiveEncodingDecision(This);
202 SATEncoder *satEncoder = This->satEncoder;
203 encodeAllSATEncoder(This, satEncoder);
204 int result = solveCNF(satEncoder->cnf);
205 model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);
206 for (uint i = 1; i <= satEncoder->cnf->solver->solutionsize; i++) {
207 model_print("%d, ", satEncoder->cnf->solver->solution[i]);
213 uint64_t getElementValue(CSolver *This, Element *element) {
214 switch (GETELEMENTTYPE(element)) {
218 return getElementValueSATTranslator(This, element);
225 bool getBooleanValue( CSolver *This, Boolean *boolean) {
226 switch (GETBOOLEANTYPE(boolean)) {
228 return getBooleanVariableValueSATTranslator(This, boolean);
235 HappenedBefore getOrderConstraintValue(CSolver *This, Order *order, uint64_t first, uint64_t second) {
236 return getOrderConstraintValueSATTranslator(This, order, first, second);