From 2f70d96546d82e6beb1e4492bfee46c962d9cfe4 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Wed, 26 May 2010 20:52:37 +0000 Subject: [PATCH] Adding CnfStream unit tests --- test/unit/Makefile.am | 1 + test/unit/prop/cnf_stream_black.h | 183 ++++++++++++++++++++++++++++++ 2 files changed, 184 insertions(+) create mode 100644 test/unit/prop/cnf_stream_black.h diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index b3a8e12eb..e626da47b 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -11,6 +11,7 @@ UNIT_TESTS = \ expr/attribute_black \ expr/declaration_scope_black \ parser/parser_black \ + prop/cnf_stream_black \ context/context_black \ context/context_white \ context/context_mm_black \ diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h new file mode 100644 index 000000000..7b062cfd7 --- /dev/null +++ b/test/unit/prop/cnf_stream_black.h @@ -0,0 +1,183 @@ +/********************* */ +/** cnf_stream_black.h + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): dejan, mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** White box testing of CVC4::prop::CnfStream. + **/ + +#include +/* #include */ +/* #include */ + +#include "util/Assert.h" + +/** Mock objects and definitions from sat.h*/ + +/* Prevent sat.h from being included, so we can mock it. */ +/* #define __CVC4__PROP__SAT_H */ + +/* namespace CVC4 { */ +/* namespace prop { */ + +/* typedef unsigned int SatVariable; */ +/* typedef int SatLiteralValue; */ + +/* class SatLiteral { */ +/* friend class SatSolver; */ + +/* SatLiteralValue d_value; */ + +/* public: */ +/* SatLiteral(SatVariable x) { */ +/* AlwaysAssert( x > 0 ); */ +/* d_value = (SatLiteralValue)x; */ +/* } */ + +/* friend SatLiteral operator~(SatLiteral lit); */ +/* }; */ + +/* SatLiteral operator~(SatLiteral lit) { */ +/* return SatLiteral(-lit.d_value); */ +/* } */ + +/* typedef std::vector SatClause; */ + + +/* class SatSolver { */ +/* SatVariable d_nextVar; */ + +/* public: */ +/* /\** Hash function for literals *\/ */ +/* struct SatLiteralHashFunction { */ +/* size_t operator()(const SatLiteral& literal) const { */ +/* return literal.d_value; */ +/* } */ +/* }; */ + +/* SatSolver() : */ +/* d_nextVar(1) { */ +/* } */ + +/* SatVariable newVar(bool theoryAtom) { */ +/* return d_nextVar++; */ +/* } */ + +/* void addClause(SatClause& clause) { */ +/* // do nothing */ +/* } */ +/* }; */ +/* } */ +/* } */ + +#include "expr/expr_manager.h" +#include "expr/node_manager.h" +#include "context/context.h" +#include "prop/cnf_stream.h" +#include "prop/prop_engine.h" +#include "prop/sat.h" +#include "smt/smt_engine.h" +#include "util/options.h" +#include "util/decision_engine.h" + +using namespace CVC4; +using namespace CVC4::context; +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 { + SatVariable d_nextVar; +public: + FakeSatSolver() : + d_nextVar(0) { + } + + void addClause(SatClause& clause) { } + + SatVariable newVar(bool theoryAtom) { + return d_nextVar++; + } + +// MOCK_METHOD1(addClause, void (SatClause&)); +// MOCK_METHOD1(newVar, SatVariable (bool)); +}; + +class CnfStreamBlack : public CxxTest::TestSuite { + /** The SAT solver proxy */ + SatInputInterface *d_satSolver; + + /** The CNF converter in use */ + CnfStream* d_cnfStream; + + Context* d_context; + + /* SmtEngine* d_smtEngine; */ + +// * The decision engine + /* DecisionEngine* d_decisionEngine; */ + +// * The decision engine + /* TheoryEngine* d_theoryEngine; */ + + /* ExprManager *d_exprManager; */ + NodeManager *d_nodeManager; + +void setUp() { + /* int argc = 1; */ + /* char *argv[] = { static_cast("cnf_stream_black") }; */ + /* ::testing::GTEST_FLAG(throw_on_failure) = true; */ + /* ::testing::InitGoogleMock(&argc, argv); */ + + d_context = new Context; + d_nodeManager = new NodeManager(d_context); + d_satSolver = new FakeSatSolver; + /* d_exprManager = new ExprManager(); */ + + /* opts = new Options; */ + /* d_smtEngine = new SmtEngine(d_exprManager, opts); */ + /* d_cnfStream = d_smtEngine->getPropEngine()->getCnfStream(); */ + /* d_decisionEngine = new DecisionEngine; */ + /* d_theoryEngine = new TheoryEngine(d_smtEngine, d_ctxt); */ + /* d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine, d_ctxt); */ + /* d_satSolver = new SatSolver(d_propEngine, d_theoryEngine, d_context, opts); */ + d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver); + /* d_satSolver->setCnfStream(d_cnfStream); */ +} + +void tearDown() { + NodeManagerScope nms(d_nodeManager); + delete d_cnfStream; + delete d_satSolver; + delete d_nodeManager; +} + +public: +void testTrue() { + NodeManagerScope nms(d_nodeManager); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true) ); +} + +void testIte() { + NodeManagerScope nms(d_nodeManager); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode( + kind::EQUAL, + d_nodeManager->mkNode( + kind::ITE, + d_nodeManager->mkVar(d_nodeManager->booleanType()), + d_nodeManager->mkVar(d_nodeManager->integerType()), + d_nodeManager->mkVar(d_nodeManager->integerType()) + ), + d_nodeManager->mkVar(d_nodeManager->integerType()) + )); + +} +}; -- 2.30.2