mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
change projection function
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
8b3abe120c
commit
8829fa96de
|
@ -325,20 +325,14 @@ namespace qe {
|
|||
TRACE("qe", tout << "unsat core: " << lits << "\n";);
|
||||
// optionally minimize core using superposition.
|
||||
return mbi_unsat;
|
||||
case l_true: {
|
||||
case l_true:
|
||||
m_solver->get_model(mdl);
|
||||
if (!get_literals(mdl, lits)) {
|
||||
return mbi_undef;
|
||||
}
|
||||
project0(mdl, lits);
|
||||
project(mdl, lits);
|
||||
return mbi_sat;
|
||||
}
|
||||
default:
|
||||
// TBD: if not running solver to completion, then:
|
||||
// 1. extract unit literals from m_solver.
|
||||
// 2. run a cc over the units
|
||||
// 3. extract equalities or other assignments over the congruence classes
|
||||
// 4. ensure that at least some progress is made over original lits.
|
||||
return mbi_undef;
|
||||
}
|
||||
}
|
||||
|
|
|
@ -774,11 +774,13 @@ namespace qe {
|
|||
TRACE("qe", tout << "literals: " << res << "\n";);
|
||||
}
|
||||
|
||||
void mk_distinct(expr_ref_vector& res) {
|
||||
vector<ptr_vector<term>> decl2terms; // terms that use function f
|
||||
ptr_vector<func_decl> decls;
|
||||
decl2terms.reset();
|
||||
vector<ptr_vector<term>> m_decl2terms; // terms that use function f
|
||||
ptr_vector<func_decl> m_decls;
|
||||
|
||||
void collect_decl2terms() {
|
||||
// Collect the projected function symbols.
|
||||
m_decl2terms.reset();
|
||||
m_decls.reset();
|
||||
for (term *t : m_tg.m_terms) {
|
||||
expr* e = t->get_expr();
|
||||
if (!is_app(e)) continue;
|
||||
|
@ -787,28 +789,45 @@ namespace qe {
|
|||
func_decl* d = a->get_decl();
|
||||
if (d->get_arity() == 0) continue;
|
||||
unsigned id = d->get_decl_id();
|
||||
decl2terms.reserve(id+1);
|
||||
if (decl2terms[id].empty()) decls.push_back(d);
|
||||
decl2terms[id].push_back(t);
|
||||
m_decl2terms.reserve(id+1);
|
||||
if (m_decl2terms[id].empty()) m_decls.push_back(d);
|
||||
m_decl2terms[id].push_back(t);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
void args_are_distinct(expr_ref_vector& res) {
|
||||
//
|
||||
// for each projected function that occurs
|
||||
// (may occur) in multiple congruence classes,
|
||||
// produce assertions that non-congruent arguments
|
||||
// are forced distinct.
|
||||
// are distinct.
|
||||
//
|
||||
for (func_decl* d : decls) {
|
||||
for (func_decl* d : m_decls) {
|
||||
unsigned id = d->get_decl_id();
|
||||
ptr_vector<term> const& terms = decl2terms[id];
|
||||
ptr_vector<term> const& terms = m_decl2terms[id];
|
||||
if (terms.size() <= 1) continue;
|
||||
unsigned arity = d->get_arity();
|
||||
for (unsigned i = 0; i < arity; ++i) {
|
||||
obj_hashtable<expr> roots;
|
||||
obj_hashtable<expr> roots, root_vals;
|
||||
expr_ref_vector pinned(m);
|
||||
for (term* t : terms) {
|
||||
expr* arg = to_app(t->get_expr())->get_arg(i);
|
||||
term const& root = m_tg.get_term(arg)->get_root();
|
||||
roots.insert(root.get_expr());
|
||||
expr* r = root.get_expr();
|
||||
// if a model is given, then use the equivalence class induced
|
||||
// by the model. Otherwise, use the congruence class.
|
||||
if (m_model) {
|
||||
expr_ref tmp(m);
|
||||
tmp = (*m_model)(r);
|
||||
if (!root_vals.contains(tmp)) {
|
||||
root_vals.insert(tmp);
|
||||
roots.insert(r);
|
||||
pinned.push_back(tmp);
|
||||
}
|
||||
}
|
||||
else {
|
||||
roots.insert(r);
|
||||
}
|
||||
}
|
||||
if (roots.size() > 1) {
|
||||
ptr_buffer<expr> args;
|
||||
|
@ -820,6 +839,11 @@ namespace qe {
|
|||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void mk_distinct(expr_ref_vector& res) {
|
||||
collect_decl2terms();
|
||||
args_are_distinct(res);
|
||||
TRACE("qe", tout << res << "\n";);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue