From edf36c0c6c3107809268465a62370e2fee09e659 Mon Sep 17 00:00:00 2001 From: lianah Date: Mon, 8 Apr 2013 15:31:08 -0400 Subject: added support for dumping the SAT problem the sat solver is working on --- src/prop/minisat/core/Solver.h | 3 +++ src/prop/minisat/simp/SimpSolver.cc | 4 ++++ src/prop/options | 3 +++ 3 files changed, 10 insertions(+) diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 9338f9b55..55780479a 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -173,6 +173,7 @@ public: bool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions. bool okay () const; // FALSE means solver is in a conflicting state + void toDimacs (); void toDimacs (FILE* f, const vec& assumps); // Write CNF to file in DIMACS-format. void toDimacs (const char *file, const vec& assumps); void toDimacs (FILE* f, Clause& c, vec& map, Var& max); @@ -539,12 +540,14 @@ inline bool Solver::solve (const vec& assumps){ budgetOff(); as inline lbool Solver::solveLimited (const vec& assumps){ assumps.copyTo(assumptions); return solve_(); } inline bool Solver::okay () const { return ok; } +inline void Solver::toDimacs () { vec as; toDimacs(stdout, as); } inline void Solver::toDimacs (const char* file){ vec as; toDimacs(file, as); } inline void Solver::toDimacs (const char* file, Lit p){ vec as; as.push(p); toDimacs(file, as); } inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec as; as.push(p); as.push(q); toDimacs(file, as); } inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); } + //================================================================================================= // Debug etc: diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 9c3e59954..0e0e5d3ae 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -113,6 +113,10 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) { + if (options::minisatDumpDimacs()) { + toDimacs(); + return l_Undef; + } popTrail(); vec extra_frozen; diff --git a/src/prop/options b/src/prop/options index cda99538c..e3a0f814a 100644 --- a/src/prop/options +++ b/src/prop/options @@ -28,4 +28,7 @@ option sat_refine_conflicts --refine-conflicts bool option minisatUseElim --minisat-elimination bool :default true :read-write use Minisat elimination +option minisatDumpDimacs --minisat-dump-dimacs bool :default false + instead of solving minisat dumps the asserted clauses in Dimacs format + endmodule -- cgit v1.2.3 From f39bf07dcc2b770a4166325c4c8f94cb70af3388 Mon Sep 17 00:00:00 2001 From: lianah Date: Tue, 9 Apr 2013 20:30:06 -0400 Subject: started work on bv1 to boolean lifting --- src/theory/bv/bv_to_bool.cpp | 103 +++++++++++++++++++++++++++++++++++++++++++ src/theory/bv/bv_to_bool.h | 71 +++++++++++++++++++++++++++++ 2 files changed, 174 insertions(+) create mode 100644 src/theory/bv/bv_to_bool.cpp create mode 100644 src/theory/bv/bv_to_bool.h diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp new file mode 100644 index 000000000..fb25f4348 --- /dev/null +++ b/src/theory/bv/bv_to_bool.cpp @@ -0,0 +1,103 @@ +/********************* */ +/*! \file bv_to_bool.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: None. + ** Minor contributors (to current version): None. + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans. + ** + ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. + **/ + + +#include "util/node_visitor.h" + + +void BVToBoolVisitor::addBvToBool(TNode bv_term, Node bool_term) { + Assert (!hasBoolTerm(bv_term)); + Assert (bool_term.getType().isBoolean()); + d_bvToBool[bv_term] = bool_term; +} + +Node BVToBoolVisitor::toBoolTerm(TNode bv_term) const { + Assert (hasBoolTerm(bv_term)); + return d_bvToBool.find(bv_term)->second; +} + +bool BVToBoolVisitor::hasBoolTerm(TNode bv_term) const { + Assert (bv_term.getType().isBitVector()); + return d_bvToBool.find(bv_term) != d_bvToBool.end(); +} + +void BVToBoolVisitor::start(TNode node) {} + +return_type BVToBoolVisitor::done(TNode node) { + return 0; +} + +bool BvToBoolVisitor::alreadyVisited(TNode current, TNode parent) { + return d_visited.find(current) != d_visited.end(); +} + +bool BvToBoolVisitor::isConvertibleToBool(TNode current) { + if (current.getNumChildren() == 0) { + return current.getType().getBitVectorSize() == 1; + } + + Kind kind = current.getKind(); + if (kind == kind::BITVECTOR_OR || + kind == kind::BITVECTOR_AND || + kind == kind::BITVECTOR_XOR || + kind == kind::BITVECTOR_NOT || + kind == kind::BITVECTOR_ADD || + kind == kind::BITVECTOR_NOT || + kind == kind::BITVECTOR_ULT || + kind == kind::BITVECTOR_ULE) { + return current[0].getType().getBitVectorSize() == 1; + } +} + +void BvToBoolVisitor::visit(TNode current, TNode parent) { + Assert (!alreadyVisited()); + + if (current.getType().isBitVector() && + current.getType().getBitVectorSize() != 1) { + // we only care about bit-vector terms of size 1 + d_visited.push_back(current); + return; + } + + d_visited.insert(current); + + if (current.getNumChildren() == 0 && + current.getType().isBitVector() && + current.getType().getBitVectorSize() == 1) { + Node bool_current; + if (current.getKind() == kind::CONST_BITVECTOR) { + bool_current = current == d_one? utils::mkTrue() : utils::mkFalse(); + } else { + bool_current = utils::mkNode(kind::EQUAL, current, d_one); + } + addBvToBool(current, current_eq_one); + return; + } + + // if it has more than one child + if (current.getKind().isBitVectorKind() && isConvertibleToBool(current)) { + Kind bool_kind = boolToBvKind(current.getKind()); + NodeBuilder<> builder(bool_kind); + for (unsigned i = 0; i < current.getNumChildren(); ++i) { + builder << toBoolTerm(current[i]); + } + Node bool_current = builder; + addBvToBool(current, bool_current); + } +} + +return_type BvToBoolVisitor::done(TNode node) {} + diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h new file mode 100644 index 000000000..6e865658f --- /dev/null +++ b/src/theory/bv/bv_to_bool.h @@ -0,0 +1,71 @@ +/********************* */ +/*! \file bv_to_bool.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: None. + ** Minor contributors (to current version): None. + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Preprocessing pass that lifts bit-vectors of size 1 to booleans. + ** + ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H +#define __CVC4__THEORY__BV__BV_TO_BOOL_H + +namespace CVC4 { +namespace theory { +namespace bv { + +class BvToBoolVisitor { + typedef unsigned return_type; + typedef __gnu_cxx::hash_set TNodeSet; + typedef __gnu_cxx::hash_map TNodeNodeMap; + TNodeNodeMap d_bvToBool; + TNodeSet d_visited; + Node d_one; + Node d_zero; + + void addBvToBool(TNode bv_term, Node bool_term); + Node toBoolTerm(TNode bv_term) const; + bool hasBoolTerm(TNode bv_term) const; + +public: + BvToBoolVisitor() + : d_substitution(), + d_visited, + d_one(utils::mkConst(BitVector(1, 1u))), + d_zero(utils::mkConst(BitVector(1, 0u))) + {} + void start(TNode node); + bool alreadyVisited(TNode current, TNode parent); + void visit(TNode current, TNode parent); + return_type done(TNode node); + Node liftBoolToBV(TNode node); + +}; + +class BvToBoolPreprocessor { + BvToBoolVisitor d_visitor; +public: + BvToBoolPreprocessor() + : d_visitor + {} + ~BvToBoolPreprocessor() {} + Node liftBvToBool(TNode assertion); +}; + + +}/* CVC4::theory::bv namespace */ +}/* CVC4::theory namespace */ + +}/* CVC4 namespace */ + + +#endif /* __CVC4__THEORY__BV__BV_TO_BOOL_H */ -- cgit v1.2.3 From c3f618c1bc4ede1e975bc33903ec5dffb012c897 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Wed, 10 Apr 2013 00:03:02 -0400 Subject: more work on boolean lifting --- src/theory/bv/Makefile.am | 4 +- src/theory/bv/bv_to_bool.cpp | 135 +++++++++++++++++++++++++++++++------------ src/theory/bv/bv_to_bool.h | 30 +++++----- 3 files changed, 117 insertions(+), 52 deletions(-) diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index a70521791..8651f280b 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -12,6 +12,8 @@ libbv_la_SOURCES = \ type_enumerator.h \ bitblaster.h \ bitblaster.cpp \ + bv_to_bool.h \ + bv_to_bool.cpp \ bv_subtheory.h \ bv_subtheory_core.h \ bv_subtheory_core.cpp \ @@ -36,7 +38,7 @@ libbv_la_SOURCES = \ theory_bv_type_rules.h \ theory_bv_rewriter.h \ theory_bv_rewriter.cpp \ - cd_set_collection.h + cd_set_collection.h EXTRA_DIST = \ kinds diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index fb25f4348..f39d12a39 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -16,88 +16,149 @@ #include "util/node_visitor.h" +#include "theory/bv/bv_to_bool.h" +using namespace std; +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; -void BVToBoolVisitor::addBvToBool(TNode bv_term, Node bool_term) { - Assert (!hasBoolTerm(bv_term)); +void BvToBoolVisitor::addToCache(TNode bv_term, Node bool_term) { + Assert (!hasCache(bv_term)); Assert (bool_term.getType().isBoolean()); - d_bvToBool[bv_term] = bool_term; + d_cache[bv_term] = bool_term; } -Node BVToBoolVisitor::toBoolTerm(TNode bv_term) const { - Assert (hasBoolTerm(bv_term)); - return d_bvToBool.find(bv_term)->second; +Node BvToBoolVisitor::getCache(TNode bv_term) const { + Assert (hasCache(bv_term)); + return d_cache.find(bv_term)->second; } -bool BVToBoolVisitor::hasBoolTerm(TNode bv_term) const { +bool BvToBoolVisitor::hasCache(TNode bv_term) const { Assert (bv_term.getType().isBitVector()); - return d_bvToBool.find(bv_term) != d_bvToBool.end(); + return d_cache.find(bv_term) != d_cache.end(); } -void BVToBoolVisitor::start(TNode node) {} - -return_type BVToBoolVisitor::done(TNode node) { - return 0; -} +void BvToBoolVisitor::start(TNode node) {} bool BvToBoolVisitor::alreadyVisited(TNode current, TNode parent) { return d_visited.find(current) != d_visited.end(); } bool BvToBoolVisitor::isConvertibleToBool(TNode current) { - if (current.getNumChildren() == 0) { - return current.getType().getBitVectorSize() == 1; + TypeNode type = current.getType(); + if (current.getNumChildren() == 0 && type.isBitVector()) { + return type.getBitVectorSize() == 1; } + if (current.getKind() == kind::NOT) { + current = current[0]; + } Kind kind = current.getKind(); + // checking bit-vector kinds if (kind == kind::BITVECTOR_OR || kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_XOR || kind == kind::BITVECTOR_NOT || - kind == kind::BITVECTOR_ADD || - kind == kind::BITVECTOR_NOT || + // kind == kind::BITVECTOR_PLUS || + // kind == kind::BITVECTOR_SUB || + // kind == kind::BITVECTOR_NEG || kind == kind::BITVECTOR_ULT || - kind == kind::BITVECTOR_ULE) { + kind == kind::BITVECTOR_ULE || + kind == kind::EQUAL) { return current[0].getType().getBitVectorSize() == 1; } + if (kind == kind::ITE && + type.isBitVector()) { + return type.getBitVectorSize() == 1; + } + return false; } -void BvToBoolVisitor::visit(TNode current, TNode parent) { - Assert (!alreadyVisited()); - - if (current.getType().isBitVector() && - current.getType().getBitVectorSize() != 1) { - // we only care about bit-vector terms of size 1 - d_visited.push_back(current); - return; +Node BvToBoolVisitor::convertToBool(TNode current) { + Kind kind = current.getKind(); + if (kind == kind::BITVECTOR_ULT) { + TNode a = getCache(current[0]); + TNode b = getCache(current[1]); + Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero); + Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one); + Node new_current = utils::mkNode(kind::AND, a_eq_0, b_eq_1); + return new_current; + } + if (kind == kind::BITVECTOR_ULE) { + TNode a = getCache(current[0]); + TNode b = getCache(current[1]); + Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero); + Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one); + Node a_lt_b = utils::mkNode(kind::AND, a_eq_0, b_eq_1); + Node a_eq_b = utils::mkNode(kind::EQUAL, a, b); + Node new_current = utils::mkNode(kind::OR, a_lt_b, a_eq_b); + return new_current; } + + Kind new_kind; + switch (kind) { + case kind::BITVECTOR_OR : + new_kind = kind::OR; + case kind::BITVECTOR_AND: + new_kind = kind::AND; + case kind::BITVECTOR_XOR: + new_kind = kind::XOR; + case kind::BITVECTOR_NOT: + new_kind = kind::NOT; + case kind::BITVECTOR_ULT: + default: + Unreachable(); + } + NodeBuilder<> builder(new_kind); + for (unsigned i = 0; i < current.getNumChildren(); ++i) { + builder << getCache(current[i]); + } + return builder; +} + +void BvToBoolVisitor::visit(TNode current, TNode parent) { + Assert (!alreadyVisited(current, parent)); d_visited.insert(current); if (current.getNumChildren() == 0 && - current.getType().isBitVector() && - current.getType().getBitVectorSize() == 1) { + isConvertibleToBool(current)) { Node bool_current; if (current.getKind() == kind::CONST_BITVECTOR) { bool_current = current == d_one? utils::mkTrue() : utils::mkFalse(); } else { bool_current = utils::mkNode(kind::EQUAL, current, d_one); } - addBvToBool(current, current_eq_one); + addToCache(current, bool_current); return; } // if it has more than one child - if (current.getKind().isBitVectorKind() && isConvertibleToBool(current)) { - Kind bool_kind = boolToBvKind(current.getKind()); - NodeBuilder<> builder(bool_kind); + if (isConvertibleToBool(current)) { + Node bool_current = convertToBool(current); + addToCache(current, bool_current); + } else { + NodeBuilder<> builder(current.getKind()); for (unsigned i = 0; i < current.getNumChildren(); ++i) { - builder << toBoolTerm(current[i]); + Node converted = getCache(current[i]); + if (converted.getType() == current[i].getType()) { + builder << converted; + } else { + builder << current[i]; + } } - Node bool_current = builder; - addBvToBool(current, bool_current); - } + Node result = builder; + addToCache(current, result); + } } -return_type BvToBoolVisitor::done(TNode node) {} +BvToBoolVisitor::return_type BvToBoolVisitor::done(TNode node) { + Assert (hasCache(node)); + return getCache(node); +} +Node BvToBoolPreprocessor::liftBoolToBV(TNode assertion) { + Node result = NodeVisitor::run(d_visitor, assertion); + return result; +} diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index 6e865658f..ef80930b4 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -15,6 +15,7 @@ **/ #include "cvc4_private.h" +#include "theory/bv/theory_bv_utils.h" #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H #define __CVC4__THEORY__BV__BV_TO_BOOL_H @@ -24,22 +25,25 @@ namespace theory { namespace bv { class BvToBoolVisitor { - typedef unsigned return_type; - typedef __gnu_cxx::hash_set TNodeSet; - typedef __gnu_cxx::hash_map TNodeNodeMap; - TNodeNodeMap d_bvToBool; + + typedef __gnu_cxx::hash_set TNodeSet; + typedef __gnu_cxx::hash_map TNodeNodeMap; + TNodeNodeMap d_cache; TNodeSet d_visited; Node d_one; Node d_zero; - void addBvToBool(TNode bv_term, Node bool_term); - Node toBoolTerm(TNode bv_term) const; - bool hasBoolTerm(TNode bv_term) const; - + void addToCache(TNode bv_term, Node bool_term); + Node getCache(TNode bv_term) const; + bool hasCache(TNode bv_term) const; + + bool isConvertibleToBool(TNode current); + Node convertToBool(TNode current); public: + typedef Node return_type; BvToBoolVisitor() - : d_substitution(), - d_visited, + : d_cache(), + d_visited(), d_one(utils::mkConst(BitVector(1, 1u))), d_zero(utils::mkConst(BitVector(1, 0u))) {} @@ -47,18 +51,16 @@ public: bool alreadyVisited(TNode current, TNode parent); void visit(TNode current, TNode parent); return_type done(TNode node); - Node liftBoolToBV(TNode node); - }; class BvToBoolPreprocessor { BvToBoolVisitor d_visitor; public: BvToBoolPreprocessor() - : d_visitor + : d_visitor() {} ~BvToBoolPreprocessor() {} - Node liftBvToBool(TNode assertion); + Node liftBoolToBV(TNode assertion); }; -- cgit v1.2.3 From c5c8a6497f8ac52c4f2c57fcd5ed23790f26c735 Mon Sep 17 00:00:00 2001 From: lianah Date: Fri, 12 Apr 2013 16:15:30 -0400 Subject: finished implementing bv to bool lifting and added --bv-to-bool option --- src/smt/smt_engine.cpp | 22 +++++- src/theory/bv/bv_to_bool.cpp | 179 +++++++++++++++++++++++++++---------------- src/theory/bv/bv_to_bool.h | 13 +++- src/theory/bv/options | 3 + src/theory/bv/theory_bv.cpp | 9 ++- src/theory/theory_engine.cpp | 9 ++- src/theory/theory_engine.h | 4 + 7 files changed, 165 insertions(+), 74 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 55000c94d..9ee2c5722 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -349,7 +349,9 @@ private: */ bool checkForBadSkolems(TNode n, TNode skolem, hash_map& cache); - + // Lift bit-vectors of size 1 to booleans + void bvToBool(); + // Simplify ITE structure void simpITE(); @@ -1925,6 +1927,14 @@ bool SmtEnginePrivate::nonClausalSimplify() { } +void SmtEnginePrivate::bvToBool() { + Trace("simplify") << "SmtEnginePrivate::bvToBool()" << endl; + + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + d_assertionsToCheck[i] = d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck[i]); + } +} + void SmtEnginePrivate::simpITE() { TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime); @@ -2474,6 +2484,16 @@ bool SmtEnginePrivate::simplifyAssertions() Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + // Lift bit-vectors of size 1 to bool + if(options::bvToBool()) { + Chat() << "...doing bvToBool..." << endl; + bvToBool(); + } + + Trace("smt") << "POST bvToBool" << endl; + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) { Chat() << "...doing another round of nonclausal simplification..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index f39d12a39..5ab7cf144 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -23,22 +23,40 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; -void BvToBoolVisitor::addToCache(TNode bv_term, Node bool_term) { - Assert (!hasCache(bv_term)); +void BvToBoolVisitor::storeBvToBool(TNode bv_term, Node bool_term) { + Assert (!hasBoolTerm(bv_term)); Assert (bool_term.getType().isBoolean()); - d_cache[bv_term] = bool_term; + d_bvToBoolTerm[bv_term] = bool_term; } -Node BvToBoolVisitor::getCache(TNode bv_term) const { - Assert (hasCache(bv_term)); - return d_cache.find(bv_term)->second; +Node BvToBoolVisitor::getBoolTerm(TNode bv_term) const { + Assert(hasBoolTerm(bv_term)); + return d_bvToBoolTerm.find(bv_term)->second; } -bool BvToBoolVisitor::hasCache(TNode bv_term) const { +bool BvToBoolVisitor::hasBoolTerm(TNode bv_term) const { Assert (bv_term.getType().isBitVector()); - return d_cache.find(bv_term) != d_cache.end(); + return d_bvToBoolTerm.find(bv_term) != d_bvToBoolTerm.end(); } +void BvToBoolVisitor::addToCache(TNode term, Node new_term) { + Assert (new_term != Node()); + Assert (!hasCache(term)); + d_cache[term] = new_term; +} + +Node BvToBoolVisitor::getCache(TNode term) const { + if (!hasCache(term)) { + return term; + } + return d_cache.find(term)->second; +} + +bool BvToBoolVisitor::hasCache(TNode term) const { + return d_cache.find(term) != d_cache.end(); +} + + void BvToBoolVisitor::start(TNode node) {} bool BvToBoolVisitor::alreadyVisited(TNode current, TNode parent) { @@ -60,95 +78,126 @@ bool BvToBoolVisitor::isConvertibleToBool(TNode current) { kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_XOR || kind == kind::BITVECTOR_NOT || - // kind == kind::BITVECTOR_PLUS || - // kind == kind::BITVECTOR_SUB || - // kind == kind::BITVECTOR_NEG || kind == kind::BITVECTOR_ULT || kind == kind::BITVECTOR_ULE || kind == kind::EQUAL) { - return current[0].getType().getBitVectorSize() == 1; + // we can convert it to bool if all of the children can also be converted + // to bool + if (! current[0].getType().getBitVectorSize() == 1) + return false; + for (unsigned i = 0; i < current.getNumChildren(); ++i) { + // we assume that the children have been visited + if (!hasBoolTerm(current[i])) + return false; + } + return true; } if (kind == kind::ITE && type.isBitVector()) { - return type.getBitVectorSize() == 1; + return type.getBitVectorSize() == 1 && hasBoolTerm(current[1]) && hasBoolTerm(current[2]); } return false; } + Node BvToBoolVisitor::convertToBool(TNode current) { + Debug("bv-to-bool") << "BvToBoolVisitor::convertToBool (" << current << ") "; Kind kind = current.getKind(); - if (kind == kind::BITVECTOR_ULT) { - TNode a = getCache(current[0]); - TNode b = getCache(current[1]); + + Node new_current; + if (current.getNumChildren() == 0) { + if (current.getKind() == kind::CONST_BITVECTOR) { + new_current = current == d_one? utils::mkTrue() : utils::mkFalse(); + } else { + new_current = utils::mkNode(kind::EQUAL, current, d_one); + } + Debug("bv-to-bool") << "=> " << new_current << "\n"; + } else if (kind == kind::BITVECTOR_ULT) { + TNode a = getBoolTerm(current[0]); + TNode b = getBoolTerm(current[1]); Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero); Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one); - Node new_current = utils::mkNode(kind::AND, a_eq_0, b_eq_1); - return new_current; - } - if (kind == kind::BITVECTOR_ULE) { - TNode a = getCache(current[0]); - TNode b = getCache(current[1]); + new_current = utils::mkNode(kind::AND, a_eq_0, b_eq_1); + } else if (kind == kind::BITVECTOR_ULE) { + TNode a = getBoolTerm(current[0]); + TNode b = getBoolTerm(current[1]); Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero); Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one); Node a_lt_b = utils::mkNode(kind::AND, a_eq_0, b_eq_1); Node a_eq_b = utils::mkNode(kind::EQUAL, a, b); - Node new_current = utils::mkNode(kind::OR, a_lt_b, a_eq_b); - return new_current; + new_current = utils::mkNode(kind::OR, a_lt_b, a_eq_b); + } else if (kind == kind::ITE) { + TNode cond = current[0]; + TNode a = getBoolTerm(current[1]); + TNode b = getBoolTerm(current[2]); + new_current = utils::mkNode(kind::ITE, cond, a, b); + } else { + Kind new_kind; + switch (kind) { + case kind::BITVECTOR_OR : + new_kind = kind::OR; + break; + case kind::BITVECTOR_AND: + new_kind = kind::AND; + break; + case kind::BITVECTOR_XOR: + new_kind = kind::XOR; + break; + case kind::BITVECTOR_NOT: + new_kind = kind::NOT; + break; + case kind::EQUAL: + new_kind = kind::IFF; + break; + default: + Unreachable("Unknown kind ", kind); + } + NodeBuilder<> builder(new_kind); + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { + builder << current.getOperator(); + } + for (unsigned i = 0; i < current.getNumChildren(); ++i) { + builder << getBoolTerm(current[i]); + } + new_current = builder; } - - Kind new_kind; - switch (kind) { - case kind::BITVECTOR_OR : - new_kind = kind::OR; - case kind::BITVECTOR_AND: - new_kind = kind::AND; - case kind::BITVECTOR_XOR: - new_kind = kind::XOR; - case kind::BITVECTOR_NOT: - new_kind = kind::NOT; - case kind::BITVECTOR_ULT: - default: - Unreachable(); - } - NodeBuilder<> builder(new_kind); - for (unsigned i = 0; i < current.getNumChildren(); ++i) { - builder << getCache(current[i]); + Debug("bv-to-bool") << "=> " << new_current << "\n"; + if (current.getType().isBitVector()) { + storeBvToBool(current, new_current); + } else { + addToCache(current, new_current); } - return builder; + return new_current; } void BvToBoolVisitor::visit(TNode current, TNode parent) { + Debug("bv-to-bool") << "BvToBoolVisitor visit (" << current << ", " << parent << ")\n"; Assert (!alreadyVisited(current, parent)); d_visited.insert(current); - - if (current.getNumChildren() == 0 && - isConvertibleToBool(current)) { - Node bool_current; - if (current.getKind() == kind::CONST_BITVECTOR) { - bool_current = current == d_one? utils::mkTrue() : utils::mkFalse(); - } else { - bool_current = utils::mkNode(kind::EQUAL, current, d_one); - } - addToCache(current, bool_current); - return; - } + Node result; // if it has more than one child if (isConvertibleToBool(current)) { - Node bool_current = convertToBool(current); - addToCache(current, bool_current); + result = convertToBool(current); } else { - NodeBuilder<> builder(current.getKind()); - for (unsigned i = 0; i < current.getNumChildren(); ++i) { - Node converted = getCache(current[i]); - if (converted.getType() == current[i].getType()) { - builder << converted; - } else { - builder << current[i]; + if (current.getNumChildren() == 0) { + result = current; + } else { + NodeBuilder<> builder(current.getKind()); + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { + builder << current.getOperator(); + } + for (unsigned i = 0; i < current.getNumChildren(); ++i) { + Node converted = getCache(current[i]); + if (converted.getType() == current[i].getType()) { + builder << converted; + } else { + builder << current[i]; + } } + result = builder; } - Node result = builder; addToCache(current, result); } } diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index ef80930b4..d5673a295 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -29,20 +29,27 @@ class BvToBoolVisitor { typedef __gnu_cxx::hash_set TNodeSet; typedef __gnu_cxx::hash_map TNodeNodeMap; TNodeNodeMap d_cache; + TNodeNodeMap d_bvToBoolTerm; TNodeSet d_visited; Node d_one; Node d_zero; - void addToCache(TNode bv_term, Node bool_term); - Node getCache(TNode bv_term) const; - bool hasCache(TNode bv_term) const; + void storeBvToBool(TNode bv_term, Node bool_term); + Node getBoolTerm(TNode bv_term) const; + bool hasBoolTerm(TNode bv_term) const; + void addToCache(TNode term, Node new_term); + Node getCache(TNode term) const; + bool hasCache(TNode term) const; + + bool isConvertibleToBool(TNode current); Node convertToBool(TNode current); public: typedef Node return_type; BvToBoolVisitor() : d_cache(), + d_bvToBoolTerm(), d_visited(), d_one(utils::mkConst(BitVector(1, 1u))), d_zero(utils::mkConst(BitVector(1, 0u))) diff --git a/src/theory/bv/options b/src/theory/bv/options index 2e53b029c..7b87baa21 100644 --- a/src/theory/bv/options +++ b/src/theory/bv/options @@ -19,5 +19,8 @@ option bitvectorInequalitySolver --bv-inequality-solver bool :default true option bitvectorCoreSolver --bv-core-solver bool turn on the core solver for the bit-vector theory + +option bvToBool --bv-to-bool bool + lift bit-vectors of size 1 to booleans when possible endmodule diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 433223308..fd2946d24 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -124,6 +124,7 @@ void TheoryBV::sendConflict() { void TheoryBV::check(Effort e) { + Trace("bitvector") <<"TheoryBV::check (" << e << ")\n"; Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; if (options::bitvectorEagerBitblast()) { return; @@ -244,10 +245,10 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu Node TheoryBV::ppRewrite(TNode t) { - if (RewriteRule::applies(t)) { - Node result = RewriteRule::run(t); - return Rewriter::rewrite(result); - } + // if (RewriteRule::applies(t)) { + // Node result = RewriteRule::run(t); + // return Rewriter::rewrite(result); + // } if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) { std::vector equalities; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 442b1ef1c..6f965879d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -119,7 +119,8 @@ TheoryEngine::TheoryEngine(context::Context* context, d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms), - d_unconstrainedSimp(context, logicInfo) + d_unconstrainedSimp(context, logicInfo), + d_bvToBoolPreprocessor() { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { d_theoryTable[theoryId] = NULL; @@ -1276,6 +1277,12 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { } } +Node TheoryEngine::ppBvToBool(TNode assertion) { + Node result = d_bvToBoolPreprocessor.liftBoolToBV(assertion); + result = Rewriter::rewrite(result); + return result; +} + Node TheoryEngine::ppSimpITE(TNode assertion) { Node result = d_iteSimplifier.simpITE(assertion); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 9abdaa034..324b952b0 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -45,6 +45,7 @@ #include "theory/ite_simplifier.h" #include "theory/unconstrained_simplifier.h" #include "theory/uf/equality_engine.h" +#include "theory/bv/bv_to_bool.h" namespace CVC4 { @@ -748,8 +749,11 @@ private: /** For preprocessing pass simplifying unconstrained expressions */ UnconstrainedSimplifier d_unconstrainedSimp; + /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ + theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; public: + Node ppBvToBool(TNode assertion); Node ppSimpITE(TNode assertion); void ppUnconstrainedSimp(std::vector& assertions); -- cgit v1.2.3 From 1da2e989b6060fcadc060722b213e80b0cfce7ab Mon Sep 17 00:00:00 2001 From: lianah Date: Tue, 16 Apr 2013 10:57:04 -0400 Subject: uncompiling new bv to bool lifting --- src/smt/smt_engine.cpp | 26 ++-- src/theory/bv/bv_to_bool.cpp | 307 +++++++++++++++++++++++++------------------ src/theory/bv/bv_to_bool.h | 36 +++-- src/theory/theory_engine.cpp | 6 +- src/theory/theory_engine.h | 2 +- 5 files changed, 216 insertions(+), 161 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9ee2c5722..f8ec22943 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1929,9 +1929,10 @@ bool SmtEnginePrivate::nonClausalSimplify() { void SmtEnginePrivate::bvToBool() { Trace("simplify") << "SmtEnginePrivate::bvToBool()" << endl; - + std::vector new_assertions; + d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck, new_assertions); for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { - d_assertionsToCheck[i] = d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck[i]); + d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]); } } @@ -2484,16 +2485,6 @@ bool SmtEnginePrivate::simplifyAssertions() Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - // Lift bit-vectors of size 1 to bool - if(options::bvToBool()) { - Chat() << "...doing bvToBool..." << endl; - bvToBool(); - } - - Trace("smt") << "POST bvToBool" << endl; - Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; - Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) { Chat() << "...doing another round of nonclausal simplification..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " @@ -2792,6 +2783,17 @@ void SmtEnginePrivate::processAssertions() { } dumpAssertions("post-static-learning", d_assertionsToCheck); + // Lift bit-vectors of size 1 to bool + if(options::bvToBool()) { + Chat() << "...doing bvToBool..." << endl; + bvToBool(); + } + + Trace("smt") << "POST bvToBool" << endl; + Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; + Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + + dumpAssertions("pre-ite-removal", d_assertionsToCheck); { Chat() << "removing term ITEs..." << endl; diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index 5ab7cf144..7d3f58c8e 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -23,22 +23,6 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; -void BvToBoolVisitor::storeBvToBool(TNode bv_term, Node bool_term) { - Assert (!hasBoolTerm(bv_term)); - Assert (bool_term.getType().isBoolean()); - d_bvToBoolTerm[bv_term] = bool_term; -} - -Node BvToBoolVisitor::getBoolTerm(TNode bv_term) const { - Assert(hasBoolTerm(bv_term)); - return d_bvToBoolTerm.find(bv_term)->second; -} - -bool BvToBoolVisitor::hasBoolTerm(TNode bv_term) const { - Assert (bv_term.getType().isBitVector()); - return d_bvToBoolTerm.find(bv_term) != d_bvToBoolTerm.end(); -} - void BvToBoolVisitor::addToCache(TNode term, Node new_term) { Assert (new_term != Node()); Assert (!hasCache(term)); @@ -56,130 +40,167 @@ bool BvToBoolVisitor::hasCache(TNode term) const { return d_cache.find(term) != d_cache.end(); } - void BvToBoolVisitor::start(TNode node) {} +void BvToBoolVisitor::storeBvToBool(TNode bv_term, TNode bool_term) { + Assert (bv_term.getType().isBitVector() && + bv_term.getType().getBitVectorSize() == 1); + Assert (bool_term.getType().isBoolean() && d_bvToBoolMap.find(bv_term) == d_bvToBoolMap.end()); + d_bvToBoolMap[bv_term] = bool_term; +} + +Node BvToBoolVisitor::getBoolForBvTerm(TNode node) { + Assert (d_bvToBoolMap.find(node) != d_bvToBoolMap.end()); + return d_bvToBoolMap[node]; +} + bool BvToBoolVisitor::alreadyVisited(TNode current, TNode parent) { - return d_visited.find(current) != d_visited.end(); + return d_cache.find(current) != d_cache.end(); +} + +bool BvToBoolVisitor::isConvertibleBvAtom(TNode node) { + Kind kind = node.getKind(); + return (kind == kind::BITVECTOR_ULT || + kind == kind::BITVECTOR_ULE || + kind == kind::EQUAL) && + node[0].getType().isBitVector() && + node[0].getType().getBitVectorSize() == 1; } -bool BvToBoolVisitor::isConvertibleToBool(TNode current) { - TypeNode type = current.getType(); - if (current.getNumChildren() == 0 && type.isBitVector()) { - return type.getBitVectorSize() == 1; - } - - if (current.getKind() == kind::NOT) { - current = current[0]; - } - Kind kind = current.getKind(); - // checking bit-vector kinds - if (kind == kind::BITVECTOR_OR || - kind == kind::BITVECTOR_AND || - kind == kind::BITVECTOR_XOR || - kind == kind::BITVECTOR_NOT || - kind == kind::BITVECTOR_ULT || - kind == kind::BITVECTOR_ULE || - kind == kind::EQUAL) { - // we can convert it to bool if all of the children can also be converted - // to bool - if (! current[0].getType().getBitVectorSize() == 1) - return false; - for (unsigned i = 0; i < current.getNumChildren(); ++i) { - // we assume that the children have been visited - if (!hasBoolTerm(current[i])) +bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) { + // we have already converted it and the result is cached + if (d_bvToBoolMap.find(node) != d_bvToBoolMap.end()) { + return true; + } + + Kind kind = node.getKind(); + if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1) + return false; + + if (kind == kind::CONST_BITVECTOR) { + return true; + } + + if (kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR || + kind == kind::BITVECTOR_NOT || kind == kind::BITVECTOR_XOR) { + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + if (!isConvertibleBvTerm(node[i])) return false; } return true; } - if (kind == kind::ITE && - type.isBitVector()) { - return type.getBitVectorSize() == 1 && hasBoolTerm(current[1]) && hasBoolTerm(current[2]); - } return false; } - -Node BvToBoolVisitor::convertToBool(TNode current) { - Debug("bv-to-bool") << "BvToBoolVisitor::convertToBool (" << current << ") "; - Kind kind = current.getKind(); - - Node new_current; - if (current.getNumChildren() == 0) { - if (current.getKind() == kind::CONST_BITVECTOR) { - new_current = current == d_one? utils::mkTrue() : utils::mkFalse(); - } else { - new_current = utils::mkNode(kind::EQUAL, current, d_one); - } - Debug("bv-to-bool") << "=> " << new_current << "\n"; - } else if (kind == kind::BITVECTOR_ULT) { - TNode a = getBoolTerm(current[0]); - TNode b = getBoolTerm(current[1]); - Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero); - Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one); - new_current = utils::mkNode(kind::AND, a_eq_0, b_eq_1); - } else if (kind == kind::BITVECTOR_ULE) { - TNode a = getBoolTerm(current[0]); - TNode b = getBoolTerm(current[1]); +Node BvToBoolVisitor::convertBvAtom(TNode node) { + Assert (node.getType().isBoolean()); + Kind kind = node.getKind(); + Node result; + switch(kind) { + case kind::BITVECTOR_ULT: { + TNode a = getBoolForBvTerm(node[0]); + TNode b = getBoolForBvTerm(node[1]); Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero); Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one); - Node a_lt_b = utils::mkNode(kind::AND, a_eq_0, b_eq_1); - Node a_eq_b = utils::mkNode(kind::EQUAL, a, b); - new_current = utils::mkNode(kind::OR, a_lt_b, a_eq_b); - } else if (kind == kind::ITE) { - TNode cond = current[0]; - TNode a = getBoolTerm(current[1]); - TNode b = getBoolTerm(current[2]); - new_current = utils::mkNode(kind::ITE, cond, a, b); - } else { - Kind new_kind; - switch (kind) { - case kind::BITVECTOR_OR : - new_kind = kind::OR; - break; - case kind::BITVECTOR_AND: - new_kind = kind::AND; - break; - case kind::BITVECTOR_XOR: - new_kind = kind::XOR; - break; - case kind::BITVECTOR_NOT: - new_kind = kind::NOT; - break; - case kind::EQUAL: - new_kind = kind::IFF; - break; - default: - Unreachable("Unknown kind ", kind); - } - NodeBuilder<> builder(new_kind); - if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { - builder << current.getOperator(); + result = utils::mkNode(kind::AND, a_eq_0, b_eq_1); + break; + } + case kind::BITVECTOR_ULE: { + TNode a = getBoolForBvTerm(node[0]); + TNode b = getBoolForBvTerm(node[1]); + Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero); + Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one); + Node a_lt_b = utils::mkNode(kind::AND, a_eq_0, b_eq_1); + Node a_eq_b = utils::mkNode(kind::EQUAL, a, b); + result = utils::mkNode(kind::OR, a_lt_b, a_eq_b); + break; + } + case kind::EQUAL: { + TNode a = getBoolForBvTerm(node[0]); + TNode b = getBoolForBvTerm(node[1]); + result = utils::mkNode(kind::IFF, a, b); + break; + } + default: + Unhandled(); + } + Assert (result != Node()); + return result; +} + +Node BvToBoolVisitor::convertBvTerm(TNode node) { + Assert (node.getType().isBitVector() && + node.getType().getBitVectorSize() == 1); + Kind kind = node.getKind(); + + if (node.getNumChildren() == 0) { + if (node.getKind() == kind::VARIABLE) { + return getBoolForBvTerm(node); } - for (unsigned i = 0; i < current.getNumChildren(); ++i) { - builder << getBoolTerm(current[i]); + if (node.getKind() == kind::CONST_BITVECTOR) { + return (node == d_one ? utils::mkTrue() : utils::mkFalse()); } - new_current = builder; } - Debug("bv-to-bool") << "=> " << new_current << "\n"; - if (current.getType().isBitVector()) { - storeBvToBool(current, new_current); - } else { - addToCache(current, new_current); + if (kind == kind::ITE) { + TNode cond = getCache(node[0]); + TNode true_branch = getBoolForBvTerm(node[1]); + TNode false_branch = getBoolForBvTerm(node[2]); + Node result = utils::mkNode(kind::ITE, cond, true_branch, false_branch); + storeBvToBool(node, result); + return result; + } + + Kind new_kind; + switch(kind) { + case kind::BITVECTOR_OR: + new_kind = kind::OR; + break; + case kind::BITVECTOR_AND: + new_kind = kind::AND; + break; + case kind::BITVECTOR_XOR: + new_kind = kind::XOR; + break; + case kind::BITVECTOR_NOT: + new_kind = kind::NOT; + break; + default: + Unhandled(); + } + + NodeBuilder<> builder(new_kind); + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + builder << getBoolForBvTerm(node[i]); + } + Node result = builder; + storeBvToBool(node, result); + return result; +} + +void BvToBoolVisitor::check(TNode current, TNode parent) { + if (d_bvToBoolMap.find(current) != d_bvToBoolMap.end()) { + if (!isConvertibleBvTerm(parent) && !isConvertibleBvAtom(parent)) { + Debug("bv-to-bool") << "BvToBoolVisitor::check " << current << " in non boolean context: \n" + << " " << parent << "\n"; + } } - return new_current; } void BvToBoolVisitor::visit(TNode current, TNode parent) { Debug("bv-to-bool") << "BvToBoolVisitor visit (" << current << ", " << parent << ")\n"; - Assert (!alreadyVisited(current, parent)); - d_visited.insert(current); + Assert (!alreadyVisited(current, parent) && + !hasCache(current)); + + Node result; - Node result; - // if it has more than one child - if (isConvertibleToBool(current)) { - result = convertToBool(current); + // make sure that the bv terms we are replacing to not occur in other contexts + check(current, parent); + + if (isConvertibleBvAtom(current)) { + result = convertBvAtom(current); + } else if (isConvertibleBvTerm(current)) { + result = convertBvTerm(current); } else { if (current.getNumChildren() == 0) { result = current; @@ -190,24 +211,60 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) { } for (unsigned i = 0; i < current.getNumChildren(); ++i) { Node converted = getCache(current[i]); - if (converted.getType() == current[i].getType()) { - builder << converted; - } else { - builder << current[i]; - } + Assert (converted.getType() == current[i].getType()); + builder << converted; } result = builder; } - addToCache(current, result); } + Assert (result != Node()); + addToCache(current, result); } + BvToBoolVisitor::return_type BvToBoolVisitor::done(TNode node) { Assert (hasCache(node)); return getCache(node); } -Node BvToBoolPreprocessor::liftBoolToBV(TNode assertion) { - Node result = NodeVisitor::run(d_visitor, assertion); - return result; +bool BvToBoolPreprocessor::matchesBooleanPatern(TNode current) { + // we are looking for something of the type (= (bvvar 1) (some predicate)) + if (current.getKind() == kind::IFF && + current[0].getKind() == kind::EQUAL && + current[0][0].getType().isBitVector() && + current[0][0].getType().getBitVectorSize() == 1 && + current[0][0].getKind() == kind::VARIABLE && + current[0][1].getKind() == kind::CONST_BITVECTOR) { + return true; + } + return false; +} + + +void BvToBoolPreprocessor::liftBoolToBV(const std::vector& assertions, std::vector& new_assertions) { + TNodeNodeMap candidates; + for (unsigned i = 0; i < assertions.size(); ++i) { + if (matchesBooleanPatern(assertions[i])) { + TNode assertion = assertions[i]; + TNode bv_var = assertion[0][0]; + Assert (bv_var.getKind() == kind::VARIABLE && + bv_var.getType().isBitVector() && + bv_bar.getType().getBitVectorSize() == 1); + TNode bool_cond = assertion[1]; + Assert (bool_cond.getType().isBoolean()); + if (candidates.find(bv_var) == candidates.end()) { + Debug("bv-to-bool") << "BBvToBoolPreprocessor::liftBvToBoolBV candidate: " << bv_var <<"\n"; + candidates[bv_var] = bool_cond; + } else { + Debug("bv-to-bool") << "BvToBoolPreprocessor::liftBvToBoolBV multiple def " << bv_var <<"\n"; + } + } + } + + BvToBoolVisitor bvToBoolVisitor(candidates); + for (unsigned i = 0; i < assertions.size(); ++i) { + Node new_assertion = NodeVisitor::run(bvToBoolVisitor, + assertions[i]); + new_assertions.push_back(new_assertion); + } } diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index d5673a295..9b1534b41 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -24,33 +24,31 @@ namespace CVC4 { namespace theory { namespace bv { -class BvToBoolVisitor { +typedef __gnu_cxx::hash_set TNodeSet; +typedef __gnu_cxx::hash_map TNodeNodeMap; - typedef __gnu_cxx::hash_set TNodeSet; - typedef __gnu_cxx::hash_map TNodeNodeMap; +class BvToBoolVisitor { + TNodeNodeMap d_bvToBoolMap; TNodeNodeMap d_cache; - TNodeNodeMap d_bvToBoolTerm; - TNodeSet d_visited; Node d_one; Node d_zero; - void storeBvToBool(TNode bv_term, Node bool_term); - Node getBoolTerm(TNode bv_term) const; - bool hasBoolTerm(TNode bv_term) const; - void addToCache(TNode term, Node new_term); Node getCache(TNode term) const; bool hasCache(TNode term) const; - - bool isConvertibleToBool(TNode current); - Node convertToBool(TNode current); + bool isConvertibleBvTerm(TNode node); + bool isConvertibleBvAtom(TNode node); + Node getBoolForBvTerm(TNode node); + void storeBvToBool(TNode bv_term, TNode bool_term); + Node convertBvAtom(TNode node); + Node convertBvTerm(TNode node); + void check(TNode current, TNode parent); public: typedef Node return_type; - BvToBoolVisitor() - : d_cache(), - d_bvToBoolTerm(), - d_visited(), + BvToBoolVisitor(TNodeNodeMap& bvToBool) + : d_bvToBoolMap(bvToBool), + d_cache(), d_one(utils::mkConst(BitVector(1, 1u))), d_zero(utils::mkConst(BitVector(1, 0u))) {} @@ -60,14 +58,14 @@ public: return_type done(TNode node); }; + class BvToBoolPreprocessor { - BvToBoolVisitor d_visitor; + bool matchesBooleanPatern(TNode node); public: BvToBoolPreprocessor() - : d_visitor() {} ~BvToBoolPreprocessor() {} - Node liftBoolToBV(TNode assertion); + void liftBoolToBV(const std::vector& assertions, std::vector& new_assertions); }; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6f965879d..8c430d6d4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1277,10 +1277,8 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { } } -Node TheoryEngine::ppBvToBool(TNode assertion) { - Node result = d_bvToBoolPreprocessor.liftBoolToBV(assertion); - result = Rewriter::rewrite(result); - return result; +void TheoryEngine::ppBvToBool(const std::vector& assertions, std::vector new_assertions) { + d_bvToBoolPreprocessor.liftBoolToBV(assertions, new_assertions); } Node TheoryEngine::ppSimpITE(TNode assertion) diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 324b952b0..d581aeda2 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -753,7 +753,7 @@ private: theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; public: - Node ppBvToBool(TNode assertion); + void ppBvToBool(const std::vector& assertions, std::vector new_assertions); Node ppSimpITE(TNode assertion); void ppUnconstrainedSimp(std::vector& assertions); -- cgit v1.2.3 From f5750be0382d74569532ae53865158659cf9f2f3 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Tue, 16 Apr 2013 11:17:36 -0400 Subject: fixed compile error --- src/theory/bv/bv_to_bool.cpp | 4 ++-- src/theory/bv/bv_to_bool.h | 2 +- src/theory/theory_engine.cpp | 2 +- src/theory/theory_engine.h | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index 7d3f58c8e..44c4bd021 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -241,7 +241,7 @@ bool BvToBoolPreprocessor::matchesBooleanPatern(TNode current) { } -void BvToBoolPreprocessor::liftBoolToBV(const std::vector& assertions, std::vector& new_assertions) { +void BvToBoolPreprocessor::liftBoolToBV(const std::vector& assertions, std::vector& new_assertions) { TNodeNodeMap candidates; for (unsigned i = 0; i < assertions.size(); ++i) { if (matchesBooleanPatern(assertions[i])) { @@ -249,7 +249,7 @@ void BvToBoolPreprocessor::liftBoolToBV(const std::vector& assertions, st TNode bv_var = assertion[0][0]; Assert (bv_var.getKind() == kind::VARIABLE && bv_var.getType().isBitVector() && - bv_bar.getType().getBitVectorSize() == 1); + bv_var.getType().getBitVectorSize() == 1); TNode bool_cond = assertion[1]; Assert (bool_cond.getType().isBoolean()); if (candidates.find(bv_var) == candidates.end()) { diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index 9b1534b41..39c6b4251 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -65,7 +65,7 @@ public: BvToBoolPreprocessor() {} ~BvToBoolPreprocessor() {} - void liftBoolToBV(const std::vector& assertions, std::vector& new_assertions); + void liftBoolToBV(const std::vector& assertions, std::vector& new_assertions); }; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 8c430d6d4..22a0b00ed 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1277,7 +1277,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { } } -void TheoryEngine::ppBvToBool(const std::vector& assertions, std::vector new_assertions) { +void TheoryEngine::ppBvToBool(const std::vector& assertions, std::vector new_assertions) { d_bvToBoolPreprocessor.liftBoolToBV(assertions, new_assertions); } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index d581aeda2..6d355ccce 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -753,7 +753,7 @@ private: theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; public: - void ppBvToBool(const std::vector& assertions, std::vector new_assertions); + void ppBvToBool(const std::vector& assertions, std::vector new_assertions); Node ppSimpITE(TNode assertion); void ppUnconstrainedSimp(std::vector& assertions); -- cgit v1.2.3 From eaa9f9af40941ef1aeb93367884e692301b60280 Mon Sep 17 00:00:00 2001 From: lianah Date: Wed, 17 Apr 2013 15:34:16 -0400 Subject: innd examples are solved fast, but destruction assertion fail --- src/smt/smt_engine.cpp | 4 +- src/theory/bv/bv_to_bool.cpp | 91 +++++++++++++++++++++++----------- src/theory/bv/bv_to_bool.h | 13 ++--- src/theory/term_registration_visitor.h | 6 ++- src/theory/theory_engine.cpp | 2 +- src/theory/theory_engine.h | 2 +- 6 files changed, 79 insertions(+), 39 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f8ec22943..35db0975e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1928,11 +1928,11 @@ bool SmtEnginePrivate::nonClausalSimplify() { void SmtEnginePrivate::bvToBool() { - Trace("simplify") << "SmtEnginePrivate::bvToBool()" << endl; + Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl; std::vector new_assertions; d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck, new_assertions); for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { - d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]); + d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]); } } diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index 44c4bd021..8084a7282 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -30,7 +30,7 @@ void BvToBoolVisitor::addToCache(TNode term, Node new_term) { } Node BvToBoolVisitor::getCache(TNode term) const { - if (!hasCache(term)) { + if (!hasCache(term) || term.getKind() == kind::CONST_BITVECTOR) { return term; } return d_cache.find(term)->second; @@ -62,9 +62,11 @@ bool BvToBoolVisitor::isConvertibleBvAtom(TNode node) { Kind kind = node.getKind(); return (kind == kind::BITVECTOR_ULT || kind == kind::BITVECTOR_ULE || + kind == kind::BITVECTOR_SLT || + kind == kind::BITVECTOR_SLE || kind == kind::EQUAL) && - node[0].getType().isBitVector() && - node[0].getType().getBitVectorSize() == 1; + isConvertibleBvTerm(node[0]) && + isConvertibleBvTerm(node[1]); } bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) { @@ -81,6 +83,10 @@ bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) { return true; } + if (kind == kind::ITE) { + return isConvertibleBvTerm(node[1]) && isConvertibleBvTerm(node[2]); + } + if (kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR || kind == kind::BITVECTOR_NOT || kind == kind::BITVECTOR_XOR) { for (unsigned i = 0; i < node.getNumChildren(); ++i) { @@ -98,32 +104,51 @@ Node BvToBoolVisitor::convertBvAtom(TNode node) { Node result; switch(kind) { case kind::BITVECTOR_ULT: { - TNode a = getBoolForBvTerm(node[0]); - TNode b = getBoolForBvTerm(node[1]); - Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero); - Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one); + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); + Node a_eq_0 = utils::mkNode(kind::IFF, a, utils::mkFalse()); + Node b_eq_1 = utils::mkNode(kind::IFF, b, utils::mkTrue()); result = utils::mkNode(kind::AND, a_eq_0, b_eq_1); break; } case kind::BITVECTOR_ULE: { - TNode a = getBoolForBvTerm(node[0]); - TNode b = getBoolForBvTerm(node[1]); - Node a_eq_0 = utils::mkNode(kind::EQUAL, a, d_zero); - Node b_eq_1 = utils::mkNode(kind::EQUAL, b, d_one); + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); + Node a_eq_0 = utils::mkNode(kind::IFF, a, utils::mkFalse()); + Node b_eq_1 = utils::mkNode(kind::IFF, b, utils::mkTrue()); Node a_lt_b = utils::mkNode(kind::AND, a_eq_0, b_eq_1); - Node a_eq_b = utils::mkNode(kind::EQUAL, a, b); + Node a_eq_b = utils::mkNode(kind::IFF, a, b); result = utils::mkNode(kind::OR, a_lt_b, a_eq_b); break; } + case kind::BITVECTOR_SLT: { + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); + Node a_eq_1 = utils::mkNode(kind::IFF, a, utils::mkTrue()); + Node b_eq_0 = utils::mkNode(kind::IFF, b, utils::mkFalse()); + result = utils::mkNode(kind::AND, a_eq_1, b_eq_0); + break; + } + case kind::BITVECTOR_SLE: { + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); + Node a_eq_1 = utils::mkNode(kind::IFF, a, utils::mkTrue()); + Node b_eq_0 = utils::mkNode(kind::IFF, b, utils::mkFalse()); + Node a_slt_b = utils::mkNode(kind::AND, a_eq_1, b_eq_0); + Node a_eq_b = utils::mkNode(kind::IFF, a, b); + result = utils::mkNode(kind::OR, a_slt_b, a_eq_b); + break; + } case kind::EQUAL: { - TNode a = getBoolForBvTerm(node[0]); - TNode b = getBoolForBvTerm(node[1]); + Node a = getBoolForBvTerm(node[0]); + Node b = getBoolForBvTerm(node[1]); result = utils::mkNode(kind::IFF, a, b); break; } default: Unhandled(); } + Debug("bv-to-bool") << "BvToBoolVisitor::convertBvAtom " << node <<" => " << result << "\n"; Assert (result != Node()); return result; } @@ -138,16 +163,19 @@ Node BvToBoolVisitor::convertBvTerm(TNode node) { return getBoolForBvTerm(node); } if (node.getKind() == kind::CONST_BITVECTOR) { - return (node == d_one ? utils::mkTrue() : utils::mkFalse()); + Node result = node == d_one ? utils::mkTrue() : utils::mkFalse(); + storeBvToBool(node, result); + return result; } } if (kind == kind::ITE) { - TNode cond = getCache(node[0]); - TNode true_branch = getBoolForBvTerm(node[1]); - TNode false_branch = getBoolForBvTerm(node[2]); + Node cond = getCache(node[0]); + Node true_branch = getBoolForBvTerm(node[1]); + Node false_branch = getBoolForBvTerm(node[2]); Node result = utils::mkNode(kind::ITE, cond, true_branch, false_branch); storeBvToBool(node, result); + Debug("bv-to-bool") << "BvToBoolVisitor::convertBvTerm " << node <<" => " << result << "\n"; return result; } @@ -175,6 +203,7 @@ Node BvToBoolVisitor::convertBvTerm(TNode node) { } Node result = builder; storeBvToBool(node, result); + Debug("bv-to-bool") << "BvToBoolVisitor::convertBvTerm " << node <<" => " << result << "\n"; return result; } @@ -191,9 +220,8 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) { Debug("bv-to-bool") << "BvToBoolVisitor visit (" << current << ", " << parent << ")\n"; Assert (!alreadyVisited(current, parent) && !hasCache(current)); - - Node result; + Node result; // make sure that the bv terms we are replacing to not occur in other contexts check(current, parent); @@ -217,14 +245,20 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) { result = builder; } } - Assert (result != Node()); + Assert (result != Node()); + Debug("bv-to-bool") << " =>" << result <<"\n"; addToCache(current, result); } BvToBoolVisitor::return_type BvToBoolVisitor::done(TNode node) { Assert (hasCache(node)); - return getCache(node); + Node result = getCache(node); + return result; +} + +bool BvToBoolVisitor::hasBoolTerm(TNode node) { + return d_bvToBoolMap.find(node) != d_bvToBoolMap.end(); } bool BvToBoolPreprocessor::matchesBooleanPatern(TNode current) { @@ -242,7 +276,8 @@ bool BvToBoolPreprocessor::matchesBooleanPatern(TNode current) { void BvToBoolPreprocessor::liftBoolToBV(const std::vector& assertions, std::vector& new_assertions) { - TNodeNodeMap candidates; + BvToBoolVisitor bvToBoolVisitor; + for (unsigned i = 0; i < assertions.size(); ++i) { if (matchesBooleanPatern(assertions[i])) { TNode assertion = assertions[i]; @@ -250,21 +285,21 @@ void BvToBoolPreprocessor::liftBoolToBV(const std::vector& assertions, std Assert (bv_var.getKind() == kind::VARIABLE && bv_var.getType().isBitVector() && bv_var.getType().getBitVectorSize() == 1); - TNode bool_cond = assertion[1]; + Node bool_cond = NodeVisitor::run(bvToBoolVisitor, assertion[1]); Assert (bool_cond.getType().isBoolean()); - if (candidates.find(bv_var) == candidates.end()) { + if (!bvToBoolVisitor.hasBoolTerm(bv_var)) { Debug("bv-to-bool") << "BBvToBoolPreprocessor::liftBvToBoolBV candidate: " << bv_var <<"\n"; - candidates[bv_var] = bool_cond; + bvToBoolVisitor.storeBvToBool(bv_var, bool_cond); } else { Debug("bv-to-bool") << "BvToBoolPreprocessor::liftBvToBoolBV multiple def " << bv_var <<"\n"; } } } - BvToBoolVisitor bvToBoolVisitor(candidates); for (unsigned i = 0; i < assertions.size(); ++i) { Node new_assertion = NodeVisitor::run(bvToBoolVisitor, assertions[i]); - new_assertions.push_back(new_assertion); + new_assertions.push_back(new_assertion); + Trace("bv-to-bool") << " " << assertions[i] <<" => " << new_assertions[i] <<"\n"; } } diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index 39c6b4251..186f2b317 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -25,11 +25,11 @@ namespace theory { namespace bv { typedef __gnu_cxx::hash_set TNodeSet; -typedef __gnu_cxx::hash_map TNodeNodeMap; +typedef __gnu_cxx::hash_map NodeNodeMap; class BvToBoolVisitor { - TNodeNodeMap d_bvToBoolMap; - TNodeNodeMap d_cache; + NodeNodeMap d_bvToBoolMap; + NodeNodeMap d_cache; Node d_one; Node d_zero; @@ -40,14 +40,13 @@ class BvToBoolVisitor { bool isConvertibleBvTerm(TNode node); bool isConvertibleBvAtom(TNode node); Node getBoolForBvTerm(TNode node); - void storeBvToBool(TNode bv_term, TNode bool_term); Node convertBvAtom(TNode node); Node convertBvTerm(TNode node); void check(TNode current, TNode parent); public: typedef Node return_type; - BvToBoolVisitor(TNodeNodeMap& bvToBool) - : d_bvToBoolMap(bvToBool), + BvToBoolVisitor() + : d_bvToBoolMap(), d_cache(), d_one(utils::mkConst(BitVector(1, 1u))), d_zero(utils::mkConst(BitVector(1, 0u))) @@ -56,6 +55,8 @@ public: bool alreadyVisited(TNode current, TNode parent); void visit(TNode current, TNode parent); return_type done(TNode node); + void storeBvToBool(TNode bv_term, TNode bool_term); + bool hasBoolTerm(TNode node); }; diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 768508d2c..5f89af9c6 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -95,7 +95,11 @@ public: * Notifies the engine of all the theories used. */ bool done(TNode node); - + ~PreRegisterVisitor() { + for (TNodeToTheorySetMap::const_iterator it = d_visited.begin(); it != d_visited.end(); ++it) { + std::cout << it->first <<"\n"; + } + } }; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 22a0b00ed..6c8341345 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1277,7 +1277,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { } } -void TheoryEngine::ppBvToBool(const std::vector& assertions, std::vector new_assertions) { +void TheoryEngine::ppBvToBool(const std::vector& assertions, std::vector& new_assertions) { d_bvToBoolPreprocessor.liftBoolToBV(assertions, new_assertions); } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 6d355ccce..c21819ea1 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -753,7 +753,7 @@ private: theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; public: - void ppBvToBool(const std::vector& assertions, std::vector new_assertions); + void ppBvToBool(const std::vector& assertions, std::vector& new_assertions); Node ppSimpITE(TNode assertion); void ppUnconstrainedSimp(std::vector& assertions); -- cgit v1.2.3 From 12f48b0a11207ddbd34b2b2b88362250e9692ac2 Mon Sep 17 00:00:00 2001 From: lianah Date: Sun, 21 Apr 2013 19:00:09 -0400 Subject: added some bv rewrite rules --- src/theory/bv/theory_bv.cpp | 2 +- src/theory/bv/theory_bv_rewrite_rules.h | 12 ++++- .../theory_bv_rewrite_rules_operator_elimination.h | 32 +++++++++---- .../bv/theory_bv_rewrite_rules_simplification.h | 55 ++++++++++++++++++++++ src/theory/bv/theory_bv_rewriter.cpp | 10 ++-- src/theory/term_registration_visitor.h | 5 -- 6 files changed, 98 insertions(+), 18 deletions(-) diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index fd2946d24..7cb06ca15 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -250,7 +250,7 @@ Node TheoryBV::ppRewrite(TNode t) // return Rewriter::rewrite(result); // } - if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) { + if (/*options::bitvectorCoreSolver() && */t.getKind() == kind::EQUAL) { std::vector equalities; Slicer::splitEqualities(t, equalities); return utils::mkAnd(equalities); diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index e9a3494f0..cff85b92b 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -125,6 +125,10 @@ enum RewriteRuleId { UremOne, UremSelf, ShiftZero, + + UltOne, + SltZero, + ZeroUlt, /// normalization rules ExtractBitwise, @@ -262,7 +266,10 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case OrSimplify : out << "OrSimplify"; return out; case XorSimplify : out << "XorSimplify"; return out; case NegPlus : out << "NegPlus"; return out; - case BBPlusNeg : out << "BBPlusNeg"; return out; + case BBPlusNeg : out << "BBPlusNeg"; return out; + case UltOne : out << "UltOne"; return out; + case SltZero : out << "SltZero"; return out; + case ZeroUlt : out << "ZeroUlt"; return out; default: Unreachable(); } @@ -477,6 +484,9 @@ struct AllRewriteRules { RewriteRule rule111; RewriteRule rule112; RewriteRule rule113; + RewriteRule rule114; + RewriteRule rule115; + }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 06ddc215d..b466aceae 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -103,6 +103,24 @@ Node RewriteRule::apply(TNode node) { } +// template <> +// bool RewriteRule::applies(TNode node) { +// return (node.getKind() == kind::BITVECTOR_SLE); +// } + +// template <> +// Node RewriteRule::apply(TNode node) { +// Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + +// unsigned size = utils::getSize(node[0]); +// Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1))); +// Node a = utils::mkNode(kind::BITVECTOR_PLUS, node[0], pow_two); +// Node b = utils::mkNode(kind::BITVECTOR_PLUS, node[1], pow_two); + +// return utils::mkNode(kind::BITVECTOR_ULE, a, b); + +// } + template <> bool RewriteRule::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SLE); @@ -111,16 +129,14 @@ bool RewriteRule::applies(TNode node) { template <> Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; - - unsigned size = utils::getSize(node[0]); - Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1))); - Node a = utils::mkNode(kind::BITVECTOR_PLUS, node[0], pow_two); - Node b = utils::mkNode(kind::BITVECTOR_PLUS, node[1], pow_two); - - return utils::mkNode(kind::BITVECTOR_ULE, a, b); - + + TNode a = node[0]; + TNode b = node[1]; + Node b_slt_a = utils::mkNode(kind::BITVECTOR_SLT, b, a); + return utils::mkNode(kind::NOT, b_slt_a); } + template <> bool RewriteRule::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_COMP); diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index bcfb189af..d660dde29 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -523,6 +523,25 @@ Node RewriteRule::apply(TNode node) { return utils::mkTrue(); } +/** + * ZeroUlt + * + * 0 < a ==> a != 0 + */ + +template<> inline +bool RewriteRule::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_ULT && + node[0] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0)))); +} + +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + return utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, node[0], node[1])); +} + + /** * UltZero * @@ -541,6 +560,42 @@ Node RewriteRule::apply(TNode node) { return utils::mkFalse(); } + +/** + * + */ +template<> inline +bool RewriteRule::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_ULT && + node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(1)))); +} + +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + return utils::mkNode(kind::EQUAL, node[0], utils::mkConst(BitVector(utils::getSize(node[0]), 0u))); +} + +/** + * + */ +template<> inline +bool RewriteRule::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_SLT && + node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0)))); +} + +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + unsigned size = utils::getSize(node[0]); + Node most_significant_bit = utils::mkExtract(node[0], size - 1, size - 1); + Node one = utils::mkConst(BitVector(1, 1u)); + + return utils::mkNode(kind::EQUAL, most_significant_bit, one); +} + + /** * UltSelf * diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index a712a8391..07499d01a 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -75,8 +75,10 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule, // if both arguments are constants evaluates - RewriteRule + RewriteRule, // a < 0 rewrites to false + RewriteRule, + RewriteRule >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); @@ -84,7 +86,8 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy - < RewriteRule < EvalSlt > + < RewriteRule < EvalSlt >, + RewriteRule < SltZero > >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); @@ -110,7 +113,8 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){ RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy - < RewriteRule < EvalSle > + < RewriteRule , + RewriteRule >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h index 5f89af9c6..d573213b7 100644 --- a/src/theory/term_registration_visitor.h +++ b/src/theory/term_registration_visitor.h @@ -95,11 +95,6 @@ public: * Notifies the engine of all the theories used. */ bool done(TNode node); - ~PreRegisterVisitor() { - for (TNodeToTheorySetMap::const_iterator it = d_visited.begin(); it != d_visited.end(); ++it) { - std::cout << it->first <<"\n"; - } - } }; -- cgit v1.2.3 From c2cf8201afa6b44a5d3103cf8938eccb69cec590 Mon Sep 17 00:00:00 2001 From: lianah Date: Thu, 25 Apr 2013 18:43:12 -0400 Subject: added bvule, bvsle operator elimination rulesl; added bvurem lemma generation --- src/prop/bvminisat/bvminisat.cpp | 1 + src/theory/bv/bv_to_bool.cpp | 19 ++++++++++---- src/theory/bv/theory_bv.cpp | 29 ++++++++++++++++++++++ src/theory/bv/theory_bv.h | 8 +++++- src/theory/bv/theory_bv_rewrite_rules.h | 5 ++-- .../theory_bv_rewrite_rules_operator_elimination.h | 16 ++++++++++++ src/theory/bv/theory_bv_rewriter.cpp | 18 +++++++------- 7 files changed, 79 insertions(+), 17 deletions(-) diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 6bbe4bb3e..ab25fa6cb 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -106,6 +106,7 @@ SatValue BVMinisatSatSolver::solve(){ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){ Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; + ++d_statistics.d_statCallsToSolve; if(resource == 0) { d_minisat->budgetOff(); } else { diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index 8084a7282..7bec805ef 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -44,8 +44,11 @@ void BvToBoolVisitor::start(TNode node) {} void BvToBoolVisitor::storeBvToBool(TNode bv_term, TNode bool_term) { Assert (bv_term.getType().isBitVector() && - bv_term.getType().getBitVectorSize() == 1); - Assert (bool_term.getType().isBoolean() && d_bvToBoolMap.find(bv_term) == d_bvToBoolMap.end()); + bv_term.getType().getBitVectorSize() == 1 && + bool_term.getType().isBoolean() && bv_term != Node() && bool_term != Node()); + if (d_bvToBoolMap.find(bv_term) != d_bvToBoolMap.end()) { + Assert (d_bvToBoolMap[bv_term] == bool_term); + } d_bvToBoolMap[bv_term] = bool_term; } @@ -75,9 +78,10 @@ bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) { return true; } - Kind kind = node.getKind(); if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1) return false; + + Kind kind = node.getKind(); if (kind == kind::CONST_BITVECTOR) { return true; @@ -95,6 +99,10 @@ bool BvToBoolVisitor::isConvertibleBvTerm(TNode node) { } return true; } + if (kind == kind::VARIABLE) { + storeBvToBool(node, utils::mkNode(kind::EQUAL, node, utils::mkConst(BitVector(1, 1u)))); + return true; + } return false; } @@ -226,7 +234,8 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) { check(current, parent); if (isConvertibleBvAtom(current)) { - result = convertBvAtom(current); + result = convertBvAtom(current); + addToCache(current, result); } else if (isConvertibleBvTerm(current)) { result = convertBvTerm(current); } else { @@ -244,10 +253,10 @@ void BvToBoolVisitor::visit(TNode current, TNode parent) { } result = builder; } + addToCache(current, result); } Assert (result != Node()); Debug("bv-to-bool") << " =>" << result <<"\n"; - addToCache(current, result); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 7cb06ca15..bd7d4c70b 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -43,6 +43,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_subtheories(), d_subtheoryMap(), d_statistics(), + d_lemmasAdded(c, false), d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), @@ -122,6 +123,28 @@ void TheoryBV::sendConflict() { } } +void TheoryBV::checkForLemma(TNode fact) { + if (fact.getKind() == kind::EQUAL) { + if (fact[0].getKind() == kind::BITVECTOR_UREM_TOTAL) { + TNode urem = fact[0]; + TNode result = fact[1]; + TNode divisor = urem[1]; + Node result_ult_div = utils::mkNode(kind::BITVECTOR_ULT, result, divisor); + Node split = utils::mkNode(kind::OR, utils::mkNode(kind::NOT, fact), result_ult_div); + lemma(split); + } + if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) { + TNode urem = fact[1]; + TNode result = fact[0]; + TNode divisor = urem[1]; + Node result_ult_div = utils::mkNode(kind::BITVECTOR_ULT, result, divisor); + Node split = utils::mkNode(kind::OR, utils::mkNode(kind::NOT, fact), result_ult_div); + lemma(split); + } + } +} + + void TheoryBV::check(Effort e) { Trace("bitvector") <<"TheoryBV::check (" << e << ")\n"; @@ -141,8 +164,14 @@ void TheoryBV::check(Effort e) return; } + if (Theory::fullEffort(e)) { + Trace("bitvector-fulleffort") << "TheoryBV::fullEffort \n"; + printFacts( Trace("bitvector-fulleffort") ); + } + while (!done()) { TNode fact = get().assertion; + checkForLemma(fact); for (unsigned i = 0; i < d_subtheories.size(); ++i) { d_subtheories[i]->assertFact(fact); } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 8b184f972..827b6e878 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -84,6 +84,8 @@ private: Statistics d_statistics; + context::CDO d_lemmasAdded; + // Are we in conflict? context::CDO d_conflict; @@ -96,6 +98,8 @@ private: /** Index of the next literal to propagate */ context::CDO d_literalsToPropagateIndex; + + /** * Keeps a map from nodes to the subtheory that propagated it so that we can explain it * properly. @@ -146,7 +150,9 @@ private: void sendConflict(); - void lemma(TNode node) { d_out->lemma(node); } + void lemma(TNode node) { d_out->lemma(node); d_lemmasAdded = true; } + + void checkForLemma(TNode node); friend class Bitblaster; friend class BitblastSolver; diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index cff85b92b..d362fa603 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -152,7 +152,7 @@ enum RewriteRuleId { AndSimplify, OrSimplify, XorSimplify, - + UleEliminate, // rules to simplify bitblasting BBPlusNeg }; @@ -269,7 +269,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case BBPlusNeg : out << "BBPlusNeg"; return out; case UltOne : out << "UltOne"; return out; case SltZero : out << "SltZero"; return out; - case ZeroUlt : out << "ZeroUlt"; return out; + case ZeroUlt : out << "ZeroUlt"; return out; + case UleEliminate : out << "UleEliminate"; return out; default: Unreachable(); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index b466aceae..a63721de1 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -85,6 +85,7 @@ Node RewriteRule::apply(TNode node) { return result; } + template <> bool RewriteRule::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SLT); @@ -136,6 +137,21 @@ Node RewriteRule::apply(TNode node) { return utils::mkNode(kind::NOT, b_slt_a); } +template <> +bool RewriteRule::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_ULE); +} + +template <> +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + + TNode a = node[0]; + TNode b = node[1]; + Node b_ult_a = utils::mkNode(kind::BITVECTOR_ULT, b, a); + return utils::mkNode(kind::NOT, b_ult_a); +} + template <> bool RewriteRule::applies(TNode node) { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 07499d01a..f6d138f5d 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -75,10 +75,10 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { Node resultNode = LinearRewriteStrategy < RewriteRule, // if both arguments are constants evaluates - RewriteRule, + RewriteRule // a < 0 rewrites to false - RewriteRule, - RewriteRule + // RewriteRule, + // RewriteRule >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); @@ -86,8 +86,8 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) { RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy - < RewriteRule < EvalSlt >, - RewriteRule < SltZero > + < RewriteRule < EvalSlt > + // RewriteRule < SltZero > >::apply(node); return RewriteResponse(REWRITE_DONE, resultNode); @@ -106,18 +106,18 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){ RewriteRule, RewriteRule, RewriteRule, - RewriteRule + RewriteRule, + RewriteRule >::apply(node); return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode); } RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){ Node resultNode = LinearRewriteStrategy - < RewriteRule , + < RewriteRule , RewriteRule >::apply(node); - - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteResponse(resultNode == node? REWRITE_DONE : REWRITE_AGAIN, resultNode); } RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){ -- cgit v1.2.3 From 7a088fea6ba227437106091558ce656bbe8f29b8 Mon Sep 17 00:00:00 2001 From: lianah Date: Tue, 30 Apr 2013 13:42:50 -0400 Subject: added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExtend) and bvurem lemma --- src/prop/bvminisat/bvminisat.cpp | 25 +--- src/theory/bv/theory_bv.cpp | 14 ++- src/theory/bv/theory_bv_rewrite_rules.h | 8 +- .../bv/theory_bv_rewrite_rules_normalization.h | 137 +++++++++++++++++++-- src/theory/bv/theory_bv_rewriter.cpp | 36 ++++-- src/theory/bv/theory_bv_utils.h | 7 ++ 6 files changed, 177 insertions(+), 50 deletions(-) diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index ab25fa6cb..fa5f53113 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -101,6 +101,7 @@ void BVMinisatSatSolver::interrupt(){ } SatValue BVMinisatSatSolver::solve(){ + ++d_statistics.d_statCallsToSolve; return toSatLiteralValue(d_minisat->solve()); } @@ -121,30 +122,6 @@ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){ return result; } -// SatValue BVMinisatSatSolver::solve(const context::CDList & assumptions, bool only_bcp){ -// ++d_solveCount; -// ++d_statistics.d_statCallsToSolve; - -// Debug("sat::minisat") << "Solve with assumptions "; -// context::CDList::const_iterator it = assumptions.begin(); -// BVMinisat::vec assump; -// for(; it!= assumptions.end(); ++it) { -// SatLiteral lit = *it; -// Debug("sat::minisat") << lit <<" "; -// assump.push(toMinisatLit(lit)); -// } -// Debug("sat::minisat") <<"\n"; - -// clock_t begin, end; -// begin = clock(); -// d_minisat->setOnlyBCP(only_bcp); -// SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump)); -// end = clock(); -// d_statistics.d_statSolveTime = d_statistics.d_statSolveTime.getData() + (end - begin)/(double)CLOCKS_PER_SEC; -// return result; -// } - - void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) { // TODO add assertion to check the call was after an unsat call for (int i = 0; i < d_minisat->conflict.size(); ++i) { diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index bd7d4c70b..91226f032 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -129,16 +129,22 @@ void TheoryBV::checkForLemma(TNode fact) { TNode urem = fact[0]; TNode result = fact[1]; TNode divisor = urem[1]; - Node result_ult_div = utils::mkNode(kind::BITVECTOR_ULT, result, divisor); - Node split = utils::mkNode(kind::OR, utils::mkNode(kind::NOT, fact), result_ult_div); + Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor); + Node divisor_eq_0 = mkNode(kind::EQUAL, + divisor, + mkConst(BitVector(getSize(divisor), 0u))); + Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div); lemma(split); } if (fact[1].getKind() == kind::BITVECTOR_UREM_TOTAL) { TNode urem = fact[1]; TNode result = fact[0]; TNode divisor = urem[1]; - Node result_ult_div = utils::mkNode(kind::BITVECTOR_ULT, result, divisor); - Node split = utils::mkNode(kind::OR, utils::mkNode(kind::NOT, fact), result_ult_div); + Node result_ult_div = mkNode(kind::BITVECTOR_ULT, result, divisor); + Node divisor_eq_0 = mkNode(kind::EQUAL, + divisor, + mkConst(BitVector(getSize(divisor), 0u))); + Node split = utils::mkNode(kind::OR, divisor_eq_0, mkNode(kind::NOT, fact), result_ult_div); lemma(split); } } diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index d362fa603..baaf7e133 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -52,6 +52,7 @@ enum RewriteRuleId { SubEliminate, SltEliminate, SleEliminate, + UleEliminate, CompEliminate, RepeatEliminate, RotateLeftEliminate, @@ -135,6 +136,7 @@ enum RewriteRuleId { ExtractNot, ExtractArith, ExtractArith2, + ExtractSignExtend, DoubleNeg, NegMult, NegSub, @@ -152,7 +154,7 @@ enum RewriteRuleId { AndSimplify, OrSimplify, XorSimplify, - UleEliminate, + BitwiseSlicing, // rules to simplify bitblasting BBPlusNeg }; @@ -270,7 +272,9 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case UltOne : out << "UltOne"; return out; case SltZero : out << "SltZero"; return out; case ZeroUlt : out << "ZeroUlt"; return out; - case UleEliminate : out << "UleEliminate"; return out; + case UleEliminate : out << "UleEliminate"; return out; + case BitwiseSlicing : out << "BitwiseSlicing"; return out; + case ExtractSignExtend : out << "ExtractSignExtend"; return out; default: Unreachable(); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 4ba09ef67..035bd4469 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -72,6 +72,58 @@ Node RewriteRule::apply(TNode node) { return utils::mkNode(kind::BITVECTOR_NOT, a); } +/** + * ExtractSignExtend + * + * (sign_extend k x) [i:j] => pushes extract in + * + * @return + */ + +template<> inline +bool RewriteRule::applies(TNode node) { + if (node.getKind() == kind::BITVECTOR_EXTRACT && + node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND) { + return true; + } + return false; +} + +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + TNode extendee = node[0][0]; + unsigned extendee_size = utils::getSize(extendee); + + unsigned high = utils::getExtractHigh(node); + unsigned low = utils::getExtractLow(node); + + Node resultNode; + // extract falls on extendee + if (high < extendee_size) { + resultNode = utils::mkExtract(extendee, high, low); + } else if (low < extendee_size && high >= extendee_size) { + // if extract overlaps sign extend and extendee + Node low_extract = utils::mkExtract(extendee, extendee_size - 1, low); + unsigned new_ammount = high - extendee_size + 1; + resultNode = utils::mkSignExtend(low_extract, new_ammount); + } else { + // extract only over sign extend + Assert (low >= extendee_size); + unsigned top = utils::getSize(extendee) - 1; + Node most_significant_bit = utils::mkExtract(extendee, top, top); + std::vector bits; + for (unsigned i = 0; i < high - low + 1; ++i) { + bits.push_back(most_significant_bit); + } + resultNode = utils::mkNode(kind::BITVECTOR_CONCAT, bits); + } + Debug("bv-rewrite") << " =>" << resultNode << std::endl; + return resultNode; +} + + + /** * ExtractArith * @@ -1032,19 +1084,84 @@ Node RewriteRule::apply(TNode node) { } +/** + * BitwiseSlicing + * + * (a bvand c) ==> (concat (bvand a[i0:j0] c0) ... (bvand a[in:jn] cn)) + * where c0,..., cn are maximally continuous substrings of 0 or 1 in the constant c + * + * Note: this rule assumes AndSimplify has already been called on the node + */ +template<> inline +bool RewriteRule::applies(TNode node) { + if ((node.getKind() != kind::BITVECTOR_AND && + node.getKind() != kind::BITVECTOR_OR && + node.getKind() != kind::BITVECTOR_XOR) || + utils::getSize(node) == 1) + return false; + + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + if (node[i].getKind() == kind::CONST_BITVECTOR) { + BitVector constant = node[i].getConst(); + // we do not apply the rule if the constant is all 0s or all 1s + if (constant == BitVector(utils::getSize(node), 0u)) + return false; + + for (unsigned i = 0; i < constant.getSize(); ++i) { + if (!constant.isBitSet(i)) + return true; + } + } + } + return false; +} +template<> inline +Node RewriteRule::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + // get the constant + bool found_constant = false; + TNode constant; + std::vector other_children; + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + if (node[i].getKind() == kind::CONST_BITVECTOR) { + constant = node[i]; + Assert (!found_constant); + found_constant = true; + } else { + other_children.push_back(node[i]); + } + } + Assert (found_constant && other_children.size() == node.getNumChildren() - 1); -// template<> inline -// bool RewriteRule::applies(TNode node) { -// return (node.getKind() == kind::BITVECTOR_AND); -// } - -// template<> inline -// Node RewriteRule::apply(TNode node) { -// Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; -// return resultNode; -// } + Node other = utils::mkNode(node.getKind(), other_children); + + BitVector bv_constant = constant.getConst(); + std::vector concat_children; + int start = bv_constant.getSize() - 1; + int end = start; + for (int i = end - 1; i >= 0; --i) { + if (bv_constant.isBitSet(i + 1) != bv_constant.isBitSet(i)) { + Node other_extract = utils::mkExtract(other, end, start); + Node const_extract = utils::mkExtract(constant, end, start); + Node bitwise_op = utils::mkNode(node.getKind(), const_extract, other_extract); + concat_children.push_back(bitwise_op); + start = end = i; + } else { + start--; + } + if (i == 0) { + Node other_extract = utils::mkExtract(other, end, 0); + Node const_extract = utils::mkExtract(constant, end, 0); + Node bitwise_op = utils::mkNode(node.getKind(), const_extract, other_extract); + concat_children.push_back(bitwise_op); + } + } + Node result = utils::mkNode(kind::BITVECTOR_CONCAT, concat_children); + Debug("bv-rewrite") << " =>" << result << std::endl; + return result; +} // template<> inline // bool RewriteRule<>::applies(TNode node) { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index f6d138f5d..44c498947 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -177,6 +177,11 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } + // if (RewriteRule::applies(node)) { + // resultNode = RewriteRule::run(node); + // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + // } + if (RewriteRule::applies(node)) { resultNode = RewriteRule::run(node); return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); @@ -223,14 +228,14 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){ resultNode = LinearRewriteStrategy < RewriteRule, - RewriteRule - // RewriteRule, - // RewriteRule, - // //RewriteRule, -> might need rw again - // RewriteRule, - // RewriteRule + RewriteRule//, + // RewriteRule >::apply(node); + if (resultNode.getKind() != node.getKind()) { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + return RewriteResponse(REWRITE_DONE, resultNode); } @@ -239,8 +244,13 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){ resultNode = LinearRewriteStrategy < RewriteRule, - RewriteRule + RewriteRule//, + // RewriteRule >::apply(node); + + if (resultNode.getKind() != node.getKind()) { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } return RewriteResponse(REWRITE_DONE, resultNode); } @@ -251,7 +261,8 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) { resultNode = LinearRewriteStrategy < RewriteRule, // flatten the expression RewriteRule, // simplify duplicates and constants - RewriteRule // checks if the constant part is zero and eliminates it + RewriteRule//, // checks if the constant part is zero and eliminates it + // RewriteRule >::apply(node); // this simplification introduces new terms and might require further @@ -261,6 +272,10 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } + if (resultNode.getKind() != node.getKind()) { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } + return RewriteResponse(REWRITE_DONE, resultNode); } @@ -301,7 +316,8 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) { resultNode = LinearRewriteStrategy < RewriteRule, // flattens and sorts - RewriteRule // multiplies constant part and checks for 0 + RewriteRule, // multiplies constant part and checks for 0 + RewriteRule // replaces multiplication by a power of 2 by a shift >::apply(node); // only apply if every subterm was already rewritten @@ -317,7 +333,7 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) { if(resultNode == node) { return RewriteResponse(REWRITE_DONE, resultNode); } - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool preregister) { diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index dffdf10df..5b69dc86d 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -84,6 +84,7 @@ inline Node mkSortedNode(Kind kind, std::vector& children) { inline Node mkNode(Kind kind, std::vector& children) { + Assert (children.size() > 0); if (children.size() == 1) { return children[0]; } @@ -133,6 +134,12 @@ inline Node mkXor(TNode node1, TNode node2) { } +inline Node mkSignExtend(TNode node, unsigned ammount) { + NodeManager* nm = NodeManager::currentNM(); + Node signExtendOp = nm->mkConst(BitVectorSignExtend(ammount)); + return nm->mkNode(signExtendOp, node); +} + inline Node mkExtract(TNode node, unsigned high, unsigned low) { Node extractOp = NodeManager::currentNM()->mkConst(BitVectorExtract(high, low)); std::vector children; -- cgit v1.2.3 From 07c2ba8ec0fba4e63620ea4861a2c79ceb9d8507 Mon Sep 17 00:00:00 2001 From: lianah Date: Tue, 30 Apr 2013 15:52:40 -0400 Subject: updated the author name --- .../bv/theory_bv_rewrite_rules_normalization.h | 2 +- src/theory/bv/theory_bv_rewriter.cpp | 20 ++++++++++---------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 035bd4469..2da4dfa6a 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -1120,7 +1120,7 @@ template<> inline Node RewriteRule::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; // get the constant - bool found_constant = false; + bool found_constant CVC4_UNUSED = false ; TNode constant; std::vector other_children; for (unsigned i = 0; i < node.getNumChildren(); ++i) { diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 44c498947..0775cb1f8 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -177,10 +177,10 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } - // if (RewriteRule::applies(node)) { - // resultNode = RewriteRule::run(node); - // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); - // } + if (RewriteRule::applies(node)) { + resultNode = RewriteRule::run(node); + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + } if (RewriteRule::applies(node)) { resultNode = RewriteRule::run(node); @@ -228,8 +228,8 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){ resultNode = LinearRewriteStrategy < RewriteRule, - RewriteRule//, - // RewriteRule + RewriteRule, + RewriteRule >::apply(node); if (resultNode.getKind() != node.getKind()) { @@ -244,8 +244,8 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){ resultNode = LinearRewriteStrategy < RewriteRule, - RewriteRule//, - // RewriteRule + RewriteRule, + RewriteRule >::apply(node); if (resultNode.getKind() != node.getKind()) { @@ -261,8 +261,8 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) { resultNode = LinearRewriteStrategy < RewriteRule, // flatten the expression RewriteRule, // simplify duplicates and constants - RewriteRule//, // checks if the constant part is zero and eliminates it - // RewriteRule + RewriteRule, // checks if the constant part is zero and eliminates it + RewriteRule >::apply(node); // this simplification introduces new terms and might require further -- cgit v1.2.3