1 /********************* */
2 /*! \file theory_arith_white.h
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): barrett, 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
, NULL
);
97 d_scope
= new NodeManagerScope(d_nm
);
98 d_outputChannel
.clear();
99 d_arith
= new TheoryArith(d_ctxt
, d_outputChannel
, Valuation(NULL
));
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
);
145 Node x
= d_nm
->mkVar(*d_realType
);
146 Node c0
= d_nm
->mkConst
<Rational
>(d_zero
);
147 Node c1
= d_nm
->mkConst
<Rational
>(d_one
);
149 Node leq0
= d_nm
->mkNode(LEQ
, x
, c0
);
150 Node leq1
= d_nm
->mkNode(LEQ
, x
, c1
);
151 Node geq1
= d_nm
->mkNode(GEQ
, x
, c1
);
152 Node lt1
= d_nm
->mkNode(NOT
, geq1
);
153 Node gt0
= d_nm
->mkNode(NOT
, leq0
);
154 Node gt1
= d_nm
->mkNode(NOT
, leq1
);
156 fakeTheoryEnginePreprocess(leq0
);
157 fakeTheoryEnginePreprocess(leq1
);
158 fakeTheoryEnginePreprocess(geq1
);
160 d_arith
->assertFact(lt1
);
163 d_arith
->check(d_level
);
164 d_arith
->propagate(d_level
);
166 Node gt1ThenGt0
= NodeBuilder
<2>(IMPLIES
) << gt1
<< gt0
;
167 Node geq1ThenGt0
= NodeBuilder
<2>(IMPLIES
) << geq1
<< gt0
;
168 Node lt1ThenLeq1
= NodeBuilder
<2>(IMPLIES
) << lt1
<< leq1
;
170 TS_ASSERT_EQUALS(d_outputChannel
.getNumCalls(), 3u);
172 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(0), LEMMA
);
173 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(0), gt1ThenGt0
);
175 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(1), LEMMA
);
176 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(1), geq1ThenGt0
);
178 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(2), LEMMA
);
179 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(2), lt1ThenLeq1
);
184 Node x
= d_nm
->mkVar(*d_realType
);
185 Node c0
= d_nm
->mkConst
<Rational
>(d_zero
);
186 Node c1
= d_nm
->mkConst
<Rational
>(d_one
);
188 Node leq0
= d_nm
->mkNode(LEQ
, x
, c0
);
189 Node leq1
= d_nm
->mkNode(LEQ
, x
, c1
);
190 Node geq1
= d_nm
->mkNode(GEQ
, x
, c1
);
191 Node lt1
= d_nm
->mkNode(NOT
, geq1
);
192 Node gt0
= d_nm
->mkNode(NOT
, leq0
);
193 Node gt1
= d_nm
->mkNode(NOT
, leq1
);
195 fakeTheoryEnginePreprocess(leq0
);
196 fakeTheoryEnginePreprocess(leq1
);
197 fakeTheoryEnginePreprocess(geq1
);
199 d_arith
->assertFact(leq0
);
202 d_arith
->check(d_level
);
204 Node gt1ThenGt0
= NodeBuilder
<2>(IMPLIES
) << gt1
<< gt0
;
205 Node geq1ThenGt0
= NodeBuilder
<2>(IMPLIES
) << geq1
<< gt0
;
206 Node lt1ThenLeq1
= NodeBuilder
<2>(IMPLIES
) << lt1
<< leq1
;
208 TS_ASSERT_EQUALS(d_outputChannel
.getNumCalls(), 3u);
210 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(0), LEMMA
);
211 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(0), gt1ThenGt0
);
213 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(1), LEMMA
);
214 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(1), geq1ThenGt0
);
216 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(2), LEMMA
);
217 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(2), lt1ThenLeq1
);
220 Node x
= d_nm
->mkVar(*d_realType
);
221 Node c0
= d_nm
->mkConst
<Rational
>(d_zero
);
222 Node c1
= d_nm
->mkConst
<Rational
>(d_one
);
224 Node leq0
= d_nm
->mkNode(LEQ
, x
, c0
);
225 Node leq1
= d_nm
->mkNode(LEQ
, x
, c1
);
226 Node geq1
= d_nm
->mkNode(GEQ
, x
, c1
);
227 Node lt1
= d_nm
->mkNode(NOT
, geq1
);
228 Node gt0
= d_nm
->mkNode(NOT
, leq0
);
229 Node gt1
= d_nm
->mkNode(NOT
, leq1
);
231 fakeTheoryEnginePreprocess(leq0
);
232 fakeTheoryEnginePreprocess(leq1
);
233 fakeTheoryEnginePreprocess(geq1
);
235 d_arith
->assertFact(leq1
);
238 d_arith
->check(d_level
);
239 d_arith
->propagate(d_level
);
241 Node gt1ThenGt0
= NodeBuilder
<2>(IMPLIES
) << gt1
<< gt0
;
242 Node geq1ThenGt0
= NodeBuilder
<2>(IMPLIES
) << geq1
<< gt0
;
243 Node lt1ThenLeq1
= NodeBuilder
<2>(IMPLIES
) << lt1
<< leq1
;
245 TS_ASSERT_EQUALS(d_outputChannel
.getNumCalls(), 3u);
247 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(0), LEMMA
);
248 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(0), gt1ThenGt0
);
250 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(1), LEMMA
);
251 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(1), geq1ThenGt0
);
253 TS_ASSERT_EQUALS(d_outputChannel
.getIthCallType(2), LEMMA
);
254 TS_ASSERT_EQUALS(d_outputChannel
.getIthNode(2), lt1ThenLeq1
);