Merge branch 'hamed' into brian
[satune.git] / src / csolver.c
1 #include "csolver.h"
2 #include "set.h"
3 #include "mutableset.h"
4 #include "element.h"
5 #include "boolean.h"
6 #include "predicate.h"
7 #include "order.h"
8 #include "table.h"
9 #include "function.h"
10 #include "satencoder.h"
11
12 CSolver * allocCSolver() {
13         CSolver * tmp=(CSolver *) ourmalloc(sizeof(CSolver));
14         tmp->constraints=allocDefVectorBoolean();
15         tmp->allBooleans=allocDefVectorBoolean();
16         tmp->allSets=allocDefVectorSet();
17         tmp->allElements=allocDefVectorElement();
18         tmp->allPredicates = allocDefVectorPredicate();
19         tmp->allTables = allocDefVectorTable();
20         tmp->allOrders = allocDefVectorOrder();
21         tmp->allFunctions = allocDefVectorFunction();
22         return tmp;
23 }
24
25 /** This function tears down the solver and the entire AST */
26
27 void deleteSolver(CSolver *This) {
28         deleteVectorBoolean(This->constraints);
29
30         uint size=getSizeVectorBoolean(This->allBooleans);
31         for(uint i=0;i<size;i++) {
32                 deleteBoolean(getVectorBoolean(This->allBooleans, i));
33         }
34         deleteVectorBoolean(This->allBooleans);
35
36         size=getSizeVectorSet(This->allSets);
37         for(uint i=0;i<size;i++) {
38                 deleteSet(getVectorSet(This->allSets, i));
39         }
40         deleteVectorSet(This->allSets);
41
42         size=getSizeVectorElement(This->allElements);
43         for(uint i=0;i<size;i++) {
44                 deleteElement(getVectorElement(This->allElements, i));
45         }
46         deleteVectorElement(This->allElements);
47
48         size=getSizeVectorTable(This->allTables);
49         for(uint i=0;i<size;i++) {
50                 deleteTable(getVectorTable(This->allTables, i));
51         }
52         deleteVectorTable(This->allTables);
53
54         size=getSizeVectorPredicate(This->allPredicates);
55         for(uint i=0;i<size;i++) {
56                 deletePredicate(getVectorPredicate(This->allPredicates, i));
57         }
58         deleteVectorPredicate(This->allPredicates);
59
60         size=getSizeVectorOrder(This->allOrders);
61         for(uint i=0;i<size;i++) {
62                 deleteOrder(getVectorOrder(This->allOrders, i));
63         }
64         deleteVectorOrder(This->allOrders);
65
66         size=getSizeVectorFunction(This->allFunctions);
67         for(uint i=0;i<size;i++) {
68                 deleteFunction(getVectorFunction(This->allFunctions, i));
69         }
70         deleteVectorFunction(This->allFunctions);
71         ourfree(This);
72 }
73
74 Set * createSet(CSolver * This, VarType type, uint64_t * elements, uint numelements) {
75         Set * set=allocSet(type, elements, numelements);
76         pushVectorSet(This->allSets, set);
77         return set;
78 }
79
80 Set * createRangeSet(CSolver * This, VarType type, uint64_t lowrange, uint64_t highrange) {
81         Set * set=allocSetRange(type, lowrange, highrange);
82         pushVectorSet(This->allSets, set);
83         return set;
84 }
85
86 MutableSet * createMutableSet(CSolver * This, VarType type) {
87         MutableSet * set=allocMutableSet(type);
88         pushVectorSet(This->allSets, set);
89         return set;
90 }
91
92 void addItem(CSolver *solver, MutableSet * set, uint64_t element) {
93         addElementMSet(set, element);
94 }
95
96 uint64_t createUniqueItem(CSolver *solver, MutableSet * set) {
97         uint64_t element=set->low++;
98         addElementMSet(set, element);
99         return element;
100 }
101
102 Element * getElementVar(CSolver *This, Set * set) {
103         Element * element=allocElementSet(set);
104         pushVectorElement(This->allElements, element);
105         return element;
106 }
107
108 Boolean * getBooleanVar(CSolver *solver, VarType type) {
109         Boolean* boolean= allocBoolean(type);
110         pushVectorBoolean(solver->allBooleans, boolean);
111         return boolean;
112 }
113
114 Function * createFunctionOperator(CSolver *solver, ArithOp op, Set ** domain, uint numDomain, Set * range,OverFlowBehavior overflowbehavior) {
115         Function* function = allocFunctionOperator(op, domain, numDomain, range, overflowbehavior);
116         pushVectorFunction(solver->allFunctions, function);
117         return function;
118 }
119
120 Predicate * createPredicateOperator(CSolver *solver, CompOp op, Set ** domain, uint numDomain) {
121         Predicate* predicate= allocPredicateOperator(op, domain,numDomain);
122         pushVectorPredicate(solver->allPredicates, predicate);
123         return predicate;
124 }
125
126 Table * createTable(CSolver *solver, Set **domains, uint numDomain, Set * range) {
127         Table* table= allocTable(domains,numDomain,range);
128         pushVectorTable(solver->allTables, table);
129         return table;
130 }
131
132 void addTableEntry(CSolver *solver, Table* table, uint64_t* inputs, uint inputSize, uint64_t result) {
133         addNewTableEntry(table,inputs, inputSize,result);
134 }
135
136 Function * completeTable(CSolver *solver, Table * table) {
137         Function* function = allocFunctionTable(table);
138         pushVectorFunction(solver->allFunctions,function);
139         return function;
140 }
141
142 Element * applyFunction(CSolver *solver, Function * function, Element ** array, uint numArrays, Boolean * overflowstatus) {
143         Element* element= allocElementFunction(function,array,numArrays,overflowstatus);
144         pushVectorElement(solver->allElements, element);
145         return element;
146 }
147
148 Boolean * applyPredicate(CSolver *solver, Predicate * predicate, Element ** inputs, uint numInputs) {
149         Boolean* boolean= allocBooleanPredicate(predicate, inputs, numInputs);
150         pushVectorBoolean(solver->allBooleans, boolean);
151         return boolean;
152 }
153
154 Boolean * applyLogicalOperation(CSolver *solver, LogicOp op, Boolean ** array, uint asize) {
155         return allocBooleanLogicArray(solver, op, array, asize);
156 }
157
158 void addBoolean(CSolver *This, Boolean * constraint) {
159         pushVectorBoolean(This->constraints, constraint);
160 }
161
162 Order * createOrder(CSolver *solver, OrderType type, Set * set) {
163         Order* order = allocOrder(type, set);
164         pushVectorOrder(solver->allOrders, order);
165         return order;
166 }
167
168 Boolean * orderConstraint(CSolver *solver, Order * order, uint64_t first, uint64_t second) {
169         Boolean* constraint = allocBooleanOrder(order, first, second);
170         pushVectorBoolean(solver->allBooleans,constraint);
171         return constraint;
172 }
173
174 void startEncoding(CSolver* solver){
175         naiveEncodingDecision(solver);
176         SATEncoder* satEncoder = allocSATEncoder();
177         encodeAllSATEncoder(solver, satEncoder);
178         finishedClauses(satEncoder->satSolver);
179         int result= solve(satEncoder->satSolver);
180         model_print("sat_solver's result:%d\n", result);
181         //For now, let's just delete it, and in future for doing queries 
182         //we may need it.
183         deleteSATEncoder(satEncoder);
184 }