mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix a few bugs, debugging eufi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ba504e4243
commit
6d79b19170
|
@ -116,7 +116,7 @@ namespace qe {
|
|||
m_dual_solver(sNot)
|
||||
{
|
||||
params_ref p;
|
||||
p.set_bool("smt.core.minimize", true);
|
||||
p.set_bool("core.minimize", true);
|
||||
m_solver->updt_params(p);
|
||||
m_dual_solver->updt_params(p);
|
||||
expr_ref_vector fmls(m);
|
||||
|
|
|
@ -625,7 +625,7 @@ namespace qe {
|
|||
|
||||
expr_ref_vector m_pinned; // tracks expr in the maps
|
||||
|
||||
expr* mk_pure(term& t) {
|
||||
expr* mk_pure(term const& t) {
|
||||
expr* e = nullptr;
|
||||
if (m_term2app.find(t.get_id(), e)) return e;
|
||||
e = t.get_expr();
|
||||
|
@ -643,7 +643,7 @@ namespace qe {
|
|||
}
|
||||
|
||||
bool is_better_rep(expr *t1, expr *t2) {
|
||||
if (!t2) return t1;
|
||||
if (!t2) return t1 != nullptr;
|
||||
return m.is_unique_value(t1) && !m.is_unique_value(t2);
|
||||
}
|
||||
|
||||
|
@ -755,13 +755,21 @@ namespace qe {
|
|||
}
|
||||
|
||||
void mk_pure_equalities(const term &t, expr_ref_vector &res) {
|
||||
SASSERT(t.is_root());
|
||||
expr *rep = nullptr;
|
||||
if (!m_root2rep.find(t.get_id(), rep)) return;
|
||||
for (term *it = &t.get_next(); it != &t; it = &it->get_next()) {
|
||||
expr* member = mk_pure(*it);
|
||||
if (member)
|
||||
obj_hashtable<expr> members;
|
||||
members.insert(rep);
|
||||
term const * r = &t;
|
||||
do {
|
||||
expr* member = nullptr;
|
||||
if (m_term2app.find(r->get_id(), member) && !members.contains(member)) {
|
||||
res.push_back (m.mk_eq (rep, member));
|
||||
members.insert(member);
|
||||
}
|
||||
r = &r->get_next();
|
||||
}
|
||||
while (r != &t);
|
||||
}
|
||||
|
||||
bool is_projected(const term &t) {
|
||||
|
@ -771,13 +779,17 @@ namespace qe {
|
|||
void mk_unpure_equalities(const term &t, expr_ref_vector &res) {
|
||||
expr *rep = nullptr;
|
||||
if (!m_root2rep.find(t.get_id(), rep)) return;
|
||||
for (term *it = &t.get_next(); it != &t; it = &it->get_next()) {
|
||||
expr* member = mk_pure(*it);
|
||||
obj_hashtable<expr> members;
|
||||
term const * r = &t;
|
||||
do {
|
||||
expr* member = mk_pure(*r);
|
||||
SASSERT(member);
|
||||
if (!is_projected(*it) || !is_solved_eq(rep, member)) {
|
||||
if (member != rep && (!is_projected(*r) || !is_solved_eq(rep, member))) {
|
||||
res.push_back(m.mk_eq(rep, member));
|
||||
}
|
||||
r = &r->get_next();
|
||||
}
|
||||
while (r != &t);
|
||||
}
|
||||
|
||||
void mk_equalities(bool pure, expr_ref_vector &res) {
|
||||
|
|
|
@ -50,12 +50,12 @@ struct mus::imp {
|
|||
}
|
||||
|
||||
bool is_literal(expr* lit) const {
|
||||
expr* l;
|
||||
expr* l;
|
||||
return is_uninterp_const(lit) || (m.is_not(lit, l) && is_uninterp_const(l));
|
||||
}
|
||||
|
||||
unsigned add_soft(expr* lit) {
|
||||
SASSERT(is_literal(lit));
|
||||
//SASSERT(is_literal(lit));
|
||||
unsigned idx = m_lit2expr.size();
|
||||
m_expr2lit.insert(lit, idx);
|
||||
m_lit2expr.push_back(lit);
|
||||
|
|
Loading…
Reference in a new issue