+/********************* */
+/*! \file theory_arith_white.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** 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 "theory/theory.h"
-#include "theory/arith/theory_arith.h"
+#include <vector>
+
+#include "context/context.h"
#include "expr/node.h"
#include "expr/node_manager.h"
-#include "context/context.h"
-#include "util/rational.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 <vector>
+#include "util/rational.h"
using namespace CVC4;
using namespace CVC4::theory;
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;
- NodeManagerScope* d_scope;
+ 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;
public:
- TheoryArithWhite() : d_level(Theory::FULL_EFFORT), d_zero(0), d_one(1), debug(false) {}
-
- void setUp() {
- d_ctxt = new Context;
- d_nm = new NodeManager(d_ctxt);
- d_scope = new NodeManagerScope(d_nm);
- d_outputChannel.clear();
- d_arith = new TheoryArith(d_ctxt, d_outputChannel);
-
- preregistered = new std::set<Node>();
-
- d_booleanType = new TypeNode(d_nm->booleanType());
- d_realType = new TypeNode(d_nm->realType());
-
- }
-
- void tearDown() {
- delete d_realType;
- delete d_booleanType;
-
- delete preregistered;
-
- delete d_arith;
- d_outputChannel.clear();
- delete d_scope;
- delete d_nm;
- delete d_ctxt;
- }
+ TheoryArithWhite() : d_level(Theory::EFFORT_FULL), d_zero(0), d_one(1), debug(false) {}
- Node fakeTheoryEnginePreprocess(TNode inp){
- Node rewrite = d_arith->rewrite(inp);
+ void fakeTheoryEnginePreprocess(TNode inp){
+ Node rewrite = inp; //FIXME this needs to enforce that inp is fully rewritten already!
if(debug) cout << rewrite << inp << endl;
if(debug) cout << n.getId() << " "<< n << endl;
d_arith->preRegisterTerm(n);
}
+ }
+
+ void setUp() {
+ d_em = new ExprManager();
+ d_nm = NodeManager::fromExprManager(d_em);
+ d_smt = new SmtEngine(d_em);
+ d_smt->setOption("incremental", CVC4::SExpr(false));
+ d_ctxt = d_smt->d_context;
+ d_uctxt = d_smt->d_userContext;
+ d_scope = new SmtScope(d_smt);
+ d_outputChannel.clear();
+ d_logicInfo.lock();
+
+ // guard against duplicate statistics assertion errors
+ delete d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH];
+ delete d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH];
+ d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH] = NULL;
+ d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH] = NULL;
+
+ d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL),
+ d_logicInfo);
+
+ 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() {
+ delete d_intType;
+ delete d_realType;
+ delete d_booleanType;
+
+ delete preregistered;
- return rewrite;
+ delete d_arith;
+ 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 leq = d_nm->mkNode(LEQ, x, c);
- Node rLeq = fakeTheoryEnginePreprocess(leq);
+ Node gt = d_nm->mkNode(GT, x, c);
+ Node leq = gt.notNode();
+ fakeTheoryEnginePreprocess(leq);
- d_arith->assertFact(rLeq);
+ d_arith->assertFact(leq, true);
d_arith->check(d_level);
return dis;
}
- void testAssertEqualityEagerSplit() {
+ void testTPLt1() {
Node x = d_nm->mkVar(*d_realType);
- Node c = d_nm->mkConst<Rational>(d_zero);
-
- Node eq = d_nm->mkNode(EQUAL, x, c);
- Node expectedDisjunct = simulateSplit(x,c);
+ Node c0 = d_nm->mkConst<Rational>(d_zero);
+ Node c1 = d_nm->mkConst<Rational>(d_one);
- Node rEq = fakeTheoryEnginePreprocess(eq);
+ 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();
- d_arith->assertFact(rEq);
+ fakeTheoryEnginePreprocess(leq0);
+ fakeTheoryEnginePreprocess(leq1);
+ fakeTheoryEnginePreprocess(geq1);
+ d_arith->presolve();
+ d_arith->assertFact(lt1, true);
d_arith->check(d_level);
+ d_arith->propagate(d_level);
- TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 1u);
-
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), expectedDisjunct);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), AUG_LEMMA);
-
- }
- void testLtRewrite() {
- Node x = d_nm->mkVar(*d_realType);
- Node c = d_nm->mkConst<Rational>(d_zero);
-
- Node lt = d_nm->mkNode(LT, x, c);
- Node geq = d_nm->mkNode(GEQ, x, c);
- Node expectedRewrite = d_nm->mkNode(NOT, geq);
-
- Node rewrite = d_arith->rewrite(lt);
-
- TS_ASSERT_EQUALS(expectedRewrite, rewrite);
- }
-
- void testBasicConflict() {
- Node x = d_nm->mkVar(*d_realType);
- Node c = d_nm->mkConst<Rational>(d_zero);
-
- Node eq = d_nm->mkNode(EQUAL, x, c);
- Node lt = d_nm->mkNode(LT, x, c);
- Node expectedDisjunct = simulateSplit(x,c);
-
- Node rEq = fakeTheoryEnginePreprocess(eq);
- Node rLt = fakeTheoryEnginePreprocess(lt);
-
- d_arith->assertFact(rEq);
- d_arith->assertFact(rLt);
+ Node gt0Orlt1 = NodeBuilder<2>(OR) << gt0 << lt1;
+ Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1;
- d_arith->check(d_level);
+ 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(), 2u);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), expectedDisjunct);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), AUG_LEMMA);
+ TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), CONFLICT);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1);
- Node expectedClonflict = d_nm->mkNode(AND, rEq, rLt);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), expectedClonflict);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), PROPAGATE);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq1);
}
- void testBasicPropagate() {
- Node x = d_nm->mkVar(*d_realType);
- Node c = d_nm->mkConst<Rational>(d_zero);
-
- Node eq = d_nm->mkNode(EQUAL, x, c);
- Node lt = d_nm->mkNode(LT, x, c);
- Node expectedDisjunct = simulateSplit(x,c);
- Node rEq = fakeTheoryEnginePreprocess(eq);
- Node rLt = fakeTheoryEnginePreprocess(lt);
+ 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);
- d_arith->assertFact(rEq);
+ 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);
- TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), AUG_LEMMA);
-
-
- Node expectedProp = d_nm->mkNode(GEQ, x, c);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPOGATE);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), expectedProp);
-
- }
- 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 leq0 = d_nm->mkNode(LEQ, x, c0);
- Node leq1 = d_nm->mkNode(LEQ, x, c1);
- Node lt1 = d_nm->mkNode(LT, x, c1);
+ Node gt0Orlt1 = NodeBuilder<2>(OR) << gt0 << lt1;
+ Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1;
- Node rLeq0 = fakeTheoryEnginePreprocess(leq0);
- Node rLt1 = fakeTheoryEnginePreprocess(lt1);
- Node rLeq1 = fakeTheoryEnginePreprocess(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;
- d_arith->assertFact(rLt1);
+ TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 4u);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1);
- d_arith->check(d_level);
- d_arith->propagate(d_level);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
-#ifdef CVC4_ASSERTIONS
- TS_ASSERT_THROWS( d_arith->explain(rLeq0, d_level), AssertionException );
- TS_ASSERT_THROWS( d_arith->explain(rLt1, d_level), AssertionException );
-#endif
- d_arith->explain(rLeq1, d_level);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), PROPAGATE);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1 );
- TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPOGATE);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), EXPLANATION);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq1);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), rLt1);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(3), PROPAGATE);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(3), leq1);
}
-
- void testTPLeq0() {
+ 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 leq0 = d_nm->mkNode(LEQ, x, c0);
- Node leq1 = d_nm->mkNode(LEQ, x, c1);
- Node lt1 = d_nm->mkNode(LT, x, c1);
-
- Node rLeq0 = fakeTheoryEnginePreprocess(leq0);
- Node rLt1 = fakeTheoryEnginePreprocess(lt1);
- Node rLeq1 = fakeTheoryEnginePreprocess(leq1);
-
- d_arith->assertFact(rLeq0);
+ 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;
- d_arith->explain(rLt1, d_level);
-#ifdef CVC4_ASSERTIONS
- TS_ASSERT_THROWS( d_arith->explain(rLeq0, d_level), AssertionException );
-#endif
- d_arith->explain(rLeq1, d_level);
-
- TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 4u);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPOGATE);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPOGATE);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), EXPLANATION);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(3), EXPLANATION);
+ cout << d_outputChannel.getIthNode(0) << endl;
+ cout << d_outputChannel.getIthNode(1) << endl;
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), rLt1);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), rLeq1);
+ 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.getIthNode(2), rLeq0);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(3), rLeq0);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
+ TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
}
- void testTPLeq1() {
- Node x = d_nm->mkVar(*d_realType);
+
+ void testIntNormalForm() {
+ Node x = d_nm->mkVar(*d_intType);
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 leq0 = d_nm->mkNode(LEQ, x, c0);
- Node leq1 = d_nm->mkNode(LEQ, x, c1);
- Node lt1 = d_nm->mkNode(LT, x, c1);
- Node rLeq0 = fakeTheoryEnginePreprocess(leq0);
- Node rLt1 = fakeTheoryEnginePreprocess(lt1);
- Node rLeq1 = fakeTheoryEnginePreprocess(leq1);
+ Node geq0 = d_nm->mkNode(GEQ, x, c0);
+ Node geq1 = d_nm->mkNode(GEQ, x, c1);
+ Node geq2 = d_nm->mkNode(GEQ, x, c2);
- d_arith->assertFact(rLeq1);
+ 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);
- d_arith->check(d_level);
- d_arith->propagate(d_level);
+ TS_ASSERT_EQUALS(Rewriter::rewrite(gt0), Rewriter::rewrite(geq1));
+ TS_ASSERT_EQUALS(Rewriter::rewrite(gt1), Rewriter::rewrite(geq2));
-#ifdef CVC4_ASSERTIONS
- TS_ASSERT_THROWS( d_arith->explain(rLeq0, d_level), AssertionException );
- TS_ASSERT_THROWS( d_arith->explain(rLeq1, d_level), AssertionException );
- TS_ASSERT_THROWS( d_arith->explain(rLt1, d_level), AssertionException );
-#endif
+ Node lt0 = d_nm->mkNode(LT, x, c0);
+ Node lt1 = d_nm->mkNode(LT, x, c1);
- TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u);
+ 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()));
}
};
projects / cvc5.git / blobdiff