Interface should be bool, not happenedbefore

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index 0d6e352b50bcad23f6b6210bb80d04eddb25bd28..22b0661cb9228b765f7f7f4111ebecd8dd9bb6a7 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -11,10 +11,12 @@
 #include "sattranslator.h"
 #include "tunable.h"
 #include "polarityassignment.h"
-#include "analyzer.h"
+#include "decomposeordertransform.h"
 #include "autotuner.h"
 #include "astops.h"
 #include "structs.h"
+#include "orderresolver.h"
+#include "integerencoding.h"
 
 CSolver::CSolver() :
        boolTrue(new BooleanConst(true)),
@@ -208,7 +210,7 @@ Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint nu
 
 Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
        BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
-       Boolean * b = boolMap.get(boolean);
+       Boolean *b = boolMap.get(boolean);
        if (b == NULL) {
                boolMap.put(boolean, boolean);
                allBooleans.push(boolean);
@@ -227,57 +229,72 @@ bool CSolver::isFalse(Boolean *b) {
        return b->isFalse();
 }
 
-Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean * arg1, Boolean * arg2) {
-       Boolean * array[] = {arg1, arg2};
+Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg1, Boolean *arg2) {
+       Boolean *array[] = {arg1, arg2};
        return applyLogicalOperation(op, array, 2);
 }
 
 Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg) {
-       Boolean * array[] = {arg};
+       Boolean *array[] = {arg};
        return applyLogicalOperation(op, array, 1);
 }
 
 
 Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
-       Boolean * newarray[asize];
-       switch(op) {
+       Boolean *newarray[asize];
+       switch (op) {
        case SATC_NOT: {
-               if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op==SATC_NOT) {
+               if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op == SATC_NOT) {
                        return ((BooleanLogic *) array[0])->inputs.get(0);
                } else if (array[0]->type == BOOLCONST) {
                        return array[0]->isTrue() ? boolFalse : boolTrue;
                }
                break;
        }
+       case SATC_IFF: {
+               for (uint i = 0; i < 2; i++) {
+                       if (array[i]->type == BOOLCONST) {
+                               if (array[i]->isTrue()) {
+                                       return array[1 - i];
+                               } else {
+                                       newarray[0] = array[1 - i];
+                                       return applyLogicalOperation(SATC_NOT, newarray, 1);
+                               }
+                       }
+               }
+               break;
+       }
        case SATC_XOR: {
-               for(uint i=0;i<2;i++) {
+               for (uint i = 0; i < 2; i++) {
                        if (array[i]->type == BOOLCONST) {
                                if (array[i]->isTrue()) {
-                                       newarray[0]=array[1-i];
+                                       newarray[0] = array[1 - i];
                                        return applyLogicalOperation(SATC_NOT, newarray, 1);
                                } else
-                                       return array[1-i];
+                                       return array[1 - i];
                        }
                }
                break;
        }
        case SATC_OR: {
-               uint newindex=0;
-               for(uint i=0;i<asize;i++) {
-                       Boolean *b=array[i];
+               uint newindex = 0;
+               for (uint i = 0; i < asize; i++) {
+                       Boolean *b = array[i];
                        if (b->type == BOOLCONST) {
                                if (b->isTrue())
-                                       return b;
+                                       return boolTrue;
                                else
                                        continue;
                        } else
-                               newarray[newindex++]=b;
+                               newarray[newindex++] = b;
                }
-               if (newindex==1)
+               if (newindex == 0) {
+                       return boolFalse;
+               } else if (newindex == 1)
                        return newarray[0];
                else if (newindex == 2) {
-                       bool isNot0 = (newarray[0]->type==BOOLCONST) && ((BooleanLogic *)newarray[0])->op == SATC_NOT;
-                       bool isNot1 = (newarray[1]->type==BOOLCONST) && ((BooleanLogic *)newarray[1])->op == SATC_NOT;
+                       bool isNot0 = (newarray[0]->type == BOOLCONST) && ((BooleanLogic *)newarray[0])->op == SATC_NOT;
+                       bool isNot1 = (newarray[1]->type == BOOLCONST) && ((BooleanLogic *)newarray[1])->op == SATC_NOT;
 
                        if (isNot0 != isNot1) {
                                if (isNot0) {
@@ -296,18 +313,20 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                break;
        }
        case SATC_AND: {
-               uint newindex=0;
-               for(uint i=0;i<asize;i++) {
-                       Boolean *b=array[i];
+               uint newindex = 0;
+               for (uint i = 0; i < asize; i++) {
+                       Boolean *b = array[i];
                        if (b->type == BOOLCONST) {
                                if (b->isTrue())
                                        continue;
                                else
-                                       return b;
+                                       return boolFalse;
                        } else
-                               newarray[newindex++]=b;
+                               newarray[newindex++] = b;
                }
-               if(newindex==1) {
+               if (newindex == 0) {
+                       return boolTrue;
+               } else if (newindex == 1) {
                        return newarray[0];
                } else {
                        array = newarray;
@@ -332,13 +351,14 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                break;
        }
        }
-       
+
+       ASSERT(asize != 0);
        Boolean *boolean = new BooleanLogic(this, op, array, asize);
        Boolean *b = boolMap.get(boolean);
        if (b == NULL) {
                boolMap.put(boolean, boolean);
                allBooleans.push(boolean);
-               return boolean;         
+               return boolean;
        } else {
                delete boolean;
                return b;
@@ -363,19 +383,27 @@ void CSolver::addConstraint(Boolean *constraint) {
 Order *CSolver::createOrder(OrderType type, Set *set) {
        Order *order = new Order(type, set);
        allOrders.push(order);
+       activeOrders.add(order);
        return order;
 }
 
-int CSolver::startEncoding() {
+int CSolver::solve() {
        bool deleteTuner = false;
        if (tuner == NULL) {
                tuner = new DefaultTuner();
                deleteTuner = true;
        }
-               
+
        long long startTime = getTimeNano();
        computePolarities(this);
-       orderAnalysis(this);
+
+       DecomposeOrderTransform dot(this);
+       dot.doTransform();
+
+       //This leaks like crazy
+       //      IntegerEncodingTransform iet(this);
+       //iet.doTransform();
+
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
        int result = unsat ? IS_UNSAT : satEncoder->solve();
@@ -410,8 +438,8 @@ bool CSolver::getBooleanValue(Boolean *boolean) {
        exit(-1);
 }
 
-HappenedBefore CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) {
-       return getOrderConstraintValueSATTranslator(this, order, first, second);
+bool CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) {
+       return order->encoding.resolver->resolveOrder(first, second);
 }
 
 long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
@@ -419,7 +447,7 @@ long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
 long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); }
 
 void CSolver::autoTune(uint budget) {
-       AutoTuner * autotuner=new AutoTuner(budget);
+       AutoTuner *autotuner = new AutoTuner(budget);
        autotuner->addProblem(this);
        autotuner->tune();
        delete autotuner;