1 /********************* */
2 /*! \file bv_subtheory_core.cpp
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Aina Niemetz, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Algebraic solver.
17 #include "theory/bv/bv_subtheory_core.h"
19 #include "options/bv_options.h"
20 #include "options/smt_options.h"
21 #include "smt/smt_statistics_registry.h"
22 #include "theory/bv/theory_bv.h"
23 #include "theory/bv/theory_bv_utils.h"
24 #include "theory/ext_theory.h"
25 #include "theory/theory_model.h"
29 using namespace CVC4::context
;
30 using namespace CVC4::theory
;
31 using namespace CVC4::theory::bv
;
32 using namespace CVC4::theory::bv::utils
;
34 CoreSolver::CoreSolver(context::Context
* c
, TheoryBV
* bv
, ExtTheory
* extt
)
35 : SubtheorySolver(c
, bv
),
37 d_isComplete(c
, true),
39 d_preregisterCalled(false),
47 CoreSolver::~CoreSolver() {}
49 bool CoreSolver::needsEqualityEngine(EeSetupInfo
& esi
)
51 esi
.d_notify
= &d_notify
;
52 esi
.d_name
= "theory::bv::ee";
56 void CoreSolver::finishInit()
58 // use the parent's equality engine, which may be the one we allocated above
59 d_equalityEngine
= d_bv
->getEqualityEngine();
61 // The kinds we are treating as function application in congruence
62 d_equalityEngine
->addFunctionKind(kind::BITVECTOR_CONCAT
, true);
63 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_AND);
64 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_OR);
65 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_XOR);
66 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_NOT);
67 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_NAND);
68 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_NOR);
69 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_XNOR);
70 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_COMP);
71 d_equalityEngine
->addFunctionKind(kind::BITVECTOR_MULT
, true);
72 d_equalityEngine
->addFunctionKind(kind::BITVECTOR_PLUS
, true);
73 d_equalityEngine
->addFunctionKind(kind::BITVECTOR_EXTRACT
, true);
74 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SUB);
75 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_NEG);
76 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_UDIV);
77 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_UREM);
78 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SDIV);
79 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SREM);
80 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SMOD);
81 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SHL);
82 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_LSHR);
83 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_ASHR);
84 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_ULT);
85 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_ULE);
86 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_UGT);
87 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_UGE);
88 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SLT);
89 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SLE);
90 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SGT);
91 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SGE);
92 d_equalityEngine
->addFunctionKind(kind::BITVECTOR_TO_NAT
);
93 d_equalityEngine
->addFunctionKind(kind::INT_TO_BITVECTOR
);
96 void CoreSolver::preRegister(TNode node
) {
97 d_preregisterCalled
= true;
98 if (node
.getKind() == kind::EQUAL
) {
99 d_equalityEngine
->addTriggerPredicate(node
);
101 d_equalityEngine
->addTerm(node
);
102 // Register with the extended theory, for context-dependent simplification.
103 // Notice we do this for registered terms but not internally generated
104 // equivalence classes. The two should roughly cooincide. Since ExtTheory is
105 // being used as a heuristic, it is good enough to be registered here.
106 d_extTheory
->registerTerm(node
);
111 void CoreSolver::explain(TNode literal
, std::vector
<TNode
>& assumptions
) {
112 bool polarity
= literal
.getKind() != kind::NOT
;
113 TNode atom
= polarity
? literal
: literal
[0];
114 if (atom
.getKind() == kind::EQUAL
) {
115 d_equalityEngine
->explainEquality(atom
[0], atom
[1], polarity
, assumptions
);
117 d_equalityEngine
->explainPredicate(atom
, polarity
, assumptions
);
121 bool CoreSolver::check(Theory::Effort e
) {
122 Trace("bitvector::core") << "CoreSolver::check \n";
124 d_bv
->spendResource(ResourceManager::Resource::TheoryCheckStep
);
126 d_checkCalled
= true;
127 Assert(!d_bv
->inConflict());
128 ++(d_statistics
.d_numCallstoCheck
);
130 std::vector
<Node
> core_eqs
;
134 if (d_isComplete
&& !isCompleteForTerm(fact
, seen
)) {
135 d_isComplete
= false;
138 // only reason about equalities
139 if (fact
.getKind() == kind::EQUAL
|| (fact
.getKind() == kind::NOT
&& fact
[0].getKind() == kind::EQUAL
)) {
140 ok
= assertFactToEqualityEngine(fact
, fact
);
142 ok
= assertFactToEqualityEngine(fact
, fact
);
148 if (Theory::fullEffort(e
) && isComplete()) {
155 void CoreSolver::buildModel()
157 Debug("bv-core") << "CoreSolver::buildModel() \n";
158 NodeManager
* nm
= NodeManager::currentNM();
159 d_modelValues
.clear();
161 TNodeSet constants_in_eq_engine
;
162 // collect constants in equality engine
163 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(d_equalityEngine
);
164 while (!eqcs_i
.isFinished())
166 TNode repr
= *eqcs_i
;
167 if (repr
.getKind() == kind::CONST_BITVECTOR
)
169 // must check if it's just the constant
170 eq::EqClassIterator
it(repr
, d_equalityEngine
);
171 if (!(++it
).isFinished() || true)
173 constants
.insert(repr
);
174 constants_in_eq_engine
.insert(repr
);
180 // build repr to value map
182 eqcs_i
= eq::EqClassesIterator(d_equalityEngine
);
183 while (!eqcs_i
.isFinished())
185 TNode repr
= *eqcs_i
;
188 if (!repr
.isVar() && repr
.getKind() != kind::CONST_BITVECTOR
189 && !d_bv
->isSharedTerm(repr
))
194 TypeNode type
= repr
.getType();
195 if (type
.isBitVector() && repr
.getKind() != kind::CONST_BITVECTOR
)
197 Debug("bv-core-model") << " processing " << repr
<< "\n";
198 // we need to assign a value for it
199 TypeEnumerator
te(type
);
205 // Debug("bv-core-model") << " trying value " << val << "\n";
206 // Debug("bv-core-model") << " is in set? " << constants.count(val) <<
207 // "\n"; Debug("bv-core-model") << " enumerator done? " <<
208 // te.isFinished() << "\n";
209 } while (constants
.count(val
) != 0 && !(te
.isFinished()));
211 if (te
.isFinished() && constants
.count(val
) != 0)
213 // if we cannot enumerate anymore values we just return the lemma
214 // stating that at least two of the representatives are equal.
215 std::vector
<TNode
> representatives
;
216 representatives
.push_back(repr
);
218 for (TNodeSet::const_iterator it
= constants_in_eq_engine
.begin();
219 it
!= constants_in_eq_engine
.end();
222 TNode constant
= *it
;
223 if (utils::getSize(constant
) == utils::getSize(repr
))
225 representatives
.push_back(constant
);
228 for (ModelValue::const_iterator it
= d_modelValues
.begin();
229 it
!= d_modelValues
.end();
232 representatives
.push_back(it
->first
);
234 std::vector
<Node
> equalities
;
235 for (unsigned i
= 0; i
< representatives
.size(); ++i
)
237 for (unsigned j
= i
+ 1; j
< representatives
.size(); ++j
)
239 TNode a
= representatives
[i
];
240 TNode b
= representatives
[j
];
241 if (a
.getKind() == kind::CONST_BITVECTOR
242 && b
.getKind() == kind::CONST_BITVECTOR
)
247 if (utils::getSize(a
) == utils::getSize(b
))
249 equalities
.push_back(nm
->mkNode(kind::EQUAL
, a
, b
));
253 // better off letting the SAT solver split on values
254 if (equalities
.size() > d_lemmaThreshold
)
256 d_isComplete
= false;
260 if (equalities
.size() == 0)
262 Debug("bv-core") << " lemma: true (no equalities)" << std::endl
;
266 Node lemma
= utils::mkOr(equalities
);
268 Debug("bv-core") << " lemma: " << lemma
<< std::endl
;
273 Debug("bv-core-model") << " " << repr
<< " => " << val
<< "\n";
274 constants
.insert(val
);
275 d_modelValues
[repr
] = val
;
280 bool CoreSolver::assertFactToEqualityEngine(TNode fact
, TNode reason
) {
281 // Notify the equality engine
282 if (!d_bv
->inConflict() && (!d_bv
->wasPropagatedBySubtheory(fact
) || d_bv
->getPropagatingSubtheory(fact
) != SUB_CORE
)) {
283 Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact
<< endl
;
284 // Debug("bv-slicer-eq") << " reason=" << reason << endl;
285 bool negated
= fact
.getKind() == kind::NOT
;
286 TNode predicate
= negated
? fact
[0] : fact
;
287 if (predicate
.getKind() == kind::EQUAL
) {
290 d_equalityEngine
->assertEquality(predicate
, false, reason
);
293 d_equalityEngine
->assertEquality(predicate
, true, reason
);
296 // Adding predicate if the congruence over it is turned on
297 if (d_equalityEngine
->isFunctionKind(predicate
.getKind()))
299 d_equalityEngine
->assertPredicate(predicate
, !negated
, reason
);
304 // checking for a conflict
305 if (d_bv
->inConflict()) {
311 bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate
, bool value
) {
312 Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate
<< ", " << (value
? "true" : "false" ) << ")" << std::endl
;
314 return d_solver
.storePropagation(predicate
);
316 return d_solver
.storePropagation(predicate
.notNode());
319 bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag
, TNode t1
, TNode t2
, bool value
) {
320 Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1
<< ", " << t2
<< ")" << std::endl
;
322 return d_solver
.storePropagation(t1
.eqNode(t2
));
324 return d_solver
.storePropagation(t1
.eqNode(t2
).notNode());
328 void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1
, TNode t2
) {
329 d_solver
.conflict(t1
, t2
);
332 bool CoreSolver::storePropagation(TNode literal
) {
333 return d_bv
->storePropagation(literal
, SUB_CORE
);
336 void CoreSolver::conflict(TNode a
, TNode b
) {
337 std::vector
<TNode
> assumptions
;
338 d_equalityEngine
->explainEquality(a
, b
, true, assumptions
);
339 Node conflict
= flattenAnd(assumptions
);
340 d_bv
->setConflict(conflict
);
343 bool CoreSolver::isCompleteForTerm(TNode term
, TNodeBoolMap
& seen
) {
344 return utils::isEqualityTerm(term
, seen
);
347 bool CoreSolver::collectModelInfo(TheoryModel
* m
, bool fullModel
)
349 if (Debug
.isOn("bitvector-model")) {
350 context::CDQueue
<Node
>::const_iterator it
= d_assertionQueue
.begin();
351 for (; it
!= d_assertionQueue
.end(); ++it
) {
352 Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert "
357 d_bv
->computeRelevantTerms(termSet
);
358 if (!m
->assertEqualityEngine(d_equalityEngine
, &termSet
))
363 Debug("bitvector-model") << "CoreSolver::collectModelInfo complete.";
364 for (ModelValue::const_iterator it
= d_modelValues
.begin(); it
!= d_modelValues
.end(); ++it
) {
367 Debug("bitvector-model") << "CoreSolver::collectModelInfo modelValues "
368 << a
<< " => " << b
<<")\n";
369 if (!m
->assertEquality(a
, b
, true))
378 Node
CoreSolver::getModelValue(TNode var
) {
379 Debug("bitvector-model") << "CoreSolver::getModelValue (" << var
<<")";
380 Assert(isComplete());
381 TNode repr
= d_equalityEngine
->getRepresentative(var
);
382 Node result
= Node();
383 if (repr
.getKind() == kind::CONST_BITVECTOR
) {
385 } else if (d_modelValues
.find(repr
) == d_modelValues
.end()) {
386 // it may be a shared term that never gets asserted
387 // result is just Null
388 Assert(d_bv
->isSharedTerm(var
));
390 result
= d_modelValues
[repr
];
392 Debug("bitvector-model") << " => " << result
<<"\n";
396 void CoreSolver::addSharedTerm(TNode t
)
398 d_equalityEngine
->addTriggerTerm(t
, THEORY_BV
);
401 EqualityStatus
CoreSolver::getEqualityStatus(TNode a
, TNode b
)
403 if (d_equalityEngine
->areEqual(a
, b
))
405 // The terms are implied to be equal
406 return EQUALITY_TRUE
;
408 if (d_equalityEngine
->areDisequal(a
, b
, false))
410 // The terms are implied to be dis-equal
411 return EQUALITY_FALSE
;
413 return EQUALITY_UNKNOWN
;
416 bool CoreSolver::hasTerm(TNode node
) const
418 return d_equalityEngine
->hasTerm(node
);
420 void CoreSolver::addTermToEqualityEngine(TNode node
)
422 d_equalityEngine
->addTerm(node
);
425 CoreSolver::Statistics::Statistics()
426 : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
428 smtStatisticsRegistry()->registerStat(&d_numCallstoCheck
);
430 CoreSolver::Statistics::~Statistics() {
431 smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck
);