google test: theory: Migrate theory_arith_white. (#5977)

4 files changed, 324 insertions, 333 deletions

diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index 72d8bb744..4951d07b6 100644
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -38,6 +38,21 @@ class TestSmt : public TestInternal
   std::unique_ptr<NodeManager> d_nodeManager;
   std::unique_ptr<SmtEngine> d_smtEngine;
 };
+
+class TestSmtNoFinishInit : public TestInternal
+{
+ protected:
+  void SetUp() override
+  {
+    d_nodeManager.reset(new NodeManager(nullptr));
+    d_scope.reset(new NodeManagerScope(d_nodeManager.get()));
+    d_smtEngine.reset(new SmtEngine(d_nodeManager.get()));
+  }
+
+  std::unique_ptr<NodeManagerScope> d_scope;
+  std::unique_ptr<NodeManager> d_nodeManager;
+  std::unique_ptr<SmtEngine> d_smtEngine;
+};
 }  // namespace test
 }  // namespace CVC4
 #endif
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 03968ce75..c867f15a1 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -14,7 +14,7 @@ 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)
-cvc4_add_cxx_unit_test_white(theory_arith_white theory)
+cvc4_add_unit_test_white(theory_arith_white theory)
 cvc4_add_cxx_unit_test_white(theory_bags_normal_form_white theory)
 cvc4_add_cxx_unit_test_white(theory_bags_rewriter_white theory)
 cvc4_add_cxx_unit_test_white(theory_bags_type_rules_white theory)
diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp
new file mode 100644
index 000000000..53238ca43
--- /dev/null
+++ b/test/unit/theory/theory_arith_white.cpp
@@ -0,0 +1,308 @@
+/*********************                                                        */
+/*! \file theory_arith_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Tim King, Dejan Jovanovic
+ ** 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 Whitebox tests for theory Arithmetic.
+ **/
+
+#include <vector>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "test_smt.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
+#include "theory/theory_test_utils.h"
+#include "util/rational.h"
+
+namespace CVC4 {
+
+using namespace theory;
+using namespace theory::arith;
+using namespace expr;
+using namespace context;
+using namespace kind;
+using namespace smt;
+
+namespace test {
+
+class TestTheoryWhiteArith : public TestSmtNoFinishInit
+{
+ protected:
+  void SetUp() override
+  {
+    TestSmtNoFinishInit::SetUp();
+    d_smtEngine->setOption("incremental", CVC4::SExpr(false));
+    d_smtEngine->finishInit();
+    d_context = d_smtEngine->getContext();
+    d_user_context = d_smtEngine->getUserContext();
+    d_outputChannel.clear();
+    d_logicInfo.lock();
+    d_smtEngine->getTheoryEngine()
+        ->d_theoryTable[THEORY_ARITH]
+        ->setOutputChannel(d_outputChannel);
+    d_arith = static_cast<TheoryArith*>(
+        d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_ARITH]);
+
+    d_preregistered.reset(new std::set<Node>());
+
+    d_booleanType.reset(new TypeNode(d_nodeManager->booleanType()));
+    d_realType.reset(new TypeNode(d_nodeManager->realType()));
+    d_intType.reset(new TypeNode(d_nodeManager->integerType()));
+  }
+
+  void fakeTheoryEnginePreprocess(TNode input)
+  {
+    Assert(input == Rewriter::rewrite(input));
+    Node rewrite = input;
+    if (d_debug)
+    {
+      std::cout << "input " << input << " rewrite " << rewrite << std::endl;
+    }
+
+    std::list<Node> toPreregister;
+
+    toPreregister.push_back(rewrite);
+    for (std::list<Node>::iterator i = toPreregister.begin();
+         i != toPreregister.end();
+         ++i)
+    {
+      Node n = *i;
+      d_preregistered->insert(n);
+
+      for (Node::iterator citer = n.begin(); citer != n.end(); ++citer)
+      {
+        Node c = *citer;
+        if (d_preregistered->find(c) == d_preregistered->end())
+        {
+          toPreregister.push_back(c);
+        }
+      }
+    }
+    for (std::list<Node>::reverse_iterator i = toPreregister.rbegin();
+         i != toPreregister.rend();
+         ++i)
+    {
+      Node n = *i;
+      if (d_debug)
+      {
+        std::cout << "id " << n.getId() << " " << n << std::endl;
+      }
+      d_arith->preRegisterTerm(n);
+    }
+  }
+
+  Context* d_context;
+  UserContext* d_user_context;
+  TestOutputChannel d_outputChannel;
+  LogicInfo d_logicInfo;
+  Theory::Effort d_level = Theory::EFFORT_FULL;
+  TheoryArith* d_arith;
+  std::unique_ptr<std::set<Node>> d_preregistered;
+  std::unique_ptr<TypeNode> d_booleanType;
+  std::unique_ptr<TypeNode> d_realType;
+  std::unique_ptr<TypeNode> d_intType;
+  const Rational d_zero = 0;
+  const Rational d_one = 1;
+  bool d_debug = false;
+};
+
+TEST_F(TestTheoryWhiteArith, assert)
+{
+  Node x = d_nodeManager->mkVar(*d_realType);
+  Node c = d_nodeManager->mkConst<Rational>(d_zero);
+
+  Node gt = d_nodeManager->mkNode(GT, x, c);
+  Node leq = Rewriter::rewrite(gt.notNode());
+  fakeTheoryEnginePreprocess(leq);
+
+  d_arith->assertFact(leq, true);
+
+  d_arith->check(d_level);
+
+  ASSERT_EQ(d_outputChannel.getNumCalls(), 0u);
+}
+
+TEST_F(TestTheoryWhiteArith, TPLt1)
+{
+  Node x = d_nodeManager->mkVar(*d_realType);
+  Node c0 = d_nodeManager->mkConst<Rational>(d_zero);
+  Node c1 = d_nodeManager->mkConst<Rational>(d_one);
+
+  Node gt0 = d_nodeManager->mkNode(GT, x, c0);
+  Node gt1 = d_nodeManager->mkNode(GT, x, c1);
+  Node geq1 = d_nodeManager->mkNode(GEQ, x, c1);
+  Node leq0 = Rewriter::rewrite(gt0.notNode());
+  Node leq1 = Rewriter::rewrite(gt1.notNode());
+  Node lt1 = Rewriter::rewrite(geq1.notNode());
+
+  fakeTheoryEnginePreprocess(leq0);
+  fakeTheoryEnginePreprocess(leq1);
+  fakeTheoryEnginePreprocess(geq1);
+
+  d_arith->presolve();
+  d_arith->assertFact(lt1, true);
+  d_arith->check(d_level);
+  d_arith->propagate(d_level);
+
+  Node gt0OrLt1 = NodeBuilder<2>(OR) << gt0 << lt1;
+  Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1;
+  gt0OrLt1 = Rewriter::rewrite(gt0OrLt1);
+  geq0OrLeq1 = Rewriter::rewrite(geq0OrLeq1);
+
+  std::cout << d_outputChannel.getIthNode(0) << std::endl << std::endl;
+  std::cout << d_outputChannel.getIthNode(1) << std::endl << std::endl;
+  std::cout << d_outputChannel.getIthNode(2) << std::endl << std::endl;
+
+  ASSERT_EQ(d_outputChannel.getNumCalls(), 3u);
+
+  ASSERT_EQ(d_outputChannel.getIthCallType(0), LEMMA);
+  ASSERT_TRUE(d_outputChannel.getIthNode(0) == gt0OrLt1);
+
+  ASSERT_EQ(d_outputChannel.getIthCallType(1), LEMMA);
+  ASSERT_TRUE(d_outputChannel.getIthNode(1) == geq0OrLeq1);
+
+  ASSERT_EQ(d_outputChannel.getIthCallType(2), PROPAGATE);
+  ASSERT_EQ(d_outputChannel.getIthNode(2), leq1);
+}
+
+TEST_F(TestTheoryWhiteArith, TPLeq0)
+{
+  Node x = d_nodeManager->mkVar(*d_realType);
+  Node c0 = d_nodeManager->mkConst<Rational>(d_zero);
+  Node c1 = d_nodeManager->mkConst<Rational>(d_one);
+
+  Node gt0 = d_nodeManager->mkNode(GT, x, c0);
+  Node gt1 = d_nodeManager->mkNode(GT, x, c1);
+  Node geq1 = d_nodeManager->mkNode(GEQ, x, c1);
+  Node leq0 = Rewriter::rewrite(gt0.notNode());
+  Node leq1 = Rewriter::rewrite(gt1.notNode());
+  Node lt1 = Rewriter::rewrite(geq1.notNode());
+
+  fakeTheoryEnginePreprocess(leq0);
+  fakeTheoryEnginePreprocess(leq1);
+  fakeTheoryEnginePreprocess(geq1);
+
+  d_arith->presolve();
+  d_arith->assertFact(leq0, true);
+  d_arith->check(d_level);
+  d_arith->propagate(d_level);
+
+  Node gt0OrLt1 = NodeBuilder<2>(OR) << gt0 << lt1;
+  Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1;
+  gt0OrLt1 = Rewriter::rewrite(gt0OrLt1);
+  geq0OrLeq1 = Rewriter::rewrite(geq0OrLeq1);
+
+  std::cout << d_outputChannel.getIthNode(0) << std::endl;
+  std::cout << d_outputChannel.getIthNode(1) << std::endl;
+  std::cout << d_outputChannel.getIthNode(2) << std::endl;
+  std::cout << d_outputChannel.getIthNode(3) << std::endl;
+
+  ASSERT_EQ(d_outputChannel.getNumCalls(), 4u);
+
+  ASSERT_EQ(d_outputChannel.getIthCallType(0), LEMMA);
+  ASSERT_EQ(d_outputChannel.getIthNode(0), gt0OrLt1);
+
+  ASSERT_EQ(d_outputChannel.getIthCallType(1), LEMMA);
+  ASSERT_EQ(d_outputChannel.getIthNode(1), geq0OrLeq1);
+
+  ASSERT_EQ(d_outputChannel.getIthCallType(2), PROPAGATE);
+  ASSERT_EQ(d_outputChannel.getIthNode(2), lt1);
+
+  ASSERT_EQ(d_outputChannel.getIthCallType(3), PROPAGATE);
+  ASSERT_EQ(d_outputChannel.getIthNode(3), leq1);
+}
+
+TEST_F(TestTheoryWhiteArith, TPLeq1)
+{
+  Node x = d_nodeManager->mkVar(*d_realType);
+  Node c0 = d_nodeManager->mkConst<Rational>(d_zero);
+  Node c1 = d_nodeManager->mkConst<Rational>(d_one);
+
+  Node gt0 = d_nodeManager->mkNode(GT, x, c0);
+  Node gt1 = d_nodeManager->mkNode(GT, x, c1);
+  Node geq1 = d_nodeManager->mkNode(GEQ, x, c1);
+  Node leq0 = Rewriter::rewrite(gt0.notNode());
+  Node leq1 = Rewriter::rewrite(gt1.notNode());
+  Node lt1 = Rewriter::rewrite(geq1.notNode());
+
+  fakeTheoryEnginePreprocess(leq0);
+  fakeTheoryEnginePreprocess(leq1);
+  fakeTheoryEnginePreprocess(geq1);
+
+  d_arith->presolve();
+  d_arith->assertFact(leq1, true);
+  d_arith->check(d_level);
+  d_arith->propagate(d_level);
+
+  Node gt0OrLt1 = NodeBuilder<2>(OR) << gt0 << lt1;
+  Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1;
+  gt0OrLt1 = Rewriter::rewrite(gt0OrLt1);
+  geq0OrLeq1 = Rewriter::rewrite(geq0OrLeq1);
+
+  std::cout << d_outputChannel.getIthNode(0) << std::endl;
+  std::cout << d_outputChannel.getIthNode(1) << std::endl;
+
+  ASSERT_EQ(d_outputChannel.getNumCalls(), 2u);
+
+  ASSERT_EQ(d_outputChannel.getIthCallType(0), LEMMA);
+  ASSERT_EQ(d_outputChannel.getIthNode(0), gt0OrLt1);
+
+  ASSERT_EQ(d_outputChannel.getIthCallType(1), LEMMA);
+  ASSERT_EQ(d_outputChannel.getIthNode(1), geq0OrLeq1);
+}
+
+TEST_F(TestTheoryWhiteArith, int_normal_form)
+{
+  Node x = d_nodeManager->mkVar(*d_intType);
+  Node xr = d_nodeManager->mkVar(*d_realType);
+  Node c0 = d_nodeManager->mkConst<Rational>(d_zero);
+  Node c1 = d_nodeManager->mkConst<Rational>(d_one);
+  Node c2 = d_nodeManager->mkConst<Rational>(Rational(2));
+
+  Node geq0 = d_nodeManager->mkNode(GEQ, x, c0);
+  Node geq1 = d_nodeManager->mkNode(GEQ, x, c1);
+  Node geq2 = d_nodeManager->mkNode(GEQ, x, c2);
+
+  ASSERT_EQ(Rewriter::rewrite(geq0), geq0);
+  ASSERT_EQ(Rewriter::rewrite(geq1), geq1);
+
+  Node gt0 = d_nodeManager->mkNode(GT, x, c0);
+  Node gt1 = d_nodeManager->mkNode(GT, x, c1);
+
+  ASSERT_EQ(Rewriter::rewrite(gt0), Rewriter::rewrite(geq1));
+  ASSERT_EQ(Rewriter::rewrite(gt1), Rewriter::rewrite(geq2));
+
+  Node lt0 = d_nodeManager->mkNode(LT, x, c0);
+  Node lt1 = d_nodeManager->mkNode(LT, x, c1);
+
+  ASSERT_EQ(Rewriter::rewrite(lt0), Rewriter::rewrite(geq0.notNode()));
+  ASSERT_EQ(Rewriter::rewrite(lt1), Rewriter::rewrite(geq1.notNode()));
+
+  Node leq0 = d_nodeManager->mkNode(LEQ, x, c0);
+  Node leq1 = d_nodeManager->mkNode(LEQ, x, c1);
+
+  ASSERT_EQ(Rewriter::rewrite(leq0), Rewriter::rewrite(geq1.notNode()));
+  ASSERT_EQ(Rewriter::rewrite(leq1), Rewriter::rewrite(geq2.notNode()));
+
+  // (abs x) --> (abs x)
+  Node absX = d_nodeManager->mkNode(ABS, x);
+  ASSERT_EQ(Rewriter::rewrite(absX), absX);
+
+  // (exp (+ 2 + x)) --> (* (exp x) (exp 1) (exp 1))
+  Node t =
+      d_nodeManager->mkNode(EXPONENTIAL, d_nodeManager->mkNode(PLUS, c2, xr))
+          .eqNode(c0);
+  ASSERT_EQ(Rewriter::rewrite(Rewriter::rewrite(t)), Rewriter::rewrite(t));
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
deleted file mode 100644
index 3475b1dc8..000000000
--- a/test/unit/theory/theory_arith_white.h
+++ /dev/null
@@ -1,332 +0,0 @@
-/*********************                                                        */
-/*! \file theory_arith_white.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Andres Noetzli, 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <vector>
-
-#include "context/context.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/theory.h"
-#include "theory/theory_engine.h"
-#include "theory/theory_test_utils.h"
-#include "util/rational.h"
-
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
-using namespace CVC4::expr;
-using namespace CVC4::context;
-using namespace CVC4::kind;
-using namespace CVC4::smt;
-
-using namespace std;
-
-class TheoryArithWhite : public CxxTest::TestSuite {
-
-  Context* d_ctxt;
-  UserContext* d_uctxt;
-  ExprManager* d_em;
-  NodeManager* d_nm;
-  SmtScope* d_scope;
-  SmtEngine* d_smt;
-
-  TestOutputChannel d_outputChannel;
-  LogicInfo d_logicInfo;
-  Theory::Effort d_level;
-
-  TheoryArith* d_arith;
-
-  TypeNode* d_booleanType;
-  TypeNode* d_realType;
-  TypeNode* d_intType;
-
-  const Rational d_zero;
-  const Rational d_one;
-
-  std::set<Node>* preregistered;
-
-  bool debug;
-
-public:
-
-  TheoryArithWhite() : d_level(Theory::EFFORT_FULL), d_zero(0), d_one(1), debug(false) {}
-
-  void fakeTheoryEnginePreprocess(TNode inp){
-    Node rewrite = inp; //FIXME this needs to enforce that inp is fully rewritten already!
-
-    if(debug) cout << rewrite << inp << endl;
-
-    std::list<Node> toPreregister;
-
-    toPreregister.push_back(rewrite);
-    for(std::list<Node>::iterator i = toPreregister.begin(); i != toPreregister.end(); ++i){
-      Node n = *i;
-      preregistered->insert(n);
-
-      for(Node::iterator citer = n.begin(); citer != n.end(); ++citer){
-        Node c = *citer;
-        if(preregistered->find(c) == preregistered->end()){
-          toPreregister.push_back(c);
-        }
-      }
-    }
-    for(std::list<Node>::reverse_iterator i = toPreregister.rbegin(); i != toPreregister.rend(); ++i){
-      Node n = *i;
-      if(debug) cout << n.getId() << " "<< n << endl;
-      d_arith->preRegisterTerm(n);
-    }
-  }
-
-  void setUp() override
-  {
-    d_em = new ExprManager();
-    d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_nm);
-    d_smt->setOption("incremental", CVC4::SExpr(false));
-    d_ctxt = d_smt->getContext();
-    d_uctxt = d_smt->getUserContext();
-    d_scope = new SmtScope(d_smt);
-    d_outputChannel.clear();
-    d_logicInfo.lock();
-
-    // 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_smt->getTheoryEngine()->d_theoryTable[THEORY_ARITH]->setOutputChannel(
-        d_outputChannel);
-    d_arith = static_cast<TheoryArith*>(
-        d_smt->getTheoryEngine()->d_theoryTable[THEORY_ARITH]);
-
-    preregistered = new std::set<Node>();
-
-    d_booleanType = new TypeNode(d_nm->booleanType());
-    d_realType = new TypeNode(d_nm->realType());
-    d_intType = new TypeNode(d_nm->integerType());
-
-  }
-
-  void tearDown() override
-  {
-    delete d_intType;
-    delete d_realType;
-    delete d_booleanType;
-
-    delete preregistered;
-
-    d_outputChannel.clear();
-    delete d_scope;
-    delete d_smt;
-    delete d_em;
-  }
-
-  void testAssert() {
-    Node x = d_nm->mkVar(*d_realType);
-    Node c = d_nm->mkConst<Rational>(d_zero);
-
-    Node gt = d_nm->mkNode(GT, x, c);
-    Node leq = gt.notNode();
-    fakeTheoryEnginePreprocess(leq);
-
-    d_arith->assertFact(leq, true);
-
-    d_arith->check(d_level);
-
-    TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u);
-  }
-
-  Node simulateSplit(TNode l, TNode r){
-    Node eq = d_nm->mkNode(EQUAL, l, r);
-    Node lt = d_nm->mkNode(LT, l, r);
-    Node gt = d_nm->mkNode(GT, l, r);
-
-    Node dis = d_nm->mkNode(OR, eq, lt, gt);
-    return dis;
-  }
-
-  void testTPLt1() {
-    Node x = d_nm->mkVar(*d_realType);
-    Node c0 = d_nm->mkConst<Rational>(d_zero);
-    Node c1 = d_nm->mkConst<Rational>(d_one);
-
-    Node gt0 = d_nm->mkNode(GT, x, c0);
-    Node gt1 = d_nm->mkNode(GT, x, c1);
-    Node geq1 = d_nm->mkNode(GEQ, x, c1);
-    Node leq0 = gt0.notNode();
-    Node leq1 = gt1.notNode();
-    Node lt1 = geq1.notNode();
-
-    fakeTheoryEnginePreprocess(leq0);
-    fakeTheoryEnginePreprocess(leq1);
-    fakeTheoryEnginePreprocess(geq1);
-
-    d_arith->presolve();
-    d_arith->assertFact(lt1, true);
-    d_arith->check(d_level);
-    d_arith->propagate(d_level);
-
-
-    Node gt0Orlt1  = NodeBuilder<2>(OR) << gt0 << lt1;
-    Node geq0OrLeq1  = NodeBuilder<2>(OR) << geq1 << leq1;
-
-    cout << d_outputChannel.getIthNode(0) << endl << endl;
-    cout << d_outputChannel.getIthNode(1) << endl << endl;
-    cout << d_outputChannel.getIthNode(2) << endl << endl;
-
-    TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
-
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1);
-
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
-
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), PROPAGATE);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq1);
-  }
-
-
-  void testTPLeq0() {
-    Node x = d_nm->mkVar(*d_realType);
-    Node c0 = d_nm->mkConst<Rational>(d_zero);
-    Node c1 = d_nm->mkConst<Rational>(d_one);
-
-    Node gt0 = d_nm->mkNode(GT, x, c0);
-    Node gt1 = d_nm->mkNode(GT, x, c1);
-    Node geq1 = d_nm->mkNode(GEQ, x, c1);
-    Node leq0 = gt0.notNode();
-    Node leq1 = gt1.notNode();
-    Node lt1 = geq1.notNode();
-
-    fakeTheoryEnginePreprocess(leq0);
-    fakeTheoryEnginePreprocess(leq1);
-    fakeTheoryEnginePreprocess(geq1);
-
-    d_arith->presolve();
-    d_arith->assertFact(leq0, true);
-    d_arith->check(d_level);
-    d_arith->propagate(d_level);
-
-    Node gt0Orlt1  = NodeBuilder<2>(OR) << gt0 << lt1;
-    Node geq0OrLeq1  = NodeBuilder<2>(OR) << geq1 << leq1;
-
-    cout << d_outputChannel.getIthNode(0) << endl;
-    cout << d_outputChannel.getIthNode(1) << endl;
-    cout << d_outputChannel.getIthNode(2) << endl;
-    cout << d_outputChannel.getIthNode(3) << endl;
-
-    TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 4u);
-
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1);
-
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
-
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), PROPAGATE);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1 );
-
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(3), PROPAGATE);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(3), leq1);
-  }
-
-  void testTPLeq1() {
-    Node x = d_nm->mkVar(*d_realType);
-    Node c0 = d_nm->mkConst<Rational>(d_zero);
-    Node c1 = d_nm->mkConst<Rational>(d_one);
-
-    Node gt0 = d_nm->mkNode(GT, x, c0);
-    Node gt1 = d_nm->mkNode(GT, x, c1);
-    Node geq1 = d_nm->mkNode(GEQ, x, c1);
-    Node leq0 = gt0.notNode();
-    Node leq1 = gt1.notNode();
-    Node lt1 = geq1.notNode();
-
-    fakeTheoryEnginePreprocess(leq0);
-    fakeTheoryEnginePreprocess(leq1);
-    fakeTheoryEnginePreprocess(geq1);
-
-    d_arith->presolve();
-    d_arith->assertFact(leq1, true);
-    d_arith->check(d_level);
-    d_arith->propagate(d_level);
-
-    Node gt0Orlt1  = NodeBuilder<2>(OR) << gt0 << lt1;
-    Node geq0OrLeq1  = NodeBuilder<2>(OR) << geq1 << leq1;
-
-    cout << d_outputChannel.getIthNode(0) << endl;
-    cout << d_outputChannel.getIthNode(1) << endl;
-
-    TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
-
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1);
-
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
-  }
-
-  void testIntNormalForm() {
-    Node x = d_nm->mkVar(*d_intType);
-    Node xr = d_nm->mkVar(*d_realType);
-    Node c0 = d_nm->mkConst<Rational>(d_zero);
-    Node c1 = d_nm->mkConst<Rational>(d_one);
-    Node c2 = d_nm->mkConst<Rational>(Rational(2));
-
-
-    Node geq0 = d_nm->mkNode(GEQ, x, c0);
-    Node geq1 = d_nm->mkNode(GEQ, x, c1);
-    Node geq2 = d_nm->mkNode(GEQ, x, c2);
-
-    TS_ASSERT_EQUALS(Rewriter::rewrite(geq0), geq0);
-    TS_ASSERT_EQUALS(Rewriter::rewrite(geq1), geq1);
-
-    Node gt0 = d_nm->mkNode(GT, x, c0);
-    Node gt1 = d_nm->mkNode(GT, x, c1);
-
-    TS_ASSERT_EQUALS(Rewriter::rewrite(gt0), Rewriter::rewrite(geq1));
-    TS_ASSERT_EQUALS(Rewriter::rewrite(gt1), Rewriter::rewrite(geq2));
-
-    Node lt0 = d_nm->mkNode(LT, x, c0);
-    Node lt1 = d_nm->mkNode(LT, x, c1);
-
-    TS_ASSERT_EQUALS(Rewriter::rewrite(lt0), Rewriter::rewrite(geq0.notNode()));
-    TS_ASSERT_EQUALS(Rewriter::rewrite(lt1), Rewriter::rewrite(geq1.notNode()));
-
-    Node leq0 = d_nm->mkNode(LEQ, x, c0);
-    Node leq1 = d_nm->mkNode(LEQ, x, c1);
-
-    TS_ASSERT_EQUALS(Rewriter::rewrite(leq0), Rewriter::rewrite(geq1.notNode()));
-    TS_ASSERT_EQUALS(Rewriter::rewrite(leq1), Rewriter::rewrite(geq2.notNode()));
-
-    // (abs x) --> (abs x)
-    Node absX = d_nm->mkNode(ABS, x);
-    TS_ASSERT_EQUALS(Rewriter::rewrite(absX), absX);
-
-    // (exp (+ 2 + x)) --> (* (exp x) (exp 1) (exp 1))
-    Node t = d_nm->mkNode(EXPONENTIAL, d_nm->mkNode(PLUS, c2, xr)).eqNode(c0);
-    TS_ASSERT_EQUALS(Rewriter::rewrite(Rewriter::rewrite(t)),
-                     Rewriter::rewrite(t));
-  }
-};