/********************* */
/*! \file theory_arith_white.h
** \verbatim
- ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): barrett, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** 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
**
** \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) {}
+ 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!
}
void setUp() {
- d_ctxt = new Context;
- d_nm = new NodeManager(d_ctxt);
- d_scope = new NodeManagerScope(d_nm);
+ 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_arith = new TheoryArith(0, d_ctxt, d_outputChannel);
+ 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 d_arith;
d_outputChannel.clear();
delete d_scope;
- delete d_nm;
- delete d_ctxt;
+ 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 gt = d_nm->mkNode(GT, x, c);
+ Node leq = gt.notNode();
fakeTheoryEnginePreprocess(leq);
- d_arith->assertFact(leq);
+ d_arith->assertFact(leq, true);
d_arith->check(d_level);
return dis;
}
-// 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(NOT, d_nm->mkNode(GEQ, x, c));
-// Node expectedDisjunct = simulateSplit(x,c);
-//
-// fakeTheoryEnginePreprocess(eq);
-// fakeTheoryEnginePreprocess(lt);
-//
-// d_arith->assertFact(eq);
-// d_arith->assertFact(lt);
-//
-// d_arith->check(d_level);
-//
-// 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.getIthCallType(1), CONFLICT);
-//
-// Node expectedClonflict = d_nm->mkNode(AND, eq, lt);
-//
-// TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), expectedClonflict);
-// }
-
-// 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(NOT, d_nm->mkNode(GEQ, x, c));
-// Node expectedDisjunct = simulateSplit(x,c);
-//
-// fakeTheoryEnginePreprocess(eq);
-// fakeTheoryEnginePreprocess(lt);
-//
-// d_arith->assertFact(eq);
-//
-//
-// 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), PROPAGATE);
-// 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 gt0 = d_nm->mkNode(GT, x, c0);
+ Node gt1 = d_nm->mkNode(GT, x, c1);
Node geq1 = d_nm->mkNode(GEQ, x, c1);
- Node lt1 = d_nm->mkNode(NOT, geq1);
+ Node leq0 = gt0.notNode();
+ Node leq1 = gt1.notNode();
+ Node lt1 = geq1.notNode();
fakeTheoryEnginePreprocess(leq0);
fakeTheoryEnginePreprocess(leq1);
fakeTheoryEnginePreprocess(geq1);
- d_arith->assertFact(lt1);
-
-
+ d_arith->presolve();
+ d_arith->assertFact(lt1, true);
d_arith->check(d_level);
d_arith->propagate(d_level);
-#ifdef CVC4_ASSERTIONS
- TS_ASSERT_THROWS( d_arith->explain(leq0, d_level), AssertionException );
- TS_ASSERT_THROWS( d_arith->explain(lt1, d_level), AssertionException );
-#endif
- d_arith->explain(leq1, d_level);
- TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPAGATE);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), EXPLANATION);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq1);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1);
+ 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);
}
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 gt0 = d_nm->mkNode(GT, x, c0);
+ Node gt1 = d_nm->mkNode(GT, x, c1);
Node geq1 = d_nm->mkNode(GEQ, x, c1);
- Node lt1 = d_nm->mkNode(NOT, geq1);
+ Node leq0 = gt0.notNode();
+ Node leq1 = gt1.notNode();
+ Node lt1 = geq1.notNode();
fakeTheoryEnginePreprocess(leq0);
fakeTheoryEnginePreprocess(leq1);
fakeTheoryEnginePreprocess(geq1);
- d_arith->assertFact(leq0);
-
-
+ 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;
- d_arith->explain(lt1, d_level);
-#ifdef CVC4_ASSERTIONS
- TS_ASSERT_THROWS( d_arith->explain(leq0, d_level), AssertionException );
-#endif
- d_arith->explain(leq1, d_level);
+ 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), PROPAGATE);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPAGATE);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), EXPLANATION);
- TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(3), EXPLANATION);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq1);
+ 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.getIthNode(2), leq0);
- TS_ASSERT_EQUALS(d_outputChannel.getIthNode(3), leq0);
+ 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 leq0 = d_nm->mkNode(LEQ, x, c0);
- Node leq1 = d_nm->mkNode(LEQ, x, c1);
+ 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 lt1 = d_nm->mkNode(NOT, geq1);
+ Node leq0 = gt0.notNode();
+ Node leq1 = gt1.notNode();
+ Node lt1 = geq1.notNode();
fakeTheoryEnginePreprocess(leq0);
fakeTheoryEnginePreprocess(leq1);
fakeTheoryEnginePreprocess(geq1);
- d_arith->assertFact(leq1);
-
-
+ d_arith->presolve();
+ d_arith->assertFact(leq1, true);
d_arith->check(d_level);
d_arith->propagate(d_level);
-#ifdef CVC4_ASSERTIONS
- TS_ASSERT_THROWS( d_arith->explain(leq0, d_level), AssertionException );
- TS_ASSERT_THROWS( d_arith->explain(leq1, d_level), AssertionException );
- TS_ASSERT_THROWS( d_arith->explain(lt1, d_level), AssertionException );
-#endif
+ Node gt0Orlt1 = NodeBuilder<2>(OR) << gt0 << lt1;
+ Node geq0OrLeq1 = NodeBuilder<2>(OR) << geq1 << leq1;
- TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u);
+ 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 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()));
}
};
projects / cvc5.git / blobdiff