google test: theory: Migrate evaluator_white. (#5972)

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 6c4e627655e4ea8ee947755e9da72f158968e00b..03968ce75568d1688073d844eb147e555a54f89d 100644 (file)
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -10,7 +10,7 @@
 ##
 cvc4_add_unit_test_black(regexp_operation_black theory)
 cvc4_add_cxx_unit_test_black(theory_black theory)
-cvc4_add_cxx_unit_test_white(evaluator_white theory)
+cvc4_add_unit_test_white(evaluator_white theory)
 cvc4_add_cxx_unit_test_white(logic_info_white theory)
 cvc4_add_cxx_unit_test_white(sequences_rewriter_white theory)
 cvc4_add_unit_test_white(strings_rewriter_white theory)

diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp
new file mode 100644 (file)
index 0000000..039a5f1
--- /dev/null
+++ b/test/unit/theory/evaluator_white.cpp
@@ -0,0 +1,161 @@
+/*********************                                                        */
+/*! \file evaluator_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include <vector>
+
+#include "expr/node.h"
+#include "test_smt.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/evaluator.h"
+#include "theory/rewriter.h"
+#include "theory/theory_test_utils.h"
+#include "util/rational.h"
+
+namespace CVC4 {
+
+using namespace smt;
+using namespace theory;
+
+namespace test {
+
+class TestTheoryWhiteEvaluator : public TestSmt
+{
+};
+
+TEST_F(TestTheoryWhiteEvaluator, simple)
+{
+  TypeNode bv64Type = d_nodeManager->mkBitVectorType(64);
+
+  Node w = d_nodeManager->mkVar("w", bv64Type);
+  Node x = d_nodeManager->mkVar("x", bv64Type);
+  Node y = d_nodeManager->mkVar("y", bv64Type);
+  Node z = d_nodeManager->mkVar("z", bv64Type);
+
+  Node zero = d_nodeManager->mkConst(BitVector(64, (unsigned int)0));
+  Node one = d_nodeManager->mkConst(BitVector(64, (unsigned int)1));
+  Node c1 = d_nodeManager->mkConst(BitVector(
+      64,
+      (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
+  Node c2 = d_nodeManager->mkConst(BitVector(
+      64,
+      (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
+
+  Node t = d_nodeManager->mkNode(
+      kind::ITE, d_nodeManager->mkNode(kind::EQUAL, y, one), x, w);
+
+  std::vector<Node> args = {w, x, y, z};
+  std::vector<Node> vals = {c1, zero, one, c1};
+
+  Evaluator eval;
+  Node r = eval.eval(t, args, vals);
+  ASSERT_EQ(r,
+            Rewriter::rewrite(t.substitute(
+                args.begin(), args.end(), vals.begin(), vals.end())));
+}
+
+TEST_F(TestTheoryWhiteEvaluator, loop)
+{
+  TypeNode bv64Type = d_nodeManager->mkBitVectorType(64);
+
+  Node w = d_nodeManager->mkBoundVar(bv64Type);
+  Node x = d_nodeManager->mkVar("x", bv64Type);
+
+  Node zero = d_nodeManager->mkConst(BitVector(1, (unsigned int)0));
+  Node one = d_nodeManager->mkConst(BitVector(64, (unsigned int)1));
+  Node c = d_nodeManager->mkConst(BitVector(
+      64,
+      (unsigned int)0b0001111000010111110000110110001101011110111001101100000101010100));
+
+  Node largs = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, w);
+  Node lbody = d_nodeManager->mkNode(
+      kind::BITVECTOR_CONCAT, bv::utils::mkExtract(w, 62, 0), zero);
+  Node lambda = d_nodeManager->mkNode(kind::LAMBDA, largs, lbody);
+  Node t =
+      d_nodeManager->mkNode(kind::BITVECTOR_AND,
+                            d_nodeManager->mkNode(kind::APPLY_UF, lambda, one),
+                            d_nodeManager->mkNode(kind::APPLY_UF, lambda, x));
+
+  std::vector<Node> args = {x};
+  std::vector<Node> vals = {c};
+  Evaluator eval;
+  Node r = eval.eval(t, args, vals);
+  ASSERT_EQ(r,
+            Rewriter::rewrite(t.substitute(
+                args.begin(), args.end(), vals.begin(), vals.end())));
+}
+
+TEST_F(TestTheoryWhiteEvaluator, strIdOf)
+{
+  Node a = d_nodeManager->mkConst(String("A"));
+  Node empty = d_nodeManager->mkConst(String(""));
+  Node one = d_nodeManager->mkConst(Rational(1));
+  Node two = d_nodeManager->mkConst(Rational(2));
+
+  std::vector<Node> args;
+  std::vector<Node> vals;
+  Evaluator eval;
+
+  {
+    Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, empty, one);
+    Node r = eval.eval(n, args, vals);
+    ASSERT_EQ(r, Rewriter::rewrite(n));
+  }
+
+  {
+    Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, a, one);
+    Node r = eval.eval(n, args, vals);
+    ASSERT_EQ(r, Rewriter::rewrite(n));
+  }
+
+  {
+    Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, empty, two);
+    Node r = eval.eval(n, args, vals);
+    ASSERT_EQ(r, Rewriter::rewrite(n));
+  }
+
+  {
+    Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, a, two);
+    Node r = eval.eval(n, args, vals);
+    ASSERT_EQ(r, Rewriter::rewrite(n));
+  }
+}
+
+TEST_F(TestTheoryWhiteEvaluator, code)
+{
+  Node a = d_nodeManager->mkConst(String("A"));
+  Node empty = d_nodeManager->mkConst(String(""));
+
+  std::vector<Node> args;
+  std::vector<Node> vals;
+  Evaluator eval;
+
+  // (str.code "A") ---> 65
+  {
+    Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, a);
+    Node r = eval.eval(n, args, vals);
+    ASSERT_EQ(r, d_nodeManager->mkConst(Rational(65)));
+  }
+
+  // (str.code "") ---> -1
+  {
+    Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, empty);
+    Node r = eval.eval(n, args, vals);
+    ASSERT_EQ(r, d_nodeManager->mkConst(Rational(-1)));
+  }
+}
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h
deleted file mode 100644 (file)
index 1f33d0f..0000000
--- a/test/unit/theory/evaluator_white.h
+++ /dev/null
@@ -1,184 +0,0 @@
-/*********************                                                        */
-/*! \file evaluator_white.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli, Andrew Reynolds
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include <cxxtest/TestSuite.h>
-#include <vector>
-
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "theory/evaluator.h"
-#include "theory/rewriter.h"
-#include "theory/theory_test_utils.h"
-#include "util/rational.h"
-
-using namespace CVC4;
-using namespace CVC4::smt;
-using namespace CVC4::theory;
-
-using namespace std;
-
-class TheoryEvaluatorWhite : public CxxTest::TestSuite
-{
-  ExprManager *d_em;
-  NodeManager *d_nm;
-  SmtEngine *d_smt;
-  SmtScope *d_scope;
-
- public:
-  TheoryEvaluatorWhite() {}
-
-  void setUp() override
-  {
-    Options opts;
-    opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
-    d_em = new ExprManager;
-    d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_nm, &opts);
-    d_scope = new SmtScope(d_smt);
-    d_smt->finishInit();
-  }
-
-  void tearDown() override
-  {
-    delete d_scope;
-    delete d_smt;
-    delete d_em;
-  }
-
-  void testSimple()
-  {
-    TypeNode bv64Type = d_nm->mkBitVectorType(64);
-
-    Node w = d_nm->mkVar("w", bv64Type);
-    Node x = d_nm->mkVar("x", bv64Type);
-    Node y = d_nm->mkVar("y", bv64Type);
-    Node z = d_nm->mkVar("z", bv64Type);
-
-    Node zero = d_nm->mkConst(BitVector(64, (unsigned int)0));
-    Node one = d_nm->mkConst(BitVector(64, (unsigned int)1));
-    Node c1 = d_nm->mkConst(BitVector(
-        64,
-        (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
-    Node c2 = d_nm->mkConst(BitVector(
-        64,
-        (unsigned int)0b0000000100000101001110111001101000101110011101011011110011100111));
-
-    Node t = d_nm->mkNode(kind::ITE, d_nm->mkNode(kind::EQUAL, y, one), x, w);
-
-    std::vector<Node> args = {w, x, y, z};
-    std::vector<Node> vals = {c1, zero, one, c1};
-
-    Evaluator eval;
-    Node r = eval.eval(t, args, vals);
-    TS_ASSERT_EQUALS(r,
-                     Rewriter::rewrite(t.substitute(
-                         args.begin(), args.end(), vals.begin(), vals.end())));
-  }
-
-  void testLoop()
-  {
-    TypeNode bv64Type = d_nm->mkBitVectorType(64);
-
-    Node w = d_nm->mkBoundVar(bv64Type);
-    Node x = d_nm->mkVar("x", bv64Type);
-
-    Node zero = d_nm->mkConst(BitVector(1, (unsigned int)0));
-    Node one = d_nm->mkConst(BitVector(64, (unsigned int)1));
-    Node c = d_nm->mkConst(BitVector(
-        64,
-        (unsigned int)0b0001111000010111110000110110001101011110111001101100000101010100));
-
-    Node largs = d_nm->mkNode(kind::BOUND_VAR_LIST, w);
-    Node lbody = d_nm->mkNode(
-        kind::BITVECTOR_CONCAT, bv::utils::mkExtract(w, 62, 0), zero);
-    Node lambda = d_nm->mkNode(kind::LAMBDA, largs, lbody);
-    Node t = d_nm->mkNode(kind::BITVECTOR_AND,
-                          d_nm->mkNode(kind::APPLY_UF, lambda, one),
-                          d_nm->mkNode(kind::APPLY_UF, lambda, x));
-
-    std::vector<Node> args = {x};
-    std::vector<Node> vals = {c};
-    Evaluator eval;
-    Node r = eval.eval(t, args, vals);
-    TS_ASSERT_EQUALS(r,
-                     Rewriter::rewrite(t.substitute(
-                         args.begin(), args.end(), vals.begin(), vals.end())));
-  }
-
-  void testStrIdOf()
-  {
-    Node a = d_nm->mkConst(String("A"));
-    Node empty = d_nm->mkConst(String(""));
-    Node one = d_nm->mkConst(Rational(1));
-    Node two = d_nm->mkConst(Rational(2));
-
-    std::vector<Node> args;
-    std::vector<Node> vals;
-    Evaluator eval;
-
-    {
-      Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, empty, one);
-      Node r = eval.eval(n, args, vals);
-      TS_ASSERT_EQUALS(r, Rewriter::rewrite(n));
-    }
-
-    {
-      Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, a, one);
-      Node r = eval.eval(n, args, vals);
-      TS_ASSERT_EQUALS(r, Rewriter::rewrite(n));
-    }
-
-    {
-      Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, empty, two);
-      Node r = eval.eval(n, args, vals);
-      TS_ASSERT_EQUALS(r, Rewriter::rewrite(n));
-    }
-
-    {
-      Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, a, two);
-      Node r = eval.eval(n, args, vals);
-      TS_ASSERT_EQUALS(r, Rewriter::rewrite(n));
-    }
-  }
-
-  void testCode()
-  {
-    Node a = d_nm->mkConst(String("A"));
-    Node empty = d_nm->mkConst(String(""));
-
-    std::vector<Node> args;
-    std::vector<Node> vals;
-    Evaluator eval;
-
-    // (str.code "A") ---> 65
-    {
-      Node n = d_nm->mkNode(kind::STRING_TO_CODE, a);
-      Node r = eval.eval(n, args, vals);
-      TS_ASSERT_EQUALS(r, d_nm->mkConst(Rational(65)));
-    }
-
-    // (str.code "") ---> -1
-    {
-      Node n = d_nm->mkNode(kind::STRING_TO_CODE, empty);
-      Node r = eval.eval(n, args, vals);
-      TS_ASSERT_EQUALS(r, d_nm->mkConst(Rational(-1)));
-    }
-  }
-};