1 /********************* */
2 /*! \file bv_subtheory_algebraic.cpp
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Tim King, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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"
27 using namespace CVC4::context
;
28 using namespace CVC4::prop
;
29 using namespace CVC4::theory::bv::utils
;
37 bool hasExpensiveBVOperators(TNode fact
);
38 Node
mergeExplanations(const std::vector
<Node
>& expls
);
39 Node
mergeExplanations(TNode expl1
, TNode expl2
);
42 SubstitutionEx::SubstitutionEx(theory::SubstitutionMap
* modelMap
)
45 , d_cacheInvalid(true)
46 , d_modelMap(modelMap
)
49 bool SubstitutionEx::addSubstitution(TNode from
, TNode to
, TNode reason
) {
50 Debug("bv-substitution") << "SubstitutionEx::addSubstitution: "<< from
51 <<" => "<< to
<< "\n" << " reason "<<reason
<< "\n";
53 if (d_substitutions
.find(from
) != d_substitutions
.end()) {
57 d_modelMap
->addSubstitution(from
, to
);
59 d_cacheInvalid
= true;
60 d_substitutions
[from
] = SubstitutionElement(to
, reason
);
64 Node
SubstitutionEx::apply(TNode node
) {
65 Debug("bv-substitution") << "SubstitutionEx::apply("<< node
<<")\n";
68 d_cacheInvalid
= false;
71 SubstitutionsCache::iterator it
= d_cache
.find(node
);
73 if (it
!= d_cache
.end()) {
74 Node res
= it
->second
.to
;
75 Debug("bv-substitution") << " =>"<< res
<<"\n";
79 Node result
= internalApply(node
);
80 Debug("bv-substitution") << " =>"<< result
<<"\n";
84 Node
SubstitutionEx::internalApply(TNode node
) {
85 if (d_substitutions
.empty())
88 vector
<SubstitutionStackElement
> stack
;
89 stack
.push_back(SubstitutionStackElement(node
));
91 while (!stack
.empty()) {
92 SubstitutionStackElement head
= stack
.back();
95 TNode current
= head
.node
;
97 if (hasCache(current
)) {
101 // check if it has substitution
102 Substitutions::const_iterator it
= d_substitutions
.find(current
);
103 if (it
!= d_substitutions
.end()) {
104 vector
<Node
> reasons
;
105 TNode to
= it
->second
.to
;
106 reasons
.push_back(it
->second
.reason
);
107 // check if the thing we subsituted to has substitutions
108 TNode res
= internalApply(to
);
110 reasons
.push_back(getReason(to
));
111 Node reason
= mergeExplanations(reasons
);
112 storeCache(current
, res
, reason
);
116 // if no children then just continue
117 if(current
.getNumChildren() == 0) {
118 storeCache(current
, current
, utils::mkTrue());
122 // children already processed
123 if (head
.childrenAdded
) {
124 NodeBuilder
<> nb(current
.getKind());
125 std::vector
<Node
> reasons
;
127 if (current
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
128 TNode op
= current
.getOperator();
129 Assert (hasCache(op
));
131 reasons
.push_back(getReason(op
));
133 for (unsigned i
= 0; i
< current
.getNumChildren(); ++i
) {
134 Assert (hasCache(current
[i
]));
135 nb
<< getCache(current
[i
]);
136 reasons
.push_back(getReason(current
[i
]));
139 // if the node is new apply substitutions to it
140 Node subst_result
= result
;
141 if (result
!= current
) {
142 subst_result
= result
!= current
? internalApply(result
) : result
;
143 reasons
.push_back(getReason(result
));
145 Node reason
= mergeExplanations(reasons
);
146 storeCache(current
, subst_result
, reason
);
149 // add children to stack
150 stack
.push_back(SubstitutionStackElement(current
, true));
151 if (current
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
152 stack
.push_back(SubstitutionStackElement(current
.getOperator()));
154 for (unsigned i
= 0; i
< current
.getNumChildren(); ++i
) {
155 stack
.push_back(SubstitutionStackElement(current
[i
]));
160 Assert(hasCache(node
));
161 return getCache(node
);
164 Node
SubstitutionEx::explain(TNode node
) const {
165 if(!hasCache(node
)) {
166 return utils::mkTrue();
169 Debug("bv-substitution") << "SubstitutionEx::explain("<< node
<<")\n";
170 Node res
= getReason(node
);
171 Debug("bv-substitution") << " with "<< res
<<"\n";
175 Node
SubstitutionEx::getReason(TNode node
) const {
176 Assert(hasCache(node
));
177 SubstitutionsCache::const_iterator it
= d_cache
.find(node
);
178 return it
->second
.reason
;
181 bool SubstitutionEx::hasCache(TNode node
) const {
182 return d_cache
.find(node
) != d_cache
.end();
185 Node
SubstitutionEx::getCache(TNode node
) const {
186 Assert (hasCache(node
));
187 return d_cache
.find(node
)->second
.to
;
190 void SubstitutionEx::storeCache(TNode from
, TNode to
, Node reason
) {
191 // Debug("bv-substitution") << "SubstitutionEx::storeCache(" << from <<", " << to <<", "<< reason<<")\n";
192 Assert (!hasCache(from
));
193 d_cache
[from
] = SubstitutionElement(to
, reason
);
196 AlgebraicSolver::AlgebraicSolver(context::Context
* c
, TheoryBV
* bv
)
197 : SubtheorySolver(c
, bv
)
199 , d_quickSolver(new BVQuickCheck("alg", bv
))
200 , d_isComplete(c
, false)
201 , d_isDifficult(c
, false)
202 , d_budget(options::bitvectorAlgebraicBudget())
204 , d_inputAssertions()
208 , d_ctx(new context::Context())
209 , d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("alg", d_quickSolver
) : NULL
)
213 AlgebraicSolver::~AlgebraicSolver() {
214 if(d_modelMap
!= NULL
) { delete d_modelMap
; }
215 delete d_quickXplain
;
216 delete d_quickSolver
;
222 bool AlgebraicSolver::check(Theory::Effort e
) {
223 Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
);
225 if (!Theory::fullEffort(e
)) {
229 if (!useHeuristic()) {
235 TimerStat::CodeTimer
algebraicTimer(d_statistics
.d_solveTime
);
236 Debug("bv-subtheory-algebraic") << "AlgebraicSolver::check (" << e
<< ")\n";
237 ++(d_statistics
.d_numCallstoCheck
);
239 d_explanations
.clear();
241 d_inputAssertions
.clear();
243 std::vector
<WorklistElement
> worklist
;
245 uint64_t original_bb_cost
= 0;
247 NodeSet seen_assertions
;
248 // Processing assertions from scratch
249 for (AssertionQueue::const_iterator it
= assertionsBegin(); it
!= assertionsEnd(); ++it
) {
250 Debug("bv-subtheory-algebraic") << " " << *it
<< "\n";
251 TNode assertion
= *it
;
252 unsigned id
= worklist
.size();
253 d_ids
[assertion
] = id
;
254 worklist
.push_back(WorklistElement(assertion
, id
));
255 d_inputAssertions
.insert(assertion
);
256 storeExplanation(assertion
);
258 uint64_t assertion_size
= d_quickSolver
->computeAtomWeight(assertion
, seen_assertions
);
259 Assert (original_bb_cost
<= original_bb_cost
+ assertion_size
);
260 original_bb_cost
+= assertion_size
;
263 for (unsigned i
= 0; i
< worklist
.size(); ++i
) {
264 d_ids
[worklist
[i
].node
] = worklist
[i
].id
;
267 Debug("bv-subtheory-algebraic") << "Assertions " << worklist
.size() <<" : \n";
269 Assert (d_explanations
.size() == worklist
.size());
272 d_modelMap
= new SubstitutionMap(d_context
);
273 SubstitutionEx
subst(d_modelMap
);
275 // first round of substitutions
276 processAssertions(worklist
, subst
);
278 if (!d_isDifficult
.get()) {
279 // skolemize all possible extracts
280 ExtractSkolemizer
skolemizer(d_modelMap
);
281 skolemizer
.skolemize(worklist
);
282 // second round of substitutions
283 processAssertions(worklist
, subst
);
287 uint64_t subst_bb_cost
= 0;
292 for (; r
< worklist
.size(); ++r
) {
294 TNode fact
= worklist
[r
].node
;
295 unsigned id
= worklist
[r
].id
;
297 if (Dump
.isOn("bv-algebraic")) {
298 Node expl
= d_explanations
[id
];
299 Node query
= utils::mkNot(utils::mkNode(kind::IMPLIES
, expl
, fact
));
300 Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
301 Dump("bv-algebraic") << PushCommand();
302 Dump("bv-algebraic") << AssertCommand(query
.toExpr());
303 Dump("bv-algebraic") << CheckSatCommand();
304 Dump("bv-algebraic") << PopCommand();
307 if (fact
.isConst() &&
308 fact
.getConst
<bool>() == true) {
312 if (fact
.isConst() &&
313 fact
.getConst
<bool>() == false) {
314 // we have a conflict
315 Node conflict
= BooleanSimplification::simplify(d_explanations
[id
]);
316 d_bv
->setConflict(conflict
);
317 d_isComplete
.set(true);
318 Debug("bv-subtheory-algebraic") << " UNSAT: assertion simplfies to false with conflict: "<< conflict
<< "\n";
320 if (Dump
.isOn("bv-algebraic")) {
321 Dump("bv-algebraic") << EchoCommand("TheoryBV::AlgebraicSolver::conflict");
322 Dump("bv-algebraic") << PushCommand();
323 Dump("bv-algebraic") << AssertCommand(conflict
.toExpr());
324 Dump("bv-algebraic") << CheckSatCommand();
325 Dump("bv-algebraic") << PopCommand();
329 ++(d_statistics
.d_numSimplifiesToFalse
);
334 subst_bb_cost
+= d_quickSolver
->computeAtomWeight(fact
, subst_seen
);
335 worklist
[w
] = WorklistElement(fact
, id
);
336 Node expl
= BooleanSimplification::simplify(d_explanations
[id
]);
337 storeExplanation(id
, expl
);
345 if(Debug
.isOn("bv-subtheory-algebraic")) {
346 Debug("bv-subtheory-algebraic") << "Assertions post-substitutions " << worklist
.size() << ":\n";
347 for (unsigned i
= 0; i
< worklist
.size(); ++i
) {
348 Debug("bv-subtheory-algebraic") << " " << worklist
[i
].node
<< "\n";
353 // all facts solved to true
354 if (worklist
.empty()) {
355 Debug("bv-subtheory-algebraic") << " SAT: everything simplifies to true.\n";
356 ++(d_statistics
.d_numSimplifiesToTrue
);
361 double ratio
= ((double)subst_bb_cost
)/original_bb_cost
;
363 !d_isDifficult
.get()) {
364 // give up if problem not reduced enough
365 d_isComplete
.set(false);
369 d_quickSolver
->clearSolver();
371 d_quickSolver
->push();
372 std::vector
<Node
> facts
;
373 for (unsigned i
= 0; i
< worklist
.size(); ++i
) {
374 facts
.push_back(worklist
[i
].node
);
376 bool ok
= quickCheck(facts
);
378 Debug("bv-subtheory-algebraic") << "AlgebraicSolver::check done " << ok
<< ".\n";
382 bool AlgebraicSolver::quickCheck(std::vector
<Node
>& facts
) {
383 SatValue res
= d_quickSolver
->checkSat(facts
, d_budget
);
385 if (res
== SAT_VALUE_UNKNOWN
) {
386 d_isComplete
.set(false);
387 Debug("bv-subtheory-algebraic") << " Unknown.\n";
388 ++(d_statistics
.d_numUnknown
);
392 if (res
== SAT_VALUE_TRUE
) {
393 Debug("bv-subtheory-algebraic") << " Sat.\n";
394 ++(d_statistics
.d_numSat
);
396 d_isComplete
.set(true);
400 Assert (res
== SAT_VALUE_FALSE
);
401 Assert (d_quickSolver
->inConflict());
402 d_isComplete
.set(true);
403 Debug("bv-subtheory-algebraic") << " Unsat.\n";
405 ++(d_statistics
.d_numUnsat
);
408 Node conflict
= d_quickSolver
->getConflict();
409 Debug("bv-subtheory-algebraic") << " Conflict: " << conflict
<< "\n";
411 // singleton conflict
412 if (conflict
.getKind() != kind::AND
) {
413 Assert (d_ids
.find(conflict
) != d_ids
.end());
414 unsigned id
= d_ids
[conflict
];
415 Assert (id
< d_explanations
.size());
416 Node theory_confl
= d_explanations
[id
];
417 d_bv
->setConflict(theory_confl
);
421 Assert (conflict
.getKind() == kind::AND
);
422 if (options::bitvectorQuickXplain()) {
423 d_quickSolver
->popToZero();
424 Debug("bv-quick-xplain") << "AlgebraicSolver::quickCheck original conflict size " << conflict
.getNumChildren() << "\n";
425 conflict
= d_quickXplain
->minimizeConflict(conflict
);
426 Debug("bv-quick-xplain") << "AlgebraicSolver::quickCheck minimized conflict size " << conflict
.getNumChildren() << "\n";
429 vector
<TNode
> theory_confl
;
430 for (unsigned i
= 0; i
< conflict
.getNumChildren(); ++i
) {
431 TNode c
= conflict
[i
];
433 Assert (d_ids
.find(c
) != d_ids
.end());
434 unsigned c_id
= d_ids
[c
];
435 Assert (c_id
< d_explanations
.size());
436 TNode c_expl
= d_explanations
[c_id
];
437 theory_confl
.push_back(c_expl
);
440 Node confl
= BooleanSimplification::simplify(utils::mkAnd(theory_confl
));
442 Debug("bv-subtheory-algebraic") << " Out Conflict: " << confl
<< "\n";
447 void AlgebraicSolver::setConflict(TNode conflict
) {
448 Node final_conflict
= conflict
;
449 if (options::bitvectorQuickXplain() &&
450 conflict
.getKind() == kind::AND
&&
451 conflict
.getNumChildren() > 4) {
452 final_conflict
= d_quickXplain
->minimizeConflict(conflict
);
454 d_bv
->setConflict(final_conflict
);
457 bool AlgebraicSolver::solve(TNode fact
, TNode reason
, SubstitutionEx
& subst
) {
458 if (fact
.getKind() != kind::EQUAL
) return false;
460 TNode left
= fact
[0];
461 TNode right
= fact
[1];
464 if (left
.isVar() && !right
.hasSubterm(left
)) {
465 bool changed
= subst
.addSubstitution(left
, right
, reason
);
468 if (right
.isVar() && !left
.hasSubterm(right
)) {
469 bool changed
= subst
.addSubstitution(right
, left
, reason
);
473 // xor simplification
474 if (right
.getKind() == kind::BITVECTOR_XOR
&&
475 left
.getKind() == kind::BITVECTOR_XOR
) {
477 if (var
.getMetaKind() != kind::metakind::VARIABLE
)
480 // simplify xor with same variable on both sides
481 if (right
.hasSubterm(var
)) {
482 std::vector
<Node
> right_children
;
483 for (unsigned i
= 0; i
< right
.getNumChildren(); ++i
) {
485 right_children
.push_back(right
[i
]);
487 Assert (right_children
.size());
488 Node new_right
= right_children
.size() > 1 ? utils::mkNode(kind::BITVECTOR_XOR
, right_children
)
490 std::vector
<Node
> left_children
;
491 for (unsigned i
= 1; i
< left
.getNumChildren(); ++i
) {
492 left_children
.push_back(left
[i
]);
494 Node new_left
= left_children
.size() > 1 ? utils::mkNode(kind::BITVECTOR_XOR
, left_children
)
496 Node new_fact
= utils::mkNode(kind::EQUAL
, new_left
, new_right
);
497 bool changed
= subst
.addSubstitution(fact
, new_fact
, reason
);
501 NodeBuilder
<> nb(kind::BITVECTOR_XOR
);
502 for (unsigned i
= 1; i
< left
.getNumChildren(); ++i
) {
505 Node inverse
= left
.getNumChildren() == 2? (Node
)left
[1] : (Node
)nb
;
506 Node new_right
= utils::mkNode(kind::BITVECTOR_XOR
, right
, inverse
);
507 bool changed
= subst
.addSubstitution(var
, new_right
, reason
);
509 if (Dump
.isOn("bv-algebraic")) {
510 Node query
= utils::mkNot(utils::mkNode(kind::IFF
, fact
, utils::mkNode(kind::EQUAL
, var
, new_right
)));
511 Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
512 Dump("bv-algebraic") << PushCommand();
513 Dump("bv-algebraic") << AssertCommand(query
.toExpr());
514 Dump("bv-algebraic") << CheckSatCommand();
515 Dump("bv-algebraic") << PopCommand();
522 // (a xor t = a) <=> (t = 0)
523 if (left
.getKind() == kind::BITVECTOR_XOR
&&
524 right
.getMetaKind() == kind::metakind::VARIABLE
&&
525 left
.hasSubterm(right
)) {
527 Node new_left
= utils::mkNode(kind::BITVECTOR_XOR
, var
, left
);
528 Node zero
= utils::mkConst(utils::getSize(var
), 0u);
529 Node new_fact
= utils::mkNode(kind::EQUAL
, zero
, new_left
);
530 bool changed
= subst
.addSubstitution(fact
, new_fact
, reason
);
534 if (right
.getKind() == kind::BITVECTOR_XOR
&&
535 left
.getMetaKind() == kind::metakind::VARIABLE
&&
536 right
.hasSubterm(left
)) {
538 Node new_right
= utils::mkNode(kind::BITVECTOR_XOR
, var
, right
);
539 Node zero
= utils::mkConst(utils::getSize(var
), 0u);
540 Node new_fact
= utils::mkNode(kind::EQUAL
, zero
, new_right
);
541 bool changed
= subst
.addSubstitution(fact
, new_fact
, reason
);
545 // (a xor b = 0) <=> (a = b)
546 if (left
.getKind() == kind::BITVECTOR_XOR
&&
547 left
.getNumChildren() == 2 &&
548 right
.getKind() == kind::CONST_BITVECTOR
&&
549 right
.getConst
<BitVector
>() == BitVector(utils::getSize(left
), 0u)) {
550 Node new_fact
= utils::mkNode(kind::EQUAL
, left
[0], left
[1]);
551 bool changed
= subst
.addSubstitution(fact
, new_fact
, reason
);
559 bool AlgebraicSolver::isSubstitutableIn(TNode node
, TNode in
) {
560 if (node
.getMetaKind() == kind::metakind::VARIABLE
&&
561 !in
.hasSubterm(node
))
566 void AlgebraicSolver::processAssertions(std::vector
<WorklistElement
>& worklist
, SubstitutionEx
& subst
) {
569 // d_bv->spendResource();
571 for (unsigned i
= 0; i
< worklist
.size(); ++i
) {
572 // apply current substitutions
573 Node current
= subst
.apply(worklist
[i
].node
);
574 unsigned current_id
= worklist
[i
].id
;
575 Node subst_expl
= subst
.explain(worklist
[i
].node
);
576 worklist
[i
] = WorklistElement(Rewriter::rewrite(current
), current_id
);
577 // explanation for this assertion
578 Node old_expl
= d_explanations
[current_id
];
579 Node new_expl
= mergeExplanations(subst_expl
, old_expl
);
580 storeExplanation(current_id
, new_expl
);
582 // use the new substitution to solve
583 if(solve(worklist
[i
].node
, new_expl
, subst
)) {
588 // check for concat slicings
589 for (unsigned i
= 0; i
< worklist
.size(); ++i
) {
590 TNode fact
= worklist
[i
].node
;
591 unsigned current_id
= worklist
[i
].id
;
593 if (fact
.getKind() != kind::EQUAL
) {
597 TNode left
= fact
[0];
598 TNode right
= fact
[1];
599 if (left
.getKind() != kind::BITVECTOR_CONCAT
||
600 right
.getKind() != kind::BITVECTOR_CONCAT
||
601 left
.getNumChildren() != right
.getNumChildren()) {
605 bool can_slice
= true;
606 for (unsigned j
= 0; j
< left
.getNumChildren(); ++j
) {
607 if (utils::getSize(left
[j
]) != utils::getSize(right
[j
]))
615 for (unsigned j
= 0; j
< left
.getNumChildren(); ++j
) {
616 Node eq_j
= utils::mkNode(kind::EQUAL
, left
[j
], right
[j
]);
617 unsigned id
= d_explanations
.size();
618 TNode expl
= d_explanations
[current_id
];
619 storeExplanation(expl
);
620 worklist
.push_back(WorklistElement(eq_j
, id
));
623 worklist
[i
] = WorklistElement(utils::mkTrue(), worklist
[i
].id
);
626 Assert (d_explanations
.size() == worklist
.size());
630 void AlgebraicSolver::storeExplanation(unsigned id
, TNode explanation
) {
631 Assert (checkExplanation(explanation
));
632 d_explanations
[id
] = explanation
;
635 void AlgebraicSolver::storeExplanation(TNode explanation
) {
636 Assert (checkExplanation(explanation
));
637 d_explanations
.push_back(explanation
);
640 bool AlgebraicSolver::checkExplanation(TNode explanation
) {
641 Node simplified_explanation
= explanation
; //BooleanSimplification::simplify(explanation);
642 if (simplified_explanation
.getKind() != kind::AND
) {
643 return d_inputAssertions
.find(simplified_explanation
) != d_inputAssertions
.end();
645 for (unsigned i
= 0; i
< simplified_explanation
.getNumChildren(); ++i
) {
646 if (d_inputAssertions
.find(simplified_explanation
[i
]) == d_inputAssertions
.end()) {
654 bool AlgebraicSolver::isComplete() {
655 return d_isComplete
.get();
658 bool AlgebraicSolver::useHeuristic() {
662 double success_rate
= double(d_numSolved
)/double(d_numCalls
);
663 d_statistics
.d_useHeuristic
.setData(success_rate
);
664 return success_rate
> 0.8;
668 void AlgebraicSolver::assertFact(TNode fact
) {
669 d_assertionQueue
.push_back(fact
);
670 d_isComplete
.set(false);
671 if (!d_isDifficult
.get()) {
672 d_isDifficult
.set(hasExpensiveBVOperators(fact
));
676 EqualityStatus
AlgebraicSolver::getEqualityStatus(TNode a
, TNode b
) {
677 return EQUALITY_UNKNOWN
;
679 void AlgebraicSolver::collectModelInfo(TheoryModel
* model
, bool fullModel
) {
680 Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n";
681 AlwaysAssert (!d_quickSolver
->inConflict());
683 d_bv
->computeRelevantTerms(termSet
);
685 // collect relevant terms that the bv theory abstracts to variables
686 // (variables and parametric terms such as select apply_uf)
687 std::vector
<TNode
> variables
;
688 std::vector
<Node
> values
;
689 for (set
<Node
>::const_iterator it
= termSet
.begin(); it
!= termSet
.end(); ++it
) {
691 if (term
.getType().isBitVector() &&
692 (term
.getMetaKind() == kind::metakind::VARIABLE
||
693 Theory::theoryOf(term
) != THEORY_BV
)) {
694 variables
.push_back(term
);
695 values
.push_back(term
);
700 Debug("bitvector-model") << "Substitutions:\n";
701 for (unsigned i
= 0; i
< variables
.size(); ++i
) {
702 TNode current
= variables
[i
];
703 TNode subst
= Rewriter::rewrite(d_modelMap
->apply(current
));
704 Debug("bitvector-model") << " " << current
<< " => " << subst
<< "\n";
706 utils::collectVariables(subst
, leaf_vars
);
709 Debug("bitvector-model") << "Model:\n";
711 for (NodeSet::const_iterator it
= leaf_vars
.begin(); it
!= leaf_vars
.end(); ++it
) {
713 Node value
= d_quickSolver
->getVarValue(var
, true);
714 Assert (!value
.isNull() || !fullModel
);
716 // may be a shared term that did not appear in the current assertions
717 if (!value
.isNull()) {
718 Debug("bitvector-model") << " " << var
<< " => " << value
<< "\n";
719 Assert (value
.getKind() == kind::CONST_BITVECTOR
);
720 d_modelMap
->addSubstitution(var
, value
);
724 Debug("bitvector-model") << "Final Model:\n";
725 for (unsigned i
= 0; i
< variables
.size(); ++i
) {
726 TNode current
= values
[i
];
727 TNode subst
= Rewriter::rewrite(d_modelMap
->apply(current
));
728 Debug("bitvector-model") << "AlgebraicSolver: " << variables
[i
] << " => " << subst
<< "\n";
729 // Doesn't have to be constant as it may be irrelevant
730 Assert (subst
.getKind() == kind::CONST_BITVECTOR
);
731 model
->assertEquality(variables
[i
], subst
, true);
736 Node
AlgebraicSolver::getModelValue(TNode node
) {
740 AlgebraicSolver::Statistics::Statistics()
741 : d_numCallstoCheck("theory::bv::AlgebraicSolver::NumCallsToCheck", 0)
742 , d_numSimplifiesToTrue("theory::bv::AlgebraicSolver::NumSimplifiesToTrue", 0)
743 , d_numSimplifiesToFalse("theory::bv::AlgebraicSolver::NumSimplifiesToFalse", 0)
744 , d_numUnsat("theory::bv::AlgebraicSolver::NumUnsat", 0)
745 , d_numSat("theory::bv::AlgebraicSolver::NumSat", 0)
746 , d_numUnknown("theory::bv::AlgebraicSolver::NumUnknown", 0)
747 , d_solveTime("theory::bv::AlgebraicSolver::SolveTime")
748 , d_useHeuristic("theory::bv::AlgebraicSolver::UseHeuristic", 0.2)
750 smtStatisticsRegistry()->registerStat(&d_numCallstoCheck
);
751 smtStatisticsRegistry()->registerStat(&d_numSimplifiesToTrue
);
752 smtStatisticsRegistry()->registerStat(&d_numSimplifiesToFalse
);
753 smtStatisticsRegistry()->registerStat(&d_numUnsat
);
754 smtStatisticsRegistry()->registerStat(&d_numSat
);
755 smtStatisticsRegistry()->registerStat(&d_numUnknown
);
756 smtStatisticsRegistry()->registerStat(&d_solveTime
);
757 smtStatisticsRegistry()->registerStat(&d_useHeuristic
);
760 AlgebraicSolver::Statistics::~Statistics() {
761 smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck
);
762 smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToTrue
);
763 smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToFalse
);
764 smtStatisticsRegistry()->unregisterStat(&d_numUnsat
);
765 smtStatisticsRegistry()->unregisterStat(&d_numSat
);
766 smtStatisticsRegistry()->unregisterStat(&d_numUnknown
);
767 smtStatisticsRegistry()->unregisterStat(&d_solveTime
);
768 smtStatisticsRegistry()->unregisterStat(&d_useHeuristic
);
771 bool hasExpensiveBVOperatorsRec(TNode fact
, TNodeSet
& seen
) {
772 if (fact
.getKind() == kind::BITVECTOR_MULT
||
773 fact
.getKind() == kind::BITVECTOR_UDIV_TOTAL
||
774 fact
.getKind() == kind::BITVECTOR_UREM_TOTAL
) {
778 if (seen
.find(fact
) != seen
.end()) {
782 if (fact
.getNumChildren() == 0) {
785 for (unsigned i
= 0; i
< fact
.getNumChildren(); ++i
) {
786 bool difficult
= hasExpensiveBVOperatorsRec(fact
[i
], seen
);
794 bool hasExpensiveBVOperators(TNode fact
) {
796 return hasExpensiveBVOperatorsRec(fact
, seen
);
799 void ExtractSkolemizer::skolemize(std::vector
<WorklistElement
>& facts
) {
801 for (unsigned i
= 0; i
< facts
.size(); ++i
) {
802 TNode current
= facts
[i
].node
;
803 collectExtracts(current
, seen
);
806 for (VarExtractMap::iterator it
= d_varToExtract
.begin(); it
!= d_varToExtract
.end(); ++it
) {
807 ExtractList
& el
= it
->second
;
808 TNode var
= it
->first
;
809 Base
& base
= el
.base
;
811 unsigned bw
= utils::getSize(var
);
812 // compute decomposition
813 std::vector
<unsigned> cuts
;
814 for (unsigned i
= 1; i
<= bw
; ++i
) {
815 if (base
.isCutPoint(i
)) {
819 unsigned previous
= 0;
820 unsigned current
= 0;
821 std::vector
<Node
> skolems
;
822 for (unsigned i
= 0; i
< cuts
.size(); ++i
) {
824 Assert (current
> 0);
825 int size
= current
- previous
;
827 Node sk
= utils::mkVar(size
);
828 skolems
.push_back(sk
);
831 if (current
< bw
-1) {
832 int size
= bw
- current
;
834 Node sk
= utils::mkVar(size
);
835 skolems
.push_back(sk
);
837 NodeBuilder
<> skolem_nb(kind::BITVECTOR_CONCAT
);
839 for (int i
= skolems
.size() - 1; i
>= 0; --i
) {
840 skolem_nb
<< skolems
[i
];
843 Node skolem_concat
= skolems
.size() == 1 ? (Node
)skolems
[0] : (Node
) skolem_nb
;
844 Assert (utils::getSize(skolem_concat
) == utils::getSize(var
));
845 storeSkolem(var
, skolem_concat
);
847 for (unsigned i
= 0; i
< el
.extracts
.size(); ++i
) {
848 unsigned h
= el
.extracts
[i
].high
;
849 unsigned l
= el
.extracts
[i
].low
;
850 Node extract
= utils::mkExtract(var
, h
, l
);
851 Node skolem_extract
= Rewriter::rewrite(utils::mkExtract(skolem_concat
, h
, l
));
852 Assert (skolem_extract
.getMetaKind() == kind::metakind::VARIABLE
||
853 skolem_extract
.getKind() == kind::BITVECTOR_CONCAT
);
854 storeSkolem(extract
, skolem_extract
);
858 for (unsigned i
= 0; i
< facts
.size(); ++i
) {
859 facts
[i
] = WorklistElement(skolemize(facts
[i
].node
), facts
[i
].id
);
863 Node
ExtractSkolemizer::mkSkolem(Node node
) {
864 Assert (node
.getKind() == kind::BITVECTOR_EXTRACT
&&
865 node
[0].getMetaKind() == kind::metakind::VARIABLE
);
866 Assert (!d_skolemSubst
.hasSubstitution(node
));
867 return utils::mkVar(utils::getSize(node
));
870 void ExtractSkolemizer::unSkolemize(std::vector
<WorklistElement
>& facts
) {
871 for (unsigned i
= 0; i
< facts
.size(); ++i
) {
872 facts
[i
] = WorklistElement(unSkolemize(facts
[i
].node
), facts
[i
].id
);
876 void ExtractSkolemizer::storeSkolem(TNode node
, TNode skolem
) {
877 d_skolemSubst
.addSubstitution(node
, skolem
);
878 d_modelMap
->addSubstitution(node
, skolem
);
879 d_skolemSubstRev
.addSubstitution(skolem
, node
);
882 Node
ExtractSkolemizer::unSkolemize(TNode node
) {
883 return d_skolemSubstRev
.apply(node
);
886 Node
ExtractSkolemizer::skolemize(TNode node
) {
887 return d_skolemSubst
.apply(node
);
890 void ExtractSkolemizer::ExtractList::addExtract(Extract
& e
) {
891 extracts
.push_back(e
);
893 base
.sliceAt(e
.high
+1);
896 void ExtractSkolemizer::storeExtract(TNode var
, unsigned high
, unsigned low
) {
897 Assert (var
.getMetaKind() == kind::metakind::VARIABLE
);
898 if (d_varToExtract
.find(var
) == d_varToExtract
.end()) {
899 d_varToExtract
[var
] = ExtractList(utils::getSize(var
));
901 VarExtractMap::iterator it
= d_varToExtract
.find(var
);
902 ExtractList
& el
= it
->second
;
903 Extract
e(high
, low
);
907 void ExtractSkolemizer::collectExtracts(TNode node
, TNodeSet
& seen
) {
908 if (seen
.find(node
) != seen
.end()) {
912 if (node
.getKind() == kind::BITVECTOR_EXTRACT
&&
913 node
[0].getMetaKind() == kind::metakind::VARIABLE
) {
914 unsigned high
= utils::getExtractHigh(node
);
915 unsigned low
= utils::getExtractLow(node
);
917 storeExtract(var
, high
, low
);
922 if (node
.getNumChildren() == 0)
925 for (unsigned i
= 0; i
< node
.getNumChildren(); ++i
) {
926 collectExtracts(node
[i
], seen
);
931 ExtractSkolemizer::ExtractSkolemizer(theory::SubstitutionMap
* modelMap
)
934 , d_modelMap(modelMap
)
935 , d_skolemSubst(&d_emptyContext
)
936 , d_skolemSubstRev(&d_emptyContext
)
939 ExtractSkolemizer::~ExtractSkolemizer() {
942 Node
mergeExplanations(const std::vector
<Node
>& expls
) {
944 for (unsigned i
= 0; i
< expls
.size(); ++i
) {
945 TNode expl
= expls
[i
];
946 Assert (expl
.getType().isBoolean());
947 if (expl
.getKind() == kind::AND
) {
948 for (unsigned i
= 0; i
< expl
.getNumChildren(); ++i
) {
949 TNode child
= expl
[i
];
950 if (child
== utils::mkTrue())
952 literals
.insert(child
);
954 } else if (expl
!= utils::mkTrue()) {
955 literals
.insert(expl
);
959 if (literals
.size() == 0) {
960 return utils::mkTrue();
961 }else if (literals
.size() == 1) {
962 return *literals
.begin();
965 NodeBuilder
<> nb(kind::AND
);
967 for (TNodeSet::const_iterator it
= literals
.begin(); it
!= literals
.end(); ++it
) {
973 Node
mergeExplanations(TNode expl1
, TNode expl2
) {
974 std::vector
<Node
> expls
;
975 expls
.push_back(expl1
);
976 expls
.push_back(expl2
);
977 return mergeExplanations(expls
);
980 } /* namespace CVC4::theory::bv */
981 } /* namespace CVc4::theory */
982 } /* namespace CVC4 */