Small edit

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index 343754c48914cc18ae4c99fe80fba176c0446573..0270758af28faa087efc0d2f2cc358e15a221d53 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -11,8 +11,10 @@
 #include "sattranslator.h"
 #include "tunable.h"
 #include "polarityassignment.h"
-#include "analyzer.h"
+#include "transformer.h"
 #include "autotuner.h"
+#include "astops.h"
+#include "structs.h"
 
 CSolver::CSolver() :
        boolTrue(new BooleanConst(true)),
@@ -22,6 +24,7 @@ CSolver::CSolver() :
        elapsedTime(0)
 {
        satEncoder = new SATEncoder(this);
+       transformer = new Transformer(this);
 }
 
 /** This function tears down the solver and the entire AST */
@@ -65,12 +68,13 @@ CSolver::~CSolver() {
        delete boolTrue;
        delete boolFalse;
        delete satEncoder;
+       delete transformer;
 }
 
 CSolver *CSolver::clone() {
        CSolver *copy = new CSolver();
        CloneMap map;
-       HSIteratorBoolean *it = getConstraints();
+       SetIteratorBoolean *it = getConstraints();
        while (it->hasNext()) {
                Boolean *b = it->next();
                copy->addConstraint(b->clone(copy, &map));
@@ -91,6 +95,11 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange
        return set;
 }
 
+Element *CSolver::createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange) {
+       Set *s = createRangeSet(type, lowrange, highrange);
+       return getElementVar(s);
+}
+
 MutableSet *CSolver::createMutableSet(VarType type) {
        MutableSet *set = new MutableSet(type);
        allSets.push(set);
@@ -102,7 +111,7 @@ void CSolver::addItem(MutableSet *set, uint64_t element) {
 }
 
 uint64_t CSolver::createUniqueItem(MutableSet *set) {
-       uint64_t element = set->low++;
+       uint64_t element = set->getNewUniqueItem();
        set->addElementMSet(element);
        return element;
 }
@@ -212,38 +221,67 @@ Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, ui
        }
 }
 
+bool CSolver::isTrue(Boolean *b) {
+       return b->isTrue();
+}
+
+bool CSolver::isFalse(Boolean *b) {
+       return b->isFalse();
+}
+
+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};
+       return applyLogicalOperation(op, array, 1);
+}
+
+
 Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
        Boolean * newarray[asize];
        switch(op) {
-       case L_NOT: {
-               if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op==L_NOT) {
+       case 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) {
-                       bool isTrue = ((BooleanConst *) array[0])->isTrue;
-                       return isTrue ? boolFalse : boolTrue;
+                       return array[0]->isTrue() ? boolFalse : boolTrue;
                }
                break;
        }
-       case L_XOR: {
+       case SATC_IFF: {
                for(uint i=0;i<2;i++) {
                        if (array[i]->type == BOOLCONST) {
-                               bool isTrue = ((BooleanConst *) array[i])->isTrue;
-                               if (isTrue) {
+                               if (array[i]->isTrue()) {
+                                       return array[1-i];
+                               } else {
                                        newarray[0]=array[1-i];
-                                       return applyLogicalOperation(L_NOT, newarray, 1);
+                                       return applyLogicalOperation(SATC_NOT, newarray, 1);
+                               }
+                       }
+               }
+               break;
+       }
+       case SATC_XOR: {
+               for(uint i=0;i<2;i++) {
+                       if (array[i]->type == BOOLCONST) {
+                               if (array[i]->isTrue()) {
+                                       newarray[0]=array[1-i];
+                                       return applyLogicalOperation(SATC_NOT, newarray, 1);
                                } else
                                        return array[1-i];
                        }
                }
                break;
        }
-       case L_OR: {
+       case SATC_OR: {
                uint newindex=0;
                for(uint i=0;i<asize;i++) {
                        Boolean *b=array[i];
                        if (b->type == BOOLCONST) {
-                               bool isTrue = ((BooleanConst *) b)->isTrue;
-                               if (isTrue)
+                               if (b->isTrue())
                                        return b;
                                else
                                        continue;
@@ -253,8 +291,8 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                if (newindex==1)
                        return newarray[0];
                else if (newindex == 2) {
-                       bool isNot0 = (newarray[0]->type==BOOLCONST) && ((BooleanLogic *)newarray[0])->op == L_NOT;
-                       bool isNot1 = (newarray[1]->type==BOOLCONST) && ((BooleanLogic *)newarray[1])->op == L_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) {
@@ -264,7 +302,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                                        array[1] = array[0];
                                        array[0] = tmp;
                                }
-                               return applyLogicalOperation(L_IMPLIES, newarray, 2);
+                               return applyLogicalOperation(SATC_IMPLIES, newarray, 2);
                        }
                } else {
                        array = newarray;
@@ -272,13 +310,12 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                }
                break;
        }
-       case L_AND: {
+       case SATC_AND: {
                uint newindex=0;
                for(uint i=0;i<asize;i++) {
                        Boolean *b=array[i];
                        if (b->type == BOOLCONST) {
-                               bool isTrue = ((BooleanConst *) b)->isTrue;
-                               if (isTrue)
+                               if (b->isTrue())
                                        continue;
                                else
                                        return b;
@@ -293,20 +330,18 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                }
                break;
        }
-       case L_IMPLIES: {
+       case SATC_IMPLIES: {
                if (array[0]->type == BOOLCONST) {
-                       BooleanConst *b=(BooleanConst *) array[0];
-                       if (b->isTrue) {
+                       if (array[0]->isTrue()) {
                                return array[1];
                        } else {
                                return boolTrue;
                        }
                } else if (array[1]->type == BOOLCONST) {
-                       BooleanConst *b=(BooleanConst *) array[0];
-                       if (b->isTrue) {
-                               return b;
+                       if (array[1]->isTrue()) {
+                               return array[1];
                        } else {
-                               return applyLogicalOperation(L_NOT, array, 1);
+                               return applyLogicalOperation(SATC_NOT, array, 1);
                        }
                }
                break;
@@ -346,7 +381,7 @@ Order *CSolver::createOrder(OrderType type, Set *set) {
        return order;
 }
 
-int CSolver::startEncoding() {
+int CSolver::solve() {
        bool deleteTuner = false;
        if (tuner == NULL) {
                tuner = new DefaultTuner();
@@ -355,7 +390,7 @@ int CSolver::startEncoding() {
                
        long long startTime = getTimeNano();
        computePolarities(this);
-       orderAnalysis(this);
+       transformer->orderAnalysis();
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
        int result = unsat ? IS_UNSAT : satEncoder->solve();