mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

bind nested variables

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-21 20:11:29 -07:00 • committed by Arie Gurfinkel
parent d95e167d61
commit efb1f50d00
4 changed files with 27 additions and 82 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/qe/qe_arith.cpp
View file

@ -299,20 +299,19 @@ namespace qe {
obj_map<expr, unsigned> tids; obj_map<expr, unsigned> tids;
expr_ref_vector pinned(m); expr_ref_vector pinned(m);
unsigned j = 0; unsigned j = 0;
TRACE("qe", tout << "fmls: " << fmls << "\n";);
for (unsigned i = 0; i < fmls.size(); ++i) { for (unsigned i = 0; i < fmls.size(); ++i) {
expr* fml = fmls[i].get(); expr * fml = fmls.get(i);
if (!linearize(mbo, eval, fml, fmls, tids)) { if (!linearize(mbo, eval, fml, fmls, tids)) {
if (i != j) { fmls[j++] = fml;
fmls[j] = fmls[i].get();
}
++j;
} }
else { else {
TRACE("qe", tout << mk_pp(fml, m) << "\n";); TRACE("qe", tout << "could not linearize: " << mk_pp(fml, m) << "\n";);
pinned.push_back(fml); pinned.push_back(fml);
} }
} }
fmls.resize(j); fmls.shrink(j);
TRACE("qe", tout << "linearized: " << fmls << "\n";);
// fmls holds residue, // fmls holds residue,
// mbo holds linear inequalities that are in scope // mbo holds linear inequalities that are in scope
@ -328,13 +327,13 @@ namespace qe {
if (is_arith(v) && !tids.contains(v)) { if (is_arith(v) && !tids.contains(v)) {
rational r; rational r;
expr_ref val = eval(v); expr_ref val = eval(v);
a.is_numeral(val, r); VERIFY(a.is_numeral(val, r));
TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";); TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";);
tids.insert(v, mbo.add_var(r, a.is_int(v))); tids.insert(v, mbo.add_var(r, a.is_int(v)));
} }
} }
for (expr* fml : fmls) { for (expr* fml : fmls) {
fmls_mark.mark(fml); mark_rec(fmls_mark, fml);
} }
ptr_vector<expr> index2expr; ptr_vector<expr> index2expr;
for (auto& kv : tids) { for (auto& kv : tids) {
@ -346,8 +345,7 @@ namespace qe {
} }
j = 0; j = 0;
unsigned_vector real_vars; unsigned_vector real_vars;
for (unsigned i = 0; i < vars.size(); ++i) { for (app* v : vars) {
app* v = vars[i].get();
if (is_arith(v) && !fmls_mark.is_marked(v)) { if (is_arith(v) && !fmls_mark.is_marked(v)) {
real_vars.push_back(tids.find(v)); real_vars.push_back(tids.find(v));
} }
@ -355,7 +353,7 @@ namespace qe {
vars[j++] = v; vars[j++] = v;
} }
} }
vars.resize(j); vars.shrink(j);
TRACE("qe", tout << "remaining vars: " << vars << "\n"; TRACE("qe", tout << "remaining vars: " << vars << "\n";
for (unsigned v : real_vars) { for (unsigned v : real_vars) {
tout << "v" << v << " " << mk_pp(index2expr[v], m) << "\n"; tout << "v" << v << " " << mk_pp(index2expr[v], m) << "\n";
@ -391,8 +389,7 @@ namespace qe {
CTRACE("qe", !m.is_true(val), tout << "Evaluated unit " << t << " to " << val << "\n";); CTRACE("qe", !m.is_true(val), tout << "Evaluated unit " << t << " to " << val << "\n";);
continue; continue;
} }
for (j = 0; j < r.m_vars.size(); ++j) { for (var const& v : r.m_vars) {
var const& v = r.m_vars[j];
t = index2expr[v.m_id]; t = index2expr[v.m_id];
if (!v.m_coeff.is_one()) { if (!v.m_coeff.is_one()) {
t = a.mk_mul(a.mk_numeral(v.m_coeff, a.is_int(t)), t); t = a.mk_mul(a.mk_numeral(v.m_coeff, a.is_int(t)), t);
@ -418,11 +415,9 @@ namespace qe {
break; break;
} }
} }
fmls.push_back(t); fmls.push_back(t);
val = eval(t); val = eval(t);
CTRACE("qe", !m.is_true(val), tout << "Evaluated " << t << " to " << val << "\n";); CTRACE("qe", !m.is_true(val), tout << "Evaluated " << t << " to " << val << "\n";);
} }
} }

10
src/qe/qe_arrays.cpp
View file

@ -1390,9 +1390,9 @@ namespace qe {
array_project_eqs_util pe (m); array_project_eqs_util pe (m);
pe (mdl, arr_vars, fml, aux_vars); pe (mdl, arr_vars, fml, aux_vars);
TRACE ("qe", TRACE ("qe",
tout << "Projected array eqs:\n" << fml << "\n"; tout << "Projected array eqs: " << fml << "\n";
tout << "Remaining array vars:\n" << arr_vars; tout << "Remaining array vars: " << arr_vars << "\n";
tout << "Aux vars:\n" << aux_vars; tout << "Aux vars: " << aux_vars << "\n";
); );
// 2. reduce selects // 2. reduce selects
@ -1406,8 +1406,8 @@ namespace qe {
ps (mdl, arr_vars, fml, aux_vars); ps (mdl, arr_vars, fml, aux_vars);
TRACE ("qe", TRACE ("qe",
tout << "Projected array selects:\n" << fml << "\n"; tout << "Projected array selects: " << fml << "\n";
tout << "All aux vars:\n" << aux_vars; tout << "All aux vars: " << aux_vars << "\n";
); );
} }

68
src/qe/qe_mbp.cpp
View file

@ -77,42 +77,6 @@ expr_ref project_plugin::pick_equality(ast_manager& m, model& model, expr* t) {
return expr_ref(nullptr, m); return expr_ref(nullptr, m);
} }
void project_plugin::partition_values(model& model, expr_ref_vector const& vals, expr_ref_vector& lits) {
ast_manager& m = vals.get_manager();
expr_ref val(m);
expr_ref_vector trail(m), reps(m);
obj_map<expr, expr*> roots;
for (unsigned i = 0; i < vals.size(); ++i) {
expr* v = vals[i], *root;
VERIFY (model.eval(v, val));
if (roots.find(val, root)) {
lits.push_back(m.mk_eq(v, root));
}
else {
roots.insert(val, v);
trail.push_back(val);
reps.push_back(v);
}
}
if (reps.size() > 1) {
lits.push_back(mk_distinct(reps));
}
}
#if 0
void project_plugin::partition_args(model& model, app_ref_vector const& selects, expr_ref_vector& lits) {
ast_manager& m = selects.get_manager();
if (selects.empty()) return;
unsigned num_args = selects[0]->get_decl()->get_arity();
for (unsigned j = 1; j < num_args; ++j) {
expr_ref_vector args(m);
for (unsigned i = 0; i < selects.size(); ++i) {
args.push_back(selects[i]->get_arg(j));
}
project_plugin::partition_values(model, args, lits);
}
}
#endif
void project_plugin::erase(expr_ref_vector& lits, unsigned& i) { void project_plugin::erase(expr_ref_vector& lits, unsigned& i) {
lits[i] = lits.back(); lits[i] = lits.back();
@ -136,7 +100,6 @@ class mbp::impl {
// parameters // parameters
bool m_reduce_all_selects; bool m_reduce_all_selects;
bool m_native_mbp;
bool m_dont_sub; bool m_dont_sub;
void add_plugin(project_plugin* p) { void add_plugin(project_plugin* p) {
@ -324,8 +287,7 @@ class mbp::impl {
void operator() (app *n) { void operator() (app *n) {
expr *e1, *e2; expr *e1, *e2;
if (m_array.is_select (n)) { if (m_array.is_select (n)) {
for (unsigned i = 1; i < n->get_num_args(); ++i) { for (expr * arg : *n) {
expr * arg = n->get_arg(i);
if (m.get_sort(arg) == m.get_sort(m_var) && arg != m_var) if (m.get_sort(arg) == m.get_sort(m_var) && arg != m_var)
m_res.push_back (arg); m_res.push_back (arg);
} }
@ -378,8 +340,7 @@ class mbp::impl {
// -- evaluate to initialize eval cache // -- evaluate to initialize eval cache
(void) eval (fml); (void) eval (fml);
unsigned j = 0; unsigned j = 0;
for (unsigned i = 0; i < vars.size (); ++i) { for (app * v : vars) {
app* v = vars.get(i);
if (!project_var (eval, v, fml)) { if (!project_var (eval, v, fml)) {
vars[j++] = v; vars[j++] = v;
} }
@ -389,7 +350,6 @@ class mbp::impl {
public: public:
opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) { opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) {
arith_project_plugin arith(m); arith_project_plugin arith(m);
return arith.maximize(fmls, mdl, t, ge, gt); return arith.maximize(fmls, mdl, t, ge, gt);
@ -530,7 +490,6 @@ public:
void updt_params(params_ref const& p) { void updt_params(params_ref const& p) {
m_params.append(p); m_params.append(p);
m_reduce_all_selects = m_params.get_bool("reduce_all_selects", false); m_reduce_all_selects = m_params.get_bool("reduce_all_selects", false);
m_native_mbp = m_params.get_bool("native_mbp", false);
m_dont_sub = m_params.get_bool("dont_sub", false); m_dont_sub = m_params.get_bool("dont_sub", false);
} }
@ -549,6 +508,7 @@ public:
bool validate_model(model& model, expr_ref_vector const& fmls) { bool validate_model(model& model, expr_ref_vector const& fmls) {
expr_ref val(m); expr_ref val(m);
model_evaluator eval(model);
for (expr * f : fmls) { for (expr * f : fmls) {
VERIFY(model.eval(f, val) && m.is_true(val)); VERIFY(model.eval(f, val) && m.is_true(val));
} }
@ -677,27 +637,20 @@ public:
tout << "extended model:\n"; tout << "extended model:\n";
model_pp (tout, mdl); model_pp (tout, mdl);
tout << "Auxiliary variables of index and value sorts:\n"; tout << "Auxiliary variables of index and value sorts:\n";
tout << vars; tout << vars << "\n";
); );
} }
// project reals and ints // project reals and ints
if (!arith_vars.empty ()) { if (!arith_vars.empty ()) {
TRACE ("qe", tout << "Arith vars:\n" << arith_vars;); TRACE ("qe", tout << "Arith vars: " << arith_vars << "\n";);
if (m_native_mbp) { expr_ref_vector fmls(m);
expr_ref_vector fmls(m); flatten_and (fml, fmls);
flatten_and (fml, fmls);
(*this)(true, arith_vars, mdl, fmls);
fml = mk_and (fmls);
SASSERT (arith_vars.empty ());
}
else {
NOT_IMPLEMENTED_YET();
// qe::arith_project (mdl, arith_vars, fml);
}
(*this)(true, arith_vars, mdl, fmls);
fml = mk_and (fmls);
TRACE ("qe", TRACE ("qe",
tout << "Projected arith vars:\n" << fml << "\n"; tout << "Projected arith vars:\n" << fml << "\n";
tout << "Remaining arith vars:\n" << arith_vars << "\n";); tout << "Remaining arith vars:\n" << arith_vars << "\n";);
@ -740,7 +693,6 @@ void mbp::updt_params(params_ref const& p) {
void mbp::get_param_descrs(param_descrs & r) { void mbp::get_param_descrs(param_descrs & r) {
r.insert("reduce_all_selects", CPK_BOOL, "(default: false) reduce selects"); r.insert("reduce_all_selects", CPK_BOOL, "(default: false) reduce selects");
r.insert("native_mbp", CPK_BOOL, "(default: false) switch between native and spacer tailored mbp");
r.insert("dont_sub", CPK_BOOL, "(default: false) disable substitution of values for free variables"); r.insert("dont_sub", CPK_BOOL, "(default: false) disable substitution of values for free variables");
} }

2
src/qe/qe_mbp.h
View file

@ -40,8 +40,6 @@ namespace qe {
virtual void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { }; virtual void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { };
static expr_ref pick_equality(ast_manager& m, model& model, expr* t); static expr_ref pick_equality(ast_manager& m, model& model, expr* t);
static void partition_values(model& model, expr_ref_vector const& vals, expr_ref_vector& lits);
//static void partition_args(model& model, app_ref_vector const& sels, expr_ref_vector& lits);
static void erase(expr_ref_vector& lits, unsigned& i); static void erase(expr_ref_vector& lits, unsigned& i);
static void push_back(expr_ref_vector& lits, expr* lit); static void push_back(expr_ref_vector& lits, expr* lit);
static void mark_rec(expr_mark& visited, expr* e); static void mark_rec(expr_mark& visited, expr* e);