From cb2d8d21071b9e895158adc4b0a3e8dd052e41a4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 30 Jul 2016 19:12:41 -0700 Subject: [PATCH] add detection of non-fixed variables to consequence finding Signed-off-by: Nikolaj Bjorner --- src/api/api_opt.cpp | 50 +++++++++++++++++++++++++++++- src/api/c++/z3++.h | 2 ++ src/api/dotnet/Optimize.cs | 19 ++++++++++++ src/api/python/z3.py | 8 +++++ src/api/z3_optimization.h | 30 +++++++++++++++++- src/muz/fp/dl_cmds.cpp | 7 +---- src/opt/opt_cmds.cpp | 31 +++++++++++-------- src/opt/opt_cmds.h | 3 +- src/smt/smt_consequences.cpp | 59 ++++++++++++++++++++++++++++++++++-- src/smt/smt_context.h | 4 ++- 10 files changed, 188 insertions(+), 25 deletions(-) diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index c0a311929..58d8902c3 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -23,9 +23,10 @@ Revision History: #include"api_util.h" #include"api_model.h" #include"opt_context.h" +#include"opt_cmds.h" #include"cancel_eh.h" #include"scoped_timer.h" - +#include"smt2parser.h" extern "C" { @@ -248,6 +249,53 @@ extern "C" { Z3_CATCH_RETURN(0); } + static void Z3_optimize_from_stream( + Z3_context c, + Z3_optimize opt, + std::istream& s) { + ast_manager& m = mk_c(c)->m(); + cmd_context ctx(false, &m); + install_opt_cmds(ctx, to_optimize_ptr(opt)); + ctx.set_ignore_check(true); + if (!parse_smt2_commands(ctx, s)) { + SET_ERROR_CODE(Z3_PARSER_ERROR); + return; + } + ptr_vector::const_iterator it = ctx.begin_assertions(); + ptr_vector::const_iterator end = ctx.end_assertions(); + for (; it != end; ++it) { + to_optimize_ptr(opt)->add_hard_constraint(*it); + } + } + + void Z3_API Z3_optimize_from_string( + Z3_context c, + Z3_optimize d, + Z3_string s) { + Z3_TRY; + //LOG_Z3_optimize_from_string(c, d, s); + std::string str(s); + std::istringstream is(str); + Z3_optimize_from_stream(c, d, is); + Z3_CATCH; + } + + void Z3_API Z3_optimize_from_file( + Z3_context c, + Z3_optimize d, + Z3_string s) { + Z3_TRY; + //LOG_Z3_optimize_from_file(c, d, s); + std::ifstream is(s); + if (!is) { + SET_ERROR_CODE(Z3_PARSER_ERROR); + return; + } + Z3_optimize_from_stream(c, d, is); + Z3_CATCH; + } + + }; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 5d01ef5c2..3271d4b0f 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2035,6 +2035,8 @@ namespace z3 { } stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); } friend std::ostream & operator<<(std::ostream & out, optimize const & s); + void from_file(char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); } + void from_string(char const* constraints) { Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); } std::string help() const { char const * r = Z3_optimize_get_help(ctx(), m_opt); check_error(); return r; } }; inline std::ostream & operator<<(std::ostream & out, optimize const & s) { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; } diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index 304e3e86f..e5982e4fc 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -273,6 +273,25 @@ namespace Microsoft.Z3 return Native.Z3_optimize_to_string(Context.nCtx, NativeObject); } + /// + /// Parse an SMT-LIB2 file with optimization objectives and constraints. + /// The parsed constraints and objectives are added to the optimization context. + /// + public void FromFile(string file) + { + Native.Z3_optimize_from_file(Context.nCtx, NativeObject, file); + } + + /// + /// Similar to FromFile. Instead it takes as argument a string. + /// + public void FromString(string s) + { + Native.Z3_optimize_from_string(Context.nCtx, NativeObject, s); + } + + + /// /// Optimize statistics. /// diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 6e3ef26ac..6c4ac13a4 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -6755,6 +6755,14 @@ class Optimize(Z3PPObject): raise Z3Exception("Expecting objective handle returned by maximize/minimize") return obj.upper() + def from_file(self, filename): + """Parse assertions and objectives from a file""" + Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename) + + def from_string(self, s): + """Parse assertions and objectives from a string""" + Z3_optimize_from_string(self.ctx.ref(), self.optimize, s) + def __repr__(self): """Return a formatted string with all added rules and constraints.""" return self.sexpr() diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index c59428d9e..15a6dff16 100644 --- a/src/api/z3_optimization.h +++ b/src/api/z3_optimization.h @@ -197,6 +197,34 @@ extern "C" { */ Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o); + /** + \brief Parse an SMT-LIB2 string with assertions, + soft constraints and optimization objectives. + Add the parsed constraints and objectives to the optimization context. + + \param c - context. + \param o - optimize context. + \param s - string containing SMT2 specification. + + def_API('Z3_optimize_from_string', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(STRING))) + */ + void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s); + + + /** + \brief Parse an SMT-LIB2 file with assertions, + soft constraints and optimization objectives. + Add the parsed constraints and objectives to the optimization context. + + + \param c - context. + \param o - optimize context. + \param s - string containing SMT2 specification. + + def_API('Z3_optimize_from_file', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(STRING))) + */ + void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s); + /** \brief Return a string containing a description of parameters accepted by optimize. @@ -218,4 +246,4 @@ extern "C" { } #endif // __cplusplus -#endif \ No newline at end of file +#endif diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 049c34343..49632b39c 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -527,13 +527,8 @@ static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_c ctx.insert(alloc(dl_query_cmd, dl_ctx)); ctx.insert(alloc(dl_declare_rel_cmd, dl_ctx)); ctx.insert(alloc(dl_declare_var_cmd, dl_ctx)); - // #ifndef _EXTERNAL_RELEASE - // TODO: we need these! -#if 1 - ctx.insert(alloc(dl_push_cmd, dl_ctx)); // not exposed to keep command-extensions simple. + ctx.insert(alloc(dl_push_cmd, dl_ctx)); ctx.insert(alloc(dl_pop_cmd, dl_ctx)); -#endif - // #endif } void install_dl_cmds(cmd_context & ctx) { diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 8822f4e77..5406eaca3 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -32,7 +32,10 @@ Notes: #include "opt_params.hpp" #include "model_smt2_pp.h" -static opt::context& get_opt(cmd_context& cmd) { +static opt::context& get_opt(cmd_context& cmd, opt::context* opt) { + if (opt) { + return *opt; + } if (!cmd.get_opt()) { cmd.set_opt(alloc(opt::context, cmd.m())); } @@ -43,12 +46,14 @@ static opt::context& get_opt(cmd_context& cmd) { class assert_soft_cmd : public parametric_cmd { unsigned m_idx; expr* m_formula; + opt::context* m_opt; public: - assert_soft_cmd(): + assert_soft_cmd(opt::context* opt): parametric_cmd("assert-soft"), m_idx(0), - m_formula(0) + m_formula(0), + m_opt(opt) {} virtual ~assert_soft_cmd() { @@ -96,8 +101,8 @@ public: if (weight.is_zero()) { weight = rational::one(); } - symbol id = ps().get_sym(symbol("id"), symbol::null); - get_opt(ctx).add_soft_constraint(m_formula, weight, id); + symbol id = ps().get_sym(symbol("id"), symbol::null); + get_opt(ctx, m_opt).add_soft_constraint(m_formula, weight, id); reset(ctx); } @@ -108,11 +113,13 @@ public: class min_maximize_cmd : public cmd { bool m_is_max; + opt::context* m_opt; public: - min_maximize_cmd(bool is_max): + min_maximize_cmd(bool is_max, opt::context* opt): cmd(is_max?"maximize":"minimize"), - m_is_max(is_max) + m_is_max(is_max), + m_opt(opt) {} virtual void reset(cmd_context & ctx) { } @@ -126,7 +133,7 @@ public: if (!is_app(t)) { throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable"); } - get_opt(ctx).add_objective(to_app(t), m_is_max); + get_opt(ctx, m_opt).add_objective(to_app(t), m_is_max); } virtual void failure_cleanup(cmd_context & ctx) { @@ -139,10 +146,10 @@ public: -void install_opt_cmds(cmd_context & ctx) { - ctx.insert(alloc(assert_soft_cmd)); - ctx.insert(alloc(min_maximize_cmd, true)); - ctx.insert(alloc(min_maximize_cmd, false)); +void install_opt_cmds(cmd_context & ctx, opt::context* opt) { + ctx.insert(alloc(assert_soft_cmd, opt)); + ctx.insert(alloc(min_maximize_cmd, true, opt)); + ctx.insert(alloc(min_maximize_cmd, false, opt)); } diff --git a/src/opt/opt_cmds.h b/src/opt/opt_cmds.h index d8dd0dbfa..f0da778df 100644 --- a/src/opt/opt_cmds.h +++ b/src/opt/opt_cmds.h @@ -19,10 +19,11 @@ Notes: #define OPT_CMDS_H_ #include "ast.h" +#include "opt_context.h" class cmd_context; -void install_opt_cmds(cmd_context & ctx); +void install_opt_cmds(cmd_context & ctx, opt::context* opt = 0); #endif diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 87a50e82f..49236be1b 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -102,6 +102,47 @@ namespace smt { } } + void context::delete_unfixed(obj_map& var2val) { + ast_manager& m = m_manager; + ptr_vector to_delete; + obj_map::iterator it = var2val.begin(), end = var2val.end(); + for (; it != end; ++it) { + expr* k = it->m_key; + expr* v = it->m_value; + if (m.is_bool(k)) { + literal lit = get_literal(k); + switch (get_assignment(lit)) { + case l_true: + if (m.is_false(v)) { + to_delete.push_back(k); + } + else { + force_phase(lit.var(), false); + } + break; + case l_false: + if (m.is_true(v)) { + to_delete.push_back(k); + } + else { + force_phase(lit.var(), true); + } + break; + default: + to_delete.push_back(k); + break; + } + } + else if (e_internalized(k) && m.are_distinct(v, get_enode(k)->get_root()->get_owner())) { + to_delete.push_back(k); + } + } + IF_VERBOSE(1, verbose_stream() << "(get-consequences deleting: " << to_delete.size() << " num-values: " << var2val.size() << ")\n";); + for (unsigned i = 0; i < to_delete.size(); ++i) { + var2val.remove(to_delete[i]); + } + } + lbool context::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) { @@ -135,7 +176,10 @@ namespace smt { tout << "vars: " << vars.size() << "\n"; tout << "lits: " << num_units << "\n";); m_case_split_queue->init_search_eh(); + unsigned num_iterations = 0; + unsigned model_threshold = 2; while (!var2val.empty()) { + ++num_iterations; obj_map::iterator it = var2val.begin(); expr* e = it->m_key; expr* val = it->m_value; @@ -177,6 +221,17 @@ namespace smt { else { TRACE("context", tout << "Fixed: " << mk_pp(e, m) << "\n";); } + + TRACE("context", tout << "Unfixed variables: " << var2val.size() << "\n";); + if (model_threshold <= num_iterations) { + delete_unfixed(var2val); + // The next time we check the model is after 1.5 additional iterations. + model_threshold *= 3; + model_threshold /= 2; + } + // repeat until we either have a model with negated literal or + // the literal is implied at base. + extract_fixed_consequences(num_units, var2val, _assumptions, conseq); num_units = assigned_literals().size(); if (var2val.contains(e)) { @@ -189,10 +244,8 @@ namespace smt { SASSERT(get_assignment(lit) == l_false); } - // repeat until we either have a model with negated literal or - // the literal is implied at base. - TRACE("context", tout << "Unfixed variables: " << var2val.size() << "\n";); } + end_search(); return l_true; } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index e6ca16290..30a262285 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1345,7 +1345,9 @@ namespace smt { vector b2v, ast_translation& tr); u_map m_antecedents; - void extract_fixed_consequences(unsigned idx, obj_map& vars, uint_set const& assumptions, expr_ref_vector& conseq); + void extract_fixed_consequences(unsigned idx, obj_map& var2val, uint_set const& assumptions, expr_ref_vector& conseq); + + void delete_unfixed(obj_map& var2val); expr_ref antecedent2fml(uint_set const& ante);