1 /********************* */
2 /*! \file bv_subtheory_core.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Liana Hadarean, Aina Niemetz
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/bv_solver_lazy.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 bool CoreSolverExtTheoryCallback::getCurrentSubstitution(
36 const std::vector
<Node
>& vars
,
37 std::vector
<Node
>& subs
,
38 std::map
<Node
, std::vector
<Node
> >& exp
)
40 if (d_equalityEngine
== nullptr)
44 // get the constant equivalence classes
46 for (const Node
& n
: vars
)
48 if (d_equalityEngine
->hasTerm(n
))
50 Node nr
= d_equalityEngine
->getRepresentative(n
);
54 exp
[n
].push_back(n
.eqNode(nr
));
67 // return true if the substitution is non-trivial
71 bool CoreSolverExtTheoryCallback::getReduction(int effort
,
76 Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n
<< std::endl
;
77 if (n
.getKind() == kind::BITVECTOR_TO_NAT
)
79 nr
= utils::eliminateBv2Nat(n
);
83 else if (n
.getKind() == kind::INT_TO_BITVECTOR
)
85 nr
= utils::eliminateInt2Bv(n
);
92 CoreSolver::CoreSolver(context::Context
* c
, BVSolverLazy
* bv
)
93 : SubtheorySolver(c
, bv
),
95 d_isComplete(c
, true),
97 d_preregisterCalled(false),
101 d_extTheory(new ExtTheory(d_extTheoryCb
,
102 bv
->d_bv
.getSatContext(),
103 bv
->d_bv
.getUserContext(),
104 bv
->d_bv
.getOutputChannel())),
106 d_needsLastCallCheck(false),
107 d_extf_range_infer(bv
->d_bv
.getUserContext()),
108 d_extf_collapse_infer(bv
->d_bv
.getUserContext())
110 d_extTheory
->addFunctionKind(kind::BITVECTOR_TO_NAT
);
111 d_extTheory
->addFunctionKind(kind::INT_TO_BITVECTOR
);
114 CoreSolver::~CoreSolver() {}
116 bool CoreSolver::needsEqualityEngine(EeSetupInfo
& esi
)
118 esi
.d_notify
= &d_notify
;
119 esi
.d_name
= "theory::bv::ee";
123 void CoreSolver::finishInit()
125 // use the parent's equality engine, which may be the one we allocated above
126 d_equalityEngine
= d_bv
->d_bv
.getEqualityEngine();
128 // The kinds we are treating as function application in congruence
129 d_equalityEngine
->addFunctionKind(kind::BITVECTOR_CONCAT
, true);
130 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_AND);
131 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_OR);
132 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_XOR);
133 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_NOT);
134 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_NAND);
135 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_NOR);
136 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_XNOR);
137 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_COMP);
138 d_equalityEngine
->addFunctionKind(kind::BITVECTOR_MULT
, true);
139 d_equalityEngine
->addFunctionKind(kind::BITVECTOR_PLUS
, true);
140 d_equalityEngine
->addFunctionKind(kind::BITVECTOR_EXTRACT
, true);
141 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SUB);
142 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_NEG);
143 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_UDIV);
144 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_UREM);
145 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SDIV);
146 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SREM);
147 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SMOD);
148 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SHL);
149 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_LSHR);
150 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_ASHR);
151 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_ULT);
152 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_ULE);
153 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_UGT);
154 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_UGE);
155 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SLT);
156 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SLE);
157 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SGT);
158 // d_equalityEngine->addFunctionKind(kind::BITVECTOR_SGE);
159 d_equalityEngine
->addFunctionKind(kind::BITVECTOR_TO_NAT
);
160 d_equalityEngine
->addFunctionKind(kind::INT_TO_BITVECTOR
);
163 void CoreSolver::preRegister(TNode node
) {
164 d_preregisterCalled
= true;
165 if (node
.getKind() == kind::EQUAL
) {
166 d_equalityEngine
->addTriggerPredicate(node
);
168 d_equalityEngine
->addTerm(node
);
169 // Register with the extended theory, for context-dependent simplification.
170 // Notice we do this for registered terms but not internally generated
171 // equivalence classes. The two should roughly cooincide. Since ExtTheory is
172 // being used as a heuristic, it is good enough to be registered here.
173 d_extTheory
->registerTerm(node
);
178 void CoreSolver::explain(TNode literal
, std::vector
<TNode
>& assumptions
) {
179 bool polarity
= literal
.getKind() != kind::NOT
;
180 TNode atom
= polarity
? literal
: literal
[0];
181 if (atom
.getKind() == kind::EQUAL
) {
182 d_equalityEngine
->explainEquality(atom
[0], atom
[1], polarity
, assumptions
);
184 d_equalityEngine
->explainPredicate(atom
, polarity
, assumptions
);
188 bool CoreSolver::check(Theory::Effort e
) {
189 Trace("bitvector::core") << "CoreSolver::check \n";
191 d_bv
->d_inferManager
.spendResource(
192 ResourceManager::Resource::TheoryCheckStep
);
194 d_checkCalled
= true;
195 Assert(!d_bv
->inConflict());
196 ++(d_statistics
.d_numCallstoCheck
);
198 std::vector
<Node
> core_eqs
;
202 if (d_isComplete
&& !isCompleteForTerm(fact
, seen
)) {
203 d_isComplete
= false;
206 // only reason about equalities
207 if (fact
.getKind() == kind::EQUAL
|| (fact
.getKind() == kind::NOT
&& fact
[0].getKind() == kind::EQUAL
)) {
208 ok
= assertFactToEqualityEngine(fact
, fact
);
210 ok
= assertFactToEqualityEngine(fact
, fact
);
216 if (Theory::fullEffort(e
) && isComplete()) {
223 void CoreSolver::buildModel()
225 Debug("bv-core") << "CoreSolver::buildModel() \n";
226 NodeManager
* nm
= NodeManager::currentNM();
227 d_modelValues
.clear();
229 TNodeSet constants_in_eq_engine
;
230 // collect constants in equality engine
231 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(d_equalityEngine
);
232 while (!eqcs_i
.isFinished())
234 TNode repr
= *eqcs_i
;
235 if (repr
.getKind() == kind::CONST_BITVECTOR
)
237 // must check if it's just the constant
238 eq::EqClassIterator
it(repr
, d_equalityEngine
);
239 if (!(++it
).isFinished() || true)
241 constants
.insert(repr
);
242 constants_in_eq_engine
.insert(repr
);
248 // build repr to value map
250 eqcs_i
= eq::EqClassesIterator(d_equalityEngine
);
251 while (!eqcs_i
.isFinished())
253 TNode repr
= *eqcs_i
;
256 if (!repr
.isVar() && repr
.getKind() != kind::CONST_BITVECTOR
257 && !d_bv
->isSharedTerm(repr
))
262 TypeNode type
= repr
.getType();
263 if (type
.isBitVector() && repr
.getKind() != kind::CONST_BITVECTOR
)
265 Debug("bv-core-model") << " processing " << repr
<< "\n";
266 // we need to assign a value for it
267 TypeEnumerator
te(type
);
273 // Debug("bv-core-model") << " trying value " << val << "\n";
274 // Debug("bv-core-model") << " is in set? " << constants.count(val) <<
275 // "\n"; Debug("bv-core-model") << " enumerator done? " <<
276 // te.isFinished() << "\n";
277 } while (constants
.count(val
) != 0 && !(te
.isFinished()));
279 if (te
.isFinished() && constants
.count(val
) != 0)
281 // if we cannot enumerate anymore values we just return the lemma
282 // stating that at least two of the representatives are equal.
283 std::vector
<TNode
> representatives
;
284 representatives
.push_back(repr
);
286 for (TNodeSet::const_iterator it
= constants_in_eq_engine
.begin();
287 it
!= constants_in_eq_engine
.end();
290 TNode constant
= *it
;
291 if (utils::getSize(constant
) == utils::getSize(repr
))
293 representatives
.push_back(constant
);
296 for (ModelValue::const_iterator it
= d_modelValues
.begin();
297 it
!= d_modelValues
.end();
300 representatives
.push_back(it
->first
);
302 std::vector
<Node
> equalities
;
303 for (unsigned i
= 0; i
< representatives
.size(); ++i
)
305 for (unsigned j
= i
+ 1; j
< representatives
.size(); ++j
)
307 TNode a
= representatives
[i
];
308 TNode b
= representatives
[j
];
309 if (a
.getKind() == kind::CONST_BITVECTOR
310 && b
.getKind() == kind::CONST_BITVECTOR
)
315 if (utils::getSize(a
) == utils::getSize(b
))
317 equalities
.push_back(nm
->mkNode(kind::EQUAL
, a
, b
));
321 // better off letting the SAT solver split on values
322 if (equalities
.size() > d_lemmaThreshold
)
324 d_isComplete
= false;
328 if (equalities
.size() == 0)
330 Debug("bv-core") << " lemma: true (no equalities)" << std::endl
;
334 Node lemma
= utils::mkOr(equalities
);
336 Debug("bv-core") << " lemma: " << lemma
<< std::endl
;
341 Debug("bv-core-model") << " " << repr
<< " => " << val
<< "\n";
342 constants
.insert(val
);
343 d_modelValues
[repr
] = val
;
348 bool CoreSolver::assertFactToEqualityEngine(TNode fact
, TNode reason
) {
349 // Notify the equality engine
350 if (!d_bv
->inConflict()
351 && (!d_bv
->wasPropagatedBySubtheory(fact
)
352 || d_bv
->getPropagatingSubtheory(fact
) != SUB_CORE
))
354 Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact
<< endl
;
355 // Debug("bv-slicer-eq") << " reason=" << reason << endl;
356 bool negated
= fact
.getKind() == kind::NOT
;
357 TNode predicate
= negated
? fact
[0] : fact
;
358 if (predicate
.getKind() == kind::EQUAL
) {
361 d_equalityEngine
->assertEquality(predicate
, false, reason
);
364 d_equalityEngine
->assertEquality(predicate
, true, reason
);
367 // Adding predicate if the congruence over it is turned on
368 if (d_equalityEngine
->isFunctionKind(predicate
.getKind()))
370 d_equalityEngine
->assertPredicate(predicate
, !negated
, reason
);
375 // checking for a conflict
376 if (d_bv
->inConflict())
383 bool CoreSolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate
, bool value
) {
384 Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate
<< ", " << (value
? "true" : "false" ) << ")" << std::endl
;
386 return d_solver
.storePropagation(predicate
);
388 return d_solver
.storePropagation(predicate
.notNode());
391 bool CoreSolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag
, TNode t1
, TNode t2
, bool value
) {
392 Debug("bitvector::core") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1
<< ", " << t2
<< ")" << std::endl
;
394 return d_solver
.storePropagation(t1
.eqNode(t2
));
396 return d_solver
.storePropagation(t1
.eqNode(t2
).notNode());
400 void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1
, TNode t2
) {
401 d_solver
.conflict(t1
, t2
);
404 bool CoreSolver::storePropagation(TNode literal
) {
405 return d_bv
->storePropagation(literal
, SUB_CORE
);
408 void CoreSolver::conflict(TNode a
, TNode b
) {
409 std::vector
<TNode
> assumptions
;
410 d_equalityEngine
->explainEquality(a
, b
, true, assumptions
);
411 Node conflict
= flattenAnd(assumptions
);
412 d_bv
->setConflict(conflict
);
415 bool CoreSolver::isCompleteForTerm(TNode term
, TNodeBoolMap
& seen
) {
416 return utils::isEqualityTerm(term
, seen
);
419 bool CoreSolver::collectModelValues(TheoryModel
* m
,
420 const std::set
<Node
>& termSet
)
422 if (Debug
.isOn("bitvector-model")) {
423 context::CDQueue
<Node
>::const_iterator it
= d_assertionQueue
.begin();
424 for (; it
!= d_assertionQueue
.end(); ++it
) {
425 Debug("bitvector-model")
426 << "CoreSolver::collectModelValues (assert " << *it
<< ")\n";
430 Debug("bitvector-model") << "CoreSolver::collectModelValues complete.";
431 for (ModelValue::const_iterator it
= d_modelValues
.begin(); it
!= d_modelValues
.end(); ++it
) {
434 Debug("bitvector-model") << "CoreSolver::collectModelValues modelValues "
435 << a
<< " => " << b
<< ")\n";
436 if (!m
->assertEquality(a
, b
, true))
445 Node
CoreSolver::getModelValue(TNode var
) {
446 Debug("bitvector-model") << "CoreSolver::getModelValue (" << var
<<")";
447 Assert(isComplete());
448 TNode repr
= d_equalityEngine
->getRepresentative(var
);
449 Node result
= Node();
450 if (repr
.getKind() == kind::CONST_BITVECTOR
) {
452 } else if (d_modelValues
.find(repr
) == d_modelValues
.end()) {
453 // it may be a shared term that never gets asserted
454 // result is just Null
455 Assert(d_bv
->isSharedTerm(var
));
457 result
= d_modelValues
[repr
];
459 Debug("bitvector-model") << " => " << result
<<"\n";
463 EqualityStatus
CoreSolver::getEqualityStatus(TNode a
, TNode b
)
465 if (d_equalityEngine
->areEqual(a
, b
))
467 // The terms are implied to be equal
468 return EQUALITY_TRUE
;
470 if (d_equalityEngine
->areDisequal(a
, b
, false))
472 // The terms are implied to be dis-equal
473 return EQUALITY_FALSE
;
475 return EQUALITY_UNKNOWN
;
478 bool CoreSolver::hasTerm(TNode node
) const
480 return d_equalityEngine
->hasTerm(node
);
482 void CoreSolver::addTermToEqualityEngine(TNode node
)
484 d_equalityEngine
->addTerm(node
);
487 CoreSolver::Statistics::Statistics()
488 : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
490 smtStatisticsRegistry()->registerStat(&d_numCallstoCheck
);
492 CoreSolver::Statistics::~Statistics() {
493 smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck
);
496 void CoreSolver::checkExtf(Theory::Effort e
)
498 if (e
== Theory::EFFORT_LAST_CALL
)
500 std::vector
<Node
> nred
= d_extTheory
->getActive();
501 doExtfReductions(nred
);
503 Assert(e
== Theory::EFFORT_FULL
);
504 // do inferences (adds external lemmas) TODO: this can be improved to add
505 // internal inferences
506 std::vector
<Node
> nred
;
507 if (d_extTheory
->doInferences(0, nred
))
511 d_needsLastCallCheck
= false;
514 // other inferences involving bv2nat, int2bv
515 if (options::bvAlgExtf())
517 if (doExtfInferences(nred
))
522 if (!options::bvLazyReduceExtf())
524 if (doExtfReductions(nred
))
531 d_needsLastCallCheck
= true;
536 bool CoreSolver::needsCheckLastEffort() const { return d_needsLastCallCheck
; }
538 bool CoreSolver::doExtfInferences(std::vector
<Node
>& terms
)
540 NodeManager
* nm
= NodeManager::currentNM();
541 bool sentLemma
= false;
542 eq::EqualityEngine
* ee
= d_equalityEngine
;
543 std::map
<Node
, Node
> op_map
;
544 for (unsigned j
= 0; j
< terms
.size(); j
++)
547 Assert(n
.getKind() == kind::BITVECTOR_TO_NAT
548 || n
.getKind() == kind::INT_TO_BITVECTOR
);
549 if (n
.getKind() == kind::BITVECTOR_TO_NAT
)
552 if (d_extf_range_infer
.find(n
) == d_extf_range_infer
.end())
554 d_extf_range_infer
.insert(n
);
555 unsigned bvs
= n
[0].getType().getBitVectorSize();
556 Node min
= nm
->mkConst(Rational(0));
557 Node max
= nm
->mkConst(Rational(Integer(1).multiplyByPow2(bvs
)));
558 Node lem
= nm
->mkNode(kind::AND
,
559 nm
->mkNode(kind::GEQ
, n
, min
),
560 nm
->mkNode(kind::LT
, n
, max
));
561 Trace("bv-extf-lemma")
562 << "BV extf lemma (range) : " << lem
<< std::endl
;
563 d_bv
->d_inferManager
.lemma(lem
);
567 Node r
= (ee
&& ee
->hasTerm(n
[0])) ? ee
->getRepresentative(n
[0]) : n
[0];
570 for (unsigned j
= 0; j
< terms
.size(); j
++)
573 Node r
= (ee
&& ee
->hasTerm(n
[0])) ? ee
->getRepresentative(n
) : n
;
574 std::map
<Node
, Node
>::iterator it
= op_map
.find(r
);
575 if (it
!= op_map
.end())
577 Node parent
= it
->second
;
578 // Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(),
580 Node cterm
= parent
[0].eqNode(n
);
581 Trace("bv-extf-lemma-debug")
582 << "BV extf collapse based on : " << cterm
<< std::endl
;
583 if (d_extf_collapse_infer
.find(cterm
) == d_extf_collapse_infer
.end())
585 d_extf_collapse_infer
.insert(cterm
);
588 if (t
.getType() == parent
.getType())
590 if (n
.getKind() == kind::INT_TO_BITVECTOR
)
592 Assert(t
.getType().isInteger());
593 // congruent modulo 2^( bv width )
594 unsigned bvs
= n
.getType().getBitVectorSize();
595 Node coeff
= nm
->mkConst(Rational(Integer(1).multiplyByPow2(bvs
)));
596 Node k
= nm
->mkSkolem(
597 "int_bv_cong", t
.getType(), "for int2bv/bv2nat congruence");
598 t
= nm
->mkNode(kind::PLUS
, t
, nm
->mkNode(kind::MULT
, coeff
, k
));
600 Node lem
= parent
.eqNode(t
);
604 Assert(ee
->areEqual(parent
[0], n
));
605 lem
= nm
->mkNode(kind::IMPLIES
, parent
[0].eqNode(n
), lem
);
607 // this handles inferences of the form, e.g.:
608 // ((_ int2bv w) (bv2nat x)) == x (if x is bit-width w)
609 // (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k
610 Trace("bv-extf-lemma")
611 << "BV extf lemma (collapse) : " << lem
<< std::endl
;
612 d_bv
->d_inferManager
.lemma(lem
);
616 Trace("bv-extf-lemma-debug")
617 << "BV extf f collapse based on : " << cterm
<< std::endl
;
623 bool CoreSolver::doExtfReductions(std::vector
<Node
>& terms
)
625 std::vector
<Node
> nredr
;
626 if (d_extTheory
->doReductions(0, terms
, nredr
))
630 Assert(nredr
.empty());