c24104acc582eff0eb53fd64a7737e2002c2a3a9
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();
149 d_theoryEngine
= new TheoryEngine(d_context
, d_userContext
, *d_logicInfo
);
150 d_theoryEngine
->addTheory
<theory::builtin::TheoryBuiltin
>(theory::THEORY_BUILTIN
);
151 d_theoryEngine
->addTheory
<theory::booleans::TheoryBool
>(theory::THEORY_BOOL
);
152 d_theoryEngine
->addTheory
<theory::arith::TheoryArith
>(theory::THEORY_ARITH
);
153 d_cnfStream
= new CVC4::prop::TseitinCnfStream(d_satSolver
, new theory::TheoryRegistrar(d_theoryEngine
));
157 NodeManagerScope
nms(d_nodeManager
);
159 d_theoryEngine
->shutdown();
160 delete d_theoryEngine
;
163 delete d_nodeManager
;
164 delete d_userContext
;
170 /* [chris 5/26/2010] In the tests below, we don't attempt to delve into the
171 * deep structure of the CNF conversion. Firstly, we just want to make sure
172 * that the conversion doesn't choke on any boolean Exprs. We'll also check
173 * that addClause got called. We won't check that it gets called a particular
174 * number of times, or with what.
178 NodeManagerScope
nms(d_nodeManager
);
179 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
180 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
181 Node c
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
182 d_cnfStream
->convertAndAssert(d_nodeManager
->mkNode(kind::AND
, a
, b
, c
), false, false);
183 TS_ASSERT( d_satSolver
->addClauseCalled() );
186 void testComplexExpr() {
187 NodeManagerScope
nms(d_nodeManager
);
188 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
189 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
190 Node c
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
191 Node d
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
192 Node e
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
193 Node f
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
194 d_cnfStream
->convertAndAssert(d_nodeManager
->mkNode(kind::IMPLIES
,
195 d_nodeManager
->mkNode(kind::AND
, a
, b
),
196 d_nodeManager
->mkNode(kind::IFF
,
197 d_nodeManager
->mkNode(kind::OR
, c
, d
),
198 d_nodeManager
->mkNode(kind::NOT
,
199 d_nodeManager
->mkNode(kind::XOR
, e
, f
)))), false, false );
200 TS_ASSERT( d_satSolver
->addClauseCalled() );
204 NodeManagerScope
nms(d_nodeManager
);
205 d_cnfStream
->convertAndAssert( d_nodeManager
->mkConst(false), false, false );
206 TS_ASSERT( d_satSolver
->addClauseCalled() );
210 NodeManagerScope
nms(d_nodeManager
);
211 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
212 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
213 d_cnfStream
->convertAndAssert( d_nodeManager
->mkNode(kind::IFF
, a
, b
), false, false );
214 TS_ASSERT( d_satSolver
->addClauseCalled() );
218 NodeManagerScope
nms(d_nodeManager
);
219 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
220 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
221 d_cnfStream
->convertAndAssert( d_nodeManager
->mkNode(kind::IMPLIES
, a
, b
), false, false );
222 TS_ASSERT( d_satSolver
->addClauseCalled() );
225 // ITEs should be removed before going to CNF
227 // NodeManagerScope nms(d_nodeManager);
228 // d_cnfStream->convertAndAssert(
229 // d_nodeManager->mkNode(
231 // d_nodeManager->mkNode(
233 // d_nodeManager->mkVar(d_nodeManager->booleanType()),
234 // d_nodeManager->mkVar(d_nodeManager->integerType()),
235 // d_nodeManager->mkVar(d_nodeManager->integerType())
237 // d_nodeManager->mkVar(d_nodeManager->integerType())
243 NodeManagerScope
nms(d_nodeManager
);
244 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
245 d_cnfStream
->convertAndAssert( d_nodeManager
->mkNode(kind::NOT
, a
), false, false );
246 TS_ASSERT( d_satSolver
->addClauseCalled() );
250 NodeManagerScope
nms(d_nodeManager
);
251 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
252 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
253 Node c
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
254 d_cnfStream
->convertAndAssert( d_nodeManager
->mkNode(kind::OR
, a
, b
, c
), false, false );
255 TS_ASSERT( d_satSolver
->addClauseCalled() );
259 NodeManagerScope
nms(d_nodeManager
);
260 d_cnfStream
->convertAndAssert( d_nodeManager
->mkConst(true), false, false );
261 TS_ASSERT( d_satSolver
->addClauseCalled() );
265 NodeManagerScope
nms(d_nodeManager
);
266 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
267 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
268 d_cnfStream
->convertAndAssert(a
, false, false);
269 TS_ASSERT( d_satSolver
->addClauseCalled() );
270 d_satSolver
->reset();
271 d_cnfStream
->convertAndAssert(b
, false, false);
272 TS_ASSERT( d_satSolver
->addClauseCalled() );
276 NodeManagerScope
nms(d_nodeManager
);
277 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
278 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
279 d_cnfStream
->convertAndAssert( d_nodeManager
->mkNode(kind::XOR
, a
, b
), false, false );
280 TS_ASSERT( d_satSolver
->addClauseCalled() );
283 void testEnsureLiteral() {
284 NodeManagerScope
nms(d_nodeManager
);
285 Node a
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
286 Node b
= d_nodeManager
->mkVar(d_nodeManager
->booleanType());
287 Node a_and_b
= d_nodeManager
->mkNode(kind::AND
, a
, b
);
288 d_cnfStream
->ensureLiteral(a_and_b
);
289 // Clauses are necessary to "literal-ize" a_and_b; this perhaps
290 // doesn't belong in a black-box test though...
291 TS_ASSERT( d_satSolver
->addClauseCalled() );
292 TS_ASSERT( d_cnfStream
->hasLiteral(a_and_b
) );