From e163c1968c17a3a248abcafbf4b61597b5f56b1d Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 5 Sep 2017 20:16:40 -0700 Subject: [PATCH 1/1] Improve propagation and add preprocessor pass --- src/AST/rewriter.cc | 13 +++++++ src/ASTTransform/preprocess.cc | 66 +++++++++++++++++++++++++++++++++ src/ASTTransform/preprocess.h | 22 +++++++++++ src/Collections/structs.h | 1 + src/Translator/sattranslator.cc | 10 ++++- src/Tuner/tunable.h | 2 +- src/csolver.cc | 4 ++ 7 files changed, 115 insertions(+), 3 deletions(-) create mode 100644 src/ASTTransform/preprocess.cc create mode 100644 src/ASTTransform/preprocess.h diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index 937a8b7..b6908e1 100644 --- 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 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 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 f52e895..e9c645f 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -24,6 +24,7 @@ typedef Hashset HashsetOrderEdge; typedef Hashset HashsetOrderElement; typedef Hashset HashsetBoolean; +typedef SetIterator SetIteratorBoolean; typedef Hashtable HashtableNodeToNodeSet; typedef Hashtable HashtableOrderPair; diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc index 7c48be6..d670a94 100644 --- 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 4800345..660c77d 100644 --- 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 62f76ab..6454b37 100644 --- 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(); -- 2.34.1