mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

bug fixes and cleanup in projection functions

Browse source 
spacer would drop variables of sorts not handled by main loop.
- projection with witness needs to disable qel style preprocessing to ensure witnesses are returned.
- add euf plugin to handle uninterpreted sorts (and then uninterpreted functions)
This commit is contained in:
Nikolaj Bjorner 2025-02-15 14:11:20 -08:00
parent 0cf2b5f515
commit eee96ec312
12 changed files with 249 additions and 108 deletions
Download patch file Download diff file Expand all files Collapse all files

4
genaisrc/.gitignore vendored Normal file
View file

@ -0,0 +1,4 @@
# auto-generated
genaiscript.d.ts
tsconfig.json
jsconfig.json

79
src/muz/spacer/spacer_util.cpp
View file

@ -152,6 +152,7 @@ void qe_project_z3(ast_manager &m, app_ref_vector &vars, expr_ref &fml,
params_ref p;
p.set_bool("reduce_all_selects", reduce_all_selects);
p.set_bool("dont_sub", dont_sub);
TRACE("qe", tout << "qe-project-z3\n");
qe::mbproj mbp(m, p);
mbp.spacer(vars, mdl, fml);
@ -167,8 +168,7 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml,
bool dont_sub) {
th_rewriter rw(m);
TRACE("spacer_mbp", tout << "Before projection:\n"; tout << fml << "\n";
tout << "Vars:\n"
<< vars;);
tout << "Vars:" << vars << "\n";);
{
// Ensure that top-level AND of fml is flat
@ -182,6 +182,7 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml,
app_ref_vector arith_vars(m);
app_ref_vector array_vars(m);
app_ref_vector other_vars(m);
array_util arr_u(m);
arith_util ari_u(m);
expr_safe_replace bool_sub(m);
@ -194,8 +195,7 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml,
rw(fml);
TRACE("spacer_mbp", tout << "After qe_lite:\n";
tout << mk_pp(fml, m) << "\n"; tout << "Vars:\n"
<< vars;);
tout << mk_pp(fml, m) << "\nVars:" << vars << "\n";);
SASSERT(!m.is_false(fml));
@ -206,12 +206,13 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml,
// using model completion
model::scoped_model_completion _sc_(mdl, true);
bool_sub.insert(v, mdl(v));
} else if (arr_u.is_array(v)) {
array_vars.push_back(v);
} else {
SASSERT(ari_u.is_int(v) || ari_u.is_real(v));
arith_vars.push_back(v);
}
else if (arr_u.is_array(v))
array_vars.push_back(v);
else if (ari_u.is_int(v) || ari_u.is_real(v))
arith_vars.push_back(v);
else
other_vars.push_back(v);
}
// substitute Booleans
@ -220,8 +221,7 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml,
// -- bool_sub is not simplifying
rw(fml);
SASSERT(!m.is_false(fml));
TRACE("spacer_mbp", tout << "Projected Booleans:\n"
<< fml << "\n";);
TRACE("spacer_mbp", tout << "Projected Booleans:\n" << fml << "\n";);
bool_sub.reset();
}
@ -230,7 +230,7 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml,
vars.reset();
// project arrays
{
if (!array_vars.empty()) {
scoped_no_proof _sp(m);
// -- local rewriter that is aware of current proof mode
th_rewriter srw(m);
@ -243,14 +243,15 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml,
TRACE("spacer_mbp", tout << "extended model:\n"; model_pp(tout, mdl);
tout << "Auxiliary variables of index and value sorts:\n";
tout << vars;);
tout << vars << "\n";);
if (vars.empty()) { break; }
if (vars.empty())
break;
}
// project reals and ints
if (!arith_vars.empty()) {
TRACE("spacer_mbp", tout << "Arith vars:\n" << arith_vars;);
TRACE("spacer_mbp", tout << "Arith vars:" << arith_vars << "\n";);
if (use_native_mbp) {
qe::mbproj mbp(m);
@ -260,19 +261,19 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml,
mbp(true, arith_vars, mdl, fmls);
fml = mk_and(fmls);
SASSERT(arith_vars.empty());
} else {
}
else {
scoped_no_proof _sp(m);
spacer_qe::arith_project(mdl, arith_vars, fml);
}
TRACE("spacer_mbp", tout << "Projected arith vars:\n"
<< fml << "\n";
tout << "Remaining arith vars:\n"
<< arith_vars << "\n";);
TRACE("spacer_mbp", tout << "Projected arith vars: "<< fml << "\n";
tout << "Remaining arith vars:" << arith_vars << "\n";);
SASSERT(!m.is_false(fml));
}
if (!arith_vars.empty()) { mbqi_project(mdl, arith_vars, fml); }
if (!arith_vars.empty())
mbqi_project(mdl, arith_vars, fml);
// substitute any remaining arith vars
if (!dont_sub && !arith_vars.empty()) {
@ -289,26 +290,30 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml,
SASSERT(mev.is_true(fml)););
vars.reset();
if (dont_sub && !arith_vars.empty()) { vars.append(arith_vars); }
vars.append(other_vars);
if (dont_sub && !arith_vars.empty())
vars.append(arith_vars);
TRACE("qe", tout << "after projection: " << fml << ": " << vars << "\n");
}
static expr *apply_accessor(ast_manager &m, ptr_vector<func_decl> const &acc,
unsigned j, func_decl *f, expr *c) {
if (is_app(c) && to_app(c)->get_decl() == f) {
if (is_app(c) && to_app(c)->get_decl() == f)
return to_app(c)->get_arg(j);
} else {
else
return m.mk_app(acc[j], c);
}
}
void qe_project(ast_manager &m, app_ref_vector &vars, expr_ref &fml, model &mdl,
bool reduce_all_selects, bool use_native_mbp, bool dont_sub) {
if (use_native_mbp)
qe_project_z3(m, vars, fml, mdl, reduce_all_selects, use_native_mbp,
dont_sub);
else
if (!use_native_mbp)
qe_project_spacer(m, vars, fml, mdl, reduce_all_selects, use_native_mbp,
dont_sub);
if (!vars.empty())
qe_project_z3(m, vars, fml, mdl, reduce_all_selects, use_native_mbp,
dont_sub);
}
void expand_literals(ast_manager &m, expr_ref_vector &conjs) {
@ -329,12 +334,14 @@ void expand_literals(ast_manager &m, expr_ref_vector &conjs) {
conjs[i] = arith.mk_le(e1, e2);
if (i + 1 == conjs.size()) {
conjs.push_back(arith.mk_ge(e1, e2));
} else {
}
else {
conjs.push_back(conjs[i + 1].get());
conjs[i + 1] = arith.mk_ge(e1, e2);
}
++i;
} else if ((m.is_eq(e, c, val) && is_app(val) &&
}
else if ((m.is_eq(e, c, val) && is_app(val) &&
dt.is_constructor(to_app(val))) ||
(m.is_eq(e, val, c) && is_app(val) &&
dt.is_constructor(to_app(val)))) {
@ -346,8 +353,9 @@ void expand_literals(ast_manager &m, expr_ref_vector &conjs) {
conjs.push_back(m.mk_eq(apply_accessor(m, acc, j, f, c),
to_app(val)->get_arg(j)));
}
} else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) ||
(m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) {
}
else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) ||
(m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) {
rational two(2);
for (unsigned j = 0; j < bv_size; ++j) {
parameter p(j);
@ -355,11 +363,10 @@ void expand_literals(ast_manager &m, expr_ref_vector &conjs) {
bv.mk_extract(j, j, c));
if ((r % two).is_zero()) { e = m.mk_not(e); }
r = div(r, two);
if (j == 0) {
if (j == 0)
conjs[i] = e;
} else {
else
conjs.push_back(e);
}
}
}
}

