diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index 568ac79bf..e310f938c 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -429,11 +429,12 @@ namespace Microsoft.Z3 var lvl = BacktrackLevel; BacktrackLevel = uint.MaxValue; ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, lvl)); - if (r.Size == 1 && ((Expr)r[0]).IsFalse) { + var v = r.ToBoolExprArray(); + if (v.Length == 1 && v[0].IsFalse) { break; } - yield return r.ToBoolExprArray(); - if (r.Size == 0) { + yield return v; + if (v.Length == 0) { break; } } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 7c703653c..dc4200349 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -885,7 +885,8 @@ struct sat2goal::imp { sat::model_converter m_mc; expr_ref_vector m_var2expr; generic_model_converter_ref m_fmc; // filter for eliminating fresh variables introduced in the assertion-set --> sat conversion - + generic_model_converter_ref m_imc; // used to ensure correctness in incremental calls with simplifications that require model conversions + sat_model_converter(ast_manager & m): m_var2expr(m) { } @@ -894,6 +895,7 @@ struct sat2goal::imp { sat_model_converter(ast_manager & m, sat::solver const & s):m_var2expr(m) { m_mc.copy(s.get_model_converter()); m_fmc = alloc(generic_model_converter, m); + m_imc = nullptr; } ast_manager & m() { return m_var2expr.get_manager(); } @@ -920,6 +922,7 @@ struct sat2goal::imp { insert(l.var(), m().mk_fresh_const(0, m().mk_bool_sort()), true); } } + m_imc = nullptr; } virtual void operator()(model_ref & md) { @@ -1026,7 +1029,34 @@ struct sat2goal::imp { } void operator()(expr_ref& formula) override { - NOT_IMPLEMENTED_YET(); + if (!m_imc) { + m_imc = alloc(generic_model_converter, m()); + sat::literal_vector updates; + m_mc.expand(updates); + sat::literal_vector clause; + expr_ref_vector tail(m()); + expr_ref def(m()); + for (sat::literal l : updates) { + if (l == sat::null_literal) { + sat::literal lit0 = clause[0]; + for (unsigned i = 1; i < clause.size(); ++i) { + tail.push_back(lit2expr(~clause[i])); + } + def = m().mk_or(lit2expr(lit0), mk_and(tail)); + if (lit0.sign()) { + lit0.neg(); + def = m().mk_not(def); + } + m_imc->add(lit2expr(lit0), def); + clause.reset(); + tail.reset(); + } + else { + clause.push_back(l); + } + } + } + (*m_imc)(formula); } }; diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index 3993f20c9..19caa62ac 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -18,6 +18,7 @@ Notes: --*/ #include "ast/ast_pp.h" +#include "ast/for_each_expr.h" #include "tactic/generic_model_converter.h" #include "model/model_v2_pp.h" #include "model/model_evaluator.h" @@ -30,59 +31,89 @@ void generic_model_converter::operator()(model_ref & md) { ev.set_expand_array_equalities(false); expr_ref val(m); unsigned arity; - for (unsigned i = m_entries.size(); i-- > 0; ) { - entry const& e = m_entries[i]; - switch (e.m_instruction) { - case HIDE: - md->unregister_decl(e.m_f); - break; - case ADD: - ev(e.m_def, val); - TRACE("model_converter", tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";); - arity = e.m_f->get_arity(); - if (arity == 0) { - md->register_decl(e.m_f, val); - } - else { - func_interp * new_fi = alloc(func_interp, m, arity); - new_fi->set_else(val); - md->register_decl(e.m_f, new_fi); - } - break; + for (unsigned i = m_hide_entries.size(); i-- > 0; ) { + entry const& e = m_hide_entries[i]; + md->unregister_decl(e.m_f); + } + for (unsigned i = m_add_entries.size(); i-- > 0; ) { + entry const& e = m_add_entries[i]; + ev(e.m_def, val); + TRACE("model_converter", tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";); + arity = e.m_f->get_arity(); + if (arity == 0) { + md->register_decl(e.m_f, val); + } + else { + func_interp * new_fi = alloc(func_interp, m, arity); + new_fi->set_else(val); + md->register_decl(e.m_f, new_fi); } } TRACE("model_converter", tout << "after generic_model_converter\n"; model_v2_pp(tout, *md);); } void generic_model_converter::display(std::ostream & out) { - for (entry const& e : m_entries) { - switch (e.m_instruction) { - case HIDE: - display_del(out, e.m_f); - break; - case ADD: - display_add(out, m, e.m_f, e.m_def); - break; - } + for (entry const& e : m_hide_entries) { + display_del(out, e.m_f); + } + for (entry const& e : m_add_entries) { + display_del(out, e.m_f); } } model_converter * generic_model_converter::translate(ast_translation & translator) { ast_manager& to = translator.to(); generic_model_converter * res = alloc(generic_model_converter, to); - for (entry const& e : m_entries) - res->m_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction)); + for (entry const& e : m_hide_entries) { + res->m_hide_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction)); + } + for (entry const& e : m_add_entries) { + res->m_add_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction)); + } return res; } void generic_model_converter::collect(ast_pp_util& visitor) { m_env = &visitor.env(); - for (entry const& e : m_entries) { + for (entry const& e : m_hide_entries) { + visitor.coll.visit_func(e.m_f); + } + for (entry const& e : m_add_entries) { visitor.coll.visit_func(e.m_f); if (e.m_def) visitor.coll.visit(e.m_def); } } +struct min_app_idx_proc { + unsigned m_min; + obj_map& m_idxs; + min_app_idx_proc(obj_map& idxs) : m_min(UINT_MAX), m_idxs(idxs) {} + void operator()(app * n) { + unsigned idx; + if (m_idxs.find(n->get_decl(), idx)) { + m_min = std::min(m_min, idx); + } + } + void operator()(var * n) {} + void operator()(quantifier * n) {} +}; + void generic_model_converter::operator()(expr_ref& fml) { - NOT_IMPLEMENTED_YET(); + min_app_idx_proc min_proc(m_first_idx); + for_each_expr(min_proc, fml); + unsigned min_idx = min_proc.m_min; + for (unsigned i = m_add_entries.size(); i-- > min_idx;) { + entry const& e = m_add_entries[i]; + unsigned arity = e.m_f->get_arity(); + if (arity == 0) { + fml = m.mk_and(fml, m.mk_eq(m.mk_const(e.m_f), e.m_def)); + } + else { + NOT_IMPLEMENTED_YET(); + } + if (m_first_idx[e.m_f] == i) { + m_first_idx.remove(e.m_f); + } + m_add_entries.pop_back(); + } } diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index affafb0c1..805bad0d8 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -32,19 +32,25 @@ class generic_model_converter : public model_converter { m_f(f, m), m_def(d, m), m_instruction(i) {} }; ast_manager& m; - vector m_entries; + vector m_add_entries; + vector m_hide_entries; + obj_map m_first_idx; public: - generic_model_converter(ast_manager & m): m(m) {} + generic_model_converter(ast_manager & m) : m(m) {} virtual ~generic_model_converter() { } void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); } - void hide(func_decl * f) { m_entries.push_back(entry(f, 0, m, HIDE)); } + void hide(func_decl * f) { m_hide_entries.push_back(entry(f, 0, m, HIDE)); } - void add(func_decl * d, expr* e) { m_entries.push_back(entry(d, e, m, ADD)); } + void add(func_decl * d, expr* e) { + struct entry et(d, e, m, ADD); + m_first_idx.insert_if_not_there(et.m_f, m_add_entries.size()); + m_add_entries.push_back(et); + } - void add(expr * d, expr* e) { SASSERT(is_app(d) && to_app(d)->get_num_args() == 0); m_entries.push_back(entry(to_app(d)->get_decl(), e, m, ADD)); } + void add(expr * d, expr* e) { SASSERT(is_app(d) && to_app(d)->get_num_args() == 0); add(to_app(d)->get_decl(), e); } void operator()(labels_vec & labels) override {}