diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-02-25 18:23:10 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-02-25 18:23:10 +0000 |
commit | 7aa55e0d38e73a02b11ad0c5a60196b610674050 (patch) | |
tree | c59def0ed00dcde29a5a6498cf74ac87dc3a2a6f /src/prop/cnf_stream.cpp | |
parent | d8da6a3644d1cdbe62d44a8eb80068da4d1d2855 (diff) |
Refactored CnfStream to work with the bv theory Bitblaster:
* separated SatSolverInput interface class into two classes:
- TheoryProxy for the sat solver to communicate with the theories
- SatSolverInterface abstract class to communicate with the sat solver
* instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation
* added abstract classes for DPLLSatSolver and BVSatSolver different interfaces
Replaced TheoryBV with bitblasting implementation:
* all operators bitblasted
* only operator elimination rewrite rules so far
Diffstat (limited to 'src/prop/cnf_stream.cpp')
-rw-r--r-- | src/prop/cnf_stream.cpp | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 681e42a99..74feebd03 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -18,7 +18,6 @@ ** of given an equisatisfiable stream of assertions to PropEngine. **/ -#include "prop/sat.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "theory/theory_engine.h" @@ -28,6 +27,7 @@ #include "util/output.h" #include "expr/command.h" #include "expr/expr.h" +#include "prop/sat.h" #include <queue> @@ -43,7 +43,8 @@ using namespace CVC4::kind; namespace CVC4 { namespace prop { -CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar, bool fullLitToNodeMap) : + +CnfStream::CnfStream(SatSolverInterface *satSolver, Registrar* registrar, bool fullLitToNodeMap) : d_satSolver(satSolver), d_fullLitToNodeMap(fullLitToNodeMap), d_registrar(registrar) { @@ -55,7 +56,7 @@ void CnfStream::recordTranslation(TNode node) { } } -TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar, bool fullLitToNodeMap) : +TseitinCnfStream::TseitinCnfStream(SatSolverInterface* satSolver, Registrar* registrar, bool fullLitToNodeMap) : CnfStream(satSolver, registrar, fullLitToNodeMap) { } @@ -164,7 +165,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { SatLiteral lit; if (!hasLiteral(node)) { // If no literal, well make one - lit = variableToLiteral(d_satSolver->newVar(theoryLiteral)); + lit = SatLiteral(d_satSolver->newVar(theoryLiteral)); d_translationCache[node].literal = lit; d_translationCache[node.notNode()].literal = ~lit; } else { @@ -189,7 +190,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { // If a theory literal, we pre-register it if (theoryLiteral) { bool backup = d_removable; - d_registrar.preRegister(node); + d_registrar->preRegister(node); d_removable = backup; } @@ -212,7 +213,7 @@ SatLiteral CnfStream::convertAtom(TNode node) { Debug("cnf") << "convertAtom(" << node << ")" << endl; Assert(!isTranslated(node), "atom already mapped!"); - + // boolean variables are not theory literals bool theoryLiteral = node.getKind() != kind::VARIABLE && !node.getType().isPseudoboolean(); SatLiteral lit = newLiteral(node, theoryLiteral); |