1 /********************* */
2 /*! \file bv_subtheory_eq.cpp
4 ** Original author: dejan
5 ** Major contributors: none
6 ** Minor contributors (to current version): lianah
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 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"
26 using namespace CVC4::context
;
27 using namespace CVC4::theory
;
28 using namespace CVC4::theory::bv
;
29 using namespace CVC4::theory::bv::utils
;
31 CoreSolver::CoreSolver(context::Context
* c
, TheoryBV
* bv
)
32 : SubtheorySolver(c
, bv
),
34 d_equalityEngine(d_notify
, c
, "theory::bv::TheoryBV"),
35 d_slicer(new Slicer(c
, this)),
36 d_isCoreTheory(c
, true),
39 if (d_useEqualityEngine
) {
41 // The kinds we are treating as function application in congruence
42 d_equalityEngine
.addFunctionKind(kind::BITVECTOR_CONCAT
, true);
43 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
44 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
45 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
46 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
47 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
48 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
49 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
50 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
51 d_equalityEngine
.addFunctionKind(kind::BITVECTOR_MULT
, true);
52 d_equalityEngine
.addFunctionKind(kind::BITVECTOR_PLUS
, true);
53 d_equalityEngine
.addFunctionKind(kind::BITVECTOR_EXTRACT
, true);
54 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
55 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
56 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
57 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
58 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
59 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
60 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
61 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
62 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
63 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
64 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
65 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
66 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
67 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
68 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
69 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
70 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
71 // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
75 CoreSolver::~CoreSolver() {
78 void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
79 d_equalityEngine
.setMasterEqualityEngine(eq
);
82 void CoreSolver::preRegister(TNode node
) {
83 if (!d_useEqualityEngine
)
86 if (node
.getKind() == kind::EQUAL
) {
87 d_equalityEngine
.addTriggerEquality(node
);
88 // d_slicer->processEquality(node);
90 d_equalityEngine
.addTerm(node
);
95 void CoreSolver::explain(TNode literal
, std::vector
<TNode
>& assumptions
) {
96 bool polarity
= literal
.getKind() != kind::NOT
;
97 TNode atom
= polarity
? literal
: literal
[0];
98 if (atom
.getKind() == kind::EQUAL
) {
99 d_equalityEngine
.explainEquality(atom
[0], atom
[1], polarity
, assumptions
);
101 d_equalityEngine
.explainPredicate(atom
, polarity
, assumptions
);
105 Node
CoreSolver::getBaseDecomposition(TNode a
, std::vector
<TNode
>& explanation
) {
106 std::vector
<Node
> a_decomp
;
107 d_slicer
->getBaseDecomposition(a
, a_decomp
, explanation
);
108 Node new_a
= utils::mkConcat(a_decomp
);
109 Debug("bv-slicer") << "CoreSolver::getBaseDecomposition " << a
<<" => " << new_a
<< "\n";
113 bool CoreSolver::decomposeFact(TNode fact
) {
114 Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact
<< endl
;
115 // assert decompositions since the equality engine does not know the semantics of
117 // a == a_1 concat ... concat a_k
118 // b == b_1 concat ... concat b_k
120 if (fact
.getKind() == kind::EQUAL
) {
124 d_slicer
->processEquality(fact
);
125 std::vector
<TNode
> explanation_a
;
126 Node new_a
= getBaseDecomposition(a
, explanation_a
);
127 Node reason_a
= mkAnd(explanation_a
);
128 d_reasons
.insert(reason_a
);
130 std::vector
<TNode
> explanation_b
;
131 Node new_b
= getBaseDecomposition(b
, explanation_b
);
132 Node reason_b
= mkAnd(explanation_b
);
133 d_reasons
.insert(reason_b
);
135 std::vector
<Node
> explanation
;
136 explanation
.push_back(fact
);
137 explanation
.insert(explanation
.end(), explanation_a
.begin(), explanation_a
.end());
138 explanation
.insert(explanation
.end(), explanation_b
.begin(), explanation_b
.end());
140 Node reason
= utils::mkAnd(explanation
);
141 d_reasons
.insert(reason
);
143 Assert (utils::getSize(new_a
) == utils::getSize(new_b
) &&
144 utils::getSize(new_a
) == utils::getSize(a
));
146 NodeManager
* nm
= NodeManager::currentNM();
147 Node a_eq_new_a
= nm
->mkNode(kind::EQUAL
, a
, new_a
);
148 Node b_eq_new_b
= nm
->mkNode(kind::EQUAL
, b
, new_b
);
151 ok
= assertFactToEqualityEngine(a_eq_new_a
, reason_a
);
152 if (!ok
) return false;
153 ok
= assertFactToEqualityEngine(b_eq_new_b
, reason_a
);
154 if (!ok
) return false;
155 // assert the individual equalities as well
157 if (new_a
.getKind() == kind::BITVECTOR_CONCAT
&&
158 new_b
.getKind() == kind::BITVECTOR_CONCAT
) {
159 Assert (new_a
.getNumChildren() == new_b
.getNumChildren());
160 for (unsigned i
= 0; i
< new_a
.getNumChildren(); ++i
) {
161 Node eq_i
= nm
->mkNode(kind::EQUAL
, new_a
[i
], new_b
[i
]);
162 // this reason is not very precise!!
163 ok
= assertFactToEqualityEngine(eq_i
, reason
);
164 d_reasons
.insert(eq_i
);
165 if (!ok
) return false;
168 // merge the two terms in the slicer as well
169 d_slicer
->assertEquality(fact
);
171 // still need to register the terms
172 d_slicer
->processEquality(fact
[0]);
173 TNode a
= fact
[0][0];
174 TNode b
= fact
[0][1];
175 std::vector
<TNode
> explanation_a
;
176 Node new_a
= getBaseDecomposition(a
, explanation_a
);
177 Node reason_a
= explanation_a
.empty()? mkTrue() : mkAnd(explanation_a
);
178 assertFactToEqualityEngine(utils::mkNode(kind::EQUAL
, a
, new_a
), reason_a
);
180 std::vector
<TNode
> explanation_b
;
181 Node new_b
= getBaseDecomposition(b
, explanation_b
);
182 Node reason_b
= explanation_b
.empty()? mkTrue() : mkAnd(explanation_b
);
183 assertFactToEqualityEngine(utils::mkNode(kind::EQUAL
, b
, new_b
), reason_b
);
185 d_reasons
.insert(reason_a
);
186 d_reasons
.insert(reason_b
);
188 // finally assert the actual fact to the equality engine
189 return assertFactToEqualityEngine(fact
, fact
);
192 bool CoreSolver::check(Theory::Effort e
) {
193 Trace("bitvector::core") << "CoreSolver::check \n";
194 Assert (!d_bv
->inConflict());
195 ++(d_statistics
.d_numCallstoCheck
);
197 std::vector
<Node
> core_eqs
;
201 // update whether we are in the core fragment
202 if (d_isCoreTheory
&& !d_slicer
->isCoreTerm(fact
)) {
203 d_isCoreTheory
= false;
206 // only reason about equalities
207 if (fact
.getKind() == kind::EQUAL
|| (fact
.getKind() == kind::NOT
&& fact
[0].getKind() == kind::EQUAL
)) {
208 ok
= decomposeFact(fact
);
210 ok
= assertFactToEqualityEngine(fact
, fact
);
216 // make sure to assert the new splits
217 std::vector
<Node
> new_splits
;
218 d_slicer
->getNewSplits(new_splits
);
219 for (unsigned i
= 0; i
< new_splits
.size(); ++i
) {
220 ok
= assertFactToEqualityEngine(new_splits
[i
], utils::mkTrue());
227 bool CoreSolver::assertFactToEqualityEngine(TNode fact
, TNode reason
) {
228 // Notify the equality engine
229 if (d_useEqualityEngine
&& !d_bv
->inConflict() && (!d_bv
->wasPropagatedBySubtheory(fact
) || !d_bv
->getPropagatingSubtheory(fact
) == SUB_CORE
)) {
230 Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact
<< endl
;
231 // Debug("bv-slicer-eq") << " reason=" << reason << endl;
232 bool negated
= fact
.getKind() == kind::NOT
;
233 TNode predicate
= negated
? fact
[0] : fact
;
234 if (predicate
.getKind() == kind::EQUAL
) {
237 d_equalityEngine
.assertEquality(predicate
, false, reason
);
240 d_equalityEngine
.assertEquality(predicate
, true, reason
);
243 // Adding predicate if the congruence over it is turned on
244 if (d_equalityEngine
.isFunctionKind(predicate
.getKind())) {
245 d_equalityEngine
.assertPredicate(predicate
, !negated
, reason
);
250 // checking for a conflict
251 if (d_bv
->inConflict()) {
257 bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality
, bool value
) {
258 Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerEquality(" << equality
<< ", " << (value
? "true" : "false" )<< ")" << std::endl
;
260 return d_solver
.storePropagation(equality
);
262 return d_solver
.storePropagation(equality
.notNode());
266 bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate
, bool value
) {
267 Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate
<< ", " << (value
? "true" : "false" ) << ")" << std::endl
;
269 return d_solver
.storePropagation(predicate
);
271 return d_solver
.storePropagation(predicate
.notNode());
275 bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag
, TNode t1
, TNode t2
, bool value
) {
276 Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1
<< ", " << t2
<< ")" << std::endl
;
278 return d_solver
.storePropagation(t1
.eqNode(t2
));
280 return d_solver
.storePropagation(t1
.eqNode(t2
).notNode());
284 void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1
, TNode t2
) {
285 d_solver
.conflict(t1
, t2
);
288 bool CoreSolver::storePropagation(TNode literal
) {
289 return d_bv
->storePropagation(literal
, SUB_CORE
);
292 void CoreSolver::conflict(TNode a
, TNode b
) {
293 std::vector
<TNode
> assumptions
;
294 d_equalityEngine
.explainEquality(a
, b
, true, assumptions
);
295 Node conflict
= flattenAnd(assumptions
);
296 d_bv
->setConflict(conflict
);
301 void CoreSolver::collectModelInfo(TheoryModel
* m
) {
302 if (Debug
.isOn("bitvector-model")) {
303 context::CDQueue
<Node
>::const_iterator it
= d_assertionQueue
.begin();
304 for (; it
!= d_assertionQueue
.end(); ++it
) {
305 Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert "
310 d_bv
->computeRelevantTerms(termSet
);
311 m
->assertEqualityEngine(&d_equalityEngine
, &termSet
);
314 CoreSolver::Statistics::Statistics()
315 : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
317 StatisticsRegistry::registerStat(&d_numCallstoCheck
);
319 CoreSolver::Statistics::~Statistics() {
320 StatisticsRegistry::unregisterStat(&d_numCallstoCheck
);