3 #include "mutableset.h"
10 #include "satencoder.h"
11 #include "sattranslator.h"
13 #include "polarityassignment.h"
14 #include "decomposeordertransform.h"
15 #include "autotuner.h"
18 #include "orderresolver.h"
19 #include "integerencoding.h"
21 #include "preprocess.h"
22 #include "serializer.h"
23 #include "deserializer.h"
24 #include "encodinggraph.h"
25 #include "ordergraph.h"
26 #include "orderedge.h"
27 #include "orderanalysis.h"
28 #include "elementopt.h"
29 #include "varorderingopt.h"
32 #include "alloyinterpreter.h"
33 #include "smtinterpreter.h"
34 #include "mathsatinterpreter.h"
35 #include "smtratinterpreter.h"
38 boolTrue(BooleanEdge(new BooleanConst(true))),
39 boolFalse(boolTrue.negate()),
41 booleanVarUsed(false),
42 incrementalMode(false),
45 satsolverTimeout(NOTIMEOUT),
48 satEncoder = new SATEncoder(this);
51 /** This function tears down the solver and the entire AST */
55 uint size = allBooleans.getSize();
56 for (uint i = 0; i < size; i++) {
57 delete allBooleans.get(i);
60 size = allSets.getSize();
61 for (uint i = 0; i < size; i++) {
62 delete allSets.get(i);
65 size = allElements.getSize();
66 for (uint i = 0; i < size; i++) {
67 Element *el = allElements.get(i);
71 size = allTables.getSize();
72 for (uint i = 0; i < size; i++) {
73 delete allTables.get(i);
76 size = allPredicates.getSize();
77 for (uint i = 0; i < size; i++) {
78 delete allPredicates.get(i);
81 size = allOrders.getSize();
82 for (uint i = 0; i < size; i++) {
83 delete allOrders.get(i);
85 size = allFunctions.getSize();
86 for (uint i = 0; i < size; i++) {
87 delete allFunctions.get(i);
90 if (interpreter != NULL) {
94 delete boolTrue.getBoolean();
98 void CSolver::resetSolver() {
100 uint size = allBooleans.getSize();
101 for (uint i = 0; i < size; i++) {
102 delete allBooleans.get(i);
105 size = allSets.getSize();
106 for (uint i = 0; i < size; i++) {
107 delete allSets.get(i);
110 size = allElements.getSize();
111 for (uint i = 0; i < size; i++) {
112 Element *el = allElements.get(i);
116 size = allTables.getSize();
117 for (uint i = 0; i < size; i++) {
118 delete allTables.get(i);
121 size = allPredicates.getSize();
122 for (uint i = 0; i < size; i++) {
123 delete allPredicates.get(i);
126 size = allOrders.getSize();
127 for (uint i = 0; i < size; i++) {
128 delete allOrders.get(i);
130 size = allFunctions.getSize();
131 for (uint i = 0; i < size; i++) {
132 delete allFunctions.get(i);
134 delete boolTrue.getBoolean();
139 allPredicates.clear();
141 allFunctions.clear();
143 encodedConstraints.reset();
144 activeOrders.reset();
148 boolTrue = BooleanEdge(new BooleanConst(true));
149 boolFalse = boolTrue.negate();
151 booleanVarUsed = false;
154 satEncoder->resetSATEncoder();
158 CSolver *CSolver::clone() {
159 CSolver *copy = new CSolver();
161 SetIteratorBooleanEdge *it = getConstraints();
162 while (it->hasNext()) {
163 BooleanEdge b = it->next();
164 copy->addConstraint(cloneEdge(copy, &map, b));
170 CSolver *CSolver::deserialize(const char *file, InterpreterType itype) {
171 model_print("deserializing %s ...\n", file);
172 Deserializer deserializer(file, itype);
173 return deserializer.deserialize();
176 void CSolver::serialize() {
177 model_print("serializing ...\n");
179 long long nanotime = getTimeNano();
180 int numchars = sprintf(buffer, "DUMP%llu", nanotime);
181 Serializer serializer(buffer);
182 SetIteratorBooleanEdge *it = getConstraints();
183 while (it->hasNext()) {
184 BooleanEdge b = it->next();
185 serializeBooleanEdge(&serializer, b, true);
190 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
191 Set *set = new Set(type, elements, numelements);
196 Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange) {
197 Set *set = new Set(type, lowrange, highrange);
202 bool CSolver::itemExistInSet(Set *set, uint64_t item) {
203 return set->exists(item);
206 VarType CSolver::getSetVarType(Set *set) {
207 return set->getType();
210 Element *CSolver::createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange) {
211 Set *s = createRangeSet(type, lowrange, highrange);
212 return getElementVar(s);
215 MutableSet *CSolver::createMutableSet(VarType type) {
216 MutableSet *set = new MutableSet(type);
221 void CSolver::addItem(MutableSet *set, uint64_t element) {
222 set->addElementMSet(element);
225 uint64_t CSolver::createUniqueItem(MutableSet *set) {
226 uint64_t element = set->getNewUniqueItem();
227 set->addElementMSet(element);
231 void CSolver::finalizeMutableSet(MutableSet *set) {
235 Element *CSolver::getElementVar(Set *set) {
236 Element *element = new ElementSet(set);
237 allElements.push(element);
241 void CSolver::mustHaveValue(Element *element) {
242 element->anyValue = true;
245 void CSolver::freezeElementsVariables() {
247 for(uint i=0; i< allElements.getSize(); i++){
248 Element *e = allElements.get(i);
250 satEncoder->freezeElementVariables(&e->encoding);
256 Set *CSolver::getElementRange (Element *element) {
257 return element->getRange();
261 Element *CSolver::getElementConst(VarType type, uint64_t value) {
262 uint64_t array[] = {value};
263 Set *set = new Set(type, array, 1);
264 Element *element = new ElementConst(value, set);
265 Element *e = elemMap.get(element);
268 allElements.push(element);
269 elemMap.put(element, element);
279 Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
280 Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
281 Element *e = elemMap.get(element);
283 element->updateParents();
284 allElements.push(element);
285 elemMap.put(element, element);
293 Function *CSolver::createFunctionOperator(ArithOp op, Set *range, OverFlowBehavior overflowbehavior) {
294 Function *function = new FunctionOperator(op, range, overflowbehavior);
295 allFunctions.push(function);
299 Predicate *CSolver::createPredicateOperator(CompOp op) {
300 Predicate *predicate = new PredicateOperator(op);
301 allPredicates.push(predicate);
305 Predicate *CSolver::createPredicateTable(Table *table, UndefinedBehavior behavior) {
306 Predicate *predicate = new PredicateTable(table, behavior);
307 allPredicates.push(predicate);
311 Table *CSolver::createTable(Set *range) {
312 Table *table = new Table(range);
313 allTables.push(table);
317 Table *CSolver::createTableForPredicate() {
318 return createTable(NULL);
321 void CSolver::addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
322 table->addNewTableEntry(inputs, inputSize, result);
325 Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
326 Function *function = new FunctionTable(table, behavior);
327 allFunctions.push(function);
331 BooleanEdge CSolver::getBooleanVar(VarType type) {
332 Boolean *boolean = new BooleanVar(type);
333 allBooleans.push(boolean);
335 booleanVarUsed = true;
336 return BooleanEdge(boolean);
339 BooleanEdge CSolver::getBooleanTrue() {
343 BooleanEdge CSolver::getBooleanFalse() {
347 BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
348 return applyPredicateTable(predicate, inputs, numInputs, BooleanEdge(NULL));
351 BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus) {
352 BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
353 Boolean *b = boolMap.get(boolean);
355 boolean->updateParents();
356 boolMap.put(boolean, boolean);
357 allBooleans.push(boolean);
358 return BooleanEdge(boolean);
361 return BooleanEdge(b);
365 bool CSolver::isTrue(BooleanEdge b) {
366 return b.isNegated() ? b->isFalse() : b->isTrue();
369 bool CSolver::isFalse(BooleanEdge b) {
370 return b.isNegated() ? b->isTrue() : b->isFalse();
373 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) {
374 BooleanEdge array[] = {arg1, arg2};
375 return applyLogicalOperation(op, array, 2);
378 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) {
379 BooleanEdge array[] = {arg};
380 return applyLogicalOperation(op, array, 1);
383 static int booleanEdgeCompares(const void *p1, const void *p2) {
384 BooleanEdge be1 = *(BooleanEdge const *) p1;
385 BooleanEdge be2 = *(BooleanEdge const *) p2;
386 uint64_t b1 = be1->id;
387 uint64_t b2 = be2->id;
396 BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
397 BooleanEdge newarray[asize];
398 memcpy(newarray, array, asize * sizeof(BooleanEdge));
399 for (uint i = 0; i < asize; i++) {
400 BooleanEdge b = newarray[i];
401 if (b->type == LOGICOP) {
402 if (((BooleanLogic *) b.getBoolean())->replaced) {
403 newarray[i] = doRewrite(newarray[i]);
408 return applyLogicalOperation(op, newarray, asize);
411 BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize){
412 BooleanEdge newarray[asize + 1];
414 newarray[asize] = applyLogicalOperation(SATC_OR, array, asize);
415 for (uint i=0; i< asize; i++){
416 BooleanEdge oprand1 = array[i];
417 BooleanEdge carray [asize -1];
419 for( uint j =0; j< asize; j++){
421 BooleanEdge oprand2 = applyLogicalOperation(SATC_NOT, array[j]);
422 carray[index++] = applyLogicalOperation(SATC_IMPLIES, oprand1, oprand2);
425 ASSERT(index == asize -1);
426 newarray[i] = applyLogicalOperation(SATC_AND, carray, asize-1);
428 return applyLogicalOperation(SATC_AND, newarray, asize+1);
431 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
432 if (!useInterpreter()) {
433 BooleanEdge newarray[asize];
436 return array[0].negate();
439 for (uint i = 0; i < 2; i++) {
440 if (isTrue(array[i])) { // It can be undefined
442 } else if (isFalse(array[i])) {
443 newarray[0] = array[1 - i];
444 return applyLogicalOperation(SATC_NOT, newarray, 1);
445 } else if (array[i]->type == LOGICOP) {
446 BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
448 return rewriteLogicalOperation(op, array, asize);
455 for (uint i = 0; i < asize; i++) {
456 newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
458 return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
462 for (uint i = 0; i < asize; i++) {
463 BooleanEdge b = array[i];
464 if (b->type == LOGICOP) {
465 if (((BooleanLogic *)b.getBoolean())->replaced)
466 return rewriteLogicalOperation(op, array, asize);
470 else if (isFalse(b)) {
473 newarray[newindex++] = b;
477 } else if (newindex == 1) {
480 bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares);
487 //handle by translation
488 return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
491 //handle by translation
492 return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
497 Boolean *boolean = new BooleanLogic(this, op, array, asize);
498 Boolean *b = boolMap.get(boolean);
500 boolean->updateParents();
501 boolMap.put(boolean, boolean);
502 allBooleans.push(boolean);
503 return BooleanEdge(boolean);
506 return BooleanEdge(b);
510 Boolean *boolean = new BooleanLogic(this, op, array, asize);
511 allBooleans.push(boolean);
512 return BooleanEdge(boolean);
517 BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
518 // ASSERT(first != second);
520 return getBooleanFalse();
523 if (order->type == SATC_TOTAL) {
524 if (first > second) {
525 uint64_t tmp = first;
531 Boolean *constraint = new BooleanOrder(order, first, second);
532 if (!useInterpreter() ) {
533 Boolean *b = boolMap.get(constraint);
536 allBooleans.push(constraint);
537 boolMap.put(constraint, constraint);
538 constraint->updateParents();
539 if ( order->graph != NULL) {
540 OrderGraph *graph = order->graph;
541 OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
543 OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
545 OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
548 if (edge != NULL && edge->mustPos) {
549 replaceBooleanWithTrueNoRemove(constraint);
550 } else if (edge != NULL && edge->mustNeg) {
551 replaceBooleanWithFalseNoRemove(constraint);
552 } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
553 && invedge->mustPos) {
554 replaceBooleanWithFalseNoRemove(constraint);
564 BooleanEdge be = BooleanEdge(constraint);
565 return negate ? be.negate() : be;
568 void CSolver::addConstraint(BooleanEdge constraint) {
569 if (!useInterpreter()) {
570 if (isTrue(constraint))
572 else if (isFalse(constraint)) {
576 if (constraint->type == LOGICOP) {
577 BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
578 if (!constraint.isNegated()) {
579 if (b->op == SATC_AND) {
580 uint size = b->inputs.getSize();
581 //Handle potential concurrent modification
582 BooleanEdge array[size];
583 for (uint i = 0; i < size; i++) {
584 array[i] = b->inputs.get(i);
586 for (uint i = 0; i < size; i++) {
587 addConstraint(array[i]);
593 addConstraint(doRewrite(constraint));
597 constraints.add(constraint);
598 Boolean *ptr = constraint.getBoolean();
600 if (ptr->boolVal == BV_UNSAT) {
604 replaceBooleanWithTrueNoRemove(constraint);
605 constraint->parents.clear();
608 constraints.add(constraint);
609 constraint->parents.clear();
613 Order *CSolver::createOrder(OrderType type, Set *set) {
614 Order *order = new Order(type, set);
615 allOrders.push(order);
616 activeOrders.add(order);
620 /** Computes static ordering information to allow isTrue/isFalse
621 queries on newly created orders to work. */
623 void CSolver::inferFixedOrder(Order *order) {
624 if (order->graph != NULL) {
627 order->graph = buildMustOrderGraph(order);
628 reachMustAnalysis(this, order->graph, true);
631 void CSolver::inferFixedOrders() {
632 SetIteratorOrder *orderit = activeOrders.iterator();
633 while (orderit->hasNext()) {
634 Order *order = orderit->next();
635 inferFixedOrder(order);
639 int CSolver::solveIncremental() {
645 long long startTime = getTimeNano();
646 bool deleteTuner = false;
648 tuner = new DefaultTuner();
651 int result = IS_INDETER;
652 ASSERT (!useInterpreter());
654 computePolarities(this);
655 // long long time1 = getTimeNano();
656 // model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
657 // Preprocess pp(this);
659 // long long time2 = getTimeNano();
660 // model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
662 // DecomposeOrderTransform dot(this);
663 // dot.doTransform();
664 // time1 = getTimeNano();
665 // model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
667 // IntegerEncodingTransform iet(this);
668 // iet.doTransform();
670 //Doing element optimization on new constraints
671 // ElementOpt eop(this);
672 // eop.doTransform();
674 //Since no new element is added, we assuming adding new constraint
675 //has no impact on previous encoding decisions
676 // EncodingGraph eg(this);
679 naiveEncodingDecision(this);
681 //Order of sat solver variables don't change!
682 // VarOrderingOpt bor(this, satEncoder);
683 // bor.doTransform();
685 long long time2 = getTimeNano();
686 //Encoding newly added constraints
687 satEncoder->encodeAllSATEncoder(this);
688 long long time1 = getTimeNano();
690 model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
692 model_print("Is problem UNSAT after encoding: %d\n", unsat);
694 result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
695 model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
696 time2 = getTimeNano();
697 elapsedTime = time2 - startTime;
698 model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
707 int CSolver::solve() {
711 long long startTime = getTimeNano();
712 bool deleteTuner = false;
714 tuner = new DefaultTuner();
717 int result = IS_INDETER;
718 if (useInterpreter()) {
719 interpreter->encode();
720 model_print("Problem encoded in Interpreter\n");
721 result = interpreter->solve();
722 model_print("Problem solved by Interpreter\n");
726 SetIteratorOrder *orderit = activeOrders.iterator();
727 while (orderit->hasNext()) {
728 Order *order = orderit->next();
729 if (order->graph != NULL) {
736 computePolarities(this);
737 long long time1 = getTimeNano();
738 model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
741 long long time2 = getTimeNano();
742 model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
744 DecomposeOrderTransform dot(this);
746 time1 = getTimeNano();
747 model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
749 IntegerEncodingTransform iet(this);
752 ElementOpt eop(this);
755 EncodingGraph eg(this);
758 naiveEncodingDecision(this);
761 VarOrderingOpt bor(this, satEncoder);
764 time2 = getTimeNano();
765 model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
767 satEncoder->encodeAllSATEncoder(this);
768 time1 = getTimeNano();
770 model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
772 model_print("Is problem UNSAT after encoding: %d\n", unsat);
775 result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
776 model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
777 time2 = getTimeNano();
778 elapsedTime = time2 - startTime;
779 model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
788 void CSolver::setInterpreter(InterpreterType type) {
789 if (interpreter == NULL) {
794 interpreter = new AlloyInterpreter(this);
797 interpreter = new SMTInterpreter(this);
801 interpreter = new MathSATInterpreter(this);
805 interpreter = new SMTRatInterpreter(this);
814 void CSolver::printConstraints() {
815 SetIteratorBooleanEdge *it = getConstraints();
816 while (it->hasNext()) {
817 BooleanEdge b = it->next();
823 void CSolver::printConstraint(BooleanEdge b) {
827 uint64_t CSolver::getElementValue(Element *element) {
828 switch (element->type) {
832 return useInterpreter() ? interpreter->getValue(element) :
833 getElementValueSATTranslator(this, element);
840 void CSolver::freezeElement(Element *e){
842 if(!incrementalMode){
843 incrementalMode = true;
847 bool CSolver::getBooleanValue(BooleanEdge bedge) {
848 Boolean *boolean = bedge.getBoolean();
849 switch (boolean->type) {
851 return useInterpreter() ? interpreter->getBooleanValue(boolean) :
852 getBooleanVariableValueSATTranslator(this, boolean);
859 bool CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) {
860 return order->encoding.resolver->resolveOrder(first, second);
863 long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
865 long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); }
867 void CSolver::autoTune(uint budget) {
868 AutoTuner *autotuner = new AutoTuner(budget);
869 autotuner->addProblem(this);