Improve propagation and add preprocessor pass

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index 937a8b74cb442f2f6a0738fa039da845a0558eb8..b6908e1f1dc1b7435b21fa637345492ad4f98971 100644 (file)
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -17,6 +17,8 @@ void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
        
 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
        updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
+
+       ASSERT(bexpr->boolVal != BV_UNSAT);
        
        uint size = bexpr->parents.getSize();
        for (uint i = 0; i < size; i++) {
@@ -44,14 +46,25 @@ void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
        if (oldb.isNegated()) {
                oldb=oldb.negate();
                newb=newb.negate();
+
        }
        if (constraints.contains(oldb)) {
                constraints.remove(oldb);
                constraints.add(newb);
+               if (newb->type == BOOLEANVAR)
+                       replaceBooleanWithTrue(newb);
+               else
+                       replaceBooleanWithTrueNoRemove(newb);
+               return;
        }
        if (constraints.contains(oldb.negate())) {
                constraints.remove(oldb.negate());
                constraints.add(newb.negate());
+               if (newb->type == BOOLEANVAR)
+                       replaceBooleanWithTrue(newb.negate());
+               else
+                       replaceBooleanWithTrueNoRemove(newb.negate());
+               return;
        }
 
        BooleanEdge oldbnegated = oldb.negate();

diff --git a/src/ASTTransform/preprocess.cc b/src/ASTTransform/preprocess.cc
new file mode 100644 (file)
index 0000000..00d324e
--- /dev/null
+++ b/src/ASTTransform/preprocess.cc
@@ -0,0 +1,66 @@
+#include "preprocess.h"
+#include "boolean.h"
+#include "csolver.h"
+#include "tunable.h"
+
+Preprocess::Preprocess(CSolver *_solver)
+        : Transform(_solver)
+{
+}
+
+Preprocess::~Preprocess() {
+}
+
+void Preprocess::doTransform() {
+       if (solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
+               return;
+       
+       SetIteratorBooleanEdge *iterator = solver->getConstraints();
+       while (iterator->hasNext()) {
+               BooleanEdge boolean = iterator->next();
+               Boolean *b = boolean.getBoolean();
+               transformBoolean(b);
+       }
+       delete iterator;
+       resolveBooleanVars();
+}
+
+void Preprocess::resolveBooleanVars() {
+       SetIteratorBoolean * iterator = toremove.iterator();
+       while (iterator->hasNext()) {
+               BooleanVar *bv = (BooleanVar *) iterator->next();
+               if (bv->polarity == P_TRUE) {
+                       solver->replaceBooleanWithTrue(BooleanEdge(bv));
+               } else if (bv->polarity == P_FALSE) {
+                       solver->replaceBooleanWithFalse(BooleanEdge(bv));
+               }
+       }
+       delete iterator;
+}
+
+void Preprocess::transformBoolean(Boolean *b) {
+       if (!processed.add(b))
+               return;
+       switch (b->type) {
+       case BOOLEANVAR:
+               processBooleanVar((BooleanVar *)b);
+               break;
+       case LOGICOP:
+               processLogicOp((BooleanLogic *)b);
+               break;
+       default:
+               break;
+       }
+}
+
+void Preprocess::processBooleanVar(BooleanVar * b) {
+       if (b->polarity==P_TRUE ||
+                       b->polarity==P_FALSE) {
+               toremove.add(b);
+       }
+}
+
+void Preprocess::processLogicOp(BooleanLogic * b) {
+       for(uint i=0; i < b->inputs.getSize(); i++)
+               transformBoolean(b->inputs.get(i).getBoolean());
+}

diff --git a/src/ASTTransform/preprocess.h b/src/ASTTransform/preprocess.h
new file mode 100644 (file)
index 0000000..3aa3749
--- /dev/null
+++ b/src/ASTTransform/preprocess.h
@@ -0,0 +1,22 @@
+#ifndef PREPROCESS_H
+#define PREPROCESS_H
+#include "classlist.h"
+#include "transform.h"
+
+class Preprocess : public Transform {
+       public:
+        Preprocess(CSolver *_solver);
+        ~Preprocess();
+        void doTransform();
+
+        CMEMALLOC;
+private:
+                               HashsetBoolean processed;
+                               HashsetBoolean toremove;
+                               void transformBoolean(Boolean *b);
+                               void processBooleanVar(BooleanVar * b);
+                               void processLogicOp(BooleanLogic * b);
+                               void resolveBooleanVars();
+};
+
+#endif

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index f52e895830c1c7e503f5e4411fd0bae49fb070a1..e9c645f3a1dc85c1b8ed166cd820aa6910c9ff1f 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -24,6 +24,7 @@ typedef Hashset<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_
 typedef Hashset<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HashsetOrderEdge;
 typedef Hashset<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> HashsetOrderElement;
 typedef Hashset<Boolean *, uintptr_t, 4> HashsetBoolean;
+typedef SetIterator<Boolean *, uintptr_t, 4> SetIteratorBoolean;
 
 typedef Hashtable<OrderNode *, HashsetOrderNode *, uintptr_t, 4> HashtableNodeToNodeSet;
 typedef Hashtable<OrderPair *, OrderPair *, uintptr_t, 4, order_pair_hash_function, order_pair_equals> HashtableOrderPair;

diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc
index 7c48be6324430b094e51477ac696b8f0075e9ebd..d670a94fdff895d795ff6240233d3ff6d84369bf 100644 (file)
--- a/src/Translator/sattranslator.cc
+++ b/src/Translator/sattranslator.cc
@@ -81,8 +81,14 @@ uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
 }
 
 bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
-       int index = getEdgeVar( ((BooleanVar *) boolean)->var );
-       return getValueSolver(This->getSATEncoder()->getCNF()->solver, index);
+       if (boolean->boolVal == BV_MUSTBETRUE)
+               return true;
+       else if (boolean->boolVal == BV_MUSTBEFALSE)
+               return false;
+       else {
+               int index = getEdgeVar( ((BooleanVar *) boolean)->var );
+               return getValueSolver(This->getSATEncoder()->getCNF()->solver, index);
+       }
 }
 
 

diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index 480034516bb328fd1e418386aeb6d985ee894509..660c77db7ab0e64162b510036aaceb0f88c64235 100644 (file)
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -37,6 +37,6 @@ public:
 static TunableDesc onoff(0, 1, 1);
 static TunableDesc offon(0, 1, 0);
 
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS};
 typedef enum Tunables Tunables;
 #endif

diff --git a/src/csolver.cc b/src/csolver.cc
index 62f76ab2223065363a8fcbdcfccdba0cb2e5b862..6454b376ed4672d05fbf31a52c77fd33695570e8 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -18,6 +18,7 @@
 #include "orderresolver.h"
 #include "integerencoding.h"
 #include "qsort.h"
+#include "preprocess.h"
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
@@ -403,6 +404,9 @@ int CSolver::solve() {
        long long startTime = getTimeNano();
        computePolarities(this);
 
+       Preprocess pp(this);
+       pp.doTransform();
+       
        DecomposeOrderTransform dot(this);
        dot.doTransform();