From baa96909cca4fd81e48e1d51d6b35103e60ae77c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Jun 2018 17:13:10 -0700 Subject: [PATCH] mb-skolem for arithmetic with model repair The contract is that users of mb-skolem ensure that interface equalities are preserved (by adding a sufficient set of disequalities, such as a chain x1 < x2 < x3 .., to force that solutions for x_i does not clash). Signed-off-by: Nikolaj Bjorner --- src/math/simplex/model_based_opt.cpp | 12 +++++++----- src/model/model_core.cpp | 8 ++++---- src/qe/qe_arith.cpp | 20 +++++++++++++++++++- src/qe/qe_mbi.cpp | 4 ++-- src/qe/qe_term_graph.cpp | 3 ++- 5 files changed, 34 insertions(+), 13 deletions(-) diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index 4efab1935..09f6d5c2d 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -51,7 +51,8 @@ namespace opt { m_div = -v.m_coeff; } } - m_coeff = r.m_coeff - r.m_value; + m_coeff = r.m_coeff; + if (r.m_type == opt::t_lt) m_coeff += m_div; normalize(); SASSERT(m_div.is_pos()); } @@ -983,7 +984,7 @@ namespace opt { } else { result = def(); - result.m_coeff = eval(x); + m_var2value[x] = rational::zero(); } SASSERT(eval(result) == eval(x)); } @@ -1008,8 +1009,8 @@ namespace opt { else { result = def(m_rows[glb_index], x); } + m_var2value[x] = eval(result); #endif - SASSERT(eval(result) == eval(x)); } // The number of matching lower and upper bounds is small. @@ -1106,7 +1107,8 @@ namespace opt { } def result = project(y, compute_def); if (compute_def) { - result = (result * D) + u; + result = (result * D) + u; + m_var2value[x] = eval(result); } SASSERT(!compute_def || eval(result) == eval(x)); return result; @@ -1204,7 +1206,7 @@ namespace opt { def result; if (compute_def) { result = def(m_rows[row_id1], x); - SASSERT(eval(result) == eval(x)); + m_var2value[x] = eval(result); } retire_row(row_id1); return result; diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 648768bf3..d41854c22 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -47,8 +47,8 @@ bool model_core::eval(func_decl* f, expr_ref & r) const { void model_core::register_decl(func_decl * d, expr * v) { SASSERT(d->get_arity() == 0); - decl2expr::obj_map_entry * entry = m_interp.insert_if_not_there2(d, 0); - if (entry->get_data().m_value == 0) { + decl2expr::obj_map_entry * entry = m_interp.insert_if_not_there2(d, nullptr); + if (entry->get_data().m_value == nullptr) { // new entry m_decls.push_back(d); m_const_decls.push_back(d); @@ -67,8 +67,8 @@ void model_core::register_decl(func_decl * d, expr * v) { void model_core::register_decl(func_decl * d, func_interp * fi) { SASSERT(d->get_arity() > 0); SASSERT(&fi->m() == &m_manager); - decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, 0); - if (entry->get_data().m_value == 0) { + decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, nullptr); + if (entry->get_data().m_value == nullptr) { // new entry m_decls.push_back(d); m_func_decls.push_back(d); diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index 7e619ccd5..ff4c7dc52 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -360,7 +360,7 @@ namespace qe { ptr_vector index2expr; for (auto& kv : tids) { - index2expr.setx(kv.m_value, kv.m_key, 0); + index2expr.setx(kv.m_value, kv.m_key, nullptr); } j = 0; @@ -454,6 +454,8 @@ namespace qe { else if (!d.m_div.is_one() && !is_int) { t = a.mk_div(t, a.mk_numeral(d.m_div, is_int)); } + update_model(model, to_app(x), eval(t)); + SASSERT(eval(t) == eval(x)); result.push_back(def(expr_ref(x, m), t)); } @@ -461,6 +463,22 @@ namespace qe { return result; } + void update_model(model& mdl, app* x, expr_ref const& val) { + if (is_uninterp_const(x)) { + mdl.register_decl(x->get_decl(), val); + } + else { + func_interp* fi = mdl.get_func_interp(x->get_decl()); + if (!fi) return; + model_evaluator eval(mdl); + expr_ref_vector args(m); + for (expr* arg : *x) { + args.push_back(eval(arg)); + } + fi->insert_entry(args.c_ptr(), val); + } + } + expr_ref mk_add(expr_ref_vector const& ts) { switch (ts.size()) { case 0: diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 6b777aa02..60fb0f6f0 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -259,7 +259,7 @@ namespace qe { app_ref_vector& m_vars; arith_util arith; obj_hashtable m_exclude; - is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& shared): + is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& shared): m(vars.m()), m_vars(vars), arith(m) { for (func_decl* f : shared) m_exclude.insert(f); } @@ -484,7 +484,7 @@ namespace qe { return l_true, mbp of local, mdl of local & blocked else if !is_sat(local & lits) then return l_false, mbp of local, nullptr - else // is_sat(local & lits) && !is_sat(local & lits & blocked) + else if is_sat(local & lits) && !is_sat(local & lits & blocked) MISSING CASE MUST PRODUCE AN IMPLICANT OF LOCAL that is inconsistent with lits & blocked in this case !is_sat(local & lits & mdl) and is_sat(mdl, blocked) diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 6018d763a..95518d7fc 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -35,6 +35,7 @@ namespace qe { } }; } + namespace is_pure_ns { struct found{}; struct proc { @@ -776,7 +777,7 @@ namespace qe { for (auto &kv : val2rep) { expr *rep = kv.m_value; if (!m.is_unique_value(rep)) - reps.push_back(kv.m_value); + reps.push_back(kv.m_value); } if (reps.size() <= 1) return;