google test: prop: Migrate cnf_stream_white. (#5971)

3 files changed, 274 insertions, 286 deletions

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<FakeSatSolver> d_satSolver;
+  /** The theory engine */
+  TheoryEngine* d_theoryEngine;
+  /** The CNF converter in use */
+  std::unique_ptr<CnfStream> d_cnfStream;
+  /** The context of the CnfStream. */
+  std::unique_ptr<Context> d_cnfContext;
+  /** The registrar used by the CnfStream. */
+  std::unique_ptr<prop::NullRegistrar> 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 <cxxtest/TestSuite.h>
-/* #include <gmock/gmock.h> */
-/* #include <gtest/gtest.h> */
-
-#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));
-  }
-};