1 /********************* */
2 /*! \file theory_arith_white.h
4 ** Original author: Tim King
5 ** Major contributors: Morgan Deters
6 ** Minor contributors (to current version): Dejan Jovanovic
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
19 #include <cxxtest/TestSuite.h>
21 #include "theory/theory.h"
22 #include "theory/theory_engine.h"
23 #include "theory/arith/theory_arith.h"
24 #include "theory/quantifiers_engine.h"
25 #include "expr/node.h"
26 #include "expr/node_manager.h"
27 #include "context/context.h"
28 #include "util/rational.h"
29 #include "smt/smt_engine.h"
30 #include "smt/smt_engine_scope.h"
32 #include "theory/theory_test_utils.h"
37 using namespace CVC4::theory
;
38 using namespace CVC4::theory::arith
;
39 using namespace CVC4::expr
;
40 using namespace CVC4::context
;
41 using namespace CVC4::kind
;
42 using namespace CVC4::smt
;
46 class TheoryArithWhite
: public CxxTest::TestSuite
{
55 TestOutputChannel d_outputChannel
;
56 LogicInfo d_logicInfo
;
57 Theory::Effort d_level
;
61 TypeNode
* d_booleanType
;
65 const Rational d_zero
;
68 std::set
<Node
>* preregistered
;
74 TheoryArithWhite() : d_level(Theory::EFFORT_FULL
), d_zero(0), d_one(1), debug(false) {}
76 void fakeTheoryEnginePreprocess(TNode inp
){
77 Node rewrite
= inp
; //FIXME this needs to enforce that inp is fully rewritten already!
79 if(debug
) cout
<< rewrite
<< inp
<< endl
;
81 std::list
<Node
> toPreregister
;
83 toPreregister
.push_back(rewrite
);
84 for(std::list
<Node
>::iterator i
= toPreregister
.begin(); i
!= toPreregister
.end(); ++i
){
86 preregistered
->insert(n
);
88 for(Node::iterator citer
= n
.begin(); citer
!= n
.end(); ++citer
){
90 if(preregistered
->find(c
) == preregistered
->end()){
91 toPreregister
.push_back(c
);
95 for(std::list
<Node
>::reverse_iterator i
= toPreregister
.rbegin(); i
!= toPreregister
.rend(); ++i
){
97 if(debug
) cout
<< n
.getId() << " "<< n
<< endl
;
98 d_arith
->preRegisterTerm(n
);
103 d_em
= new ExprManager();
104 d_nm
= NodeManager::fromExprManager(d_em
);
105 d_smt
= new SmtEngine(d_em
);
106 d_ctxt
= d_smt
->d_context
;
107 d_uctxt
= d_smt
->d_userContext
;
108 d_scope
= new SmtScope(d_smt
);
109 d_outputChannel
.clear();
112 // guard against duplicate statistics assertion errors
113 delete d_smt
->d_theoryEngine
->d_theoryTable
[THEORY_ARITH
];
114 delete d_smt
->d_theoryEngine
->d_theoryOut
[THEORY_ARITH
];
115 d_smt
->d_theoryEngine
->d_theoryTable
[THEORY_ARITH
] = NULL
;
116 d_smt
->d_theoryEngine
->d_theoryOut
[THEORY_ARITH
] = NULL
;
118 d_arith
= new TheoryArith(d_ctxt
, d_uctxt
, d_outputChannel
, Valuation(NULL
), d_logicInfo
);
120 preregistered
= new std::set
<Node
>();
122 d_booleanType
= new TypeNode(d_nm
->booleanType());
123 d_realType
= new TypeNode(d_nm
->realType());
124 d_intType
= new TypeNode(d_nm
->integerType());
131 delete d_booleanType
;
133 delete preregistered
;
136 d_outputChannel
.clear();
143 Node x
= d_nm
->mkVar(*d_realType
);
144 Node c
= d_nm
->mkConst
<Rational
>(d_zero
);
146 Node gt
= d_nm
->mkNode(GT
, x
, c
);
147 Node leq
= gt
.notNode();
148 fakeTheoryEnginePreprocess(leq
);
150 d_arith
->assertFact(leq
, true);
152 d_arith
->check(d_level
);
154 TS_ASSERT_EQUALS(d_outputChannel
.getNumCalls(), 0u);
157 Node
simulateSplit(TNode l
, TNode r
){
158 Node eq
= d_nm
->mkNode(EQUAL
, l
, r
);
159 Node lt
= d_nm
->mkNode(LT
, l
, r
);
160 Node gt
= d_nm
->mkNode(GT
, l
, r
);
162 Node dis
= d_nm
->mkNode(OR
, eq
, lt
, gt
);
167 Node x
= d_nm
->mkVar(*d_realType
);
168 Node c0
= d_nm
->mkConst
<Rational
>(d_zero
);
169 Node c1
= d_nm
->mkConst
<Rational
>(d_one
);
171 Node gt0
= d_nm
->mkNode(GT
, x
, c0
);
172 Node gt1
= d_nm
->mkNode(GT
, x
, c1
);
173 Node geq1
= d_nm
->mkNode(GEQ
, x
, c1
);
174 Node leq0
= gt0
.notNode();
175 Node leq1
= gt1
.notNode();
176 Node lt1
= geq1
.notNode();
178 fakeTheoryEnginePreprocess(leq0
);
179 fakeTheoryEnginePreprocess(leq1
);
180 fakeTheoryEnginePreprocess(geq1
);
183 d_arith
->assertFact(lt1
, true);
184 d_arith
->check(d_level
);
185 d_arith
->propagate(d_level
);
188 Node gt0Orlt1
= NodeBuilder
<2>(OR
) << gt0
<< lt1
;
189 Node geq0OrLeq1
= NodeBuilder
<2>(OR
) << geq1
<< leq1
;
191 cout
<< d_outputChannel
.getIthNode(0) << endl
<< endl
;
192 cout
<< d_outputChannel
.getIthNode(1) << endl
<< endl
;
193 cout
<< d_outputChannel
.getIthNode(2) << endl
<< endl
;
195 TS_ASSERT_EQUALS(d_outputChannel
.getNumCalls(), 3u);
197 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(0), LEMMA
);
198 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(0), gt0Orlt1
);
200 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(1), LEMMA
);
201 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(1), geq0OrLeq1
);
203 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(2), PROPAGATE
);
204 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(2), leq1
);
209 Node x
= d_nm
->mkVar(*d_realType
);
210 Node c0
= d_nm
->mkConst
<Rational
>(d_zero
);
211 Node c1
= d_nm
->mkConst
<Rational
>(d_one
);
213 Node gt0
= d_nm
->mkNode(GT
, x
, c0
);
214 Node gt1
= d_nm
->mkNode(GT
, x
, c1
);
215 Node geq1
= d_nm
->mkNode(GEQ
, x
, c1
);
216 Node leq0
= gt0
.notNode();
217 Node leq1
= gt1
.notNode();
218 Node lt1
= geq1
.notNode();
220 fakeTheoryEnginePreprocess(leq0
);
221 fakeTheoryEnginePreprocess(leq1
);
222 fakeTheoryEnginePreprocess(geq1
);
225 d_arith
->assertFact(leq0
, true);
226 d_arith
->check(d_level
);
227 d_arith
->propagate(d_level
);
229 Node gt0Orlt1
= NodeBuilder
<2>(OR
) << gt0
<< lt1
;
230 Node geq0OrLeq1
= NodeBuilder
<2>(OR
) << geq1
<< leq1
;
232 cout
<< d_outputChannel
.getIthNode(0) << endl
;
233 cout
<< d_outputChannel
.getIthNode(1) << endl
;
234 cout
<< d_outputChannel
.getIthNode(2) << endl
;
235 cout
<< d_outputChannel
.getIthNode(3) << endl
;
237 TS_ASSERT_EQUALS(d_outputChannel
.getNumCalls(), 4u);
239 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(0), LEMMA
);
240 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(0), gt0Orlt1
);
242 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(1), LEMMA
);
243 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(1), geq0OrLeq1
);
245 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(2), PROPAGATE
);
246 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(2), lt1
);
248 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(3), PROPAGATE
);
249 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(3), leq1
);
253 Node x
= d_nm
->mkVar(*d_realType
);
254 Node c0
= d_nm
->mkConst
<Rational
>(d_zero
);
255 Node c1
= d_nm
->mkConst
<Rational
>(d_one
);
257 Node gt0
= d_nm
->mkNode(GT
, x
, c0
);
258 Node gt1
= d_nm
->mkNode(GT
, x
, c1
);
259 Node geq1
= d_nm
->mkNode(GEQ
, x
, c1
);
260 Node leq0
= gt0
.notNode();
261 Node leq1
= gt1
.notNode();
262 Node lt1
= geq1
.notNode();
264 fakeTheoryEnginePreprocess(leq0
);
265 fakeTheoryEnginePreprocess(leq1
);
266 fakeTheoryEnginePreprocess(geq1
);
269 d_arith
->assertFact(leq1
, true);
270 d_arith
->check(d_level
);
271 d_arith
->propagate(d_level
);
273 Node gt0Orlt1
= NodeBuilder
<2>(OR
) << gt0
<< lt1
;
274 Node geq0OrLeq1
= NodeBuilder
<2>(OR
) << geq1
<< leq1
;
276 cout
<< d_outputChannel
.getIthNode(0) << endl
;
277 cout
<< d_outputChannel
.getIthNode(1) << endl
;
279 TS_ASSERT_EQUALS(d_outputChannel
.getNumCalls(), 2u);
281 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(0), LEMMA
);
282 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(0), gt0Orlt1
);
284 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(1), LEMMA
);
285 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(1), geq0OrLeq1
);
288 void testIntNormalForm() {
289 Node x
= d_nm
->mkVar(*d_intType
);
290 Node c0
= d_nm
->mkConst
<Rational
>(d_zero
);
291 Node c1
= d_nm
->mkConst
<Rational
>(d_one
);
292 Node c2
= d_nm
->mkConst
<Rational
>(Rational(2));
295 Node geq0
= d_nm
->mkNode(GEQ
, x
, c0
);
296 Node geq1
= d_nm
->mkNode(GEQ
, x
, c1
);
297 Node geq2
= d_nm
->mkNode(GEQ
, x
, c2
);
299 TS_ASSERT_EQUALS(Rewriter::rewrite(geq0
), geq0
);
300 TS_ASSERT_EQUALS(Rewriter::rewrite(geq1
), geq1
);
302 Node gt0
= d_nm
->mkNode(GT
, x
, c0
);
303 Node gt1
= d_nm
->mkNode(GT
, x
, c1
);
305 TS_ASSERT_EQUALS(Rewriter::rewrite(gt0
), Rewriter::rewrite(geq1
));
306 TS_ASSERT_EQUALS(Rewriter::rewrite(gt1
), Rewriter::rewrite(geq2
));
308 Node lt0
= d_nm
->mkNode(LT
, x
, c0
);
309 Node lt1
= d_nm
->mkNode(LT
, x
, c1
);
311 TS_ASSERT_EQUALS(Rewriter::rewrite(lt0
), Rewriter::rewrite(geq0
.notNode()));
312 TS_ASSERT_EQUALS(Rewriter::rewrite(lt1
), Rewriter::rewrite(geq1
.notNode()));
314 Node leq0
= d_nm
->mkNode(LEQ
, x
, c0
);
315 Node leq1
= d_nm
->mkNode(LEQ
, x
, c1
);
317 TS_ASSERT_EQUALS(Rewriter::rewrite(leq0
), Rewriter::rewrite(geq1
.notNode()));
318 TS_ASSERT_EQUALS(Rewriter::rewrite(leq1
), Rewriter::rewrite(geq2
.notNode()));