Small edit

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index 310d535489f365cb6fddf73b4f6ccae8d99ff0ef..0270758af28faa087efc0d2f2cc358e15a221d53 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -11,7 +11,7 @@
 #include "sattranslator.h"
 #include "tunable.h"
 #include "polarityassignment.h"
-#include "analyzer.h"
+#include "transformer.h"
 #include "autotuner.h"
 #include "astops.h"
 #include "structs.h"
@@ -24,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 */
@@ -67,6 +68,7 @@ CSolver::~CSolver() {
        delete boolTrue;
        delete boolFalse;
        delete satEncoder;
+       delete transformer;
 }
 
 CSolver *CSolver::clone() {
@@ -93,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);
@@ -214,6 +221,25 @@ 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) {
@@ -225,6 +251,19 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize)
                }
                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++) {
                        if (array[i]->type == BOOLCONST) {
@@ -342,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();
@@ -351,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();