From f476f949543b376ebd3ff46b7074561642c240ae Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Sat, 18 Nov 2017 15:07:18 -0800 Subject: [PATCH 1/2] merge commit Signed-off-by: Miguel Angelo Da Terra Neves --- src/api/dotnet/Solver.cs | 7 ++++--- src/tactic/generic_model_converter.cpp | 2 ++ src/tactic/generic_model_converter.h | 8 +++++--- 3 files changed, 11 insertions(+), 6 deletions(-) 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/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index 629004869..7dec2f73b 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -87,5 +87,7 @@ void generic_model_converter::collect(ast_pp_util& visitor) { } void generic_model_converter::operator()(expr_ref& fml) { + // TODO: traverse expression and retrieve minimum trail index + // TODO: add func = expr starting at that index, removing from table if index is the same NOT_IMPLEMENTED_YET(); } diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index c58d0d029..1862efb8b 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -32,7 +32,9 @@ 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) {} @@ -40,9 +42,9 @@ public: 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) { m_add_entries.push_back(entry(d, e, m, ADD)); } virtual void operator()(model_ref & md, unsigned goal_idx); From 773d938925c6be6c7afc7ff1a4c861c45a3b55b9 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Tue, 21 Nov 2017 13:24:14 -0800 Subject: [PATCH 2/2] re-adding simplified constraints based on model converter Signed-off-by: Miguel Angelo Da Terra Neves --- src/sat/tactic/goal2sat.cpp | 34 ++++++++++++++++++++++++-- src/tactic/generic_model_converter.cpp | 2 +- 2 files changed, 33 insertions(+), 3 deletions(-) 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 aeec97260..19caa62ac 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -104,7 +104,6 @@ void generic_model_converter::operator()(expr_ref& 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]; - m_add_entries.pop_back(); 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)); @@ -115,5 +114,6 @@ void generic_model_converter::operator()(expr_ref& fml) { if (m_first_idx[e.m_f] == i) { m_first_idx.remove(e.m_f); } + m_add_entries.pop_back(); } }