1
src/qe/mbp/CMakeLists.txt
View file

@ -6,6 +6,7 @@ z3_add_component(mbp
mbp_basic_tg.cpp
mbp_datatypes.cpp
mbp_dt_tg.cpp
mbp_euf.cpp
mbp_qel.cpp
mbp_qel_util.cpp
mbp_plugin.cpp

2
src/qe/mbp/mbp_basic_tg.h
View file

@ -27,7 +27,7 @@ class mbp_basic_tg : public mbp_tg_plugin {
struct impl;
impl *m_impl;
public:
public:
mbp_basic_tg(ast_manager &man, mbp::term_graph &tg, model &mdl,
obj_hashtable<app> &vars_set, expr_sparse_mark &seen);
// iterate through all terms in m_tg and apply all basic MBP rules once

85
src/qe/mbp/mbp_euf.cpp Normal file
View file

@ -0,0 +1,85 @@
/*++
Copyright (c) 2025 Microsoft Corporation
--*/
#include "ast/ast_util.h"
#include "ast/for_each_expr.h"
#include "qe/mbp/mbp_euf.h"
#include "qe/mbp/mbp_term_graph.h"
namespace mbp {
euf_project_plugin::euf_project_plugin(ast_manager& m): project_plugin(m) {
}
euf_project_plugin::~euf_project_plugin() {
}
bool euf_project_plugin::project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) {
return false;
}
family_id euf_project_plugin::get_family_id() {
return basic_family_id;
}
bool euf_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
return false;
}
bool euf_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) {
if (vars.empty())
return false;
flatten_and(lits);
expr_mark var_set;
auto is_pure = [&](expr_mark& var_set, expr* v) {
return all_of(subterms::all(expr_ref(v, m)), [&](expr* w) { return !var_set.is_marked(w); });
};
for (auto v : vars)
var_set.mark(v, true);
unsigned has_def = false;
#if 1
// solve trivial equations
for (auto e : lits) {
expr* x = nullptr, *y = nullptr;
if (m.is_eq(e, x, y) && var_set.is_marked(x) && is_pure(var_set, y)) {
vars.erase(to_app(x));
defs.push_back({ expr_ref(x, m), expr_ref(y, m) });
has_def = true;
}
else if (m.is_eq(e, y, x) && var_set.is_marked(x) && is_pure(var_set, y)) {
vars.erase(to_app(x));
defs.push_back({ expr_ref(x, m), expr_ref(y, m) });
has_def = true;
}
}
if (has_def)
return true;
#endif
// check if there is a variable of uninterp sort
if (all_of(vars, [&](expr* v) { return !m.is_uninterp(v->get_sort()); }))
return has_def;
term_graph tg(m);
tg.add_lits(lits);
for (auto v : vars)
if (m.is_uninterp(v->get_sort()))
tg.add_var(v);
//
// now what:
/// walk all subterms of lits.
// push in partitions by value.
// add equations from model
// compute repr from tg.
//
return has_def;
}
}

