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 #include "sattranslator.h"
  12
  13 CSolver *allocCSolver() {
  14         CSolver *This = (CSolver *) ourmalloc(sizeof(CSolver));
  15         This->unsat = false;
  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();
  25         return This;
  26 }
  27
  28 /** This function tears down the solver and the entire AST */
  29
  30 void deleteSolver(CSolver *This) {
  31         deleteHashSetBoolean(This->constraints);
  32
  33         uint size = getSizeVectorBoolean(This->allBooleans);
  34         for (uint i = 0; i < size; i++) {
  35                 deleteBoolean(getVectorBoolean(This->allBooleans, i));
  36         }
  37         deleteVectorBoolean(This->allBooleans);
  38
  39         size = getSizeVectorSet(This->allSets);
  40         for (uint i = 0; i < size; i++) {
  41                 deleteSet(getVectorSet(This->allSets, i));
  42         }
  43         deleteVectorSet(This->allSets);
  44
  45         size = getSizeVectorElement(This->allElements);
  46         for (uint i = 0; i < size; i++) {
  47                 deleteElement(getVectorElement(This->allElements, i));
  48         }
  49         deleteVectorElement(This->allElements);
  50
  51         size = getSizeVectorTable(This->allTables);
  52         for (uint i = 0; i < size; i++) {
  53                 deleteTable(getVectorTable(This->allTables, i));
  54         }
  55         deleteVectorTable(This->allTables);
  56
  57         size = getSizeVectorPredicate(This->allPredicates);
  58         for (uint i = 0; i < size; i++) {
  59                 deletePredicate(getVectorPredicate(This->allPredicates, i));
  60         }
  61         deleteVectorPredicate(This->allPredicates);
  62
  63         size = getSizeVectorOrder(This->allOrders);
  64         for (uint i = 0; i < size; i++) {
  65                 deleteOrder(getVectorOrder(This->allOrders, i));
  66         }
  67         deleteVectorOrder(This->allOrders);
  68
  69         size = getSizeVectorFunction(This->allFunctions);
  70         for (uint i = 0; i < size; i++) {
  71                 deleteFunction(getVectorFunction(This->allFunctions, i));
  72         }
  73         deleteVectorFunction(This->allFunctions);
  74         deleteSATEncoder(This->satEncoder);
  75         ourfree(This);
  76 }
  77
  78 Set *createSet(CSolver *This, VarType type, uint64_t *elements, uint numelements) {
  79         Set *set = allocSet(type, elements, numelements);
  80         pushVectorSet(This->allSets, set);
  81         return set;
  82 }
  83
  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);
  87         return set;
  88 }
  89
  90 MutableSet *createMutableSet(CSolver *This, VarType type) {
  91         MutableSet *set = allocMutableSet(type);
  92         pushVectorSet(This->allSets, set);
  93         return set;
  94 }
  95
  96 void addItem(CSolver *This, MutableSet *set, uint64_t element) {
  97         addElementMSet(set, element);
  98 }
  99
 100 uint64_t createUniqueItem(CSolver *This, MutableSet *set) {
 101         uint64_t element = set->low++;
 102         addElementMSet(set, element);
 103         return element;
 104 }
 105
 106 Element *getElementVar(CSolver *This, Set *set) {
 107         Element *element = allocElementSet(set);
 108         pushVectorElement(This->allElements, element);
 109         return element;
 110 }
 111
 112 Element *getElementConst(CSolver *This, VarType type, uint64_t value) {
 113         Element *element = allocElementConst(value, type);
 114         pushVectorElement(This->allElements, element);
 115         return element;
 116 }
 117
 118 Boolean *getBooleanVar(CSolver *This, VarType type) {
 119         Boolean *boolean = allocBooleanVar(type);
 120         pushVectorBoolean(This->allBooleans, boolean);
 121         return boolean;
 122 }
 123
 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);
 127         return function;
 128 }
 129
 130 Predicate *createPredicateOperator(CSolver *This, CompOp op, Set **domain, uint numDomain) {
 131         Predicate *predicate = allocPredicateOperator(op, domain,numDomain);
 132         pushVectorPredicate(This->allPredicates, predicate);
 133         return predicate;
 134 }
 135
 136 Predicate *createPredicateTable(CSolver *This, Table *table, UndefinedBehavior behavior) {
 137         Predicate *predicate = allocPredicateTable(table, behavior);
 138         pushVectorPredicate(This->allPredicates, predicate);
 139         return predicate;
 140 }
 141
 142 Table *createTable(CSolver *This, Set **domains, uint numDomain, Set *range) {
 143         Table *table = allocTable(domains,numDomain,range);
 144         pushVectorTable(This->allTables, table);
 145         return table;
 146 }
 147
 148 Table *createTableForPredicate(CSolver *solver, Set **domains, uint numDomain) {
 149         return createTable(solver, domains, numDomain, NULL);
 150 }
 151
 152 void addTableEntry(CSolver *This, Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
 153         addNewTableEntry(table,inputs, inputSize,result);
 154 }
 155
 156 Function *completeTable(CSolver *This, Table *table, UndefinedBehavior behavior) {
 157         Function *function = allocFunctionTable(table, behavior);
 158         pushVectorFunction(This->allFunctions,function);
 159         return function;
 160 }
 161
 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);
 165         return element;
 166 }
 167
 168 Boolean *applyPredicate(CSolver *This, Predicate *predicate, Element **inputs, uint numInputs) {
 169         return applyPredicateTable(This, predicate, inputs, numInputs, NULL);
 170 }
 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);
 174         return boolean;
 175 }
 176
 177 Boolean *applyLogicalOperation(CSolver *This, LogicOp op, Boolean **array, uint asize) {
 178         return allocBooleanLogicArray(This, op, array, asize);
 179 }
 180
 181 void addConstraint(CSolver *This, Boolean *constraint) {
 182         addHashSetBoolean(This->constraints, constraint);
 183 }
 184
 185 Order *createOrder(CSolver *This, OrderType type, Set *set) {
 186         Order *order = allocOrder(type, set);
 187         pushVectorOrder(This->allOrders, order);
 188         return order;
 189 }
 190
 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);
 194         return constraint;
 195 }
 196
 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]);
 205         }
 206         model_print("\n");
 207         return result;
 208 }
 209
 210 uint64_t getElementValue(CSolver *This, Element *element) {
 211         switch (GETELEMENTTYPE(element)) {
 212         case ELEMSET:
 213         case ELEMCONST:
 214         case ELEMFUNCRETURN:
 215                 return getElementValueSATTranslator(This, element);
 216         default:
 217                 ASSERT(0);
 218         }
 219         exit(-1);
 220 }
 221
 222 bool getBooleanValue( CSolver *This, Boolean *boolean) {
 223         switch (GETBOOLEANTYPE(boolean)) {
 224         case BOOLEANVAR:
 225                 return getBooleanVariableValueSATTranslator(This, boolean);
 226         default:
 227                 ASSERT(0);
 228         }
 229         exit(-1);
 230 }
 231
 232 HappenedBefore getOrderConstraintValue(CSolver *This, Order *order, uint64_t first, uint64_t second) {
 233         return getOrderConstraintValueSATTranslator(This, order, first, second);
 234 }
 235