From: Aina Niemetz Date: Wed, 24 Feb 2021 08:53:23 +0000 (-0800) Subject: google test: theory: Migrate theory_arith_white. (#5977) X-Git-Tag: cvc5-1.0.0~2226 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0e1039ccd0efabe9649716029f07a96e2ee8c7d9;p=cvc5.git google test: theory: Migrate theory_arith_white. (#5977) --- 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 d_nodeManager; std::unique_ptr 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 d_scope; + std::unique_ptr d_nodeManager; + std::unique_ptr 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 + +#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( + d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_ARITH]); + + d_preregistered.reset(new std::set()); + + 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 toPreregister; + + toPreregister.push_back(rewrite); + for (std::list::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::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> d_preregistered; + std::unique_ptr d_booleanType; + std::unique_ptr d_realType; + std::unique_ptr 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(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(d_zero); + Node c1 = d_nodeManager->mkConst(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(d_zero); + Node c1 = d_nodeManager->mkConst(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(d_zero); + Node c1 = d_nodeManager->mkConst(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(d_zero); + Node c1 = d_nodeManager->mkConst(d_one); + Node c2 = d_nodeManager->mkConst(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 - -#include - -#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* 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 toPreregister; - - toPreregister.push_back(rewrite); - for(std::list::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::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( - d_smt->getTheoryEngine()->d_theoryTable[THEORY_ARITH]); - - preregistered = new std::set(); - - 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(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(d_zero); - Node c1 = d_nm->mkConst(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(d_zero); - Node c1 = d_nm->mkConst(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(d_zero); - Node c1 = d_nm->mkConst(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(d_zero); - Node c1 = d_nm->mkConst(d_one); - Node c2 = d_nm->mkConst(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)); - } -};