From bb6c74a7bb306de8b7c5d7e9701b3524eda68f4a Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Wed, 3 Apr 2013 17:55:58 -0400 Subject: [PATCH] * changing the bitblast-eager to bitblast on pre-register * the newVar interface of the sat solver now changed to include (isTheoryLiteral, preRegister, canEliminate) * when bitblast-eager all bv atoms are (theory=false, prereg = true, canelim = true) * bitblast-eager implies decision=internal --- src/prop/bvminisat/bvminisat.cpp | 4 ++-- src/prop/bvminisat/bvminisat.h | 2 +- src/prop/cnf_stream.cpp | 27 ++++++++++++++++----- src/prop/cnf_stream.h | 7 +++--- src/prop/minisat/core/Solver.cc | 6 ++--- src/prop/minisat/core/Solver.h | 2 +- src/prop/minisat/minisat.cpp | 4 ++-- src/prop/minisat/minisat.h | 2 +- src/prop/minisat/simp/SimpSolver.cc | 6 ++--- src/prop/minisat/simp/SimpSolver.h | 2 +- src/prop/sat_solver.h | 10 ++++++-- src/smt/smt_engine.cpp | 6 +++++ src/theory/bv/bitblaster.cpp | 1 + src/theory/bv/bv_subtheory_bitblast.cpp | 32 ++++++++++++------------- src/theory/bv/bv_subtheory_bitblast.h | 1 + src/theory/bv/theory_bv.cpp | 9 +++++++ 16 files changed, 79 insertions(+), 42 deletions(-) diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 032788806..6bbe4bb3e 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -88,8 +88,8 @@ void BVMinisatSatSolver::popAssumption() { d_minisat->popAssumption(); } -SatVariable BVMinisatSatSolver::newVar(bool freeze){ - return d_minisat->newVar(true, true, freeze); +SatVariable BVMinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){ + return d_minisat->newVar(true, true, !canErase); } void BVMinisatSatSolver::markUnremovable(SatLiteral lit){ diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 0dd208088..ebf4a44b4 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -80,7 +80,7 @@ public: SatValue propagate(); - SatVariable newVar(bool theoryAtom = false); + SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); SatVariable trueVar() { return d_minisat->trueVar(); } SatVariable falseVar() { return d_minisat->falseVar(); } diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 983669da3..4be58bdef 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -26,6 +26,7 @@ #include "expr/command.h" #include "expr/expr.h" #include "prop/theory_proxy.h" +#include "theory/bv/options.h" #include @@ -151,8 +152,8 @@ void TseitinCnfStream::ensureLiteral(TNode n) { Debug("ensureLiteral") << "CnfStream::ensureLiteral(): out lit is " << lit << std::endl; } -SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { - Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl; +SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister, bool canEliminate) { + Debug("cnf") << "newLiteral(" << node << ", " << isTheoryAtom << ")" << endl; Assert(node.getKind() != kind::NOT); // Get the literal for this node @@ -166,7 +167,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { lit = SatLiteral(d_satSolver->falseVar()); } } else { - lit = SatLiteral(d_satSolver->newVar(theoryLiteral)); + lit = SatLiteral(d_satSolver->newVar(isTheoryAtom, preRegister, canEliminate)); } d_nodeToLiteralMap.insert(node, lit); d_nodeToLiteralMap.insert(node.notNode(), ~lit); @@ -175,7 +176,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { } // If it's a theory literal, need to store it for back queries - if ( theoryLiteral || d_fullLitToNodeMap || + if ( isTheoryAtom || d_fullLitToNodeMap || ( CVC4_USE_REPLAY && options::replayLog() != NULL ) || (Dump.isOn("clauses")) ) { @@ -184,7 +185,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { } // If a theory literal, we pre-register it - if (theoryLiteral) { + if (preRegister) { bool backup = d_removable; d_registrar->preRegister(node); d_removable = backup; @@ -214,13 +215,27 @@ SatLiteral CnfStream::convertAtom(TNode node) { Assert(!hasLiteral(node), "atom already mapped!"); + bool theoryLiteral = false; + bool canEliminate = true; + bool preRegister = false; + // Is this a variable add it to the list if (node.isVar()) { d_booleanVariables.push_back(node); + } else { + theoryLiteral = true; + canEliminate = false; + preRegister = true; + + if (options::bitvectorEagerBitblast() && theory::Theory::theoryOf(node) == theory::THEORY_BV) { + // All BV atoms are treated as boolean except for equality + theoryLiteral = false; + canEliminate = true; + } } // Make a new literal (variables are not considered theory literals) - SatLiteral lit = newLiteral(node, !node.isVar()); + SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate); // Return the resulting literal return lit; diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index cbcca5e85..1c66be911 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -146,11 +146,12 @@ protected: * Acquires a new variable from the SAT solver to represent the node * and inserts the necessary data it into the mapping tables. * @param node a formula - * @param theoryLiteral whether this literal a theory literal (and - * therefore the theory is to be informed when set to true/false) + * @param isTheoryAtom is this a theory atom that needs to be asserted to theory + * @param preRegister whether to preregister the atom with the theory + * @param canEliminate whether the sat solver can safely eliminate this variable * @return the literal corresponding to the formula */ - SatLiteral newLiteral(TNode node, bool theoryLiteral = false); + SatLiteral newLiteral(TNode node, bool isTheoryAtom = false, bool preRegister = false, bool canEliminate = true); /** * Constructs a new literal for an atom and returns it. Calls diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index f7d67d445..c7f1780b6 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -150,7 +150,7 @@ Solver::~Solver() // Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be // used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). // -Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) +Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bool canErase) { int v = nVars(); @@ -163,12 +163,12 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) polarity .push(sign); decision .push(); trail .capacity(v+1); - theory .push(theoryAtom); + theory .push(isTheoryAtom); setDecisionVar(v, dvar); // If the variable is introduced at non-zero level, we need to reintroduce it on backtracks - if (theoryAtom) { + if (preRegister) { variables_to_register.push(VarIntroInfo(v, decisionLevel())); } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 0dad68a08..9338f9b55 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -117,7 +117,7 @@ public: // Problem specification: // - Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode. + Var newVar (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); // Add a new variable with parameters specifying variable mode. Var trueVar() const { return varTrue; } Var falseVar() const { return varFalse; } diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 886dc0f72..960f2ad62 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -140,8 +140,8 @@ void MinisatSatSolver::addClause(SatClause& clause, bool removable) { d_minisat->addClause(minisat_clause, removable); } -SatVariable MinisatSatSolver::newVar(bool theoryAtom) { - return d_minisat->newVar(true, true, theoryAtom); +SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) { + return d_minisat->newVar(true, true, isTheoryAtom, preRegister, canErase); } SatValue MinisatSatSolver::solve(unsigned long& resource) { diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 723f257f7..37e471846 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -57,7 +57,7 @@ public: void addClause(SatClause& clause, bool removable); - SatVariable newVar(bool theoryAtom = false); + SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase); SatVariable trueVar() { return d_minisat->trueVar(); } SatVariable falseVar() { return d_minisat->falseVar(); } diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index ed2dc04b9..9c3e59954 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -95,11 +95,11 @@ SimpSolver::~SimpSolver() } -Var SimpSolver::newVar(bool sign, bool dvar, bool theoryAtom) { - Var v = Solver::newVar(sign, dvar,theoryAtom); +Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bool canErase) { + Var v = Solver::newVar(sign, dvar, isTheoryAtom, preRegister, canErase); if (use_simplification){ - frozen .push((char)theoryAtom); + frozen .push((char)(!canErase)); eliminated.push((char)false); n_occ .push(0); n_occ .push(0); diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index e9116001f..878d799a5 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -46,7 +46,7 @@ class SimpSolver : public Solver { // Problem specification: // - Var newVar (bool polarity = true, bool dvar = true, bool theoryAtom = false); + Var newVar (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); bool addClause (const vec& ps, bool removable); bool addEmptyClause(bool removable); // Add the empty clause to the solver. bool addClause (Lit p, bool removable); // Add a unit clause to the solver. diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index d55788298..18a1dcf68 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -40,8 +40,14 @@ public: /** Assert a clause in the solver. */ virtual void addClause(SatClause& clause, bool removable) = 0; - /** Create a new boolean variable in the solver. */ - virtual SatVariable newVar(bool theoryAtom = false) = 0; + /** + * Create a new boolean variable in the solver. + * @param isTheoryAtom is this a theory atom that needs to be asserted to theory + * @param preRegister whether to preregister the atom with the theory + * @param canErase whether the sat solver can safely eliminate this variable + * + */ + virtual SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) = 0; /** Create a new (or return an existing) boolean variable representing the constant true */ virtual SatVariable trueVar() = 0; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 18636a486..55000c94d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -59,6 +59,7 @@ #include "theory/substitutions.h" #include "theory/uf/options.h" #include "theory/arith/options.h" +#include "theory/bv/options.h" #include "theory/theory_traits.h" #include "theory/logic_info.h" #include "theory/options.h" @@ -674,6 +675,11 @@ void SmtEngine::finalOptionsAreSet() { return; } + if (options::bitvectorEagerBitblast()) { + // Eager solver should use the internal decision strategy + options::decisionMode.set(DECISION_STRATEGY_INTERNAL); + } + if(options::checkModels()) { if(! options::produceModels()) { Notice() << "SmtEngine: turning on produce-models to support check-model" << endl; diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index cf841bb56..ad62ade38 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -104,6 +104,7 @@ void Bitblaster::bbAtom(TNode node) { d_bitblastedAtoms.insert(node); } else { d_bvOutput->lemma(atom_definition, false); + d_bitblastedAtoms.insert(node); } } diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 237b04172..d8a784544 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -54,7 +54,11 @@ void BitblastSolver::preRegister(TNode node) { node.getKind() == kind::BITVECTOR_SLT || node.getKind() == kind::BITVECTOR_SLE) && !d_bitblaster->hasBBAtom(node)) { - d_bitblastQueue.push_back(node); + if (options::bitvectorEagerBitblast()) { + d_bitblaster->bbAtom(node); + } else { + d_bitblastQueue.push_back(node); + } } } @@ -62,29 +66,23 @@ void BitblastSolver::explain(TNode literal, std::vector& assumptions) { d_bitblaster->explain(literal, assumptions); } +void BitblastSolver::bitblastQueue() { + while (!d_bitblastQueue.empty()) { + TNode atom = d_bitblastQueue.front(); + d_bitblaster->bbAtom(atom); + d_bitblastQueue.pop(); + } +} bool BitblastSolver::check(Theory::Effort e) { Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; + Assert(!options::bitvectorEagerBitblast()); + ++(d_statistics.d_numCallstoCheck); - //// Eager bit-blasting - if (options::bitvectorEagerBitblast()) { - while (!done()) { - TNode assertion = get(); - TNode atom = assertion.getKind() == kind::NOT ? assertion[0] : assertion; - if (atom.getKind() != kind::BITVECTOR_BITOF) { - d_bitblaster->bbAtom(atom); - } - return true; - } - } //// Lazy bit-blasting // bit-blast enqueued nodes - while (!d_bitblastQueue.empty()) { - TNode atom = d_bitblastQueue.front(); - d_bitblaster->bbAtom(atom); - d_bitblastQueue.pop(); - } + bitblastQueue(); // Processing assertions while (!done()) { diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 1eef61daf..1fab621cd 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -52,6 +52,7 @@ public: void collectModelInfo(TheoryModel* m); Node getModelValue(TNode node); bool isComplete() { return true; } + void bitblastQueue(); }; } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 228a4d8a3..433223308 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -102,6 +102,7 @@ void TheoryBV::preRegisterTerm(TNode node) { if (options::bitvectorEagerBitblast()) { // don't use the equality engine in the eager bit-blasting + d_subtheoryMap[SUB_BITBLAST]->preRegister(node); return; } for (unsigned i = 0; i < d_subtheories.size(); ++i) { @@ -124,6 +125,10 @@ void TheoryBV::sendConflict() { void TheoryBV::check(Effort e) { Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; + if (options::bitvectorEagerBitblast()) { + return; + } + if (Theory::fullEffort(e)) { ++(d_statistics.d_numCallsToCheckFullEffort); } else { @@ -186,6 +191,10 @@ Node TheoryBV::getModelValue(TNode var) { void TheoryBV::propagate(Effort e) { Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl; + if (options::bitvectorEagerBitblast()) { + return; + } + if (inConflict()) { return; } -- 2.30.2