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 /test/unit/prop | |
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 'test/unit/prop')
-rw-r--r-- | test/unit/prop/cnf_stream_black.h | 24 |
1 files changed, 20 insertions, 4 deletions
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index 8520dacd8..99e8b087c 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -30,10 +30,10 @@ #include "prop/prop_engine.h" #include "prop/sat.h" #include "smt/smt_engine.h" -#include "theory/registrar.h" #include "theory/theory.h" #include "theory/theory_engine.h" +#include "theory/theory_registrar.h" #include "theory/builtin/theory_builtin.h" #include "theory/booleans/theory_bool.h" @@ -45,7 +45,7 @@ using namespace CVC4::prop; using namespace std; /* This fake class relies on the face that a MiniSat variable is just an int. */ -class FakeSatSolver : public SatInputInterface { +class FakeSatSolver : public SatSolverInterface { SatVariable d_nextVar; bool d_addClauseCalled; @@ -83,6 +83,23 @@ public: void interrupt() { } + + SatLiteralValue solve() { + return SatValUnknown; + } + + SatLiteralValue solve(long unsigned int& resource) { + return SatValUnknown; + } + + SatLiteralValue value(SatLiteral l) { + return SatValUnknown; + } + + SatLiteralValue modelValue(SatLiteral l) { + return SatValUnknown; + } + }; class CnfStreamBlack : public CxxTest::TestSuite { @@ -117,8 +134,7 @@ class CnfStreamBlack : public CxxTest::TestSuite { d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN); d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL); d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH); - theory::Registrar registrar(d_theoryEngine); - d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar); + d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine)); } void tearDown() { |