mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 13:51:23 +00:00
Code Activity

Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-02-24 17:04:01 -08:00
commit dffb0ff844
2 changed files with 14 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/muz/base/proof_utils.cpp
View file

@ -156,12 +156,22 @@ public:
SASSERT(m.get_num_parents(p) == 1); SASSERT(m.get_num_parents(p) == 1);
tmp = m.get_parent(p, 0); tmp = m.get_parent(p, 0);
elim(tmp); elim(tmp);
get_literals(m.get_fact(p));
expr_set* hyps = m_hypmap.find(tmp); expr_set* hyps = m_hypmap.find(tmp);
expr_set* new_hyps = 0; expr_set* new_hyps = 0;
if (hyps) { if (hyps) {
new_hyps = alloc(expr_set, *hyps); new_hyps = alloc(expr_set, *hyps);
} }
expr* fact = m.get_fact(p);
// when hypothesis is a single literal of the form
// (or A B), and the fact of p is (or A B).
if (hyps && hyps->size() == 1 && in_hypotheses(fact, hyps)) {
m_literals.reset();
m_literals.push_back(fact);
}
else {
get_literals(fact);
}
for (unsigned i = 0; i < m_literals.size(); ++i) { for (unsigned i = 0; i < m_literals.size(); ++i) {
expr* e = m_literals[i]; expr* e = m_literals[i];
if (!in_hypotheses(e, hyps)) { if (!in_hypotheses(e, hyps)) {

3
src/opt/opt_context.cpp
View file

@ -533,6 +533,9 @@ namespace opt {
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
quick_for_each_expr(proc, visited, get_solver().get_assertion(i)); quick_for_each_expr(proc, visited, get_solver().get_assertion(i));
} }
for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
quick_for_each_expr(proc, visited, m_hard_constraints[i].get());
}
} }
catch (is_bv::found) { catch (is_bv::found) {
return false; return false;