1 /********************* */
2 /*! \file theory_black.h
4 ** Original author: taking
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): cconway, dejan
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 Black box testing of CVC4::theory::Theory.
16 ** Black box testing of CVC4::theory::Theory.
19 #include <cxxtest/TestSuite.h>
21 #include "theory/theory.h"
22 #include "expr/node.h"
23 #include "expr/node_manager.h"
24 #include "context/context.h"
29 using namespace CVC4::theory
;
30 using namespace CVC4::expr
;
31 using namespace CVC4::context
;
36 * Very basic OutputChannel for testing simple Theory Behaviour.
37 * Stores a call sequence for the output channel
39 enum OutputChannelCallType
{CONFLICT
, PROPAGATE
, LEMMA
, EXPLANATION
};
40 class TestOutputChannel
: public OutputChannel
{
42 void push(OutputChannelCallType call
, TNode n
) {
43 d_callHistory
.push_back(make_pair(call
, n
));
47 vector
< pair
<OutputChannelCallType
, Node
> > d_callHistory
;
49 TestOutputChannel() {}
51 ~TestOutputChannel() {}
53 void safePoint() throw(Interrupted
, AssertionException
) {}
55 void conflict(TNode n
, bool safe
= false) throw(Interrupted
, AssertionException
) {
59 void propagate(TNode n
, bool safe
= false) throw(Interrupted
, AssertionException
) {
63 void lemma(TNode n
, bool safe
= false) throw(Interrupted
, AssertionException
){
66 void augmentingLemma(TNode n
, bool safe
= false) throw(Interrupted
, AssertionException
){
70 void explanation(TNode n
, bool safe
= false) throw(Interrupted
, AssertionException
) {
75 d_callHistory
.clear();
78 Node
getIthNode(int i
) {
79 Node tmp
= (d_callHistory
[i
]).second
;
83 OutputChannelCallType
getIthCallType(int i
) {
84 return (d_callHistory
[i
]).first
;
87 unsigned getNumCalls() {
88 return d_callHistory
.size();
92 class DummyTheory
: public Theory
{
94 set
<Node
> d_registered
;
95 vector
<Node
> d_getSequence
;
97 DummyTheory(Context
* ctxt
, OutputChannel
& out
) :
98 Theory(0, ctxt
, out
) {
101 void registerTerm(TNode n
) {
102 // check that we registerTerm() a term only once
103 TS_ASSERT(d_registered
.find(n
) == d_registered
.end());
105 for(TNode::iterator i
= n
.begin(); i
!= n
.end(); ++i
) {
106 // check that registerTerm() is called in reverse topological order
107 TS_ASSERT(d_registered
.find(*i
) != d_registered
.end());
110 d_registered
.insert(n
);
115 d_getSequence
.push_back(n
);
123 void check(Effort e
) {
129 void preRegisterTerm(TNode n
) {}
130 void propagate(Effort level
) {}
131 void explain(TNode n
, Effort level
) {}
132 string
identify() const { return "DummyTheory"; }
135 class TheoryBlack
: public CxxTest::TestSuite
{
139 NodeManagerScope
* d_scope
;
141 TestOutputChannel d_outputChannel
;
143 DummyTheory
* d_dummy
;
151 d_ctxt
= new Context
;
152 d_nm
= new NodeManager(d_ctxt
);
153 d_scope
= new NodeManagerScope(d_nm
);
154 d_dummy
= new DummyTheory(d_ctxt
, d_outputChannel
);
155 d_outputChannel
.clear();
156 atom0
= d_nm
->mkConst(true);
157 atom1
= d_nm
->mkConst(false);
161 atom1
= Node::null();
162 atom0
= Node::null();
170 Theory::Effort m
= Theory::MIN_EFFORT
;
171 Theory::Effort q
= Theory::QUICK_CHECK
;
172 Theory::Effort s
= Theory::STANDARD
;
173 Theory::Effort f
= Theory::FULL_EFFORT
;
175 TS_ASSERT( Theory::minEffortOnly(m
));
176 TS_ASSERT(!Theory::minEffortOnly(q
));
177 TS_ASSERT(!Theory::minEffortOnly(s
));
178 TS_ASSERT(!Theory::minEffortOnly(f
));
180 TS_ASSERT(!Theory::quickCheckOnly(m
));
181 TS_ASSERT( Theory::quickCheckOnly(q
));
182 TS_ASSERT(!Theory::quickCheckOnly(s
));
183 TS_ASSERT(!Theory::quickCheckOnly(f
));
185 TS_ASSERT(!Theory::standardEffortOnly(m
));
186 TS_ASSERT(!Theory::standardEffortOnly(q
));
187 TS_ASSERT( Theory::standardEffortOnly(s
));
188 TS_ASSERT(!Theory::standardEffortOnly(f
));
190 TS_ASSERT(!Theory::fullEffort(m
));
191 TS_ASSERT(!Theory::fullEffort(q
));
192 TS_ASSERT(!Theory::fullEffort(s
));
193 TS_ASSERT( Theory::fullEffort(f
));
195 TS_ASSERT(!Theory::quickCheckOrMore(m
));
196 TS_ASSERT( Theory::quickCheckOrMore(q
));
197 TS_ASSERT( Theory::quickCheckOrMore(s
));
198 TS_ASSERT( Theory::quickCheckOrMore(f
));
200 TS_ASSERT(!Theory::standardEffortOrMore(m
));
201 TS_ASSERT(!Theory::standardEffortOrMore(q
));
202 TS_ASSERT( Theory::standardEffortOrMore(s
));
203 TS_ASSERT( Theory::standardEffortOrMore(f
));
207 TS_ASSERT(d_dummy
->doneWrapper());
209 d_dummy
->assertFact(atom0
);
210 d_dummy
->assertFact(atom1
);
212 TS_ASSERT(!d_dummy
->doneWrapper());
214 d_dummy
->check(Theory::FULL_EFFORT
);
216 TS_ASSERT(d_dummy
->doneWrapper());
219 // FIXME: move this to theory_engine test?
220 // void testRegisterTerm() {
221 // TS_ASSERT(d_dummy->doneWrapper());
223 // TypeNode typeX = d_nm->booleanType();
224 // TypeNode typeF = d_nm->mkFunctionType(typeX, typeX);
226 // Node x = d_nm->mkVar("x",typeX);
227 // Node f = d_nm->mkVar("f",typeF);
228 // Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
229 // Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
230 // Node f_x_eq_x = f_x.eqNode(x);
231 // Node x_eq_f_f_x = x.eqNode(f_f_x);
233 // d_dummy->assertFact(f_x_eq_x);
234 // d_dummy->assertFact(x_eq_f_f_x);
236 // Node got = d_dummy->getWrapper();
238 // TS_ASSERT_EQUALS(got, f_x_eq_x);
240 // TS_ASSERT_EQUALS(5u, d_dummy->d_registered.size());
241 // TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end());
242 // TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end());
243 // TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end());
244 // TS_ASSERT(d_dummy->d_registered.find(f_x_eq_x) != d_dummy->d_registered.end());
245 // TS_ASSERT(d_dummy->d_registered.find(d_nm->operatorOf(kind::EQUAL)) != d_dummy->d_registered.end());
246 // TS_ASSERT(d_dummy->d_registered.find(f_f_x) == d_dummy->d_registered.end());
247 // TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) == d_dummy->d_registered.end());
249 // TS_ASSERT(!d_dummy->doneWrapper());
251 // got = d_dummy->getWrapper();
253 // TS_ASSERT_EQUALS(got, x_eq_f_f_x);
255 // TS_ASSERT_EQUALS(7u, d_dummy->d_registered.size());
256 // TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end());
257 // TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end());
259 // TS_ASSERT(d_dummy->doneWrapper());
262 void testOutputChannelAccessors() {
263 /* void setOutputChannel(OutputChannel& out) */
264 /* OutputChannel& getOutputChannel() */
266 TestOutputChannel theOtherChannel
;
268 TS_ASSERT_EQUALS(&(d_dummy
->getOutputChannel()), &d_outputChannel
);
270 d_dummy
->setOutputChannel(theOtherChannel
);
272 TS_ASSERT_EQUALS(&(d_dummy
->getOutputChannel()), &theOtherChannel
);
274 const OutputChannel
& oc
= d_dummy
->getOutputChannel();
276 TS_ASSERT_EQUALS(&oc
, &theOtherChannel
);