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_eq.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
, Slicer
* slicer
)
32 : SubtheorySolver(c
, bv
),
34 d_equalityEngine(d_notify
, c
, "theory::bv::TheoryBV"),
38 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
);
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
);
53 d_equalityEngine
.addFunctionKind(kind::BITVECTOR_PLUS
);
54 d_equalityEngine
.addFunctionKind(kind::BITVECTOR_EXTRACT
);
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 void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
77 d_equalityEngine
.setMasterEqualityEngine(eq
);
80 void CoreSolver::preRegister(TNode node
) {
81 if (!d_useEqualityEngine
)
84 if (node
.getKind() == kind::EQUAL
) {
85 d_equalityEngine
.addTriggerEquality(node
);
87 d_equalityEngine
.addTerm(node
);
92 void CoreSolver::explain(TNode literal
, std::vector
<TNode
>& assumptions
) {
93 bool polarity
= literal
.getKind() != kind::NOT
;
94 TNode atom
= polarity
? literal
: literal
[0];
95 if (atom
.getKind() == kind::EQUAL
) {
96 d_equalityEngine
.explainEquality(atom
[0], atom
[1], polarity
, assumptions
);
98 d_equalityEngine
.explainPredicate(atom
, polarity
, assumptions
);
102 Node
CoreSolver::getBaseDecomposition(TNode a
) {
103 // if (d_normalFormCache.find(a) != d_normalFormCache.end()) {
104 // return d_normalFormCache[a];
107 // otherwise we must compute the normal form
108 std::vector
<Node
> a_decomp
;
109 d_slicer
->getBaseDecomposition(a
, a_decomp
);
110 Node new_a
= utils::mkConcat(a_decomp
);
111 // d_normalFormCache[a] = new_a;
115 bool CoreSolver::decomposeFact(TNode fact
) {
116 Debug("bv-slicer") << "CoreSolver::decomposeFact fact=" << fact
<< endl
;
117 // FIXME: are this the right things to assert?
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 TNode eq
= fact
.getKind() == kind::NOT
? fact
[0] : fact
;
126 Node new_a
= getBaseDecomposition(a
);
127 Node new_b
= getBaseDecomposition(b
);
129 Assert (utils::getSize(new_a
) == utils::getSize(new_b
) &&
130 utils::getSize(new_a
) == utils::getSize(a
));
132 NodeManager
* nm
= NodeManager::currentNM();
133 Node a_eq_new_a
= nm
->mkNode(kind::EQUAL
, a
, new_a
);
134 Node b_eq_new_b
= nm
->mkNode(kind::EQUAL
, b
, new_b
);
137 ok
= assertFact(a_eq_new_a
, utils::mkTrue());
138 if (!ok
) return false;
139 ok
= assertFact(b_eq_new_b
, utils::mkTrue());
140 if (!ok
) return false;
141 ok
= assertFact(fact
, fact
);
142 if (!ok
) return false;
144 if (fact
.getKind() == kind::EQUAL
) {
145 // assert the individual equalities as well
147 if (new_a
.getKind() == kind::BITVECTOR_CONCAT
&&
148 new_b
.getKind() == kind::BITVECTOR_CONCAT
) {
150 Assert (new_a
.getNumChildren() == new_b
.getNumChildren());
151 for (unsigned i
= 0; i
< new_a
.getNumChildren(); ++i
) {
152 Node eq_i
= nm
->mkNode(kind::EQUAL
, new_a
[i
], new_b
[i
]);
153 ok
= assertFact(eq_i
, fact
);
154 if (!ok
) return false;
161 bool CoreSolver::addAssertions(const std::vector
<TNode
>& assertions
, Theory::Effort e
) {
162 Trace("bitvector::core") << "CoreSolver::addAssertions \n";
163 Assert (!d_bv
->inConflict());
166 std::vector
<Node
> core_eqs
;
167 for (unsigned i
= 0; i
< assertions
.size(); ++i
) {
168 TNode fact
= assertions
[i
];
170 // update whether we are in the core fragment
171 // FIXME: move isCoreTerm into CoreSolver
172 if (d_isCoreTheory
&& !d_slicer
->isCoreTerm(fact
)) {
173 d_isCoreTheory
= false;
176 // only reason about equalities
177 // FIXME: should we slice when we have the terms in inequalities?
178 if (fact
.getKind() == kind::EQUAL
|| (fact
.getKind() == kind::NOT
&& fact
[0].getKind() == kind::EQUAL
)) {
179 ok
= decomposeFact(fact
);
181 ok
= assertFact(fact
, fact
);
190 bool CoreSolver::assertFact(TNode fact
, TNode reason
) {
191 Debug("bv-slicer") << "CoreSolver::assertFact fact=" << fact
<< endl
;
192 Debug("bv-slicer") << " reason=" << reason
<< endl
;
193 // Notify the equality engine
194 if (d_useEqualityEngine
&& !d_bv
->inConflict() && !d_bv
->propagatedBy(fact
, SUB_CORE
) ) {
195 Trace("bitvector::core") << " (assert " << fact
<< ")\n";
196 //d_assertions.push_back(fact);
197 bool negated
= fact
.getKind() == kind::NOT
;
198 TNode predicate
= negated
? fact
[0] : fact
;
199 if (predicate
.getKind() == kind::EQUAL
) {
202 d_equalityEngine
.assertEquality(predicate
, false, reason
);
205 d_equalityEngine
.assertEquality(predicate
, true, reason
);
208 // Adding predicate if the congruence over it is turned on
209 if (d_equalityEngine
.isFunctionKind(predicate
.getKind())) {
210 d_equalityEngine
.assertPredicate(predicate
, !negated
, reason
);
215 // checking for a conflict
216 if (d_bv
->inConflict()) {
222 bool CoreSolver::NotifyClass::eqNotifyTriggerEquality(TNode equality
, bool value
) {
223 BVDebug("bitvector::core") << "NotifyClass::eqNotifyTriggerEquality(" << equality
<< ", " << (value
? "true" : "false" )<< ")" << std::endl
;
225 return d_solver
.storePropagation(equality
);
227 return d_solver
.storePropagation(equality
.notNode());
231 bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate
, bool value
) {
232 BVDebug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate
<< ", " << (value
? "true" : "false" ) << ")" << std::endl
;
234 return d_solver
.storePropagation(predicate
);
236 return d_solver
.storePropagation(predicate
.notNode());
240 bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag
, TNode t1
, TNode t2
, bool value
) {
241 Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1
<< ", " << t2
<< ")" << std::endl
;
243 return d_solver
.storePropagation(t1
.eqNode(t2
));
245 return d_solver
.storePropagation(t1
.eqNode(t2
).notNode());
249 void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1
, TNode t2
) {
250 d_solver
.conflict(t1
, t2
);
253 bool CoreSolver::storePropagation(TNode literal
) {
254 return d_bv
->storePropagation(literal
, SUB_CORE
);
257 void CoreSolver::conflict(TNode a
, TNode b
) {
258 std::vector
<TNode
> assumptions
;
259 d_equalityEngine
.explainEquality(a
, b
, true, assumptions
);
260 d_bv
->setConflict(mkAnd(assumptions
));
263 void CoreSolver::collectModelInfo(TheoryModel
* m
) {
264 if (Debug
.isOn("bitvector-model")) {
265 context::CDList
<TNode
>::const_iterator it
= d_assertions
.begin();
266 for (; it
!= d_assertions
.end(); ++it
) {
267 Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert "
272 d_bv
->computeRelevantTerms(termSet
);
273 m
->assertEqualityEngine(&d_equalityEngine
, &termSet
);