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 | |
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')
-rw-r--r-- | test/unit/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/prop/cnf_stream_black.h | 24 | ||||
-rw-r--r-- | test/unit/theory/theory_bv_white.h | 117 |
3 files changed, 138 insertions, 4 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index b2369e2d7..bb0b5ea08 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -4,6 +4,7 @@ UNIT_TESTS = \ theory/theory_black \ theory/theory_arith_white \ theory/union_find_black \ + theory/theory_bv_white \ expr/expr_public \ expr/expr_manager_public \ expr/node_white \ 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() { diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h new file mode 100644 index 000000000..a158b167f --- /dev/null +++ b/test/unit/theory/theory_bv_white.h @@ -0,0 +1,117 @@ +/********************* */ +/*! \file theory_bv_white.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + + +#include <cxxtest/TestSuite.h> + +#include "theory/theory.h" +#include "theory/bv/bv_sat.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "context/context.h" + +#include "theory/theory_test_utils.h" + +#include <vector> + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace CVC4::theory::bv::utils; +using namespace CVC4::expr; +using namespace CVC4::context; + +using namespace std; + +class TheoryBVWhite : public CxxTest::TestSuite { + + Context* d_ctxt; + NodeManager* d_nm; + NodeManagerScope* d_scope; + + bool debug; + +public: + + TheoryBVWhite() : debug(false) {} + + + void setUp() { + d_ctxt = new Context(); + d_nm = new NodeManager(d_ctxt, NULL); + d_scope = new NodeManagerScope(d_nm); + + } + + void tearDown() { + delete d_scope; + delete d_nm; + delete d_ctxt; + } + + + void testBitblasterCore() { + // ClauseManager tests + Context* ctx = new Context(); + Bitblaster* bb = new Bitblaster(ctx); + + NodeManager* nm = NodeManager::currentNM(); + // TODO: update this + // Node a = nm->mkVar("a", nm->mkBitVectorType(4)); + // Node b = nm->mkVar("b", nm->mkBitVectorType(4)); + // Node a1 = nm->mkNode(nm->mkConst<BitVectorExtract>(BitVectorExtract(2,1)), a); + // Node b1 = nm->mkNode(nm->mkConst<BitVectorExtract>(BitVectorExtract(2,1)), b); + + // Node abeq = nm->mkNode(kind::EQUAL, a, b); + // Node neq = nm->mkNode(kind::NOT, abeq); + // Node a1b1eq = nm->mkNode(kind::EQUAL, a1, b1); + + // bb->bitblast(neq); + // bb->bitblast(a1b1eq); + + // /// constructing the rest of the problem + // Node a2 = nm->mkNode(nm->mkConst<BitVectorExtract>(BitVectorExtract(0,0)), a); + // Node b2 = nm->mkNode(nm->mkConst<BitVectorExtract>(BitVectorExtract(0,0)), b); + // Node eq2 = nm->mkNode(kind::EQUAL, a2, b2); + + // Node a3 = nm->mkNode(nm->mkConst<BitVectorExtract>(BitVectorExtract(3,3)), a); + // Node b3 = nm->mkNode(nm->mkConst<BitVectorExtract>(BitVectorExtract(3,3)), b); + // Node eq3 = nm->mkNode(kind::EQUAL, a3, b3); + + // bb->bitblast(eq2); + // bb->bitblast(eq3); + + // ctx->push(); + // bb->assertToSat(neq); + // bb->assertToSat(a1b1eq); + // bool res = bb->solve(); + // TS_ASSERT (res == true); + + // ctx->push(); + // bb->assertToSat(eq2); + // bb->assertToSat(eq3); + + // res = bb->solve(); + // TS_ASSERT(res == false); + + delete bb; + + } + +}; |