From 823f315d77fa07c0c69910a799700c9376b50f76 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 23 Feb 2021 23:38:38 -0800 Subject: [PATCH] google test: prop: Migrate cnf_stream_white. (#5971) --- test/unit/prop/CMakeLists.txt | 2 +- test/unit/prop/cnf_stream_white.cpp | 273 ++++++++++++++++++++++++++ test/unit/prop/cnf_stream_white.h | 285 ---------------------------- test/unit/test_smt.h | 4 +- 4 files changed, 276 insertions(+), 288 deletions(-) create mode 100644 test/unit/prop/cnf_stream_white.cpp delete mode 100644 test/unit/prop/cnf_stream_white.h diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt index f866e5ffa..bed0575c6 100644 --- a/test/unit/prop/CMakeLists.txt +++ b/test/unit/prop/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_cxx_unit_test_white(cnf_stream_white prop) +cvc4_add_unit_test_white(cnf_stream_white prop) diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp new file mode 100644 index 000000000..569c8a0e1 --- /dev/null +++ b/test/unit/prop/cnf_stream_white.cpp @@ -0,0 +1,273 @@ +/********************* */ +/*! \file cnf_stream_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Christopher L. Conway, Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief White box testing of CVC4::prop::CnfStream. + ** + ** White box testing of CVC4::prop::CnfStream. + **/ + +#include "base/check.h" +#include "context/context.h" +#include "prop/cnf_stream.h" +#include "prop/prop_engine.h" +#include "prop/registrar.h" +#include "prop/theory_proxy.h" +#include "test_smt.h" +#include "theory/arith/theory_arith.h" +#include "theory/booleans/theory_bool.h" +#include "theory/builtin/theory_builtin.h" +#include "theory/theory.h" +#include "theory/theory_engine.h" + +namespace CVC4 { + +using namespace context; +using namespace prop; +using namespace smt; +using namespace theory; + +namespace test { + +/* This fake class relies on the fact that a MiniSat variable is just an int. */ +class FakeSatSolver : public SatSolver +{ + public: + FakeSatSolver() : d_nextVar(0), d_addClauseCalled(false) {} + + SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) override + { + return d_nextVar++; + } + + SatVariable trueVar() override { return d_nextVar++; } + + SatVariable falseVar() override { return d_nextVar++; } + + ClauseId addClause(SatClause& c, bool lemma) override + { + d_addClauseCalled = true; + return ClauseIdUndef; + } + + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override + { + d_addClauseCalled = true; + return ClauseIdUndef; + } + + bool nativeXor() override { return false; } + + void reset() { d_addClauseCalled = false; } + + unsigned int addClauseCalled() { return d_addClauseCalled; } + + unsigned getAssertionLevel() const override { return 0; } + + bool isDecision(Node) const { return false; } + + void unregisterVar(SatLiteral lit) {} + + void renewVar(SatLiteral lit, int level = -1) {} + + bool spendResource() { return false; } + + void interrupt() override {} + + SatValue solve() override { return SAT_VALUE_UNKNOWN; } + + SatValue solve(long unsigned int& resource) override + { + return SAT_VALUE_UNKNOWN; + } + + SatValue value(SatLiteral l) override { return SAT_VALUE_UNKNOWN; } + + SatValue modelValue(SatLiteral l) override { return SAT_VALUE_UNKNOWN; } + + bool properExplanation(SatLiteral lit, SatLiteral expl) const { return true; } + + bool ok() const override { return true; } + + private: + SatVariable d_nextVar; + bool d_addClauseCalled; +}; + +class TestPropWhiteCnfStream : public TestSmt +{ + protected: + void SetUp() override + { + TestSmt::SetUp(); + d_theoryEngine = d_smtEngine->getTheoryEngine(); + d_satSolver.reset(new FakeSatSolver()); + d_cnfContext.reset(new context::Context()); + d_cnfRegistrar.reset(new prop::NullRegistrar); + d_cnfStream.reset( + new CVC4::prop::CnfStream(d_satSolver.get(), + d_cnfRegistrar.get(), + d_cnfContext.get(), + &d_smtEngine->getOutputManager(), + d_smtEngine->getResourceManager())); + } + + void TearDown() override + { + d_cnfStream.reset(nullptr); + d_cnfRegistrar.reset(nullptr); + d_cnfContext.reset(nullptr); + d_satSolver.reset(nullptr); + TestSmt::TearDown(); + } + + /** The SAT solver proxy */ + std::unique_ptr d_satSolver; + /** The theory engine */ + TheoryEngine* d_theoryEngine; + /** The CNF converter in use */ + std::unique_ptr d_cnfStream; + /** The context of the CnfStream. */ + std::unique_ptr d_cnfContext; + /** The registrar used by the CnfStream. */ + std::unique_ptr d_cnfRegistrar; +}; + +/** + * [chris 5/26/2010] In the tests below, we don't attempt to delve into the + * deep structure of the CNF conversion. Firstly, we just want to make sure + * that the conversion doesn't choke on any boolean Exprs. We'll also check + * that addClause got called. We won't check that it gets called a particular + * number of times, or with what. + */ + +TEST_F(TestPropWhiteCnfStream, and) +{ + NodeManagerScope nms(d_nodeManager.get()); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::AND, a, b, c), false, false); + ASSERT_TRUE(d_satSolver->addClauseCalled()); +} + +TEST_F(TestPropWhiteCnfStream, complex_expr) +{ + NodeManagerScope nms(d_nodeManager.get()); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node d = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node e = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node f = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode( + kind::IMPLIES, + d_nodeManager->mkNode(kind::AND, a, b), + d_nodeManager->mkNode( + kind::EQUAL, + d_nodeManager->mkNode(kind::OR, c, d), + d_nodeManager->mkNode(kind::NOT, + d_nodeManager->mkNode(kind::XOR, e, f)))), + false, + false); + ASSERT_TRUE(d_satSolver->addClauseCalled()); +} + +TEST_F(TestPropWhiteCnfStream, true) +{ + NodeManagerScope nms(d_nodeManager.get()); + d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false); + ASSERT_TRUE(d_satSolver->addClauseCalled()); +} + +TEST_F(TestPropWhiteCnfStream, false) +{ + NodeManagerScope nms(d_nodeManager.get()); + d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false); + ASSERT_TRUE(d_satSolver->addClauseCalled()); +} + +TEST_F(TestPropWhiteCnfStream, iff) +{ + NodeManagerScope nms(d_nodeManager.get()); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::EQUAL, a, b), false, false); + ASSERT_TRUE(d_satSolver->addClauseCalled()); +} + +TEST_F(TestPropWhiteCnfStream, implies) +{ + NodeManagerScope nms(d_nodeManager.get()); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false); + ASSERT_TRUE(d_satSolver->addClauseCalled()); +} + +TEST_F(TestPropWhiteCnfStream, not ) +{ + NodeManagerScope nms(d_nodeManager.get()); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::NOT, a), false, false); + ASSERT_TRUE(d_satSolver->addClauseCalled()); +} + +TEST_F(TestPropWhiteCnfStream, or) +{ + NodeManagerScope nms(d_nodeManager.get()); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::OR, a, b, c), false, false); + ASSERT_TRUE(d_satSolver->addClauseCalled()); +} + +TEST_F(TestPropWhiteCnfStream, var) +{ + NodeManagerScope nms(d_nodeManager.get()); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert(a, false, false); + ASSERT_TRUE(d_satSolver->addClauseCalled()); + d_satSolver->reset(); + d_cnfStream->convertAndAssert(b, false, false); + ASSERT_TRUE(d_satSolver->addClauseCalled()); +} + +TEST_F(TestPropWhiteCnfStream, xor) +{ + NodeManagerScope nms(d_nodeManager.get()); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + d_cnfStream->convertAndAssert( + d_nodeManager->mkNode(kind::XOR, a, b), false, false); + ASSERT_TRUE(d_satSolver->addClauseCalled()); +} + +TEST_F(TestPropWhiteCnfStream, ensure_literal) +{ + NodeManagerScope nms(d_nodeManager.get()); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); + Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b); + d_cnfStream->ensureLiteral(a_and_b); + // Clauses are necessary to "literal-ize" a_and_b + ASSERT_TRUE(d_satSolver->addClauseCalled()); + ASSERT_TRUE(d_cnfStream->hasLiteral(a_and_b)); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h deleted file mode 100644 index 5200d81d8..000000000 --- a/test/unit/prop/cnf_stream_white.h +++ /dev/null @@ -1,285 +0,0 @@ -/********************* */ -/*! \file cnf_stream_white.h - ** \verbatim - ** Top contributors (to current version): - ** Christopher L. Conway, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief White box testing of CVC4::prop::CnfStream. - ** - ** White box testing of CVC4::prop::CnfStream. - **/ - -#include -/* #include */ -/* #include */ - -#include "base/check.h" -#include "context/context.h" -#include "expr/expr_manager.h" -#include "expr/node_manager.h" -#include "prop/cnf_stream.h" -#include "prop/prop_engine.h" -#include "prop/registrar.h" -#include "prop/theory_proxy.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/arith/theory_arith.h" -#include "theory/booleans/theory_bool.h" -#include "theory/builtin/theory_builtin.h" -#include "theory/theory.h" -#include "theory/theory_engine.h" - -using namespace CVC4; -using namespace CVC4::context; -using namespace CVC4::prop; -using namespace CVC4::smt; -using namespace CVC4::theory; -using namespace std; - -/* This fake class relies on the face that a MiniSat variable is just an int. */ -class FakeSatSolver : public SatSolver { - SatVariable d_nextVar; - bool d_addClauseCalled; - - public: - FakeSatSolver() : d_nextVar(0), d_addClauseCalled(false) {} - - SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) override - { - return d_nextVar++; - } - - SatVariable trueVar() override { return d_nextVar++; } - - SatVariable falseVar() override { return d_nextVar++; } - - ClauseId addClause(SatClause& c, bool lemma) override - { - d_addClauseCalled = true; - return ClauseIdUndef; - } - - ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override - { - d_addClauseCalled = true; - return ClauseIdUndef; - } - - bool nativeXor() override { return false; } - - void reset() { d_addClauseCalled = false; } - - unsigned int addClauseCalled() { return d_addClauseCalled; } - - unsigned getAssertionLevel() const override { return 0; } - - bool isDecision(Node) const { return false; } - - void unregisterVar(SatLiteral lit) {} - - void renewVar(SatLiteral lit, int level = -1) {} - - bool spendResource() { return false; } - - void interrupt() override {} - - SatValue solve() override { return SAT_VALUE_UNKNOWN; } - - SatValue solve(long unsigned int& resource) override - { - return SAT_VALUE_UNKNOWN; - } - - SatValue value(SatLiteral l) override { return SAT_VALUE_UNKNOWN; } - - SatValue modelValue(SatLiteral l) override { return SAT_VALUE_UNKNOWN; } - - bool properExplanation(SatLiteral lit, SatLiteral expl) const { return true; } - - bool ok() const override { return true; } - -}; /* class FakeSatSolver */ - -class CnfStreamWhite : public CxxTest::TestSuite { - /** The SAT solver proxy */ - FakeSatSolver* d_satSolver; - - /** The theory engine */ - TheoryEngine* d_theoryEngine; - - /** The CNF converter in use */ - CnfStream* d_cnfStream; - - /** The context of the CnfStream. */ - Context* d_cnfContext; - - /** The registrar used by the CnfStream. */ - prop::NullRegistrar* d_cnfRegistrar; - - /** The node manager */ - NodeManager* d_nodeManager; - - ExprManager* d_exprManager; - SmtScope* d_scope; - SmtEngine* d_smt; - - void setUp() override - { - d_exprManager = new ExprManager(); - d_nodeManager = NodeManager::fromExprManager(d_exprManager); - d_smt = new SmtEngine(d_nodeManager); - d_smt->d_logic.lock(); - d_scope = new SmtScope(d_smt); - - // Notice that this unit test uses the theory engine of a created SMT - // engine d_smt. We must ensure that d_smt is properly initialized via - // the following call, which constructs its underlying theory engine. - d_smt->finishInit(); - d_theoryEngine = d_smt->getTheoryEngine(); - - d_satSolver = new FakeSatSolver(); - d_cnfContext = new context::Context(); - d_cnfRegistrar = new prop::NullRegistrar; - ResourceManager* rm = d_smt->getResourceManager(); - d_cnfStream = new CVC4::prop::CnfStream(d_satSolver, - d_cnfRegistrar, - d_cnfContext, - &d_smt->getOutputManager(), - rm); - } - - void tearDown() override - { - delete d_cnfStream; - delete d_cnfContext; - delete d_cnfRegistrar; - delete d_satSolver; - delete d_scope; - delete d_smt; - delete d_exprManager; - } - - public: - /* [chris 5/26/2010] In the tests below, we don't attempt to delve into the - * deep structure of the CNF conversion. Firstly, we just want to make sure - * that the conversion doesn't choke on any boolean Exprs. We'll also check - * that addClause got called. We won't check that it gets called a particular - * number of times, or with what. - */ - - void testAnd() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::AND, a, b, c), false, false); - TS_ASSERT(d_satSolver->addClauseCalled()); - } - - void testComplexExpr() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node d = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node e = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node f = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode( - kind::IMPLIES, - d_nodeManager->mkNode(kind::AND, a, b), - d_nodeManager->mkNode( - kind::EQUAL, - d_nodeManager->mkNode(kind::OR, c, d), - d_nodeManager->mkNode(kind::NOT, - d_nodeManager->mkNode(kind::XOR, e, f)))), - false, - false); - TS_ASSERT(d_satSolver->addClauseCalled()); - } - - void testTrue() { - NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false); - TS_ASSERT(d_satSolver->addClauseCalled()); - } - - void testFalse() { - NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false); - TS_ASSERT(d_satSolver->addClauseCalled()); - } - - void testIff() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::EQUAL, a, b), false, false); - TS_ASSERT(d_satSolver->addClauseCalled()); - } - - void testImplies() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false); - TS_ASSERT(d_satSolver->addClauseCalled()); - } - - void testNot() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::NOT, a), false, false); - TS_ASSERT(d_satSolver->addClauseCalled()); - } - - void testOr() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::OR, a, b, c), false, false); - TS_ASSERT(d_satSolver->addClauseCalled()); - } - - void testVar() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(a, false, false); - TS_ASSERT(d_satSolver->addClauseCalled()); - d_satSolver->reset(); - d_cnfStream->convertAndAssert(b, false, false); - TS_ASSERT(d_satSolver->addClauseCalled()); - } - - void testXor() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( - d_nodeManager->mkNode(kind::XOR, a, b), false, false); - TS_ASSERT(d_satSolver->addClauseCalled()); - } - - void testEnsureLiteral() { - NodeManagerScope nms(d_nodeManager); - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b); - d_cnfStream->ensureLiteral(a_and_b); - // Clauses are necessary to "literal-ize" a_and_b - TS_ASSERT(d_satSolver->addClauseCalled()); - TS_ASSERT(d_cnfStream->hasLiteral(a_and_b)); - } -}; diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 937111fe4..72d8bb744 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -29,12 +29,12 @@ class TestSmt : public TestInternal void SetUp() override { d_nodeManager.reset(new NodeManager(nullptr)); - d_scope.reset(new NodeManagerScope(d_nodeManager.get())); + d_nm_scope.reset(new NodeManagerScope(d_nodeManager.get())); d_smtEngine.reset(new SmtEngine(d_nodeManager.get())); d_smtEngine->finishInit(); } - std::unique_ptr d_scope; + std::unique_ptr d_nm_scope; std::unique_ptr d_nodeManager; std::unique_ptr d_smtEngine; }; -- 2.30.2