1 /********************* */
2 /*! \file bv_subtheory_core.cpp
4 ** Original author: Liana Hadarean
5 ** Major contributors: lianah
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Algebraic solver.
17 #include "theory/bv/bv_subtheory_core.h"
19 #include "theory/bv/theory_bv.h"
20 #include "theory/bv/theory_bv_utils.h"
21 #include "theory/bv/slicer.h"
22 #include "theory/model.h"
23 #include "theory/bv/options.h"
27 using namespace CVC4::context
;
28 using namespace CVC4::theory
;
29 using namespace CVC4::theory::bv
;
30 using namespace CVC4::theory::bv::utils
;
32 CoreSolver::CoreSolver(context::Context
* c
, TheoryBV
* bv
)
33 : SubtheorySolver(c
, bv
),
35 d_equalityEngine(d_notify
, c
, "theory::bv::TheoryBV"),
36 d_slicer(new Slicer()),
37 d_isCoreTheory(c
, true),
40 if (d_useEqualityEngine
) {
42 // The kinds we are treating as function application in congruence
43 d_equalityEngine
.addFunctionKind(kind::BITVECTOR_CONCAT
, true);
44 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
45 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
46 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
47 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
48 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
49 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
50 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
51 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
52 d_equalityEngine
.addFunctionKind(kind::BITVECTOR_MULT
, true);
53 d_equalityEngine
.addFunctionKind(kind::BITVECTOR_PLUS
, true);
54 d_equalityEngine
.addFunctionKind(kind::BITVECTOR_EXTRACT
, true);
55 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
56 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
57 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
58 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
59 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
60 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
61 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
62 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
63 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
64 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
65 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
66 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
67 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
68 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
69 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
70 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
71 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
72 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
76 CoreSolver::~CoreSolver() {
79 void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
80 d_equalityEngine
.setMasterEqualityEngine(eq
);
83 void CoreSolver::preRegister(TNode node
) {
84 if (!d_useEqualityEngine
)
87 if (node
.getKind() == kind::EQUAL
) {
88 d_equalityEngine
.addTriggerEquality(node
);
89 if (options::bitvectorCoreSolver()) {
90 d_slicer
->processEquality(node
);
93 d_equalityEngine
.addTerm(node
);
98 void CoreSolver::explain(TNode literal
, std::vector
<TNode
>& assumptions
) {
99 bool polarity
= literal
.getKind() != kind::NOT
;
100 TNode atom
= polarity
? literal
: literal
[0];
101 if (atom
.getKind() == kind::EQUAL
) {
102 d_equalityEngine
.explainEquality(atom
[0], atom
[1], polarity
, assumptions
);
104 d_equalityEngine
.explainPredicate(atom
, polarity
, assumptions
);
108 Node
CoreSolver::getBaseDecomposition(TNode a
) {
109 std::vector
<Node
> a_decomp
;
110 d_slicer
->getBaseDecomposition(a
, a_decomp
);
111 Node new_a
= utils::mkConcat(a_decomp
);
112 Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a
<<" => " << new_a
<< "\n";
116 bool CoreSolver::decomposeFact(TNode fact
) {
117 Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact
<< endl
;
118 // assert decompositions since the equality engine does not know the semantics of
120 // a == a_1 concat ... concat a_k
121 // b == b_1 concat ... concat b_k
122 Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact
<< endl
;
123 // FIXME: are this the right things to assert?
124 // assert decompositions since the equality engine does not know the semantics of
126 // a == a_1 concat ... concat a_k
127 // b == b_1 concat ... concat b_k
128 TNode eq
= fact
.getKind() == kind::NOT
? fact
[0] : fact
;
132 Node new_a
= getBaseDecomposition(a
);
133 Node new_b
= getBaseDecomposition(b
);
135 Assert (utils::getSize(new_a
) == utils::getSize(new_b
) &&
136 utils::getSize(new_a
) == utils::getSize(a
));
138 NodeManager
* nm
= NodeManager::currentNM();
139 Node a_eq_new_a
= nm
->mkNode(kind::EQUAL
, a
, new_a
);
140 Node b_eq_new_b
= nm
->mkNode(kind::EQUAL
, b
, new_b
);
143 ok
= assertFactToEqualityEngine(a_eq_new_a
, utils::mkTrue());
144 if (!ok
) return false;
145 ok
= assertFactToEqualityEngine(b_eq_new_b
, utils::mkTrue());
146 if (!ok
) return false;
147 ok
= assertFactToEqualityEngine(fact
, fact
);
148 if (!ok
) return false;
150 if (fact
.getKind() == kind::EQUAL
) {
151 // assert the individual equalities as well
153 if (new_a
.getKind() == kind::BITVECTOR_CONCAT
&&
154 new_b
.getKind() == kind::BITVECTOR_CONCAT
) {
156 Assert (new_a
.getNumChildren() == new_b
.getNumChildren());
157 for (unsigned i
= 0; i
< new_a
.getNumChildren(); ++i
) {
158 Node eq_i
= nm
->mkNode(kind::EQUAL
, new_a
[i
], new_b
[i
]);
159 ok
= assertFactToEqualityEngine(eq_i
, fact
);
160 if (!ok
) return false;
167 bool CoreSolver::check(Theory::Effort e
) {
168 Trace("bitvector::core") << "CoreSolver::check \n";
169 Assert (!d_bv
->inConflict());
170 ++(d_statistics
.d_numCallstoCheck
);
172 std::vector
<Node
> core_eqs
;
176 // update whether we are in the core fragment
177 if (d_isCoreTheory
&& !d_slicer
->isCoreTerm(fact
)) {
178 d_isCoreTheory
= false;
181 // only reason about equalities
182 if (fact
.getKind() == kind::EQUAL
|| (fact
.getKind() == kind::NOT
&& fact
[0].getKind() == kind::EQUAL
)) {
183 if (options::bitvectorCoreSolver()) {
184 ok
= decomposeFact(fact
);
186 ok
= assertFactToEqualityEngine(fact
, fact
);
189 ok
= assertFactToEqualityEngine(fact
, fact
);
195 if (Theory::fullEffort(e
) && isComplete()) {
202 void CoreSolver::buildModel() {
203 if (options::bitvectorCoreSolver()) {
208 Debug("bv-core") << "CoreSolver::buildModel() \n";
209 d_modelValues
.clear();
211 TNodeSet constants_in_eq_engine
;
212 // collect constants in equality engine
213 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(&d_equalityEngine
);
214 while (!eqcs_i
.isFinished()) {
215 TNode repr
= *eqcs_i
;
216 if (repr
.getKind() == kind::CONST_BITVECTOR
) {
217 // must check if it's just the constant
218 eq::EqClassIterator
it(repr
, &d_equalityEngine
);
219 if (!(++it
).isFinished() || true) {
220 constants
.insert(repr
);
221 constants_in_eq_engine
.insert(repr
);
226 // build repr to value map
228 eqcs_i
= eq::EqClassesIterator(&d_equalityEngine
);
229 while (!eqcs_i
.isFinished()) {
230 TNode repr
= *eqcs_i
;
233 if (repr
.getKind() != kind::VARIABLE
&&
234 repr
.getKind() != kind::SKOLEM
&&
235 repr
.getKind() != kind::CONST_BITVECTOR
&&
236 !d_bv
->isSharedTerm(repr
)) {
240 TypeNode type
= repr
.getType();
241 if (type
.isBitVector() && repr
.getKind()!= kind::CONST_BITVECTOR
) {
242 Debug("bv-core-model") << " processing " << repr
<<"\n";
243 // we need to assign a value for it
244 TypeEnumerator
te(type
);
249 // Debug("bv-core-model") << " trying value " << val << "\n";
250 // Debug("bv-core-model") << " is in set? " << constants.count(val) << "\n";
251 // Debug("bv-core-model") << " enumerator done? " << te.isFinished() << "\n";
252 } while (constants
.count(val
) != 0 && !(te
.isFinished()));
254 if (te
.isFinished() && constants
.count(val
) != 0) {
255 // if we cannot enumerate anymore values we just return the lemma stating that
256 // at least two of the representatives are equal.
257 std::vector
<TNode
> representatives
;
258 representatives
.push_back(repr
);
260 for (TNodeSet::const_iterator it
= constants_in_eq_engine
.begin();
261 it
!= constants_in_eq_engine
.end(); ++it
) {
262 TNode constant
= *it
;
263 if (utils::getSize(constant
) == utils::getSize(repr
)) {
264 representatives
.push_back(constant
);
267 for (ModelValue::const_iterator it
= d_modelValues
.begin(); it
!= d_modelValues
.end(); ++it
) {
268 representatives
.push_back(it
->first
);
270 std::vector
<Node
> equalities
;
271 for (unsigned i
= 0; i
< representatives
.size(); ++i
) {
272 for (unsigned j
= i
+ 1; j
< representatives
.size(); ++j
) {
273 TNode a
= representatives
[i
];
274 TNode b
= representatives
[j
];
275 if (utils::getSize(a
) == utils::getSize(b
)) {
276 equalities
.push_back(utils::mkNode(kind::EQUAL
, a
, b
));
280 Node lemma
= utils::mkOr(equalities
);
282 Debug("bv-core") << " lemma: " << lemma
<< "\n";
285 Debug("bv-core-model") << " " << repr
<< " => " << val
<<"\n" ;
286 constants
.insert(val
);
287 d_modelValues
[repr
] = val
;
292 bool CoreSolver::assertFactToEqualityEngine(TNode fact
, TNode reason
) {
293 // Notify the equality engine
294 if (d_useEqualityEngine
&& !d_bv
->inConflict() && (!d_bv
->wasPropagatedBySubtheory(fact
) || !d_bv
->getPropagatingSubtheory(fact
) == SUB_CORE
)) {
295 Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact
<< endl
;
296 // Debug("bv-slicer-eq") << " reason=" << reason << endl;
297 bool negated
= fact
.getKind() == kind::NOT
;
298 TNode predicate
= negated
? fact
[0] : fact
;
299 if (predicate
.getKind() == kind::EQUAL
) {
302 d_equalityEngine
.assertEquality(predicate
, false, reason
);
305 d_equalityEngine
.assertEquality(predicate
, true, reason
);
308 // Adding predicate if the congruence over it is turned on
309 if (d_equalityEngine
.isFunctionKind(predicate
.getKind())) {
310 d_equalityEngine
.assertPredicate(predicate
, !negated
, reason
);
315 // checking for a conflict
316 if (d_bv
->inConflict()) {
322 bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality
, bool value
) {
323 Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerEquality(" << equality
<< ", " << (value
? "true" : "false" )<< ")" << std::endl
;
325 return d_solver
.storePropagation(equality
);
327 return d_solver
.storePropagation(equality
.notNode());
331 bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate
, bool value
) {
332 Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate
<< ", " << (value
? "true" : "false" ) << ")" << std::endl
;
334 return d_solver
.storePropagation(predicate
);
336 return d_solver
.storePropagation(predicate
.notNode());
340 bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag
, TNode t1
, TNode t2
, bool value
) {
341 Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1
<< ", " << t2
<< ")" << std::endl
;
343 return d_solver
.storePropagation(t1
.eqNode(t2
));
345 return d_solver
.storePropagation(t1
.eqNode(t2
).notNode());
349 void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1
, TNode t2
) {
350 d_solver
.conflict(t1
, t2
);
353 bool CoreSolver::storePropagation(TNode literal
) {
354 return d_bv
->storePropagation(literal
, SUB_CORE
);
357 void CoreSolver::conflict(TNode a
, TNode b
) {
358 std::vector
<TNode
> assumptions
;
359 d_equalityEngine
.explainEquality(a
, b
, true, assumptions
);
360 Node conflict
= flattenAnd(assumptions
);
361 d_bv
->setConflict(conflict
);
364 void CoreSolver::collectModelInfo(TheoryModel
* m
) {
365 if (options::bitvectorCoreSolver()) {
369 if (Debug
.isOn("bitvector-model")) {
370 context::CDQueue
<Node
>::const_iterator it
= d_assertionQueue
.begin();
371 for (; it
!= d_assertionQueue
.end(); ++it
) {
372 Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert "
377 d_bv
->computeRelevantTerms(termSet
);
378 m
->assertEqualityEngine(&d_equalityEngine
, &termSet
);
380 Debug("bitvector-model") << "CoreSolver::collectModelInfo complete.";
381 for (ModelValue::const_iterator it
= d_modelValues
.begin(); it
!= d_modelValues
.end(); ++it
) {
384 m
->assertEquality(a
, b
, true);
389 Node
CoreSolver::getModelValue(TNode var
) {
390 // we don't need to evaluate bv expressions and only look at variable values
391 // because this only gets called when the core theory is complete (i.e. no other bv
392 // function symbols are currently asserted)
393 Assert (d_slicer
->isCoreTerm(var
));
395 Debug("bitvector-model") << "CoreSolver::getModelValue (" << var
<<")";
396 Assert (isComplete());
397 TNode repr
= d_equalityEngine
.getRepresentative(var
);
398 Node result
= Node();
399 if (repr
.getKind() == kind::CONST_BITVECTOR
) {
401 } else if (d_modelValues
.find(repr
) == d_modelValues
.end()) {
402 // it may be a shared term that never gets asserted
403 // result is just Null
404 Assert(d_bv
->isSharedTerm(var
));
406 result
= d_modelValues
[repr
];
408 Debug("bitvector-model") << " => " << result
<<"\n";
412 CoreSolver::Statistics::Statistics()
413 : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
415 StatisticsRegistry::registerStat(&d_numCallstoCheck
);
417 CoreSolver::Statistics::~Statistics() {
418 StatisticsRegistry::unregisterStat(&d_numCallstoCheck
);