summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/prop/bvminisat/bvminisat.cpp4
-rw-r--r--src/prop/bvminisat/bvminisat.h2
-rw-r--r--src/prop/cnf_stream.cpp27
-rw-r--r--src/prop/cnf_stream.h7
-rw-r--r--src/prop/minisat/core/Solver.cc6
-rw-r--r--src/prop/minisat/core/Solver.h2
-rw-r--r--src/prop/minisat/minisat.cpp4
-rw-r--r--src/prop/minisat/minisat.h2
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc6
-rw-r--r--src/prop/minisat/simp/SimpSolver.h2
-rw-r--r--src/prop/sat_solver.h10
-rw-r--r--src/smt/smt_engine.cpp6
-rw-r--r--src/theory/bv/bitblaster.cpp1
-rw-r--r--src/theory/bv/bv_subtheory_bitblast.cpp32
-rw-r--r--src/theory/bv/bv_subtheory_bitblast.h1
-rw-r--r--src/theory/bv/theory_bv.cpp9
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 <queue>
@@ -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<Lit>& 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<TNode>& 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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback