1 /********************* */
2 /*! \file bv_subtheory_algebraic.cpp
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Tim King, Aina Niemetz
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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.
16 #include "theory/bv/bv_subtheory_algebraic.h"
18 #include "options/bv_options.h"
19 #include "smt/smt_statistics_registry.h"
20 #include "smt_util/boolean_simplification.h"
21 #include "theory/bv/bv_quick_check.h"
22 #include "theory/bv/theory_bv.h"
23 #include "theory/bv/theory_bv_utils.h"
24 #include "theory/theory_model.h"
26 #include <unordered_set>
28 using namespace CVC4::context
;
29 using namespace CVC4::prop
;
30 using namespace CVC4::theory::bv::utils
;
37 /* ------------------------------------------------------------------------- */
41 /* Collect all variables under a given a node. */
42 void collectVariables(TNode node
, utils::NodeSet
& vars
)
44 std::vector
<TNode
> stack
;
45 std::unordered_set
<TNode
, TNodeHashFunction
> visited
;
47 stack
.push_back(node
);
48 while (!stack
.empty())
50 Node n
= stack
.back();
53 if (vars
.find(n
) != vars
.end()) continue;
54 if (visited
.find(n
) != visited
.end()) continue;
57 if (Theory::isLeafOf(n
, THEORY_BV
) && n
.getKind() != kind::CONST_BITVECTOR
)
62 stack
.insert(stack
.end(), n
.begin(), n
.end());
68 /* ------------------------------------------------------------------------- */
70 bool hasExpensiveBVOperators(TNode fact
);
71 Node
mergeExplanations(const std::vector
<Node
>& expls
);
72 Node
mergeExplanations(TNode expl1
, TNode expl2
);
75 SubstitutionEx::SubstitutionEx(theory::SubstitutionMap
* modelMap
)
78 , d_cacheInvalid(true)
79 , d_modelMap(modelMap
)
82 bool SubstitutionEx::addSubstitution(TNode from
, TNode to
, TNode reason
) {
83 Debug("bv-substitution") << "SubstitutionEx::addSubstitution: "<< from
84 <<" => "<< to
<< "\n" << " reason "<<reason
<< "\n";
86 if (d_substitutions
.find(from
) != d_substitutions
.end()) {
90 d_modelMap
->addSubstitution(from
, to
);
92 d_cacheInvalid
= true;
93 d_substitutions
[from
] = SubstitutionElement(to
, reason
);
97 Node
SubstitutionEx::apply(TNode node
) {
98 Debug("bv-substitution") << "SubstitutionEx::apply("<< node
<<")\n";
101 d_cacheInvalid
= false;
104 SubstitutionsCache::iterator it
= d_cache
.find(node
);
106 if (it
!= d_cache
.end()) {
107 Node res
= it
->second
.to
;
108 Debug("bv-substitution") << " =>"<< res
<<"\n";
112 Node result
= internalApply(node
);
113 Debug("bv-substitution") << " =>"<< result
<<"\n";
117 Node
SubstitutionEx::internalApply(TNode node
) {
118 if (d_substitutions
.empty())
121 vector
<SubstitutionStackElement
> stack
;
122 stack
.push_back(SubstitutionStackElement(node
));
124 while (!stack
.empty()) {
125 SubstitutionStackElement head
= stack
.back();
128 TNode current
= head
.node
;
130 if (hasCache(current
)) {
134 // check if it has substitution
135 Substitutions::const_iterator it
= d_substitutions
.find(current
);
136 if (it
!= d_substitutions
.end()) {
137 vector
<Node
> reasons
;
138 TNode to
= it
->second
.to
;
139 reasons
.push_back(it
->second
.reason
);
140 // check if the thing we subsituted to has substitutions
141 TNode res
= internalApply(to
);
143 reasons
.push_back(getReason(to
));
144 Node reason
= mergeExplanations(reasons
);
145 storeCache(current
, res
, reason
);
149 // if no children then just continue
150 if(current
.getNumChildren() == 0) {
151 storeCache(current
, current
, utils::mkTrue());
155 // children already processed
156 if (head
.childrenAdded
) {
157 NodeBuilder
<> nb(current
.getKind());
158 std::vector
<Node
> reasons
;
160 if (current
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
161 TNode op
= current
.getOperator();
162 Assert (hasCache(op
));
164 reasons
.push_back(getReason(op
));
166 for (unsigned i
= 0; i
< current
.getNumChildren(); ++i
) {
167 Assert (hasCache(current
[i
]));
168 nb
<< getCache(current
[i
]);
169 reasons
.push_back(getReason(current
[i
]));
172 // if the node is new apply substitutions to it
173 Node subst_result
= result
;
174 if (result
!= current
) {
175 subst_result
= result
!= current
? internalApply(result
) : result
;
176 reasons
.push_back(getReason(result
));
178 Node reason
= mergeExplanations(reasons
);
179 storeCache(current
, subst_result
, reason
);
182 // add children to stack
183 stack
.push_back(SubstitutionStackElement(current
, true));
184 if (current
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
185 stack
.push_back(SubstitutionStackElement(current
.getOperator()));
187 for (unsigned i
= 0; i
< current
.getNumChildren(); ++i
) {
188 stack
.push_back(SubstitutionStackElement(current
[i
]));
193 Assert(hasCache(node
));
194 return getCache(node
);
197 Node
SubstitutionEx::explain(TNode node
) const {
198 if(!hasCache(node
)) {
199 return utils::mkTrue();
202 Debug("bv-substitution") << "SubstitutionEx::explain("<< node
<<")\n";
203 Node res
= getReason(node
);
204 Debug("bv-substitution") << " with "<< res
<<"\n";
208 Node
SubstitutionEx::getReason(TNode node
) const {
209 Assert(hasCache(node
));
210 SubstitutionsCache::const_iterator it
= d_cache
.find(node
);
211 return it
->second
.reason
;
214 bool SubstitutionEx::hasCache(TNode node
) const {
215 return d_cache
.find(node
) != d_cache
.end();
218 Node
SubstitutionEx::getCache(TNode node
) const {
219 Assert (hasCache(node
));
220 return d_cache
.find(node
)->second
.to
;
223 void SubstitutionEx::storeCache(TNode from
, TNode to
, Node reason
) {
224 // Debug("bv-substitution") << "SubstitutionEx::storeCache(" << from <<", " << to <<", "<< reason<<")\n";
225 Assert (!hasCache(from
));
226 d_cache
[from
] = SubstitutionElement(to
, reason
);
229 AlgebraicSolver::AlgebraicSolver(context::Context
* c
, TheoryBV
* bv
)
230 : SubtheorySolver(c
, bv
)
232 , d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv
))
233 , d_isComplete(c
, false)
234 , d_isDifficult(c
, false)
235 , d_budget(options::bitvectorAlgebraicBudget())
237 , d_inputAssertions()
241 , d_ctx(new context::Context())
242 , d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("theory::bv::algebraic", d_quickSolver
) : NULL
)
246 AlgebraicSolver::~AlgebraicSolver() {
247 if(d_modelMap
!= NULL
) { delete d_modelMap
; }
248 delete d_quickXplain
;
249 delete d_quickSolver
;
255 bool AlgebraicSolver::check(Theory::Effort e
) {
256 Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
);
258 if (!Theory::fullEffort(e
)) {
262 if (!useHeuristic()) {
268 TimerStat::CodeTimer
algebraicTimer(d_statistics
.d_solveTime
);
269 Debug("bv-subtheory-algebraic") << "AlgebraicSolver::check (" << e
<< ")\n";
270 ++(d_statistics
.d_numCallstoCheck
);
272 d_explanations
.clear();
274 d_inputAssertions
.clear();
276 std::vector
<WorklistElement
> worklist
;
278 uint64_t original_bb_cost
= 0;
280 NodeManager
* nm
= NodeManager::currentNM();
281 NodeSet seen_assertions
;
282 // Processing assertions from scratch
283 for (AssertionQueue::const_iterator it
= assertionsBegin(); it
!= assertionsEnd(); ++it
) {
284 Debug("bv-subtheory-algebraic") << " " << *it
<< "\n";
285 TNode assertion
= *it
;
286 unsigned id
= worklist
.size();
287 d_ids
[assertion
] = id
;
288 worklist
.push_back(WorklistElement(assertion
, id
));
289 d_inputAssertions
.insert(assertion
);
290 storeExplanation(assertion
);
292 uint64_t assertion_size
= d_quickSolver
->computeAtomWeight(assertion
, seen_assertions
);
293 Assert (original_bb_cost
<= original_bb_cost
+ assertion_size
);
294 original_bb_cost
+= assertion_size
;
297 for (unsigned i
= 0; i
< worklist
.size(); ++i
) {
298 d_ids
[worklist
[i
].node
] = worklist
[i
].id
;
301 Debug("bv-subtheory-algebraic") << "Assertions " << worklist
.size() <<" : \n";
303 Assert (d_explanations
.size() == worklist
.size());
306 d_modelMap
= new SubstitutionMap(d_context
);
307 SubstitutionEx
subst(d_modelMap
);
309 // first round of substitutions
310 processAssertions(worklist
, subst
);
312 if (!d_isDifficult
.get()) {
313 // skolemize all possible extracts
314 ExtractSkolemizer
skolemizer(d_modelMap
);
315 skolemizer
.skolemize(worklist
);
316 // second round of substitutions
317 processAssertions(worklist
, subst
);
321 uint64_t subst_bb_cost
= 0;
326 for (; r
< worklist
.size(); ++r
) {
328 TNode fact
= worklist
[r
].node
;
329 unsigned id
= worklist
[r
].id
;
331 if (Dump
.isOn("bv-algebraic")) {
332 Node expl
= d_explanations
[id
];
333 Node query
= utils::mkNot(nm
->mkNode(kind::IMPLIES
, expl
, fact
));
334 Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
335 Dump("bv-algebraic") << PushCommand();
336 Dump("bv-algebraic") << AssertCommand(query
.toExpr());
337 Dump("bv-algebraic") << CheckSatCommand();
338 Dump("bv-algebraic") << PopCommand();
341 if (fact
.isConst() &&
342 fact
.getConst
<bool>() == true) {
346 if (fact
.isConst() &&
347 fact
.getConst
<bool>() == false) {
348 // we have a conflict
349 Node conflict
= BooleanSimplification::simplify(d_explanations
[id
]);
350 d_bv
->setConflict(conflict
);
351 d_isComplete
.set(true);
352 Debug("bv-subtheory-algebraic") << " UNSAT: assertion simplfies to false with conflict: "<< conflict
<< "\n";
354 if (Dump
.isOn("bv-algebraic")) {
355 Dump("bv-algebraic") << EchoCommand("TheoryBV::AlgebraicSolver::conflict");
356 Dump("bv-algebraic") << PushCommand();
357 Dump("bv-algebraic") << AssertCommand(conflict
.toExpr());
358 Dump("bv-algebraic") << CheckSatCommand();
359 Dump("bv-algebraic") << PopCommand();
363 ++(d_statistics
.d_numSimplifiesToFalse
);
368 subst_bb_cost
+= d_quickSolver
->computeAtomWeight(fact
, subst_seen
);
369 worklist
[w
] = WorklistElement(fact
, id
);
370 Node expl
= BooleanSimplification::simplify(d_explanations
[id
]);
371 storeExplanation(id
, expl
);
379 if(Debug
.isOn("bv-subtheory-algebraic")) {
380 Debug("bv-subtheory-algebraic") << "Assertions post-substitutions " << worklist
.size() << ":\n";
381 for (unsigned i
= 0; i
< worklist
.size(); ++i
) {
382 Debug("bv-subtheory-algebraic") << " " << worklist
[i
].node
<< "\n";
387 // all facts solved to true
388 if (worklist
.empty()) {
389 Debug("bv-subtheory-algebraic") << " SAT: everything simplifies to true.\n";
390 ++(d_statistics
.d_numSimplifiesToTrue
);
395 double ratio
= ((double)subst_bb_cost
)/original_bb_cost
;
397 !d_isDifficult
.get()) {
398 // give up if problem not reduced enough
399 d_isComplete
.set(false);
403 d_quickSolver
->clearSolver();
405 d_quickSolver
->push();
406 std::vector
<Node
> facts
;
407 for (unsigned i
= 0; i
< worklist
.size(); ++i
) {
408 facts
.push_back(worklist
[i
].node
);
410 bool ok
= quickCheck(facts
);
412 Debug("bv-subtheory-algebraic") << "AlgebraicSolver::check done " << ok
<< ".\n";
416 bool AlgebraicSolver::quickCheck(std::vector
<Node
>& facts
) {
417 SatValue res
= d_quickSolver
->checkSat(facts
, d_budget
);
419 if (res
== SAT_VALUE_UNKNOWN
) {
420 d_isComplete
.set(false);
421 Debug("bv-subtheory-algebraic") << " Unknown.\n";
422 ++(d_statistics
.d_numUnknown
);
426 if (res
== SAT_VALUE_TRUE
) {
427 Debug("bv-subtheory-algebraic") << " Sat.\n";
428 ++(d_statistics
.d_numSat
);
430 d_isComplete
.set(true);
434 Assert (res
== SAT_VALUE_FALSE
);
435 Assert (d_quickSolver
->inConflict());
436 d_isComplete
.set(true);
437 Debug("bv-subtheory-algebraic") << " Unsat.\n";
439 ++(d_statistics
.d_numUnsat
);
442 Node conflict
= d_quickSolver
->getConflict();
443 Debug("bv-subtheory-algebraic") << " Conflict: " << conflict
<< "\n";
445 // singleton conflict
446 if (conflict
.getKind() != kind::AND
) {
447 Assert (d_ids
.find(conflict
) != d_ids
.end());
448 unsigned id
= d_ids
[conflict
];
449 Assert (id
< d_explanations
.size());
450 Node theory_confl
= d_explanations
[id
];
451 d_bv
->setConflict(theory_confl
);
455 Assert (conflict
.getKind() == kind::AND
);
456 if (options::bitvectorQuickXplain()) {
457 d_quickSolver
->popToZero();
458 Debug("bv-quick-xplain") << "AlgebraicSolver::quickCheck original conflict size " << conflict
.getNumChildren() << "\n";
459 conflict
= d_quickXplain
->minimizeConflict(conflict
);
460 Debug("bv-quick-xplain") << "AlgebraicSolver::quickCheck minimized conflict size " << conflict
.getNumChildren() << "\n";
463 vector
<TNode
> theory_confl
;
464 for (unsigned i
= 0; i
< conflict
.getNumChildren(); ++i
) {
465 TNode c
= conflict
[i
];
467 Assert (d_ids
.find(c
) != d_ids
.end());
468 unsigned c_id
= d_ids
[c
];
469 Assert (c_id
< d_explanations
.size());
470 TNode c_expl
= d_explanations
[c_id
];
471 theory_confl
.push_back(c_expl
);
474 Node confl
= BooleanSimplification::simplify(utils::mkAnd(theory_confl
));
476 Debug("bv-subtheory-algebraic") << " Out Conflict: " << confl
<< "\n";
481 void AlgebraicSolver::setConflict(TNode conflict
) {
482 Node final_conflict
= conflict
;
483 if (options::bitvectorQuickXplain() &&
484 conflict
.getKind() == kind::AND
&&
485 conflict
.getNumChildren() > 4) {
486 final_conflict
= d_quickXplain
->minimizeConflict(conflict
);
488 d_bv
->setConflict(final_conflict
);
491 bool AlgebraicSolver::solve(TNode fact
, TNode reason
, SubstitutionEx
& subst
) {
492 if (fact
.getKind() != kind::EQUAL
) return false;
494 NodeManager
* nm
= NodeManager::currentNM();
495 TNode left
= fact
[0];
496 TNode right
= fact
[1];
498 if (left
.isVar() && !right
.hasSubterm(left
)) {
499 bool changed
= subst
.addSubstitution(left
, right
, reason
);
502 if (right
.isVar() && !left
.hasSubterm(right
)) {
503 bool changed
= subst
.addSubstitution(right
, left
, reason
);
507 // xor simplification
508 if (right
.getKind() == kind::BITVECTOR_XOR
&&
509 left
.getKind() == kind::BITVECTOR_XOR
) {
511 if (var
.getMetaKind() != kind::metakind::VARIABLE
)
514 // simplify xor with same variable on both sides
515 if (right
.hasSubterm(var
)) {
516 std::vector
<Node
> right_children
;
517 for (unsigned i
= 0; i
< right
.getNumChildren(); ++i
) {
519 right_children
.push_back(right
[i
]);
521 Assert (right_children
.size());
522 Node new_right
= utils::mkNaryNode(kind::BITVECTOR_XOR
, right_children
);
523 std::vector
<Node
> left_children
;
524 for (unsigned i
= 1; i
< left
.getNumChildren(); ++i
) {
525 left_children
.push_back(left
[i
]);
527 Node new_left
= utils::mkNaryNode(kind::BITVECTOR_XOR
, left_children
);
528 Node new_fact
= nm
->mkNode(kind::EQUAL
, new_left
, new_right
);
529 bool changed
= subst
.addSubstitution(fact
, new_fact
, reason
);
533 NodeBuilder
<> nb(kind::BITVECTOR_XOR
);
534 for (unsigned i
= 1; i
< left
.getNumChildren(); ++i
) {
537 Node inverse
= left
.getNumChildren() == 2? (Node
)left
[1] : (Node
)nb
;
538 Node new_right
= nm
->mkNode(kind::BITVECTOR_XOR
, right
, inverse
);
539 bool changed
= subst
.addSubstitution(var
, new_right
, reason
);
541 if (Dump
.isOn("bv-algebraic")) {
542 Node query
= utils::mkNot(nm
->mkNode(
543 kind::EQUAL
, fact
, nm
->mkNode(kind::EQUAL
, var
, new_right
)));
544 Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
545 Dump("bv-algebraic") << PushCommand();
546 Dump("bv-algebraic") << AssertCommand(query
.toExpr());
547 Dump("bv-algebraic") << CheckSatCommand();
548 Dump("bv-algebraic") << PopCommand();
555 // (a xor t = a) <=> (t = 0)
556 if (left
.getKind() == kind::BITVECTOR_XOR
&&
557 right
.getMetaKind() == kind::metakind::VARIABLE
&&
558 left
.hasSubterm(right
)) {
560 Node new_left
= nm
->mkNode(kind::BITVECTOR_XOR
, var
, left
);
561 Node zero
= utils::mkConst(utils::getSize(var
), 0u);
562 Node new_fact
= nm
->mkNode(kind::EQUAL
, zero
, new_left
);
563 bool changed
= subst
.addSubstitution(fact
, new_fact
, reason
);
567 if (right
.getKind() == kind::BITVECTOR_XOR
&&
568 left
.getMetaKind() == kind::metakind::VARIABLE
&&
569 right
.hasSubterm(left
)) {
571 Node new_right
= nm
->mkNode(kind::BITVECTOR_XOR
, var
, right
);
572 Node zero
= utils::mkConst(utils::getSize(var
), 0u);
573 Node new_fact
= nm
->mkNode(kind::EQUAL
, zero
, new_right
);
574 bool changed
= subst
.addSubstitution(fact
, new_fact
, reason
);
578 // (a xor b = 0) <=> (a = b)
579 if (left
.getKind() == kind::BITVECTOR_XOR
&&
580 left
.getNumChildren() == 2 &&
581 right
.getKind() == kind::CONST_BITVECTOR
&&
582 right
.getConst
<BitVector
>() == BitVector(utils::getSize(left
), 0u)) {
583 Node new_fact
= nm
->mkNode(kind::EQUAL
, left
[0], left
[1]);
584 bool changed
= subst
.addSubstitution(fact
, new_fact
, reason
);
592 bool AlgebraicSolver::isSubstitutableIn(TNode node
, TNode in
) {
593 if (node
.getMetaKind() == kind::metakind::VARIABLE
&&
594 !in
.hasSubterm(node
))
599 void AlgebraicSolver::processAssertions(std::vector
<WorklistElement
>& worklist
, SubstitutionEx
& subst
) {
600 NodeManager
* nm
= NodeManager::currentNM();
603 // d_bv->spendResource();
605 for (unsigned i
= 0; i
< worklist
.size(); ++i
) {
606 // apply current substitutions
607 Node current
= subst
.apply(worklist
[i
].node
);
608 unsigned current_id
= worklist
[i
].id
;
609 Node subst_expl
= subst
.explain(worklist
[i
].node
);
610 worklist
[i
] = WorklistElement(Rewriter::rewrite(current
), current_id
);
611 // explanation for this assertion
612 Node old_expl
= d_explanations
[current_id
];
613 Node new_expl
= mergeExplanations(subst_expl
, old_expl
);
614 storeExplanation(current_id
, new_expl
);
616 // use the new substitution to solve
617 if(solve(worklist
[i
].node
, new_expl
, subst
)) {
622 // check for concat slicings
623 for (unsigned i
= 0; i
< worklist
.size(); ++i
) {
624 TNode fact
= worklist
[i
].node
;
625 unsigned current_id
= worklist
[i
].id
;
627 if (fact
.getKind() != kind::EQUAL
) {
631 TNode left
= fact
[0];
632 TNode right
= fact
[1];
633 if (left
.getKind() != kind::BITVECTOR_CONCAT
||
634 right
.getKind() != kind::BITVECTOR_CONCAT
||
635 left
.getNumChildren() != right
.getNumChildren()) {
639 bool can_slice
= true;
640 for (unsigned j
= 0; j
< left
.getNumChildren(); ++j
) {
641 if (utils::getSize(left
[j
]) != utils::getSize(right
[j
]))
649 for (unsigned j
= 0; j
< left
.getNumChildren(); ++j
) {
650 Node eq_j
= nm
->mkNode(kind::EQUAL
, left
[j
], right
[j
]);
651 unsigned id
= d_explanations
.size();
652 TNode expl
= d_explanations
[current_id
];
653 storeExplanation(expl
);
654 worklist
.push_back(WorklistElement(eq_j
, id
));
657 worklist
[i
] = WorklistElement(utils::mkTrue(), worklist
[i
].id
);
660 Assert (d_explanations
.size() == worklist
.size());
664 void AlgebraicSolver::storeExplanation(unsigned id
, TNode explanation
) {
665 Assert (checkExplanation(explanation
));
666 d_explanations
[id
] = explanation
;
669 void AlgebraicSolver::storeExplanation(TNode explanation
) {
670 Assert (checkExplanation(explanation
));
671 d_explanations
.push_back(explanation
);
674 bool AlgebraicSolver::checkExplanation(TNode explanation
) {
675 Node simplified_explanation
= explanation
; //BooleanSimplification::simplify(explanation);
676 if (simplified_explanation
.getKind() != kind::AND
) {
677 return d_inputAssertions
.find(simplified_explanation
) != d_inputAssertions
.end();
679 for (unsigned i
= 0; i
< simplified_explanation
.getNumChildren(); ++i
) {
680 if (d_inputAssertions
.find(simplified_explanation
[i
]) == d_inputAssertions
.end()) {
688 bool AlgebraicSolver::isComplete() {
689 return d_isComplete
.get();
692 bool AlgebraicSolver::useHeuristic() {
696 double success_rate
= double(d_numSolved
)/double(d_numCalls
);
697 d_statistics
.d_useHeuristic
.setData(success_rate
);
698 return success_rate
> 0.8;
702 void AlgebraicSolver::assertFact(TNode fact
) {
703 d_assertionQueue
.push_back(fact
);
704 d_isComplete
.set(false);
705 if (!d_isDifficult
.get()) {
706 d_isDifficult
.set(hasExpensiveBVOperators(fact
));
710 EqualityStatus
AlgebraicSolver::getEqualityStatus(TNode a
, TNode b
) {
711 return EQUALITY_UNKNOWN
;
714 bool AlgebraicSolver::collectModelInfo(TheoryModel
* model
, bool fullModel
)
716 Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n";
717 AlwaysAssert (!d_quickSolver
->inConflict());
719 d_bv
->computeRelevantTerms(termSet
);
721 // collect relevant terms that the bv theory abstracts to variables
722 // (variables and parametric terms such as select apply_uf)
723 std::vector
<TNode
> variables
;
724 std::vector
<Node
> values
;
725 for (set
<Node
>::const_iterator it
= termSet
.begin(); it
!= termSet
.end(); ++it
) {
727 if (term
.getType().isBitVector() &&
728 (term
.getMetaKind() == kind::metakind::VARIABLE
||
729 Theory::theoryOf(term
) != THEORY_BV
)) {
730 variables
.push_back(term
);
731 values
.push_back(term
);
736 Debug("bitvector-model") << "Substitutions:\n";
737 for (unsigned i
= 0; i
< variables
.size(); ++i
) {
738 TNode current
= variables
[i
];
739 TNode subst
= Rewriter::rewrite(d_modelMap
->apply(current
));
740 Debug("bitvector-model") << " " << current
<< " => " << subst
<< "\n";
742 collectVariables(subst
, leaf_vars
);
745 Debug("bitvector-model") << "Model:\n";
747 for (NodeSet::const_iterator it
= leaf_vars
.begin(); it
!= leaf_vars
.end(); ++it
) {
749 Node value
= d_quickSolver
->getVarValue(var
, true);
750 Assert (!value
.isNull() || !fullModel
);
752 // may be a shared term that did not appear in the current assertions
753 // AJR: need to check whether already in map for cases where collectModelInfo is called multiple times in the same context
754 if (!value
.isNull() && !d_modelMap
->hasSubstitution(var
)) {
755 Debug("bitvector-model") << " " << var
<< " => " << value
<< "\n";
756 Assert (value
.getKind() == kind::CONST_BITVECTOR
);
757 d_modelMap
->addSubstitution(var
, value
);
761 Debug("bitvector-model") << "Final Model:\n";
762 for (unsigned i
= 0; i
< variables
.size(); ++i
) {
763 TNode current
= values
[i
];
764 TNode subst
= Rewriter::rewrite(d_modelMap
->apply(current
));
765 Debug("bitvector-model") << "AlgebraicSolver: " << variables
[i
] << " => " << subst
<< "\n";
766 // Doesn't have to be constant as it may be irrelevant
767 Assert (subst
.getKind() == kind::CONST_BITVECTOR
);
768 if (!model
->assertEquality(variables
[i
], subst
, true))
776 Node
AlgebraicSolver::getModelValue(TNode node
) {
780 AlgebraicSolver::Statistics::Statistics()
781 : d_numCallstoCheck("theory::bv::algebraic::NumCallsToCheck", 0)
782 , d_numSimplifiesToTrue("theory::bv::algebraic::NumSimplifiesToTrue", 0)
783 , d_numSimplifiesToFalse("theory::bv::algebraic::NumSimplifiesToFalse", 0)
784 , d_numUnsat("theory::bv::algebraic::NumUnsat", 0)
785 , d_numSat("theory::bv::algebraic::NumSat", 0)
786 , d_numUnknown("theory::bv::algebraic::NumUnknown", 0)
787 , d_solveTime("theory::bv::algebraic::SolveTime")
788 , d_useHeuristic("theory::bv::algebraic::UseHeuristic", 0.2)
790 smtStatisticsRegistry()->registerStat(&d_numCallstoCheck
);
791 smtStatisticsRegistry()->registerStat(&d_numSimplifiesToTrue
);
792 smtStatisticsRegistry()->registerStat(&d_numSimplifiesToFalse
);
793 smtStatisticsRegistry()->registerStat(&d_numUnsat
);
794 smtStatisticsRegistry()->registerStat(&d_numSat
);
795 smtStatisticsRegistry()->registerStat(&d_numUnknown
);
796 smtStatisticsRegistry()->registerStat(&d_solveTime
);
797 smtStatisticsRegistry()->registerStat(&d_useHeuristic
);
800 AlgebraicSolver::Statistics::~Statistics() {
801 smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck
);
802 smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToTrue
);
803 smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToFalse
);
804 smtStatisticsRegistry()->unregisterStat(&d_numUnsat
);
805 smtStatisticsRegistry()->unregisterStat(&d_numSat
);
806 smtStatisticsRegistry()->unregisterStat(&d_numUnknown
);
807 smtStatisticsRegistry()->unregisterStat(&d_solveTime
);
808 smtStatisticsRegistry()->unregisterStat(&d_useHeuristic
);
811 bool hasExpensiveBVOperatorsRec(TNode fact
, TNodeSet
& seen
) {
812 if (fact
.getKind() == kind::BITVECTOR_MULT
||
813 fact
.getKind() == kind::BITVECTOR_UDIV_TOTAL
||
814 fact
.getKind() == kind::BITVECTOR_UREM_TOTAL
) {
818 if (seen
.find(fact
) != seen
.end()) {
822 if (fact
.getNumChildren() == 0) {
825 for (unsigned i
= 0; i
< fact
.getNumChildren(); ++i
) {
826 bool difficult
= hasExpensiveBVOperatorsRec(fact
[i
], seen
);
834 bool hasExpensiveBVOperators(TNode fact
) {
836 return hasExpensiveBVOperatorsRec(fact
, seen
);
839 void ExtractSkolemizer::skolemize(std::vector
<WorklistElement
>& facts
) {
841 for (unsigned i
= 0; i
< facts
.size(); ++i
) {
842 TNode current
= facts
[i
].node
;
843 collectExtracts(current
, seen
);
846 for (VarExtractMap::iterator it
= d_varToExtract
.begin(); it
!= d_varToExtract
.end(); ++it
) {
847 ExtractList
& el
= it
->second
;
848 TNode var
= it
->first
;
849 Base
& base
= el
.base
;
851 unsigned bw
= utils::getSize(var
);
852 // compute decomposition
853 std::vector
<unsigned> cuts
;
854 for (unsigned i
= 1; i
<= bw
; ++i
) {
855 if (base
.isCutPoint(i
)) {
859 unsigned previous
= 0;
860 unsigned current
= 0;
861 std::vector
<Node
> skolems
;
862 for (unsigned i
= 0; i
< cuts
.size(); ++i
) {
864 Assert (current
> 0);
865 int size
= current
- previous
;
867 Node sk
= utils::mkVar(size
);
868 skolems
.push_back(sk
);
871 if (current
< bw
-1) {
872 int size
= bw
- current
;
874 Node sk
= utils::mkVar(size
);
875 skolems
.push_back(sk
);
877 NodeBuilder
<> skolem_nb(kind::BITVECTOR_CONCAT
);
879 for (int i
= skolems
.size() - 1; i
>= 0; --i
) {
880 skolem_nb
<< skolems
[i
];
883 Node skolem_concat
= skolems
.size() == 1 ? (Node
)skolems
[0] : (Node
) skolem_nb
;
884 Assert (utils::getSize(skolem_concat
) == utils::getSize(var
));
885 storeSkolem(var
, skolem_concat
);
887 for (unsigned i
= 0; i
< el
.extracts
.size(); ++i
) {
888 unsigned h
= el
.extracts
[i
].high
;
889 unsigned l
= el
.extracts
[i
].low
;
890 Node extract
= utils::mkExtract(var
, h
, l
);
891 Node skolem_extract
= Rewriter::rewrite(utils::mkExtract(skolem_concat
, h
, l
));
892 Assert (skolem_extract
.getMetaKind() == kind::metakind::VARIABLE
||
893 skolem_extract
.getKind() == kind::BITVECTOR_CONCAT
);
894 storeSkolem(extract
, skolem_extract
);
898 for (unsigned i
= 0; i
< facts
.size(); ++i
) {
899 facts
[i
] = WorklistElement(skolemize(facts
[i
].node
), facts
[i
].id
);
903 Node
ExtractSkolemizer::mkSkolem(Node node
) {
904 Assert (node
.getKind() == kind::BITVECTOR_EXTRACT
&&
905 node
[0].getMetaKind() == kind::metakind::VARIABLE
);
906 Assert (!d_skolemSubst
.hasSubstitution(node
));
907 return utils::mkVar(utils::getSize(node
));
910 void ExtractSkolemizer::unSkolemize(std::vector
<WorklistElement
>& facts
) {
911 for (unsigned i
= 0; i
< facts
.size(); ++i
) {
912 facts
[i
] = WorklistElement(unSkolemize(facts
[i
].node
), facts
[i
].id
);
916 void ExtractSkolemizer::storeSkolem(TNode node
, TNode skolem
) {
917 d_skolemSubst
.addSubstitution(node
, skolem
);
918 d_modelMap
->addSubstitution(node
, skolem
);
919 d_skolemSubstRev
.addSubstitution(skolem
, node
);
922 Node
ExtractSkolemizer::unSkolemize(TNode node
) {
923 return d_skolemSubstRev
.apply(node
);
926 Node
ExtractSkolemizer::skolemize(TNode node
) {
927 return d_skolemSubst
.apply(node
);
930 void ExtractSkolemizer::ExtractList::addExtract(Extract
& e
) {
931 extracts
.push_back(e
);
933 base
.sliceAt(e
.high
+1);
936 void ExtractSkolemizer::storeExtract(TNode var
, unsigned high
, unsigned low
) {
937 Assert (var
.getMetaKind() == kind::metakind::VARIABLE
);
938 if (d_varToExtract
.find(var
) == d_varToExtract
.end()) {
939 d_varToExtract
[var
] = ExtractList(utils::getSize(var
));
941 VarExtractMap::iterator it
= d_varToExtract
.find(var
);
942 ExtractList
& el
= it
->second
;
943 Extract
e(high
, low
);
947 void ExtractSkolemizer::collectExtracts(TNode node
, TNodeSet
& seen
) {
948 if (seen
.find(node
) != seen
.end()) {
952 if (node
.getKind() == kind::BITVECTOR_EXTRACT
&&
953 node
[0].getMetaKind() == kind::metakind::VARIABLE
) {
954 unsigned high
= utils::getExtractHigh(node
);
955 unsigned low
= utils::getExtractLow(node
);
957 storeExtract(var
, high
, low
);
962 if (node
.getNumChildren() == 0)
965 for (unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
966 collectExtracts(node
[i
], seen
);
971 ExtractSkolemizer::ExtractSkolemizer(theory::SubstitutionMap
* modelMap
)
974 , d_modelMap(modelMap
)
975 , d_skolemSubst(&d_emptyContext
)
976 , d_skolemSubstRev(&d_emptyContext
)
979 ExtractSkolemizer::~ExtractSkolemizer() {
982 Node
mergeExplanations(const std::vector
<Node
>& expls
) {
984 for (unsigned i
= 0; i
< expls
.size(); ++i
) {
985 TNode expl
= expls
[i
];
986 Assert (expl
.getType().isBoolean());
987 if (expl
.getKind() == kind::AND
) {
988 for (unsigned i
= 0; i
< expl
.getNumChildren(); ++i
) {
989 TNode child
= expl
[i
];
990 if (child
== utils::mkTrue())
992 literals
.insert(child
);
994 } else if (expl
!= utils::mkTrue()) {
995 literals
.insert(expl
);
999 if (literals
.size() == 0) {
1000 return utils::mkTrue();
1001 }else if (literals
.size() == 1) {
1002 return *literals
.begin();
1005 NodeBuilder
<> nb(kind::AND
);
1007 for (TNodeSet::const_iterator it
= literals
.begin(); it
!= literals
.end(); ++it
) {
1013 Node
mergeExplanations(TNode expl1
, TNode expl2
) {
1014 std::vector
<Node
> expls
;
1015 expls
.push_back(expl1
);
1016 expls
.push_back(expl2
);
1017 return mergeExplanations(expls
);
1020 } /* namespace CVC4::theory::bv */
1021 } /* namespace CVc4::theory */
1022 } /* namespace CVC4 */