From 2e89c2de3d3eafcc45cd1539642dda1e9c2d0ee7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2017 09:35:04 -0800 Subject: [PATCH 01/13] add par_or tactic to C++ API. #873 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 979d9aed7..37e6448c9 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1933,6 +1933,7 @@ namespace z3 { friend tactic repeat(tactic const & t, unsigned max); friend tactic with(tactic const & t, params const & p); friend tactic try_for(tactic const & t, unsigned ms); + friend tactic par_or(unsigned n, tactic const* tactics); param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_tactic_get_param_descrs(ctx(), m_tactic)); } }; @@ -1966,7 +1967,14 @@ namespace z3 { t.check_error(); return tactic(t.ctx(), r); } - + inline tactic par_or(unsigned n, tactic const* tactics) { + if (n == 0) { + throw exception("a non-zero number of tactics need to be passed to par_or"); + } + array buffer(n); + for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i]; + return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr())); + } class probe : public object { Z3_probe m_probe; From b42973152fea616fd634dfb4c8a231e898b079a3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Feb 2017 12:02:32 -0500 Subject: [PATCH 02/13] fix model generation for non-linear expressions, reported by Martin Suda and Giles Reger Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith.h | 1 + src/smt/theory_arith_core.h | 6 +++++- src/smt/theory_arith_nl.h | 12 +++++++++--- 3 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 5a0f8db95..77882f186 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -946,6 +946,7 @@ namespace smt { // // ----------------------------------- typedef int_hashtable > row_set; + bool m_model_depends_on_computed_epsilon; unsigned m_nl_rounds; bool m_nl_gb_exhausted; unsigned m_nl_strategy_idx; // for fairness diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 9db5e8c72..513cf36a4 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1405,6 +1405,7 @@ namespace smt { template final_check_status theory_arith::final_check_core() { + m_model_depends_on_computed_epsilon = false; unsigned old_idx = m_final_check_idx; final_check_status result = FC_DONE; final_check_status ok; @@ -1669,6 +1670,7 @@ namespace smt { m_liberal_final_check(true), m_changed_assignment(false), m_assume_eq_head(0), + m_model_depends_on_computed_epsilon(false), m_nl_rounds(0), m_nl_gb_exhausted(false), m_nl_new_exprs(m), @@ -3220,7 +3222,9 @@ namespace smt { m_factory = alloc(arith_factory, get_manager()); m.register_factory(m_factory); compute_epsilon(); - refine_epsilon(); + if (!m_model_depends_on_computed_epsilon) { + refine_epsilon(); + } } template diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index dd91ffbfb..52a117cd5 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -638,6 +638,7 @@ namespace smt { if (!val.get_infinitesimal().is_zero() && !computed_epsilon) { compute_epsilon(); computed_epsilon = true; + m_model_depends_on_computed_epsilon = true; } return val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational(); } @@ -652,14 +653,18 @@ namespace smt { bool theory_arith::check_monomial_assignment(theory_var v, bool & computed_epsilon) { SASSERT(is_pure_monomial(var2expr(v))); expr * m = var2expr(v); - rational val(1); + rational val(1), v_val; for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { expr * arg = to_app(m)->get_arg(i); theory_var curr = expr2var(arg); SASSERT(curr != null_theory_var); - val *= get_value(curr, computed_epsilon); + v_val = get_value(curr, computed_epsilon); + TRACE("non_linear", tout << mk_pp(arg, get_manager()) << " = " << v_val << "\n";); + val *= v_val; } - return get_value(v, computed_epsilon) == val; + v_val = get_value(v, computed_epsilon); + TRACE("non_linear", tout << "v" << v << " := " << v_val << " == " << val << "\n";); + return v_val == val; } @@ -2356,6 +2361,7 @@ namespace smt { */ template final_check_status theory_arith::process_non_linear() { + m_model_depends_on_computed_epsilon = false; if (m_nl_monomials.empty()) return FC_DONE; From 4c6efbbc8bce874cedbf8ffb14a3b883df62e767 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Feb 2017 16:02:51 -0500 Subject: [PATCH 03/13] expose numerator/denominators for Martin and Giles Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e5d0acaab..e60809646 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -758,6 +758,20 @@ namespace z3 { return result; } + expr numerator() const { + assert(is_numeral()); + Z3_ast r = Z3_get_numerator(ctx(), m_ast); + check_error(); + return expr(ctx(),r); + } + + + expr denominator() const { + assert(is_numeral()); + Z3_ast r = Z3_get_denominator(ctx(), m_ast); + check_error(); + return expr(ctx(),r); + } operator Z3_app() const { assert(is_app()); return reinterpret_cast(m_ast); } From b3dabc7ccf9fde3997d8aaf1c3c61fd708a24803 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Feb 2017 16:28:15 -0500 Subject: [PATCH 04/13] add missing mod/rem/is_int functionality to C++ API Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 72 ++++++++++++++++++++++++++++++++-------------- 1 file changed, 50 insertions(+), 22 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index e60809646..d8027fbbc 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -435,6 +435,8 @@ namespace z3 { Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; } unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; } friend std::ostream & operator<<(std::ostream & out, ast const & n); + std::string to_string() const { return std::string(Z3_ast_to_string(ctx(), m_ast)); } + /** \brief Return true if the ASTs are structurally identical. @@ -757,7 +759,11 @@ namespace z3 { } return result; } - + + Z3_lbool bool_value() const { + return Z3_get_bool_value(ctx(), m_ast); + } + expr numerator() const { assert(is_numeral()); Z3_ast r = Z3_get_numerator(ctx(), m_ast); @@ -889,13 +895,23 @@ namespace z3 { friend expr operator*(expr const & a, int b); friend expr operator*(int a, expr const & b); - /** - \brief Power operator - */ + /* \brief Power operator */ friend expr pw(expr const & a, expr const & b); friend expr pw(expr const & a, int b); friend expr pw(int a, expr const & b); + /* \brief mod operator */ + friend expr mod(expr const& a, expr const& b); + friend expr mod(expr const& a, int b); + friend expr mod(int a, expr const& b); + + /* \brief rem operator */ + friend expr rem(expr const& a, expr const& b); + friend expr rem(expr const& a, int b); + friend expr rem(int a, expr const& b); + + friend expr is_int(expr const& e); + friend expr operator/(expr const & a, expr const & b); friend expr operator/(expr const & a, int b); friend expr operator/(int a, expr const & b); @@ -1026,34 +1042,46 @@ namespace z3 { }; +#define _Z3_MK_BIN_(a, b, binop) \ + check_context(a, b); \ + Z3_ast r = binop(a.ctx(), a, b); \ + a.check_error(); \ + return expr(a.ctx(), r); \ + + inline expr implies(expr const & a, expr const & b) { - check_context(a, b); - assert(a.is_bool() && b.is_bool()); - Z3_ast r = Z3_mk_implies(a.ctx(), a, b); - a.check_error(); - return expr(a.ctx(), r); + assert(a.is_bool() && b.is_bool()); + _Z3_MK_BIN_(a, b, Z3_mk_implies); } inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); } inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); } - inline expr pw(expr const & a, expr const & b) { - assert(a.is_arith() && b.is_arith()); - check_context(a, b); - Z3_ast r = Z3_mk_power(a.ctx(), a, b); - a.check_error(); - return expr(a.ctx(), r); - } + inline expr pw(expr const & a, expr const & b) { _Z3_MK_BIN_(a, b, Z3_mk_power); } inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); } inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); } + inline expr mod(expr const& a, expr const& b) { _Z3_MK_BIN_(a, b, Z3_mk_mod); } + inline expr mod(expr const & a, int b) { return mod(a, a.ctx().num_val(b, a.get_sort())); } + inline expr mod(int a, expr const & b) { return mod(b.ctx().num_val(a, b.get_sort()), b); } - inline expr operator!(expr const & a) { - assert(a.is_bool()); - Z3_ast r = Z3_mk_not(a.ctx(), a); - a.check_error(); - return expr(a.ctx(), r); - } + inline expr rem(expr const& a, expr const& b) { _Z3_MK_BIN_(a, b, Z3_mk_rem); } + inline expr rem(expr const & a, int b) { return rem(a, a.ctx().num_val(b, a.get_sort())); } + inline expr rem(int a, expr const & b) { return rem(b.ctx().num_val(a, b.get_sort()), b); } + +#undef _Z3_MK_BIN_ + +#define _Z3_MK_UN_(a, mkun) \ + Z3_ast r = mkun(a.ctx(), a); \ + a.check_error(); \ + return expr(a.ctx(), r); \ + + + inline expr operator!(expr const & a) { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); } + + inline expr is_int(expr const& e) { _Z3_MK_UN_(e, Z3_mk_is_int); } + +#undef _Z3_MK_UN_ inline expr operator&&(expr const & a, expr const & b) { check_context(a, b); From 6fcba26ea6c695628fa701aee0e8cf78141ba8d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Feb 2017 09:56:49 -0800 Subject: [PATCH 05/13] make parameters accessible from expressions. Issue #896 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index f1fde1720..6729d99b5 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -868,6 +868,9 @@ class ExprRef(AstRef): _args, sz = _to_ast_array((a, b)) return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx) + def params(self): + return self.decl().params() + def decl(self): """Return the Z3 function declaration associated with a Z3 application. From e7a21dfac21c6f34576a7475b520695e5b5fb9fa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Feb 2017 08:16:39 -0800 Subject: [PATCH 06/13] add par_and_then Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 37e6448c9..e655815ca 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1934,6 +1934,7 @@ namespace z3 { friend tactic with(tactic const & t, params const & p); friend tactic try_for(tactic const & t, unsigned ms); friend tactic par_or(unsigned n, tactic const* tactics); + friend tactic par_and_then(tactic const& t1, tactic const& t2); param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_tactic_get_param_descrs(ctx(), m_tactic)); } }; @@ -1976,6 +1977,13 @@ namespace z3 { return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr())); } + inline tactic par_and_then(tactic const & t1, tactic const & t2) { + check_context(t1, t2); + Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2); + t1.check_error(); + return tactic(t1.ctx(), r); + } + class probe : public object { Z3_probe m_probe; void init(Z3_probe s) { From c67cf1653ca51d47bee7eaeee43bf3f8e5f3e3ea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Feb 2017 08:46:58 -0800 Subject: [PATCH 07/13] use non _ method from z3printer module so to be resilient against how _ is handled as indicator of private functions Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3printer.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index 8a67fa911..aef71be2f 100644 --- a/src/api/python/z3/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -678,7 +678,7 @@ class Formatter: if self.fpa_pretty: if self.is_infix(k) and n >= 3: rm = a.arg(0) - if z3.is_fprm_value(rm) and z3._dflt_rm(a.ctx).eq(rm): + if z3.is_fprm_value(rm) and z3.get_default_rounding_mode(a.ctx).eq(rm): arg1 = to_format(self.pp_expr(a.arg(1), d+1, xs)) arg2 = to_format(self.pp_expr(a.arg(2), d+1, xs)) r = [] From 61bbf8ba7e76804df07ff9f853ef076224e3acef Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 23 Feb 2017 18:24:08 -0500 Subject: [PATCH 08/13] add octal escape to seq_decl_plugin --- src/ast/seq_decl_plugin.cpp | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index c645aa1a7..66e1cf239 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -38,8 +38,16 @@ static bool is_hex_digit(char ch, unsigned& d) { return false; } +static bool is_octal_digit(char ch, unsigned& d) { + if ('0' <= ch && ch <= '7') { + d = ch - '0'; + return true; + } + return false; +} + static bool is_escape_char(char const *& s, unsigned& result) { - unsigned d1, d2; + unsigned d1, d2, d3; if (*s != '\\' || *(s + 1) == 0) { return false; } @@ -49,6 +57,12 @@ static bool is_escape_char(char const *& s, unsigned& result) { s += 4; return true; } + if (is_octal_digit(*(s + 1), d1) && is_octal_digit(*(s + 2), d2) && + is_octal_digit(*(s + 3), d3)) { + result = d1*64 + d2*8 + d3; + s += 4; + return true; + } switch (*(s + 1)) { case 'a': result = '\a'; From eb0ba26f907c0e662e0c236292757a6fd3b4ad43 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 23 Feb 2017 18:33:10 -0500 Subject: [PATCH 09/13] C-style octal escapes, including 1- and 2-digit escapes --- src/ast/seq_decl_plugin.cpp | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 66e1cf239..16ce65ec3 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -57,6 +57,23 @@ static bool is_escape_char(char const *& s, unsigned& result) { s += 4; return true; } + /* C-standard octal escapes: either 1, 2, or 3 octal digits, + * stopping either at 3 digits or at the first non-digit character. + */ + /* 1 octal digit */ + if (is_octal_digit(*(s + 1), d1) && !is_octal_digit(*(s + 2), d2)) { + result = d1; + s += 2; + return true; + } + /* 2 octal digits */ + if (is_octal_digit(*(s + 1), d1) && is_octal_digit(*(s + 2), d2) && + !is_octal_digit(*(s + 3), d3)) { + result = d1 * 8 + d2; + s += 3; + return true; + } + /* 3 octal digits */ if (is_octal_digit(*(s + 1), d1) && is_octal_digit(*(s + 2), d2) && is_octal_digit(*(s + 3), d3)) { result = d1*64 + d2*8 + d3; From e02160c67497b953aae5b131a6f02b79d7e722ca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Feb 2017 11:07:40 -0800 Subject: [PATCH 10/13] expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911 Signed-off-by: Nikolaj Bjorner --- src/api/api_opt.cpp | 28 +++++++++++++++++++++++++ src/api/dotnet/Optimize.cs | 36 +++++++++++++++++++++++++++++++++ src/api/python/z3/z3.py | 22 ++++++++++++++++++++ src/api/z3_optimization.h | 27 +++++++++++++++++++++++++ src/cmd_context/tactic_cmds.cpp | 2 +- src/opt/opt_context.cpp | 12 ++++++++++- src/opt/opt_context.h | 4 ++++ src/smt/tactic/smt_tactic.cpp | 26 +++++++++++++++++++++++- src/solver/mus.cpp | 1 + src/solver/tactic2solver.cpp | 2 ++ src/tactic/tactic.cpp | 2 +- 11 files changed, 158 insertions(+), 4 deletions(-) diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 3d8580178..a2299aec3 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -218,6 +218,34 @@ extern "C" { Z3_CATCH_RETURN(0); } + // get lower value or current approximation + Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx) { + Z3_TRY; + LOG_Z3_optimize_get_lower_as_vector(c, o, idx); + RESET_ERROR_CODE(); + expr_ref_vector es(mk_c(c)->m()); + to_optimize_ptr(o)->get_lower(idx, es); + Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); + mk_c(c)->save_object(v); + v->m_ast_vector.append(es.size(), (ast*const*)es.c_ptr()); + RETURN_Z3(of_ast_vector(v)); + Z3_CATCH_RETURN(0); + } + + // get upper or current approximation + Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx) { + Z3_TRY; + LOG_Z3_optimize_get_upper_as_vector(c, o, idx); + RESET_ERROR_CODE(); + expr_ref_vector es(mk_c(c)->m()); + to_optimize_ptr(o)->get_upper(idx, es); + Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); + mk_c(c)->save_object(v); + v->m_ast_vector.append(es.size(), (ast*const*)es.c_ptr()); + RETURN_Z3(of_ast_vector(v)); + 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); diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index c8954a473..99dd9aac0 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -144,6 +144,23 @@ namespace Microsoft.Z3 { get { return Lower; } } + + /// + /// Retrieve a lower bound for the objective handle. + /// + public ArithExpr[] LowerAsVector + { + get { return opt.GetLowerAsVector(handle); } + } + + /// + /// Retrieve an upper bound for the objective handle. + /// + public ArithExpr[] UpperAsVector + { + get { return opt.GetUpperAsVector(handle); } + } + } /// @@ -255,6 +272,25 @@ namespace Microsoft.Z3 return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index)); } + /// + /// Retrieve a lower bound for the objective handle. + /// + private ArithExpr[] GetLowerAsVector(uint index) + { + ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_lower_as_vector(Context.nCtx, NativeObject, index)); + return v.ToArithExprArray(); + } + + + /// + /// Retrieve an upper bound for the objective handle. + /// + private ArithExpr[] GetUpperAsVector(uint index) + { + ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_upper_as_vector(Context.nCtx, NativeObject, index)); + return v.ToArithExprArray(); + } + /// /// Return a string the describes why the last to check returned unknown /// diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 6729d99b5..a0aba95d6 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6719,12 +6719,24 @@ class OptimizeObjective: opt = self._opt return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx) + def lower_values(self): + opt = self._opt + return AstVector(Z3_optimize_get_lower_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx) + + def upper_values(self): + opt = self._opt + return AstVector(Z3_optimize_get_upper_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx) + def value(self): if self._is_max: return self.upper() else: return self.lower() + def __str__(self): + return "%s:%s" % (self._value, self._is_max) + + class Optimize(Z3PPObject): """Optimize API provides methods for solving using objective functions and weighted soft constraints""" @@ -6829,6 +6841,16 @@ class Optimize(Z3PPObject): raise Z3Exception("Expecting objective handle returned by maximize/minimize") return obj.upper() + def lower_values(self, obj): + if not isinstance(obj, OptimizeObjective): + raise Z3Exception("Expecting objective handle returned by maximize/minimize") + return obj.lower_values() + + def upper_values(self, obj): + if not isinstance(obj, OptimizeObjective): + raise Z3Exception("Expecting objective handle returned by maximize/minimize") + return obj.upper_values() + def from_file(self, filename): """Parse assertions and objectives from a file""" Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename) diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index f7a9a8fe9..795b4b8fd 100644 --- a/src/api/z3_optimization.h +++ b/src/api/z3_optimization.h @@ -186,6 +186,33 @@ extern "C" { */ Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx); + + /** + \brief Retrieve lower bound value or approximation for the i'th optimization objective. + The returned vector is of length 3. It always contains numerals. + The three numerals are coefficients a, b, c and encode the result of \c Z3_optimize_get_lower + a * infinity + b + c * epsilon. + + \param c - context + \param o - optimization context + \param idx - index of optimization objective + + def_API('Z3_optimize_get_lower_as_vector', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT))) + */ + Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx); + + /** + \brief Retrieve upper bound value or approximation for the i'th optimization objective. + + \param c - context + \param o - optimization context + \param idx - index of optimization objective + + def_API('Z3_optimize_get_upper_as_vector', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT))) + */ + Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx); + + /** \brief Print the current context as a string. \param c - context. diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 2f7b1ea6e..2b60486f7 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -223,7 +223,7 @@ public: cmd_context::scoped_watch sw(ctx); lbool r = l_undef; try { - r = check_sat(t, g, md, result->labels, pr, core, reason_unknown); + r = check_sat(t, g, md, result->labels, pr, core, reason_unknown); ctx.display_sat_result(r); result->set_status(r); if (r == l_undef) { diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 56b152caa..ebe56381a 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1290,6 +1290,15 @@ namespace opt { return to_expr(get_upper_as_num(idx)); } + void context::to_exprs(inf_eps const& n, expr_ref_vector& es) { + rational inf = n.get_infinity(); + rational r = n.get_rational(); + rational eps = n.get_infinitesimal(); + es.push_back(m_arith.mk_numeral(inf, inf.is_int())); + es.push_back(m_arith.mk_numeral(r, r.is_int())); + es.push_back(m_arith.mk_numeral(eps, eps.is_int())); + } + expr_ref context::to_expr(inf_eps const& n) { rational inf = n.get_infinity(); rational r = n.get_rational(); @@ -1455,9 +1464,10 @@ namespace opt { void context::validate_maxsat(symbol const& id) { maxsmt& ms = *m_maxsmts.find(id); + TRACE("opt", tout << "Validate: " << id << "\n";); for (unsigned i = 0; i < m_objectives.size(); ++i) { objective const& obj = m_objectives[i]; - if (obj.m_id == id) { + if (obj.m_id == id && obj.m_type == O_MAXSMT) { SASSERT(obj.m_type == O_MAXSMT); rational value(0); expr_ref val(m); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 461506258..f51f75830 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -207,6 +207,9 @@ namespace opt { expr_ref get_lower(unsigned idx); expr_ref get_upper(unsigned idx); + void get_lower(unsigned idx, expr_ref_vector& es) { to_exprs(get_lower_as_num(idx), es); } + void get_upper(unsigned idx, expr_ref_vector& es) { to_exprs(get_upper_as_num(idx), es); } + std::string to_string() const; @@ -238,6 +241,7 @@ namespace opt { lbool adjust_unknown(lbool r); bool scoped_lex(); expr_ref to_expr(inf_eps const& n); + void to_exprs(inf_eps const& n, expr_ref_vector& es); void reset_maxsmts(); void import_scoped_state(); diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index bd2c72c3e..ee3171d03 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -25,6 +25,9 @@ Notes: #include"filter_model_converter.h" #include"ast_util.h" #include"solver2tactic.h" +#include"smt_solver.h" +#include"solver.h" +#include"mus.h" typedef obj_map expr2expr_map; @@ -159,6 +162,8 @@ public: ref fmc; if (in->unsat_core_enabled()) { extract_clauses_and_dependencies(in, clauses, assumptions, bool2dep, fmc); + TRACE("mus", in->display_with_dependencies(tout); + tout << clauses << "\n";); if (in->proofs_enabled() && !assumptions.empty()) throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores"); for (unsigned i = 0; i < clauses.size(); ++i) { @@ -224,8 +229,26 @@ public: pr = m_ctx->get_proof(); if (in->unsat_core_enabled()) { unsigned sz = m_ctx->get_unsat_core_size(); + expr_ref_vector _core(m); + for (unsigned i = 0; i < sz; ++i) { + _core.push_back(m_ctx->get_unsat_core_expr(i)); + } + if (sz > 0 && smt_params_helper(m_params_ref).core_minimize()) { + std::cout << "size1 " << sz << " " << clauses << "\n"; + ref slv = mk_smt_solver(m, m_params_ref, m_logic); + slv->assert_expr(clauses); + mus mus(*slv.get()); + mus.add_soft(_core.size(), _core.c_ptr()); + lbool got_core = mus.get_mus(_core); + sz = _core.size(); + std::cout << "size2 " << sz << "\n"; + if (got_core != l_true) { + r = l_undef; + goto undef_case; + } + } for (unsigned i = 0; i < sz; i++) { - expr * b = m_ctx->get_unsat_core_expr(i); + expr * b = _core[i].get(); SASSERT(is_uninterp_const(b) && m.is_bool(b)); expr * d = bool2dep.find(b); lcore = m.mk_join(lcore, m.mk_leaf(d)); @@ -236,6 +259,7 @@ public: return; } case l_undef: + undef_case: if (m_ctx->canceled()) { throw tactic_exception(Z3_CANCELED_MSG); } diff --git a/src/solver/mus.cpp b/src/solver/mus.cpp index 91d47386e..d536a191b 100644 --- a/src/solver/mus.cpp +++ b/src/solver/mus.cpp @@ -89,6 +89,7 @@ struct mus::imp { lbool get_mus1(expr_ref_vector& mus) { ptr_vector unknown(m_lit2expr.size(), m_lit2expr.c_ptr()); ptr_vector core_exprs; + TRACE("mus", m_solver.display(tout);); while (!unknown.empty()) { IF_VERBOSE(12, verbose_stream() << "(mus reducing core: " << unknown.size() << " new core: " << mus.size() << ")\n";); TRACE("mus", display_vec(tout << "core: ", unknown); display_vec(tout << "mus: ", mus);); diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index b0a4c0e4f..e451f57d4 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -290,3 +290,5 @@ solver_factory * mk_tactic2solver_factory(tactic * t) { solver_factory * mk_tactic_factory2solver_factory(tactic_factory * f) { return alloc(tactic_factory2solver_factory, f); } + + diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 67fce1486..ac63a2d24 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -23,7 +23,6 @@ Notes: #include"model_v2_pp.h" - struct tactic_report::imp { char const * m_id; goal const & m_goal; @@ -175,6 +174,7 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_conve } } + lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) { bool models_enabled = g->models_enabled(); bool proofs_enabled = g->proofs_enabled(); From 183ee7e37dc5dd3ad7e956e6aafd4b099430980c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Feb 2017 11:10:18 -0800 Subject: [PATCH 11/13] expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911 Signed-off-by: Nikolaj Bjorner --- src/smt/tactic/smt_tactic.cpp | 20 +------------------- 1 file changed, 1 insertion(+), 19 deletions(-) diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index ee3171d03..127595e9e 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -229,26 +229,8 @@ public: pr = m_ctx->get_proof(); if (in->unsat_core_enabled()) { unsigned sz = m_ctx->get_unsat_core_size(); - expr_ref_vector _core(m); - for (unsigned i = 0; i < sz; ++i) { - _core.push_back(m_ctx->get_unsat_core_expr(i)); - } - if (sz > 0 && smt_params_helper(m_params_ref).core_minimize()) { - std::cout << "size1 " << sz << " " << clauses << "\n"; - ref slv = mk_smt_solver(m, m_params_ref, m_logic); - slv->assert_expr(clauses); - mus mus(*slv.get()); - mus.add_soft(_core.size(), _core.c_ptr()); - lbool got_core = mus.get_mus(_core); - sz = _core.size(); - std::cout << "size2 " << sz << "\n"; - if (got_core != l_true) { - r = l_undef; - goto undef_case; - } - } for (unsigned i = 0; i < sz; i++) { - expr * b = _core[i].get(); + expr * b = m_ctx->get_unsat_core_expr(i); SASSERT(is_uninterp_const(b) && m.is_bool(b)); expr * d = bool2dep.find(b); lcore = m.mk_join(lcore, m.mk_leaf(d)); From c7591e3c99c2681130dbb2bd15d14c95baa8c733 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Feb 2017 11:13:08 -0800 Subject: [PATCH 12/13] remove unreferenced label Signed-off-by: Nikolaj Bjorner --- src/smt/tactic/smt_tactic.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 127595e9e..eef22fe06 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -241,7 +241,6 @@ public: return; } case l_undef: - undef_case: if (m_ctx->canceled()) { throw tactic_exception(Z3_CANCELED_MSG); } From 996c0f0666f18ad4719135aa3e964fb6c9103c35 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 Feb 2017 16:14:50 -0800 Subject: [PATCH 13/13] fix type on exception message Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/enum2bv_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp index cd0f54503..08e7b0f69 100644 --- a/src/ast/rewriter/enum2bv_rewriter.cpp +++ b/src/ast/rewriter/enum2bv_rewriter.cpp @@ -85,7 +85,7 @@ struct enum2bv_rewriter::imp { void throw_non_fd(expr* e) { std::stringstream strm; - strm << "unabled nested data-type expression " << mk_pp(e, m); + strm << "unable to handle nested data-type expression " << mk_pp(e, m); throw rewriter_exception(strm.str().c_str()); }