diff options
author | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-04-03 17:55:58 -0400 |
---|---|---|
committer | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-04-03 17:55:58 -0400 |
commit | bb6c74a7bb306de8b7c5d7e9701b3524eda68f4a (patch) | |
tree | 17482f7fcc4f5af3ae46c9428e942f05f7f8abf8 /src/prop/cnf_stream.cpp | |
parent | 62748da1e72dbcc5c6daef88ad899706de8ae7db (diff) |
* 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
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r-- | src/prop/cnf_stream.cpp | 27 |
1 files changed, 21 insertions, 6 deletions
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; |