summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/prop/bvminisat/bvminisat.cpp26
-rw-r--r--src/prop/minisat/core/Solver.h3
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc4
-rw-r--r--src/prop/options3
-rw-r--r--src/smt/smt_engine.cpp31
-rw-r--r--src/theory/bv/Makefile.am4
-rw-r--r--src/theory/bv/bv_to_bool.cpp314
-rw-r--r--src/theory/bv/bv_to_bool.h79
-rw-r--r--src/theory/bv/options3
-rw-r--r--src/theory/bv/theory_bv.cpp33
-rw-r--r--src/theory/bv/theory_bv.h8
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules.h19
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_normalization.h137
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h29
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_simplification.h55
-rw-r--r--src/theory/bv/theory_bv_rewriter.cpp48
-rw-r--r--src/theory/bv/theory_bv_utils.h7
-rw-r--r--src/theory/theory_engine.cpp7
-rw-r--r--src/theory/theory_engine.h4
19 files changed, 751 insertions, 63 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 6bbe4bb3e..fa5f53113 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -101,11 +101,13 @@ void BVMinisatSatSolver::interrupt(){
}
SatValue BVMinisatSatSolver::solve(){
+ ++d_statistics.d_statCallsToSolve;
return toSatLiteralValue(d_minisat->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 {
@@ -120,30 +122,6 @@ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){
return result;
}
-// SatValue BVMinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions, bool only_bcp){
-// ++d_solveCount;
-// ++d_statistics.d_statCallsToSolve;
-
-// Debug("sat::minisat") << "Solve with assumptions ";
-// context::CDList<SatLiteral>::const_iterator it = assumptions.begin();
-// BVMinisat::vec<BVMinisat::Lit> 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/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<Lit>& assumps); // Write CNF to file in DIMACS-format.
void toDimacs (const char *file, const vec<Lit>& assumps);
void toDimacs (FILE* f, Clause& c, vec<Var>& map, Var& max);
@@ -539,12 +540,14 @@ inline bool Solver::solve (const vec<Lit>& assumps){ budgetOff(); as
inline lbool Solver::solveLimited (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
inline bool Solver::okay () const { return ok; }
+inline void Solver::toDimacs () { vec<Lit> as; toDimacs(stdout, as); }
inline void Solver::toDimacs (const char* file){ vec<Lit> as; toDimacs(file, as); }
inline void Solver::toDimacs (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec<Lit> 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<Var> 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
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 52bc0c4d3..0d473a1a1 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<Node, bool, NodeHashFunction>& cache);
-
+ // Lift bit-vectors of size 1 to booleans
+ void bvToBool();
+
// Simplify ITE structure
void simpITE();
@@ -1825,11 +1827,15 @@ bool SmtEnginePrivate::nonClausalSimplify() {
}
hash_set<TNode, TNodeHashFunction> s;
+ Trace("debugging") << "NonClausal simplify pre-preprocess\n";
for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
Node assertion = d_assertionsToPreprocess[i];
Node assertionNew = d_topLevelSubstitutions.apply(assertion);
+ Trace("debugging") << "assertion = " << assertion << endl;
+ Trace("debugging") << "assertionNew = " << assertionNew << endl;
if (assertion != assertionNew) {
assertion = Rewriter::rewrite(assertionNew);
+ Trace("debugging") << "rewrite(assertion) = " << assertion << endl;
}
Assert(Rewriter::rewrite(assertion) == assertion);
for (;;) {
@@ -1838,8 +1844,11 @@ bool SmtEnginePrivate::nonClausalSimplify() {
break;
}
++d_smt.d_stats->d_numConstantProps;
+ Trace("debugging") << "assertionNew = " << assertionNew << endl;
assertion = Rewriter::rewrite(assertionNew);
+ Trace("debugging") << "assertionNew = " << assertionNew << endl;
}
+ Trace("debugging") << "\n";
s.insert(assertion);
d_assertionsToCheck.push_back(assertion);
Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
@@ -1927,6 +1936,15 @@ bool SmtEnginePrivate::nonClausalSimplify() {
}
+void SmtEnginePrivate::bvToBool() {
+ Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl;
+ std::vector<Node> 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]);
+ }
+}
+
void SmtEnginePrivate::simpITE() {
TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime);
@@ -2780,6 +2798,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/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
new file mode 100644
index 000000000..7bec805ef
--- /dev/null
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -0,0 +1,314 @@
+/********************* */
+/*! \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"
+#include "theory/bv/bv_to_bool.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+
+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) || term.getKind() == kind::CONST_BITVECTOR) {
+ 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) {}
+
+void BvToBoolVisitor::storeBvToBool(TNode bv_term, TNode bool_term) {
+ Assert (bv_term.getType().isBitVector() &&
+ 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;
+}
+
+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_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::BITVECTOR_SLT ||
+ kind == kind::BITVECTOR_SLE ||
+ kind == kind::EQUAL) &&
+ isConvertibleBvTerm(node[0]) &&
+ isConvertibleBvTerm(node[1]);
+}
+
+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;
+ }
+
+ if (!node.getType().isBitVector() || node.getType().getBitVectorSize() != 1)
+ return false;
+
+ Kind kind = node.getKind();
+
+ if (kind == kind::CONST_BITVECTOR) {
+ 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) {
+ if (!isConvertibleBvTerm(node[i]))
+ return false;
+ }
+ return true;
+ }
+ if (kind == kind::VARIABLE) {
+ storeBvToBool(node, utils::mkNode(kind::EQUAL, node, utils::mkConst(BitVector(1, 1u))));
+ return true;
+ }
+ return false;
+}
+
+Node BvToBoolVisitor::convertBvAtom(TNode node) {
+ Assert (node.getType().isBoolean());
+ Kind kind = node.getKind();
+ Node result;
+ switch(kind) {
+ case kind::BITVECTOR_ULT: {
+ 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: {
+ 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::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: {
+ 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;
+}
+
+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);
+ }
+ if (node.getKind() == kind::CONST_BITVECTOR) {
+ Node result = node == d_one ? utils::mkTrue() : utils::mkFalse();
+ storeBvToBool(node, result);
+ return result;
+ }
+ }
+
+ if (kind == kind::ITE) {
+ 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;
+ }
+
+ 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);
+ Debug("bv-to-bool") << "BvToBoolVisitor::convertBvTerm " << node <<" => " << result << "\n";
+ 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";
+ }
+ }
+}
+
+void BvToBoolVisitor::visit(TNode current, TNode parent) {
+ Debug("bv-to-bool") << "BvToBoolVisitor visit (" << current << ", " << parent << ")\n";
+ Assert (!alreadyVisited(current, parent) &&
+ !hasCache(current));
+
+ Node result;
+ // make sure that the bv terms we are replacing to not occur in other contexts
+ check(current, parent);
+
+ if (isConvertibleBvAtom(current)) {
+ result = convertBvAtom(current);
+ addToCache(current, result);
+ } else if (isConvertibleBvTerm(current)) {
+ result = convertBvTerm(current);
+ } else {
+ 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]);
+ Assert (converted.getType() == current[i].getType());
+ builder << converted;
+ }
+ result = builder;
+ }
+ addToCache(current, result);
+ }
+ Assert (result != Node());
+ Debug("bv-to-bool") << " =>" << result <<"\n";
+}
+
+
+BvToBoolVisitor::return_type BvToBoolVisitor::done(TNode node) {
+ Assert (hasCache(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) {
+ // 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<Node>& assertions, std::vector<Node>& new_assertions) {
+ BvToBoolVisitor bvToBoolVisitor;
+
+ 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_var.getType().getBitVectorSize() == 1);
+ Node bool_cond = NodeVisitor<BvToBoolVisitor>::run(bvToBoolVisitor, assertion[1]);
+ Assert (bool_cond.getType().isBoolean());
+ if (!bvToBoolVisitor.hasBoolTerm(bv_var)) {
+ Debug("bv-to-bool") << "BBvToBoolPreprocessor::liftBvToBoolBV candidate: " << bv_var <<"\n";
+ bvToBoolVisitor.storeBvToBool(bv_var, bool_cond);
+ } else {
+ Debug("bv-to-bool") << "BvToBoolPreprocessor::liftBvToBoolBV multiple def " << bv_var <<"\n";
+ }
+ }
+ }
+
+ for (unsigned i = 0; i < assertions.size(); ++i) {
+ Node new_assertion = NodeVisitor<BvToBoolVisitor>::run(bvToBoolVisitor,
+ assertions[i]);
+ 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
new file mode 100644
index 000000000..186f2b317
--- /dev/null
+++ b/src/theory/bv/bv_to_bool.h
@@ -0,0 +1,79 @@
+/********************* */
+/*! \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"
+#include "theory/bv/theory_bv_utils.h"
+
+#ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H
+#define __CVC4__THEORY__BV__BV_TO_BOOL_H
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+typedef __gnu_cxx::hash_map<Node, Node, TNodeHashFunction> NodeNodeMap;
+
+class BvToBoolVisitor {
+ NodeNodeMap d_bvToBoolMap;
+ NodeNodeMap d_cache;
+ Node d_one;
+ Node d_zero;
+
+ void addToCache(TNode term, Node new_term);
+ Node getCache(TNode term) const;
+ bool hasCache(TNode term) const;
+
+ bool isConvertibleBvTerm(TNode node);
+ bool isConvertibleBvAtom(TNode node);
+ Node getBoolForBvTerm(TNode node);
+ Node convertBvAtom(TNode node);
+ Node convertBvTerm(TNode node);
+ void check(TNode current, TNode parent);
+public:
+ typedef Node return_type;
+ BvToBoolVisitor()
+ : d_bvToBoolMap(),
+ d_cache(),
+ 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);
+ void storeBvToBool(TNode bv_term, TNode bool_term);
+ bool hasBoolTerm(TNode node);
+};
+
+
+class BvToBoolPreprocessor {
+ bool matchesBooleanPatern(TNode node);
+public:
+ BvToBoolPreprocessor()
+ {}
+ ~BvToBoolPreprocessor() {}
+ void liftBoolToBV(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
+};
+
+
+}/* CVC4::theory::bv namespace */
+}/* CVC4::theory namespace */
+
+}/* CVC4 namespace */
+
+
+#endif /* __CVC4__THEORY__BV__BV_TO_BOOL_H */
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 c597cb083..4c31f3f44 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),
@@ -125,8 +126,37 @@ 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 = 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 = 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);
+ }
+ }
+}
+
+
void TheoryBV::check(Effort e)
{
+ Trace("bitvector") <<"TheoryBV::check (" << e << ")\n";
Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
if (options::bitvectorEagerBitblast()) {
return;
@@ -145,6 +175,7 @@ void TheoryBV::check(Effort e)
while (!done()) {
TNode fact = get().assertion;
+ // checkForLemma(fact);
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
d_subtheories[i]->assertFact(fact);
}
@@ -249,7 +280,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
Node TheoryBV::ppRewrite(TNode t)
{
if (RewriteRule<BitwiseEq>::applies(t)) {
- Node result = RewriteRule<BitwiseEq>::run<false>(t);
+ Node result = RewriteRule<BitwiseEq>::run<false>(t);
return Rewriter::rewrite(result);
}
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 481493e13..22e3d0507 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -85,6 +85,8 @@ private:
Statistics d_statistics;
+ context::CDO<bool> d_lemmasAdded;
+
// Are we in conflict?
context::CDO<bool> d_conflict;
@@ -97,6 +99,8 @@ private:
/** Index of the next literal to propagate */
context::CDO<unsigned> d_literalsToPropagateIndex;
+
+
/**
* Keeps a map from nodes to the subtheory that propagated it so that we can explain it
* properly.
@@ -147,7 +151,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 e9a3494f0..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,
@@ -125,12 +126,17 @@ enum RewriteRuleId {
UremOne,
UremSelf,
ShiftZero,
+
+ UltOne,
+ SltZero,
+ ZeroUlt,
/// normalization rules
ExtractBitwise,
ExtractNot,
ExtractArith,
ExtractArith2,
+ ExtractSignExtend,
DoubleNeg,
NegMult,
NegSub,
@@ -148,7 +154,7 @@ enum RewriteRuleId {
AndSimplify,
OrSimplify,
XorSimplify,
-
+ BitwiseSlicing,
// rules to simplify bitblasting
BBPlusNeg
};
@@ -262,7 +268,13 @@ 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;
+ case UleEliminate : out << "UleEliminate"; return out;
+ case BitwiseSlicing : out << "BitwiseSlicing"; return out;
+ case ExtractSignExtend : out << "ExtractSignExtend"; return out;
default:
Unreachable();
}
@@ -477,6 +489,9 @@ struct AllRewriteRules {
RewriteRule<BBPlusNeg> rule111;
RewriteRule<SolveEq> rule112;
RewriteRule<BitwiseEq> rule113;
+ RewriteRule<UltOne> rule114;
+ RewriteRule<SltZero> rule115;
+
};
template<> inline
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 4ba09ef67..2da4dfa6a 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<ExtractNot>::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<ExtractSignExtend>::applies(TNode node) {
+ if (node.getKind() == kind::BITVECTOR_EXTRACT &&
+ node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND) {
+ return true;
+ }
+ return false;
+}
+
+template<> inline
+Node RewriteRule<ExtractSignExtend>::apply(TNode node) {
+ Debug("bv-rewrite") << "RewriteRule<ExtractSignExtend>(" << 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<Node> 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<XorSimplify>::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<BitwiseSlicing>::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<BitVector>();
+ // 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<BitwiseSlicing>::apply(TNode node) {
+ Debug("bv-rewrite") << "RewriteRule<BitwiseSlicing>(" << node << ")" << std::endl;
+ // get the constant
+ bool found_constant CVC4_UNUSED = false ;
+ TNode constant;
+ std::vector<Node> 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<AndSimplify>::applies(TNode node) {
-// return (node.getKind() == kind::BITVECTOR_AND);
-// }
-
-// template<> inline
-// Node RewriteRule<AndSimplify>::apply(TNode node) {
-// Debug("bv-rewrite") << "RewriteRule<AndSimplify>(" << node << ")" << std::endl;
-// return resultNode;
-// }
+ Node other = utils::mkNode(node.getKind(), other_children);
+
+ BitVector bv_constant = constant.getConst<BitVector>();
+ std::vector<Node> 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_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 06ddc215d..cf36633fa 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -111,17 +111,30 @@ bool RewriteRule<SleEliminate>::applies(TNode node) {
template <>
Node RewriteRule<SleEliminate>::apply(TNode node) {
Debug("bv-rewrite") << "RewriteRule<SleEliminate>(" << 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<UleEliminate>::applies(TNode node) {
+ return (node.getKind() == kind::BITVECTOR_ULE);
+}
+
+template <>
+Node RewriteRule<UleEliminate>::apply(TNode node) {
+ Debug("bv-rewrite") << "RewriteRule<UleEliminate>(" << 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<CompEliminate>::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
@@ -524,6 +524,25 @@ Node RewriteRule<LteSelf>::apply(TNode node) {
}
/**
+ * ZeroUlt
+ *
+ * 0 < a ==> a != 0
+ */
+
+template<> inline
+bool RewriteRule<ZeroUlt>::applies(TNode node) {
+ return (node.getKind() == kind::BITVECTOR_ULT &&
+ node[0] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
+}
+
+template<> inline
+Node RewriteRule<ZeroUlt>::apply(TNode node) {
+ Debug("bv-rewrite") << "RewriteRule<ZeroUlt>(" << node << ")" << std::endl;
+ return utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, node[0], node[1]));
+}
+
+
+/**
* UltZero
*
* a < 0 ==> false
@@ -541,6 +560,42 @@ Node RewriteRule<UltZero>::apply(TNode node) {
return utils::mkFalse();
}
+
+/**
+ *
+ */
+template<> inline
+bool RewriteRule<UltOne>::applies(TNode node) {
+ return (node.getKind() == kind::BITVECTOR_ULT &&
+ node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(1))));
+}
+
+template<> inline
+Node RewriteRule<UltOne>::apply(TNode node) {
+ Debug("bv-rewrite") << "RewriteRule<UltOne>(" << node << ")" << std::endl;
+ return utils::mkNode(kind::EQUAL, node[0], utils::mkConst(BitVector(utils::getSize(node[0]), 0u)));
+}
+
+/**
+ *
+ */
+template<> inline
+bool RewriteRule<SltZero>::applies(TNode node) {
+ return (node.getKind() == kind::BITVECTOR_SLT &&
+ node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
+}
+
+template<> inline
+Node RewriteRule<SltZero>::apply(TNode node) {
+ Debug("bv-rewrite") << "RewriteRule<UltZero>(" << 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..5a43e2c57 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -77,6 +77,8 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) {
// if both arguments are constants evaluates
RewriteRule<UltZero>
// a < 0 rewrites to false
+ // RewriteRule<UltOne>,
+ // RewriteRule<ZeroUlt>
>::apply(node);
return RewriteResponse(REWRITE_DONE, resultNode);
@@ -85,6 +87,7 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) {
RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){
Node resultNode = LinearRewriteStrategy
< RewriteRule < EvalSlt >
+ // RewriteRule < SltZero >
>::apply(node);
return RewriteResponse(REWRITE_DONE, resultNode);
@@ -103,17 +106,18 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){
RewriteRule<UleMax>,
RewriteRule<ZeroUle>,
RewriteRule<UleZero>,
- RewriteRule<UleSelf>
+ RewriteRule<UleSelf>//,
+ // RewriteRule<UleEliminate>
>::apply(node);
return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode);
}
RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){
Node resultNode = LinearRewriteStrategy
- < RewriteRule < EvalSle >
+ < RewriteRule <EvalSle>//,
+ // RewriteRule <SleEliminate>
>::apply(node);
-
- return RewriteResponse(REWRITE_DONE, resultNode);
+ return RewriteResponse(resultNode == node? REWRITE_DONE : REWRITE_AGAIN, resultNode);
}
RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){
@@ -173,6 +177,11 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) {
return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
}
+ if (RewriteRule<ExtractSignExtend>::applies(node)) {
+ resultNode = RewriteRule<ExtractSignExtend>::run<false>(node);
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
+
if (RewriteRule<ExtractBitwise>::applies(node)) {
resultNode = RewriteRule<ExtractBitwise>::run<false>(node);
return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
@@ -219,14 +228,14 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){
resultNode = LinearRewriteStrategy
< RewriteRule<FlattenAssocCommut>,
- RewriteRule<AndSimplify>
- // RewriteRule<EvalAnd>,
- // RewriteRule<BitwiseIdemp>,
- // //RewriteRule<BitwiseSlice>, -> might need rw again
- // RewriteRule<AndZero>,
- // RewriteRule<AndOne>
+ RewriteRule<AndSimplify>,
+ RewriteRule<BitwiseSlicing>
>::apply(node);
+ if (resultNode.getKind() != node.getKind()) {
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
+
return RewriteResponse(REWRITE_DONE, resultNode);
}
@@ -235,8 +244,13 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){
resultNode = LinearRewriteStrategy
< RewriteRule<FlattenAssocCommut>,
- RewriteRule<OrSimplify>
+ RewriteRule<OrSimplify>,
+ RewriteRule<BitwiseSlicing>
>::apply(node);
+
+ if (resultNode.getKind() != node.getKind()) {
+ return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+ }
return RewriteResponse(REWRITE_DONE, resultNode);
}
@@ -247,7 +261,8 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) {
resultNode = LinearRewriteStrategy
< RewriteRule<FlattenAssocCommut>, // flatten the expression
RewriteRule<XorSimplify>, // simplify duplicates and constants
- RewriteRule<XorZero> // checks if the constant part is zero and eliminates it
+ RewriteRule<XorZero>, // checks if the constant part is zero and eliminates it
+ RewriteRule<BitwiseSlicing>
>::apply(node);
// this simplification introduces new terms and might require further
@@ -257,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);
}
@@ -297,7 +316,8 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) {
resultNode = LinearRewriteStrategy
< RewriteRule<FlattenAssocCommut>, // flattens and sorts
- RewriteRule<MultSimplify> // multiplies constant part and checks for 0
+ RewriteRule<MultSimplify>, // multiplies constant part and checks for 0
+ RewriteRule<MultPow2> // replaces multiplication by a power of 2 by a shift
>::apply(node);
// only apply if every subterm was already rewritten
@@ -313,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 174df03ab..5847bac3e 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<Node>& children) {
inline Node mkNode(Kind kind, std::vector<Node>& 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>(BitVectorSignExtend(ammount));
+ return nm->mkNode(signExtendOp, node);
+}
+
inline Node mkExtract(TNode node, unsigned high, unsigned low) {
Node extractOp = NodeManager::currentNM()->mkConst<BitVectorExtract>(BitVectorExtract(high, low));
std::vector<Node> children;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 442b1ef1c..6c8341345 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,10 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
}
}
+void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
+ d_bvToBoolPreprocessor.liftBoolToBV(assertions, new_assertions);
+}
+
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..c21819ea1 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:
+ void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
Node ppSimpITE(TNode assertion);
void ppUnconstrainedSimp(std::vector<Node>& assertions);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback