Improve propagation and add preprocessor pass
authorbdemsky <bdemsky@uci.edu>
Wed, 6 Sep 2017 03:16:40 +0000 (20:16 -0700)
committerbdemsky <bdemsky@uci.edu>
Wed, 6 Sep 2017 03:16:40 +0000 (20:16 -0700)
src/AST/rewriter.cc
src/ASTTransform/preprocess.cc [new file with mode: 0644]
src/ASTTransform/preprocess.h [new file with mode: 0644]
src/Collections/structs.h
src/Translator/sattranslator.cc
src/Tuner/tunable.h
src/csolver.cc

index 937a8b7..b6908e1 100644 (file)
@@ -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
@@ -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
@@ -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
index f52e895..e9c645f 100644 (file)
@@ -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;
index 7c48be6..d670a94 100644 (file)
@@ -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);
+       }
 }
 
 
index 4800345..660c77d 100644 (file)
@@ -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
index 62f76ab..6454b37 100644 (file)
@@ -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();