1 /********************* */
2 /*! \file cnf_stream_black.h
4 ** Original author: cconway
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): taking, dejan
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 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 White box testing of CVC4::prop::CnfStream.
16 ** White box testing of CVC4::prop::CnfStream.
19 #include <cxxtest/TestSuite.h>
20 /* #include <gmock/gmock.h> */
21 /* #include <gtest/gtest.h> */
23 #include "util/Assert.h"
26 #include "expr/expr_manager.h"
27 #include "expr/node_manager.h"
28 #include "context/context.h"
29 #include "prop/cnf_stream.h"
30 #include "prop/prop_engine.h"
31 #include "prop/theory_proxy.h"
32 #include "smt/smt_engine.h"
34 #include "theory/theory.h"
35 #include "theory/theory_engine.h"
36 #include "theory/theory_registrar.h"
38 #include "theory/builtin/theory_builtin.h"
39 #include "theory/booleans/theory_bool.h"
40 #include "theory/arith/theory_arith.h"
43 using namespace CVC4::context
;
44 using namespace CVC4::prop
;
47 /* This fake class relies on the face that a MiniSat variable is just an int. */
48 class FakeSatSolver
: public SatSolver
{
49 SatVariable d_nextVar
;
50 bool d_addClauseCalled
;
55 d_addClauseCalled(false) {
58 SatVariable
newVar(bool theoryAtom
) {
62 SatVariable
trueVar() {
66 SatVariable
falseVar() {
70 void addClause(SatClause
& c
, bool lemma
) {
71 d_addClauseCalled
= true;
75 d_addClauseCalled
= false;
78 unsigned int addClauseCalled() {
79 return d_addClauseCalled
;
82 unsigned getAssertionLevel() const {
86 void unregisterVar(SatLiteral lit
) {
89 void renewVar(SatLiteral lit
, int level
= -1) {
96 return SAT_VALUE_UNKNOWN
;
99 SatValue
solve(long unsigned int& resource
) {
100 return SAT_VALUE_UNKNOWN
;
103 SatValue
value(SatLiteral l
) {
104 return SAT_VALUE_UNKNOWN
;
107 SatValue
modelValue(SatLiteral l
) {
108 return SAT_VALUE_UNKNOWN
;
111 bool properExplanation(SatLiteral lit
, SatLiteral expl
) const {
115 };/* class FakeSatSolver */
117 class CnfStreamBlack
: public CxxTest::TestSuite
{
118 /** The SAT solver proxy */
119 FakeSatSolver
* d_satSolver
;
121 /** The logic info */
122 LogicInfo
* d_logicInfo
;
124 /** The theory engine */
125 TheoryEngine
* d_theoryEngine
;
127 /** The output channel */
128 theory::OutputChannel
* d_outputChannel
;
130 /** The CNF converter in use */
131 CnfStream
* d_cnfStream
;
136 /** The user context */
137 UserContext
* d_userContext
;
139 /** The node manager */
140 NodeManager
* d_nodeManager
;
143 d_context
= new Context();
144 d_userContext
= new UserContext();
145 d_nodeManager
= new NodeManager(d_context
, NULL
);
146 NodeManagerScope
nms(d_nodeManager
);
147 d_satSolver
= new FakeSatSolver();
148 d_logicInfo
= new LogicInfo();
150 d_theoryEngine
= new TheoryEngine(d_context
, d_userContext
, *d_logicInfo
);
151 d_theoryEngine
->addTheory
<theory::builtin::TheoryBuiltin
>(theory::THEORY_BUILTIN
);
152 d_theoryEngine
->addTheory
<theory::booleans::TheoryBool
>(theory::THEORY_BOOL
);
153 d_theoryEngine
->addTheory
<theory::arith::TheoryArith
>(theory::THEORY_ARITH
);
154 d_cnfStream
= new CVC4::prop::TseitinCnfStream(d_satSolver
, new theory::TheoryRegistrar(d_theoryEngine
));
158 NodeManagerScope
nms(d_nodeManager
);
160 d_theoryEngine
->shutdown();
161 delete d_theoryEngine
;
164 delete d_nodeManager
;
165 delete d_userContext
;
171 /* [chris 5/26/2010] In the tests below, we don't attempt to delve into the
172 * deep structure of the CNF conversion. Firstly, we just want to make sure
173 * that the conversion doesn't choke on any boolean Exprs. We'll also check
174 * that addClause got called. We won't check that it gets called a particular
175 * number of times, or with what.
179 NodeManagerScope
nms(d_nodeManager
);
180 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
181 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
182 Node c
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
183 d_cnfStream
->convertAndAssert(d_nodeManager
->mkNode(kind::AND
, a
, b
, c
), false, false);
184 TS_ASSERT( d_satSolver
->addClauseCalled() );
187 void testComplexExpr() {
188 NodeManagerScope
nms(d_nodeManager
);
189 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
190 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
191 Node c
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
192 Node d
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
193 Node e
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
194 Node f
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
195 d_cnfStream
->convertAndAssert(d_nodeManager
->mkNode(kind::IMPLIES
,
196 d_nodeManager
->mkNode(kind::AND
, a
, b
),
197 d_nodeManager
->mkNode(kind::IFF
,
198 d_nodeManager
->mkNode(kind::OR
, c
, d
),
199 d_nodeManager
->mkNode(kind::NOT
,
200 d_nodeManager
->mkNode(kind::XOR
, e
, f
)))), false, false );
201 TS_ASSERT( d_satSolver
->addClauseCalled() );
205 NodeManagerScope
nms(d_nodeManager
);
206 d_cnfStream
->convertAndAssert( d_nodeManager
->mkConst(true), false, false );
207 TS_ASSERT( d_satSolver
->addClauseCalled() );
211 NodeManagerScope
nms(d_nodeManager
);
212 d_cnfStream
->convertAndAssert( d_nodeManager
->mkConst(false), false, false );
213 TS_ASSERT( d_satSolver
->addClauseCalled() );
217 NodeManagerScope
nms(d_nodeManager
);
218 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
219 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
220 d_cnfStream
->convertAndAssert( d_nodeManager
->mkNode(kind::IFF
, a
, b
), false, false );
221 TS_ASSERT( d_satSolver
->addClauseCalled() );
225 NodeManagerScope
nms(d_nodeManager
);
226 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
227 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
228 d_cnfStream
->convertAndAssert( d_nodeManager
->mkNode(kind::IMPLIES
, a
, b
), false, false );
229 TS_ASSERT( d_satSolver
->addClauseCalled() );
232 // ITEs should be removed before going to CNF
234 // NodeManagerScope nms(d_nodeManager);
235 // d_cnfStream->convertAndAssert(
236 // d_nodeManager->mkNode(
238 // d_nodeManager->mkNode(
240 // d_nodeManager->mkVar(d_nodeManager->booleanType()),
241 // d_nodeManager->mkVar(d_nodeManager->integerType()),
242 // d_nodeManager->mkVar(d_nodeManager->integerType())
244 // d_nodeManager->mkVar(d_nodeManager->integerType())
250 NodeManagerScope
nms(d_nodeManager
);
251 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
252 d_cnfStream
->convertAndAssert( d_nodeManager
->mkNode(kind::NOT
, a
), false, false );
253 TS_ASSERT( d_satSolver
->addClauseCalled() );
257 NodeManagerScope
nms(d_nodeManager
);
258 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
259 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
260 Node c
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
261 d_cnfStream
->convertAndAssert( d_nodeManager
->mkNode(kind::OR
, a
, b
, c
), false, false );
262 TS_ASSERT( d_satSolver
->addClauseCalled() );
266 NodeManagerScope
nms(d_nodeManager
);
267 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
268 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
269 d_cnfStream
->convertAndAssert(a
, false, false);
270 TS_ASSERT( d_satSolver
->addClauseCalled() );
271 d_satSolver
->reset();
272 d_cnfStream
->convertAndAssert(b
, false, false);
273 TS_ASSERT( d_satSolver
->addClauseCalled() );
277 NodeManagerScope
nms(d_nodeManager
);
278 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
279 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
280 d_cnfStream
->convertAndAssert( d_nodeManager
->mkNode(kind::XOR
, a
, b
), false, false );
281 TS_ASSERT( d_satSolver
->addClauseCalled() );
284 void testEnsureLiteral() {
285 NodeManagerScope
nms(d_nodeManager
);
286 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
287 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
288 Node a_and_b
= d_nodeManager
->mkNode(kind::AND
, a
, b
);
289 d_cnfStream
->ensureLiteral(a_and_b
);
290 // Clauses are necessary to "literal-ize" a_and_b; this perhaps
291 // doesn't belong in a black-box test though...
292 TS_ASSERT( d_satSolver
->addClauseCalled() );
293 TS_ASSERT( d_cnfStream
->hasLiteral(a_and_b
) );