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
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)
--- /dev/null
+/********************* */
+/*! \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
+++ /dev/null
-/********************* */
-/*! \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));
- }
-};
projects / cvc5.git / commitdiff