30
src/qe/mbp/mbp_euf.h Normal file
View file

@ -0,0 +1,30 @@
/*++
Copyright (c) 2025 Microsoft Corporation
--*/
#pragma once
#include "model/model.h"
#include "qe/mbp/mbp_plugin.h"
namespace mbp {
class euf_project_plugin : public project_plugin {
public:
euf_project_plugin(ast_manager& m);
~euf_project_plugin() override;
bool project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override { return false; }
family_id get_family_id() override;
bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) override;
void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override { UNREACHABLE(); }
};
};

2
src/qe/mbp/mbp_plugin.cpp
View file

@ -205,7 +205,7 @@ namespace mbp {
else
extract_bools(eval, fmls, i, fml, true);
}
TRACE("qe", tout << fmls << "\n";);
TRACE("qe", tout << "fmls: " << fmls << "\n";);
}
void project_plugin::extract_bools(model_evaluator& eval, expr_ref_vector& fmls, unsigned idx, expr* fml, bool is_true) {

7
src/qe/mbp/mbp_plugin.h
View file

@ -21,6 +21,7 @@ Revision History:
#pragma once
#include "ast/ast.h"
#include "ast/ast_pp.h"
#include "util/params.h"
#include "model/model.h"
#include "math/simplex/model_based_opt.h"
@ -32,11 +33,12 @@ namespace mbp {
struct def {
expr_ref var, term;
def(const expr_ref& v, expr_ref& t): var(v), term(t) {}
};
class project_plugin {
protected:
ast_manager& m;
private:
expr_mark m_visited;
ptr_vector<expr> m_to_visit;
expr_mark m_bool_visited;
@ -110,3 +112,6 @@ namespace mbp {
};
}
inline std::ostream& operator<<(std::ostream& out, mbp::def const& d) {
return out << d.var << " -> " << d.term << "\n";
}

3
src/qe/mbp/mbp_term_graph.cpp
View file

@ -1018,8 +1018,7 @@ void term_graph::to_lits(expr_ref_vector &lits, bool all_equalities,
void term_graph::to_lits_qe_lite(expr_ref_vector &lits,
std::function<bool(expr *)> *non_core) {
DEBUG_CODE(for (auto t : m_terms) SASSERT(t->get_repr()););
DEBUG_CODE(for (auto t
: m_terms)
DEBUG_CODE(for (auto t : m_terms)
SASSERT(!t->is_cgr() || t->get_repr()->is_cgr()););
is_non_core not_in_core(non_core);
check_pred contains_nc(not_in_core, m, false);

32
src/qe/mbp/mbp_term_graph.h
View file

@ -32,10 +32,10 @@ Notes:
#include "util/plugin_manager.h"
namespace mbp {
namespace is_ground_ns {
struct proc;
struct found;
} // namespace is_ground_ns
namespace is_ground_ns {
struct proc;
struct found;
} // namespace is_ground_ns
class term;
class term_graph {
@ -246,16 +246,16 @@ private:
bool makes_cycle(term *t);
};
namespace is_ground_ns {
struct found {};
struct proc {
term_graph::is_variable_proc &m_is_var;
proc(term_graph::is_variable_proc &is_var) : m_is_var(is_var) {}
void operator()(var *n) const {}
void operator()(app const *n) const {
if (m_is_var.contains(n->get_decl())) throw found();
}
void operator()(quantifier *n) const {}
};
} // namespace is_ground_ns
namespace is_ground_ns {
struct found {};
struct proc {
term_graph::is_variable_proc &m_is_var;
proc(term_graph::is_variable_proc &is_var) : m_is_var(is_var) {}
void operator()(var *n) const {}
void operator()(app const *n) const {
if (m_is_var.contains(n->get_decl())) throw found();
}
void operator()(quantifier *n) const {}
};
} // namespace is_ground_ns
} // namespace mbp

16
src/qe/mbp/mbp_tg_plugins.h
View file

@ -23,12 +23,12 @@ Revision History:
#include "util/obj_hashtable.h"
class mbp_tg_plugin {
public:
// iterate through all terms in m_tg and apply all theory MBP rules once
// returns true if any rules were applied
virtual bool apply() { return false; };
virtual ~mbp_tg_plugin() = default;
virtual void use_model() { };
virtual void get_new_vars(app_ref_vector*&) { };
virtual family_id get_family_id() const { return null_family_id; };
public:
// iterate through all terms in m_tg and apply all theory MBP rules once
// returns true if any rules were applied
virtual bool apply() { return false; };
virtual ~mbp_tg_plugin() = default;
virtual void use_model() { };
virtual void get_new_vars(app_ref_vector*&) { };
virtual family_id get_family_id() const { return null_family_id; };
};

96
src/qe/qe_mbp.cpp
View file

@ -37,6 +37,7 @@ Revision History:
#include "qe/lite/qel.h"
#include "qe/mbp/mbp_arith.h"
#include "qe/mbp/mbp_arrays.h"
#include "qe/mbp/mbp_euf.h"
#include "qe/mbp/mbp_qel.h"
#include "qe/mbp/mbp_datatypes.h"
@ -352,6 +353,7 @@ public:
add_plugin(alloc(mbp::arith_project_plugin, m));
add_plugin(alloc(mbp::datatype_project_plugin, m));
add_plugin(alloc(mbp::array_project_plugin, m));
add_plugin(alloc(mbp::euf_project_plugin, m));
updt_params(p);
}
@ -392,18 +394,18 @@ public:
flatten_and(fml, fmls);
}
else {
extract_literals(model, vars, fmls);
bool change = true;
while (change && !vars.empty()) {
change = solve(model, vars, fmls);
for (auto* p : m_plugins) {
if (p && p->solve(model, vars, fmls)) {
change = true;
extract_literals(model, vars, fmls);
bool change = true;
while (change && !vars.empty()) {
change = solve(model, vars, fmls);
for (auto* p : m_plugins) {
if (p && p->solve(model, vars, fmls)) {
change = true;
}
}
}
}
}
}
bool validate_model(model& model, expr_ref_vector const& fmls) {
for (expr* f : fmls) {
@ -419,24 +421,27 @@ public:
return any_of(subterms::all(e), [&](expr* c) { return seq.is_char(c) || seq.is_seq(c); });
}
void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls, vector<mbp::def>* defs = nullptr) {
//don't use mbp_qel on some theories where model evaluation is
//incomplete This is not a limitation of qel. Fix this either by
//making mbp choices less dependent on the model evaluation methods
//or fix theory rewriters to make terms evaluation complete
if (m_use_qel && !has_unsupported_th(fmls) && !defs) {
bool dsub = m_dont_sub;
m_dont_sub = !force_elim;
expr_ref fml(m);
fml = mk_and(fmls);
spacer_qel(vars, model, fml);
fmls.reset();
flatten_and(fml, fmls);
m_dont_sub = dsub;
}
else {
mbp(force_elim, vars, model, fmls, defs);
}
//don't use mbp_qel on some theories where model evaluation is
//incomplete This is not a limitation of qel. Fix this either by
//making mbp choices less dependent on the model evaluation methods
//or fix theory rewriters to make terms evaluation complete
if (m_use_qel && !has_unsupported_th(fmls) && !defs) {
bool dsub = m_dont_sub;
m_dont_sub = !force_elim;
expr_ref fml(m);
fml = mk_and(fmls);
spacer_qel(vars, model, fml);
fmls.reset();
flatten_and(fml, fmls);
m_dont_sub = dsub;
TRACE("qe", tout << "spacer-qel " << vars << " " << fml << "\n");
}
else {
mbp(force_elim, vars, model, fmls, defs);
TRACE("qe", tout << "mbp " << vars << " " << fmls << "\n";
if (defs) { tout << "defs: "; for (auto const& d : *defs) tout << d << "\n"; tout << "\n";});
}
}
void mbp(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls, vector<mbp::def>* defs) {
SASSERT(validate_model(model, fmls));
@ -444,9 +449,12 @@ public:
app_ref var(m);
expr_ref_vector unused_fmls(m);
bool progress = true;
preprocess_solve(model, vars, fmls);
TRACE("qe", tout << "eliminate vars: " << vars << "fmls: " << fmls << "\n");
if (!defs)
preprocess_solve(model, vars, fmls);
filter_variables(model, vars, fmls, unused_fmls);
project_bools(model, vars, fmls);
TRACE("qe", tout << "eliminate vars: " << vars << "\nfmls: " << fmls << "\nunused: " << unused_fmls <<"\n");
while (progress && !vars.empty() && !fmls.empty() && m.limit().inc()) {
app_ref_vector new_vars(m);
progress = false;
@ -455,10 +463,12 @@ public:
unsigned sz = defs->size();
p->project(model, vars, fmls, *defs);
progress |= sz < defs->size();
TRACE("qe", tout << "after project " << m.get_family_name(p->get_family_id()) << ": " << vars << "\n");
}
else if (p)
(*p)(model, vars, fmls);
}
TRACE("qe", tout << "projecting " << vars << "\n");
while (!vars.empty() && !fmls.empty() && !defs && m.limit().inc()) {
var = vars.back();
vars.pop_back();
@ -491,16 +501,17 @@ public:
if (!m.limit().inc())
return;
vars.append(new_vars);
if (progress) {
if (progress && !defs)
preprocess_solve(model, vars, fmls);
}
TRACE("qe", tout << "looping " << vars << "\n");
}
if (fmls.empty()) {
vars.reset();
}
fmls.append(unused_fmls);
SASSERT(validate_model(model, fmls));
TRACE("qe", tout << vars << " " << fmls << "\n";);
TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n";);
}
void do_qe_lite(app_ref_vector& vars, expr_ref& fml) {
@ -529,16 +540,16 @@ public:
fml = mk_and(fmls);
}
void qel_project(app_ref_vector &vars, model &mdl, expr_ref &fml, bool reduce_all_selects) {
flatten_and(fml);
mbp::mbp_qel mbptg(m, m_params);
mbptg(vars, fml, mdl);
if (reduce_all_selects) rewrite_read_over_write(fml, mdl, fml);
m_rw(fml);
TRACE("qe", tout << "After mbp_tg:\n"
<< fml << " models " << mdl.is_true(fml) << "\n"
<< "Vars: " << vars << "\n";);
}
void qel_project(app_ref_vector &vars, model &mdl, expr_ref &fml, bool reduce_all_selects) {
flatten_and(fml);
mbp::mbp_qel mbptg(m, m_params);
mbptg(vars, fml, mdl);
if (reduce_all_selects) rewrite_read_over_write(fml, mdl, fml);
m_rw(fml);
TRACE("qe", tout << "After mbp_tg:\n"
<< fml << " models " << mdl.is_true(fml) << "\n"
<< "Vars: " << vars << "\n";);
}
void spacer_qel(app_ref_vector& vars, model& mdl, expr_ref& fml) {
TRACE("qe", tout << "Before projection:\n" << fml << "\n" << "Vars: " << vars << "\n";);
@ -600,12 +611,11 @@ public:
}
void spacer(app_ref_vector& vars, model& mdl, expr_ref& fml) {
if (m_use_qel) {
TRACE("qe", tout << "spacer " << m_use_qel << " " << fml << " " << vars << "\n");
if (m_use_qel)
spacer_qel(vars, mdl, fml);
}
else {
else
spacer_qe_lite(vars, mdl, fml);
}
}
void spacer_qe_lite(app_ref_vector& vars, model& mdl, expr_ref& fml) {