mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
bind nested variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
Arie Gurfinkel
parent
692a701516
commit
560a26127e
4 changed files with 27 additions and 77 deletions
|
|
@ -415,7 +415,7 @@ namespace qe {
|
|||
break;
|
||||
}
|
||||
}
|
||||
fmls.push_back(t);
|
||||
fmls.push_back(t);
|
||||
val = eval(t);
|
||||
CTRACE("qe", !m.is_true(val), tout << "Evaluated " << t << " to " << val << "\n";);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1390,9 +1390,9 @@ namespace qe {
|
|||
array_project_eqs_util pe (m);
|
||||
pe (mdl, arr_vars, fml, aux_vars);
|
||||
TRACE ("qe",
|
||||
tout << "Projected array eqs:\n" << fml << "\n";
|
||||
tout << "Remaining array vars:\n" << arr_vars;
|
||||
tout << "Aux vars:\n" << aux_vars;
|
||||
tout << "Projected array eqs: " << fml << "\n";
|
||||
tout << "Remaining array vars: " << arr_vars << "\n";
|
||||
tout << "Aux vars: " << aux_vars << "\n";
|
||||
);
|
||||
|
||||
// 2. reduce selects
|
||||
|
|
@ -1406,8 +1406,8 @@ namespace qe {
|
|||
ps (mdl, arr_vars, fml, aux_vars);
|
||||
|
||||
TRACE ("qe",
|
||||
tout << "Projected array selects:\n" << fml << "\n";
|
||||
tout << "All aux vars:\n" << aux_vars;
|
||||
tout << "Projected array selects: " << fml << "\n";
|
||||
tout << "All aux vars: " << aux_vars << "\n";
|
||||
);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -77,42 +77,6 @@ expr_ref project_plugin::pick_equality(ast_manager& m, model& model, expr* t) {
|
|||
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) {
|
||||
lits[i] = lits.back();
|
||||
|
|
@ -127,16 +91,15 @@ void project_plugin::push_back(expr_ref_vector& lits, expr* e) {
|
|||
|
||||
|
||||
class mbp::impl {
|
||||
ast_manager& m;
|
||||
ast_manager& m;
|
||||
params_ref m_params;
|
||||
th_rewriter m_rw;
|
||||
th_rewriter m_rw;
|
||||
ptr_vector<project_plugin> m_plugins;
|
||||
expr_mark m_visited;
|
||||
expr_mark m_bool_visited;
|
||||
|
||||
expr_mark m_visited;
|
||||
expr_mark m_bool_visited;
|
||||
|
||||
// parameters
|
||||
bool m_reduce_all_selects;
|
||||
bool m_native_mbp;
|
||||
bool m_dont_sub;
|
||||
|
||||
void add_plugin(project_plugin* p) {
|
||||
|
|
@ -282,33 +245,33 @@ class mbp::impl {
|
|||
}
|
||||
else {
|
||||
vars[j++] = var;
|
||||
}
|
||||
}
|
||||
}
|
||||
if (j == vars.size()) {
|
||||
return;
|
||||
}
|
||||
vars.shrink(j);
|
||||
j = 0;
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
j = 0;
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
expr* fml = fmls[i].get();
|
||||
sub(fml, val);
|
||||
m_rw(val);
|
||||
if (!m.is_true(val)) {
|
||||
m_rw(val);
|
||||
if (!m.is_true(val)) {
|
||||
TRACE("qe", tout << mk_pp(fml, m) << " -> " << val << "\n";);
|
||||
fmls[j++] = val;
|
||||
}
|
||||
}
|
||||
fmls.shrink(j);
|
||||
}
|
||||
}
|
||||
fmls.shrink(j);
|
||||
}
|
||||
|
||||
|
||||
void subst_vars(model_evaluator& eval, app_ref_vector const& vars, expr_ref& fml) {
|
||||
expr_safe_replace sub (m);
|
||||
for (app * v : vars) {
|
||||
sub.insert(v, eval(v));
|
||||
}
|
||||
sub(fml);
|
||||
}
|
||||
sub(fml);
|
||||
}
|
||||
|
||||
struct index_term_finder {
|
||||
ast_manager& m;
|
||||
|
|
@ -324,8 +287,7 @@ class mbp::impl {
|
|||
void operator() (app *n) {
|
||||
expr *e1, *e2;
|
||||
if (m_array.is_select (n)) {
|
||||
for (unsigned i = 1; i < n->get_num_args(); ++i) {
|
||||
expr * arg = n->get_arg(i);
|
||||
for (expr * arg : *n) {
|
||||
if (m.get_sort(arg) == m.get_sort(m_var) && arg != m_var)
|
||||
m_res.push_back (arg);
|
||||
}
|
||||
|
|
@ -378,8 +340,7 @@ class mbp::impl {
|
|||
// -- evaluate to initialize eval cache
|
||||
(void) eval (fml);
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < vars.size (); ++i) {
|
||||
app* v = vars.get(i);
|
||||
for (app * v : vars) {
|
||||
if (!project_var (eval, v, fml)) {
|
||||
vars[j++] = v;
|
||||
}
|
||||
|
|
@ -389,7 +350,6 @@ class mbp::impl {
|
|||
|
||||
public:
|
||||
|
||||
|
||||
opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) {
|
||||
arith_project_plugin arith(m);
|
||||
return arith.maximize(fmls, mdl, t, ge, gt);
|
||||
|
|
@ -530,7 +490,6 @@ public:
|
|||
void updt_params(params_ref const& p) {
|
||||
m_params.append(p);
|
||||
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);
|
||||
}
|
||||
|
||||
|
|
@ -549,6 +508,7 @@ public:
|
|||
|
||||
bool validate_model(model& model, expr_ref_vector const& fmls) {
|
||||
expr_ref val(m);
|
||||
model_evaluator eval(model);
|
||||
for (expr * f : fmls) {
|
||||
VERIFY(model.eval(f, val) && m.is_true(val));
|
||||
}
|
||||
|
|
@ -677,26 +637,19 @@ public:
|
|||
tout << "extended model:\n";
|
||||
model_pp (tout, mdl);
|
||||
tout << "Auxiliary variables of index and value sorts:\n";
|
||||
tout << vars;
|
||||
tout << vars << "\n";
|
||||
);
|
||||
|
||||
}
|
||||
// project reals and ints
|
||||
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);
|
||||
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);
|
||||
}
|
||||
|
||||
TRACE ("qe",
|
||||
tout << "Projected arith vars:\n" << fml << "\n";
|
||||
|
|
@ -733,14 +686,13 @@ mbp::mbp(ast_manager& m, params_ref const& p) {
|
|||
mbp::~mbp() {
|
||||
dealloc(m_impl);
|
||||
}
|
||||
|
||||
|
||||
void mbp::updt_params(params_ref const& p) {
|
||||
m_impl->updt_params(p);
|
||||
}
|
||||
|
||||
void mbp::get_param_descrs(param_descrs & r) {
|
||||
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");
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -40,8 +40,6 @@ namespace qe {
|
|||
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 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 push_back(expr_ref_vector& lits, expr* lit);
|
||||
static void mark_rec(expr_mark& visited, expr* e);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue