diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 7236a7682..d4dac1db3 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -185,6 +185,28 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o) { + Z3_TRY; + LOG_Z3_optimize_to_string(c, o); + RESET_ERROR_CODE(); + return mk_c(c)->mk_external_string(to_optimize_ref(o).to_string()); + Z3_CATCH_RETURN(""); + } + + Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize d) { + Z3_TRY; + LOG_Z3_optimize_get_help(c, d); + RESET_ERROR_CODE(); + std::ostringstream buffer; + param_descrs descrs; + to_optimize_ref(d).collect_param_descrs(descrs); + descrs.display(buffer); + return mk_c(c)->mk_external_string(buffer.str()); + Z3_CATCH_RETURN(""); + } + + + #if 0 /** diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index 925773fa5..fb4af9206 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -31,7 +31,6 @@ namespace Microsoft.Z3 { HashSet indices; -#if false /// /// A string that describes all available optimize solver parameters. /// @@ -43,7 +42,6 @@ namespace Microsoft.Z3 return Native.Z3_optimize_get_help(Context.nCtx, NativeObject); } } -#endif /// /// Sets the optimize solver parameters. @@ -157,7 +155,7 @@ namespace Microsoft.Z3 } } - public uint MkMaximize(ArithExpr e) + public uint MkMaximize(ArithExpr e) { uint index = Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject); indices.Add(index); @@ -166,15 +164,15 @@ namespace Microsoft.Z3 public uint MkMinimize(ArithExpr e) { - uint index = Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject); + uint index = Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject); indices.Add(index); return index; - } + } - public ArithExpr GetLower(uint index) + public ArithExpr GetLower(uint index) { Contract.Requires(indices.Contains(index)); - return new ArithExpr(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index)); + return new ArithExpr(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index)); } public ArithExpr GetUpper(uint index) @@ -183,6 +181,11 @@ namespace Microsoft.Z3 return new ArithExpr(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index)); } + public override string ToString() + { + return Native.Z3_optimize_to_string(Context.nCtx, NativeObject); + } + #region Internal internal Optimize(Context ctx, IntPtr obj) : base(ctx, obj) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 9350eb529..58bbe0fe9 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6075,6 +6075,26 @@ END_MLAPI_EXCLUDE */ Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx); + /** + \brief Print the current context as a string. + \param c - context. + \param o - optimization context. + + def_API('Z3_optimize_to_string', STRING, (_in(CONTEXT), _in(OPTIMIZE))) + */ + Z3_string Z3_API Z3_optimize_to_string( + __in Z3_context c, + __in Z3_optimize o); + + + /** + \brief Return a string containing a description of parameters accepted by optimize. + + def_API('Z3_optimize_get_help', STRING, (_in(CONTEXT), _in(OPTIMIZE))) + */ + Z3_string Z3_API Z3_optimize_get_help(__in Z3_context c, __in Z3_optimize t); + + #endif diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index b6bb15e52..413727b58 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -62,6 +62,10 @@ namespace opt { m_weights.push_back(w); } + unsigned size() const { return m_soft_constraints.size(); } + expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; } + rational weight(unsigned idx) const { return m_weights[idx]; } + void commit_assignment(); inf_eps get_value() const; inf_eps get_lower() const; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 78495c928..acbd8293d 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -22,6 +22,7 @@ Notes: #include "opt_solver.h" #include "opt_params.hpp" #include "arith_decl_plugin.h" +#include "for_each_expr.h" namespace opt { @@ -289,4 +290,114 @@ namespace opt { } } + typedef obj_hashtable func_decl_set; + + struct context::free_func_visitor { + ast_manager& m; + func_decl_set m_funcs; + obj_hashtable m_sorts; + expr_mark m_visited; + public: + free_func_visitor(ast_manager& m): m(m) {} + void operator()(var * n) { } + void operator()(app * n) { + m_funcs.insert(n->get_decl()); + sort* s = m.get_sort(n); + if (s->get_family_id() == null_family_id) { + m_sorts.insert(s); + } + } + void operator()(quantifier * n) { } + func_decl_set& funcs() { return m_funcs; } + obj_hashtable& sorts() { return m_sorts; } + + void collect(expr* e) { + for_each_expr(*this, m_visited, e); + } + }; + + std::string context::to_string() const { + smt2_pp_environment_dbg env(m); + free_func_visitor visitor(m); + std::ostringstream out; +#define PP(_e_) ast_smt2_pp(out, _e_, env); + for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { + visitor.collect(m_hard_constraints[i]); + } + for (unsigned i = 0; i < m_objectives.size(); ++i) { + objective const& obj = m_objectives[i]; + switch(obj.m_type) { + case O_MAXIMIZE: + case O_MINIMIZE: + visitor.collect(obj.m_term); + break; + case O_MAXSMT: { + maxsmt& ms = *m_maxsmts.find(obj.m_id); + for (unsigned j = 0; j < ms.size(); ++j) { + visitor.collect(ms[j]); + } + break; + } + default: + UNREACHABLE(); + break; + } + } + + obj_hashtable::iterator sit = visitor.sorts().begin(); + obj_hashtable::iterator send = visitor.sorts().end(); + for (; sit != send; ++sit) { + PP(*sit); + } + func_decl_set::iterator it = visitor.funcs().begin(); + func_decl_set::iterator end = visitor.funcs().end(); + for (; it != end; ++it) { + PP(*it); + out << "\n"; + } + for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { + out << "(assert "; + PP(m_hard_constraints[i]); + out << ")\n"; + } + for (unsigned i = 0; i < m_objectives.size(); ++i) { + objective const& obj = m_objectives[i]; + switch(obj.m_type) { + case O_MAXIMIZE: + out << "(maximize "; + PP(obj.m_term); + out << ")\n"; + break; + case O_MINIMIZE: + out << "(minimize "; + PP(obj.m_term); + out << ")\n"; + break; + case O_MAXSMT: { + maxsmt& ms = *m_maxsmts.find(obj.m_id); + for (unsigned j = 0; j < ms.size(); ++j) { + out << "(assert-soft "; + PP(ms[j]); + rational w = ms.weight(j); + if (w.is_int()) { + out << " :weight " << ms.weight(j); + } + else { + out << " :dweight " << ms.weight(j); + } + if (obj.m_id != symbol::null) { + out << " :id " << obj.m_id; + } + out << ")\n"; + } + break; + } + default: + UNREACHABLE(); + break; + } + } + return out.str(); + } + } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index cb46494cd..7ab30ec71 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -35,6 +35,7 @@ namespace opt { class opt_solver; class context { + struct free_func_visitor; typedef map map_t; typedef map map_id; enum objective_t { @@ -92,6 +93,8 @@ namespace opt { expr_ref get_lower(unsigned idx); expr_ref get_upper(unsigned idx); + std::string to_string() const; + private: void validate_feasibility(maxsmt& ms);