1 /********************* */
2 /*! \file theory_arith_white.h
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): mdeters
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief [[ Add one-line brief description here ]]
16 ** [[ Add lengthier description here ]]
17 ** \todo document this file
21 #include <cxxtest/TestSuite.h>
23 #include "theory/theory.h"
24 #include "theory/arith/theory_arith.h"
25 #include "expr/node.h"
26 #include "expr/node_manager.h"
27 #include "context/context.h"
28 #include "util/rational.h"
30 #include "theory/theory_test_utils.h"
35 using namespace CVC4::theory
;
36 using namespace CVC4::theory::arith
;
37 using namespace CVC4::expr
;
38 using namespace CVC4::context
;
39 using namespace CVC4::kind
;
43 class TheoryArithWhite
: public CxxTest::TestSuite
{
47 NodeManagerScope
* d_scope
;
49 TestOutputChannel d_outputChannel
;
50 Theory::Effort d_level
;
54 TypeNode
* d_booleanType
;
57 const Rational d_zero
;
60 std::set
<Node
>* preregistered
;
66 TheoryArithWhite() : d_level(Theory::FULL_EFFORT
), d_zero(0), d_one(1), debug(false) {}
68 void fakeTheoryEnginePreprocess(TNode inp
){
69 Node rewrite
= inp
; //FIXME this needs to enforce that inp is fully rewritten already!
71 if(debug
) cout
<< rewrite
<< inp
<< endl
;
73 std::list
<Node
> toPreregister
;
75 toPreregister
.push_back(rewrite
);
76 for(std::list
<Node
>::iterator i
= toPreregister
.begin(); i
!= toPreregister
.end(); ++i
){
78 preregistered
->insert(n
);
80 for(Node::iterator citer
= n
.begin(); citer
!= n
.end(); ++citer
){
82 if(preregistered
->find(c
) == preregistered
->end()){
83 toPreregister
.push_back(c
);
87 for(std::list
<Node
>::reverse_iterator i
= toPreregister
.rbegin(); i
!= toPreregister
.rend(); ++i
){
89 if(debug
) cout
<< n
.getId() << " "<< n
<< endl
;
90 d_arith
->preRegisterTerm(n
);
96 d_nm
= new NodeManager(d_ctxt
);
97 d_scope
= new NodeManagerScope(d_nm
);
98 d_outputChannel
.clear();
99 d_arith
= new TheoryArith(0, d_ctxt
, d_outputChannel
);
101 preregistered
= new std::set
<Node
>();
103 d_booleanType
= new TypeNode(d_nm
->booleanType());
104 d_realType
= new TypeNode(d_nm
->realType());
110 delete d_booleanType
;
112 delete preregistered
;
115 d_outputChannel
.clear();
122 Node x
= d_nm
->mkVar(*d_realType
);
123 Node c
= d_nm
->mkConst
<Rational
>(d_zero
);
125 Node leq
= d_nm
->mkNode(LEQ
, x
, c
);
126 fakeTheoryEnginePreprocess(leq
);
128 d_arith
->assertFact(leq
);
130 d_arith
->check(d_level
);
132 TS_ASSERT_EQUALS(d_outputChannel
.getNumCalls(), 0u);
135 Node
simulateSplit(TNode l
, TNode r
){
136 Node eq
= d_nm
->mkNode(EQUAL
, l
, r
);
137 Node lt
= d_nm
->mkNode(LT
, l
, r
);
138 Node gt
= d_nm
->mkNode(GT
, l
, r
);
140 Node dis
= d_nm
->mkNode(OR
, eq
, lt
, gt
);
144 void testBasicConflict() {
145 Node x
= d_nm
->mkVar(*d_realType
);
146 Node c
= d_nm
->mkConst
<Rational
>(d_zero
);
148 Node eq
= d_nm
->mkNode(EQUAL
, x
, c
);
149 Node lt
= d_nm
->mkNode(NOT
, d_nm
->mkNode(GEQ
, x
, c
));
150 Node expectedDisjunct
= simulateSplit(x
,c
);
152 fakeTheoryEnginePreprocess(eq
);
153 fakeTheoryEnginePreprocess(lt
);
155 d_arith
->assertFact(eq
);
156 d_arith
->assertFact(lt
);
159 d_arith
->check(d_level
);
161 TS_ASSERT_EQUALS(d_outputChannel
.getNumCalls(), 2u);
162 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(0), expectedDisjunct
);
163 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(0), AUG_LEMMA
);
165 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(1), CONFLICT
);
167 Node expectedClonflict
= d_nm
->mkNode(AND
, eq
, lt
);
169 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(1), expectedClonflict
);
172 void testBasicPropagate() {
173 Node x
= d_nm
->mkVar(*d_realType
);
174 Node c
= d_nm
->mkConst
<Rational
>(d_zero
);
176 Node eq
= d_nm
->mkNode(EQUAL
, x
, c
);
177 Node lt
= d_nm
->mkNode(NOT
, d_nm
->mkNode(GEQ
, x
, c
));
178 Node expectedDisjunct
= simulateSplit(x
,c
);
180 fakeTheoryEnginePreprocess(eq
);
181 fakeTheoryEnginePreprocess(lt
);
183 d_arith
->assertFact(eq
);
186 d_arith
->check(d_level
);
187 d_arith
->propagate(d_level
);
189 TS_ASSERT_EQUALS(d_outputChannel
.getNumCalls(), 2u);
190 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(0), AUG_LEMMA
);
193 Node expectedProp
= d_nm
->mkNode(GEQ
, x
, c
);
194 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(1), PROPAGATE
);
195 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(1), expectedProp
);
199 Node x
= d_nm
->mkVar(*d_realType
);
200 Node c0
= d_nm
->mkConst
<Rational
>(d_zero
);
201 Node c1
= d_nm
->mkConst
<Rational
>(d_one
);
203 Node leq0
= d_nm
->mkNode(LEQ
, x
, c0
);
204 Node leq1
= d_nm
->mkNode(LEQ
, x
, c1
);
205 Node geq1
= d_nm
->mkNode(GEQ
, x
, c1
);
206 Node lt1
= d_nm
->mkNode(NOT
, geq1
);
208 fakeTheoryEnginePreprocess(leq0
);
209 fakeTheoryEnginePreprocess(leq1
);
210 fakeTheoryEnginePreprocess(geq1
);
212 d_arith
->assertFact(lt1
);
215 d_arith
->check(d_level
);
216 d_arith
->propagate(d_level
);
218 #ifdef CVC4_ASSERTIONS
219 TS_ASSERT_THROWS( d_arith
->explain(leq0
, d_level
), AssertionException
);
220 TS_ASSERT_THROWS( d_arith
->explain(lt1
, d_level
), AssertionException
);
222 d_arith
->explain(leq1
, d_level
);
224 TS_ASSERT_EQUALS(d_outputChannel
.getNumCalls(), 2u);
225 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(0), PROPAGATE
);
226 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(1), EXPLANATION
);
227 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(0), leq1
);
228 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(1), lt1
);
233 Node x
= d_nm
->mkVar(*d_realType
);
234 Node c0
= d_nm
->mkConst
<Rational
>(d_zero
);
235 Node c1
= d_nm
->mkConst
<Rational
>(d_one
);
237 Node leq0
= d_nm
->mkNode(LEQ
, x
, c0
);
238 Node leq1
= d_nm
->mkNode(LEQ
, x
, c1
);
239 Node geq1
= d_nm
->mkNode(GEQ
, x
, c1
);
240 Node lt1
= d_nm
->mkNode(NOT
, geq1
);
242 fakeTheoryEnginePreprocess(leq0
);
243 fakeTheoryEnginePreprocess(leq1
);
244 fakeTheoryEnginePreprocess(geq1
);
246 d_arith
->assertFact(leq0
);
249 d_arith
->check(d_level
);
250 d_arith
->propagate(d_level
);
253 d_arith
->explain(lt1
, d_level
);
254 #ifdef CVC4_ASSERTIONS
255 TS_ASSERT_THROWS( d_arith
->explain(leq0
, d_level
), AssertionException
);
257 d_arith
->explain(leq1
, d_level
);
259 TS_ASSERT_EQUALS(d_outputChannel
.getNumCalls(), 4u);
260 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(0), PROPAGATE
);
261 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(1), PROPAGATE
);
262 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(2), EXPLANATION
);
263 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(3), EXPLANATION
);
265 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(1), lt1
);
266 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(0), leq1
);
269 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(2), leq0
);
270 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(3), leq0
);
273 Node x
= d_nm
->mkVar(*d_realType
);
274 Node c0
= d_nm
->mkConst
<Rational
>(d_zero
);
275 Node c1
= d_nm
->mkConst
<Rational
>(d_one
);
277 Node leq0
= d_nm
->mkNode(LEQ
, x
, c0
);
278 Node leq1
= d_nm
->mkNode(LEQ
, x
, c1
);
279 Node geq1
= d_nm
->mkNode(GEQ
, x
, c1
);
280 Node lt1
= d_nm
->mkNode(NOT
, geq1
);
282 fakeTheoryEnginePreprocess(leq0
);
283 fakeTheoryEnginePreprocess(leq1
);
284 fakeTheoryEnginePreprocess(geq1
);
286 d_arith
->assertFact(leq1
);
289 d_arith
->check(d_level
);
290 d_arith
->propagate(d_level
);
292 #ifdef CVC4_ASSERTIONS
293 TS_ASSERT_THROWS( d_arith
->explain(leq0
, d_level
), AssertionException
);
294 TS_ASSERT_THROWS( d_arith
->explain(leq1
, d_level
), AssertionException
);
295 TS_ASSERT_THROWS( d_arith
->explain(lt1
, d_level
), AssertionException
);
298 TS_ASSERT_EQUALS(d_outputChannel
.getNumCalls(), 0u);