From 2e89c2de3d3eafcc45cd1539642dda1e9c2d0ee7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2017 09:35:04 -0800 Subject: [PATCH 01/18] 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 e7a21dfac21c6f34576a7475b520695e5b5fb9fa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Feb 2017 08:16:39 -0800 Subject: [PATCH 02/18] 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 03/18] 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 04/18] 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 05/18] 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 0ebd93c8b513d8b7552a99bda491a8d01f5eebcd Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 23 Feb 2017 20:57:19 -0500 Subject: [PATCH 06/18] add _re.unroll internal operator to seq_decl_plugin --- src/ast/seq_decl_plugin.cpp | 5 +++++ src/ast/seq_decl_plugin.h | 2 ++ 2 files changed, 7 insertions(+) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 16ce65ec3..d671694e3 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -473,6 +473,7 @@ void seq_decl_plugin::init() { sort* str2TintT[3] = { strT, strT, intT }; sort* seqAintT[2] = { seqA, intT }; sort* seq3A[3] = { seqA, seqA, seqA }; + sort* reTintT[2] = { reT, intT }; m_sigs.resize(LAST_SEQ_OP); // TBD: have (par ..) construct and load parameterized signature from premable. m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq.unit", 1, 1, &A, seqA); @@ -516,6 +517,7 @@ void seq_decl_plugin::init() { m_sigs[_OP_REGEXP_EMPTY] = alloc(psig, m, "re.nostr", 0, 0, 0, reT); m_sigs[_OP_REGEXP_FULL] = alloc(psig, m, "re.allchar", 0, 0, 0, reT); m_sigs[_OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT); + m_sigs[_OP_RE_UNROLL] = alloc(psig, m, "_re.unroll", 0, 2, reTintT, strT); } void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { @@ -672,6 +674,9 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters"); } + case _OP_RE_UNROLL: + match(*m_sigs[k], arity, domain, range, rng); + return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); case OP_STRING_CONST: if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) { diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index fbbcba5de..b07e4d307 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -79,6 +79,7 @@ enum seq_op_kind { _OP_REGEXP_EMPTY, _OP_REGEXP_FULL, _OP_SEQ_SKOLEM, + _OP_RE_UNROLL, LAST_SEQ_OP }; @@ -334,6 +335,7 @@ public: MATCH_UNARY(is_opt); bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi); bool is_loop(expr const* n, expr*& body, unsigned& lo); + bool is_unroll(expr const* n) const { return is_app_of(n, m_fid, _OP_RE_UNROLL); } }; str str; re re; From e02160c67497b953aae5b131a6f02b79d7e722ca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Feb 2017 11:07:40 -0800 Subject: [PATCH 07/18] 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 08/18] 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 09/18] 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 10/18] 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()); } From 899843b7cdac31fa8d0f6435f9a5f3b7c710fbe6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Feb 2017 17:20:54 -0800 Subject: [PATCH 11/18] fix unhandled finite domain sort rewrite case. Issue #918 Signed-off-by: Nikolaj Bjorner --- src/tactic/bv/dt2bv_tactic.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 2ccbe9712..2b9cfb7f3 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -64,7 +64,10 @@ class dt2bv_tactic : public tactic { return; } - if (m_t.is_fd(a)) { + if (m_t.is_fd(a) && a->get_num_args() > 0) { + m_t.m_non_fd_sorts.insert(get_sort(a)); + } + else if (m_t.is_fd(a)) { m_t.m_fd_sorts.insert(get_sort(a)); } else { From d6c79facc7bded1ae5f474b8153fa6c9ac4c7909 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Mon, 27 Feb 2017 18:42:44 +0100 Subject: [PATCH 12/18] Java API for getting the objective value as a triple See #911 for the motivation, and e02160c67497b953aae5b131a6f02b79d7e722ca for the relevant change in C API. --- src/api/java/Optimize.java | 61 +++++++++++++++++++++++++++++++++++++- 1 file changed, 60 insertions(+), 1 deletion(-) diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index ea100d1ca..c474a34dd 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -101,7 +101,30 @@ public class Optimize extends Z3Object { return opt.GetUpper(handle); } - + + /** + * @return a triple representing the upper bound of the objective handle. + * + * The triple contains values {@code inf, value, eps}, + * where the objective value is unbounded iff {@code inf} is non-zero, + * and otherwise is represented by the expression {@code value + eps * EPSILON}, + * where {@code EPSILON} is an arbitrarily small real number. + */ + public ArithExpr[] getUpperAsVector() + { + return opt.GetUpperAsVector(handle); + } + + /** + * @return a triple representing the upper bound of the objective handle. + * + *

See {@link #getUpperAsVector()} for triple semantics. + */ + public ArithExpr[] getLowerAsVector() + { + return opt.GetLowerAsVector(handle); + } + /** * Retrieve the value of an objective. **/ @@ -227,6 +250,42 @@ public class Optimize extends Z3Object return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index)); } + /** + * @return Triple representing the upper bound for the objective handle. + * + *

See {@link Handle#getUpperAsVector}. + */ + private ArithExpr[] GetUpperAsVector(int index) { + return unpackObjectiveValueVector( + Native.optimizeGetUpperAsVector( + getContext().nCtx(), getNativeObject(), index + ) + ); + } + + /** + * @return Triple representing the upper bound for the objective handle. + * + *

See {@link Handle#getLowerAsVector}. + */ + private ArithExpr[] GetLowerAsVector(int index) { + return unpackObjectiveValueVector( + Native.optimizeGetLowerAsVector( + getContext().nCtx(), getNativeObject(), index + ) + ); + } + + private ArithExpr[] unpackObjectiveValueVector(long nativeVec) { + ASTVector vec = new ASTVector( + getContext(), nativeVec + ); + return new ArithExpr[] { + (ArithExpr) vec.get(0), (ArithExpr) vec.get(1), (ArithExpr) vec.get(2) + }; + + } + /** * Return a string the describes why the last to check returned unknown **/ From b3be83e7c59f499c6aa9ea53ed62d22f8eb3c138 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Mon, 27 Feb 2017 18:48:44 +0100 Subject: [PATCH 13/18] Sane indentation + removing extra spaces for Optimize.java --- src/api/java/Optimize.java | 165 ++++++++++++++++++------------------- 1 file changed, 79 insertions(+), 86 deletions(-) diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index c474a34dd..abc13b570 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -14,7 +14,6 @@ Author: Nikolaj Bjorner (nbjorner) 2015-07-16 Notes: - **/ package com.microsoft.z3; @@ -23,10 +22,10 @@ import com.microsoft.z3.enumerations.Z3_lbool; /** - * Object for managing optimizization context + * Object for managing optimization context **/ -public class Optimize extends Z3Object -{ +public class Optimize extends Z3Object { + /** * A string that describes all available optimize solver parameters. **/ @@ -55,7 +54,7 @@ public class Optimize extends Z3Object /** * Assert a constraint (or multiple) into the optimize solver. - **/ + **/ public void Assert(BoolExpr ... constraints) { getContext().checkContextMatch(constraints); @@ -67,103 +66,101 @@ public class Optimize extends Z3Object /** * Alias for Assert. - **/ + **/ public void Add(BoolExpr ... constraints) { - Assert(constraints); + Assert(constraints); } - + /** * Handle to objectives returned by objective functions. **/ - public class Handle - { - Optimize opt; - int handle; - Handle(Optimize opt, int h) - { - this.opt = opt; - this.handle = h; - } - - /** - * Retrieve a lower bound for the objective handle. - **/ - public ArithExpr getLower() - { - return opt.GetLower(handle); - } - - /** - * Retrieve an upper bound for the objective handle. - **/ - public ArithExpr getUpper() - { - return opt.GetUpper(handle); - } + public class Handle { - /** - * @return a triple representing the upper bound of the objective handle. - * - * The triple contains values {@code inf, value, eps}, - * where the objective value is unbounded iff {@code inf} is non-zero, - * and otherwise is represented by the expression {@code value + eps * EPSILON}, - * where {@code EPSILON} is an arbitrarily small real number. - */ - public ArithExpr[] getUpperAsVector() - { - return opt.GetUpperAsVector(handle); - } + private final Optimize opt; + private final int handle; - /** - * @return a triple representing the upper bound of the objective handle. - * - *

See {@link #getUpperAsVector()} for triple semantics. - */ - public ArithExpr[] getLowerAsVector() - { - return opt.GetLowerAsVector(handle); - } + Handle(Optimize opt, int h) + { + this.opt = opt; + this.handle = h; + } - /** - * Retrieve the value of an objective. - **/ - public ArithExpr getValue() - { - return getLower(); - } + /** + * Retrieve a lower bound for the objective handle. + **/ + public ArithExpr getLower() + { + return opt.GetLower(handle); + } - /** - * Print a string representation of the handle. - **/ - @Override - public String toString() + /** + * Retrieve an upper bound for the objective handle. + **/ + public ArithExpr getUpper() + { + return opt.GetUpper(handle); + } + + /** + * @return a triple representing the upper bound of the objective handle. + * + * The triple contains values {@code inf, value, eps}, + * where the objective value is unbounded iff {@code inf} is non-zero, + * and otherwise is represented by the expression {@code value + eps * EPSILON}, + * where {@code EPSILON} is an arbitrarily small real number. + */ + public ArithExpr[] getUpperAsVector() + { + return opt.GetUpperAsVector(handle); + } + + /** + * @return a triple representing the upper bound of the objective handle. + * + *

See {@link #getUpperAsVector()} for triple semantics. + */ + public ArithExpr[] getLowerAsVector() + { + return opt.GetLowerAsVector(handle); + } + + /** + * Retrieve the value of an objective. + **/ + public ArithExpr getValue() + { + return getLower(); + } + + /** + * Print a string representation of the handle. + **/ + @Override + public String toString() { return getValue().toString(); } } - /** + /** * Assert soft constraint * * Return an objective which associates with the group of constraints. * - **/ - + **/ public Handle AssertSoft(BoolExpr constraint, int weight, String group) { getContext().checkContextMatch(constraint); Symbol s = getContext().mkSymbol(group); return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject())); } - - /** + /** * Check satisfiability of asserted constraints. * Produce a model that (when the objectives are bounded and * don't use strict inequalities) meets the objectives. **/ - public Status Check() { Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject())); @@ -176,7 +173,7 @@ public class Optimize extends Z3Object return Status.UNKNOWN; } } - + /** * Creates a backtracking point. **/ @@ -185,13 +182,11 @@ public class Optimize extends Z3Object Native.optimizePush(getContext().nCtx(), getNativeObject()); } - - /** + /** * Backtrack one backtracking point. * * Note that an exception is thrown if Pop is called without a corresponding Push. **/ - public void Pop() { Native.optimizePop(getContext().nCtx(), getNativeObject()); @@ -214,7 +209,7 @@ public class Optimize extends Z3Object } } - /** + /** * Declare an arithmetical maximization objective. * Return a handle to the objective. The handle is used as * to retrieve the values of objectives after calling Check. @@ -223,11 +218,11 @@ public class Optimize extends Z3Object { return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject())); } - + /** * Declare an arithmetical minimization objective. * Similar to MkMaximize. - **/ + **/ public Handle MkMinimize(ArithExpr e) { return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject())); @@ -235,16 +230,15 @@ public class Optimize extends Z3Object /** * Retrieve a lower bound for the objective handle. - **/ + **/ private ArithExpr GetLower(int index) { return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index)); } - - + /** * Retrieve an upper bound for the objective handle. - **/ + **/ private ArithExpr GetUpper(int index) { return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index)); @@ -294,8 +288,7 @@ public class Optimize extends Z3Object return Native.optimizeGetReasonUnknown(getContext().nCtx(), getNativeObject()); } - - + /** * Print the context to a String (SMT-LIB parseable benchmark). **/ @@ -304,7 +297,7 @@ public class Optimize extends Z3Object { return Native.optimizeToString(getContext().nCtx(), getNativeObject()); } - + /** * Optimize statistics. **/ From be1e9918f0f6a39776318381458de45a54338e5c Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Mon, 27 Feb 2017 18:49:02 +0100 Subject: [PATCH 14/18] Class Optimize#Handle should be static, as it already includes an explicit reference to the Optimize class. --- src/api/java/Optimize.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index abc13b570..5e4535ac4 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -75,7 +75,7 @@ public class Optimize extends Z3Object { /** * Handle to objectives returned by objective functions. **/ - public class Handle { + public static class Handle { private final Optimize opt; private final int handle; From 3415672f31a48d40768e35cc31292fd6bba2ac55 Mon Sep 17 00:00:00 2001 From: Michael Lowell Roberts Date: Tue, 28 Feb 2017 08:24:35 -0800 Subject: [PATCH 15/18] fixed bug where `mk_make.py --build=...` would fail to handle absolute paths correctly. --- doc/mk_api_doc.py | 18 +++++++----------- scripts/mk_unix_dist.py | 12 ++++++------ scripts/mk_util.py | 23 +++++++++++------------ scripts/mk_win_dist.py | 22 +++++++++++----------- 4 files changed, 35 insertions(+), 40 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 45bc9a99c..edabcbd1b 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -12,10 +12,6 @@ import shutil ML_ENABLED=False BUILD_DIR='../build' -def norm_path(p): - # We use '/' on mk_project for convenience - return os.path.join(*(p.split('/'))) - def display_help(exit_code): print("mk_api_doc.py: Z3 documentation generator\n") print("\nOptions:") @@ -36,12 +32,12 @@ def parse_options(): for opt, arg in options: if opt in ('-b', '--build'): - BUILD_DIR = norm_path(arg) + BUILD_DIR = mk_util.norm_path(arg) elif opt in ('h', '--help'): display_help() exit(1) elif opt in ('--ml'): - ML_ENABLED=True + ML_ENABLED=True else: print("ERROR: Invalid command line option: %s" % opt) display_help(1) @@ -59,7 +55,7 @@ def cleanup_API(inf, outf): pat1 = re.compile(".*def_API.*") pat2 = re.compile(".*extra_API.*") _inf = open(inf, 'r') - _outf = open(outf, 'w') + _outf = open(outf, 'w') for line in _inf: if not pat1.match(line) and not pat2.match(line): _outf.write(line) @@ -90,9 +86,9 @@ try: cleanup_API('../src/api/z3_rcf.h', 'tmp/z3_rcf.h') cleanup_API('../src/api/z3_fixedpoint.h', 'tmp/z3_fixedpoint.h') cleanup_API('../src/api/z3_optimization.h', 'tmp/z3_optimization.h') - cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h') + cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h') cleanup_API('../src/api/z3_fpa.h', 'tmp/z3_fpa.h') - + print("Removed annotations from z3_api.h.") try: if subprocess.call(['doxygen', 'z3api.dox']) != 0: @@ -112,7 +108,7 @@ try: os.remove('tmp/z3_interp.h') os.remove('tmp/z3_fpa.h') print("Removed temporary file header files.") - + os.remove('tmp/website.dox') print("Removed temporary file website.dox") os.remove('tmp/z3py.py') @@ -130,7 +126,7 @@ try: print("ERROR: ocamldoc failed.") exit(1) print("Generated ML/OCaml documentation.") - + print("Documentation was successfully generated at subdirectory './api/html'.") except: exctype, value = sys.exc_info()[:2] diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 488bc4364..00cf3c706 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -1,7 +1,7 @@ ############################################ # Copyright (c) 2013 Microsoft Corporation -# -# Scripts for automatically generating +# +# Scripts for automatically generating # Linux/OSX/BSD distribution zip files. # # Author: Leonardo de Moura (leonardo) @@ -42,7 +42,7 @@ def mk_dir(d): def set_build_dir(path): global BUILD_DIR - BUILD_DIR = path + BUILD_DIR = mk_util.norm_path(path) mk_dir(BUILD_DIR) def display_help(): @@ -65,7 +65,7 @@ def display_help(): def parse_options(): global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE path = BUILD_DIR - options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', + options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 'help', 'silent', 'force', @@ -89,7 +89,7 @@ def parse_options(): elif opt == '--nodotnet': DOTNET_ENABLED = False elif opt == '--nopython': - PYTHON_ENABLED = False + PYTHON_ENABLED = False elif opt == '--dotnet-key': DOTNET_KEY_FILE = arg elif opt == '--nojava': @@ -121,7 +121,7 @@ def mk_build_dir(path): opts.append('--python') if subprocess.call(opts) != 0: raise MKException("Failed to generate build directory at '%s'" % path) - + # Create build directories def mk_build_dirs(): mk_build_dir(BUILD_DIR) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 9451e67c0..17ab8dea0 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -153,8 +153,7 @@ def is_cygwin_mingw(): return IS_CYGWIN_MINGW def norm_path(p): - # We use '/' on mk_project for convenience - return os.path.join(*(p.split('/'))) + return os.path.expanduser(os.path.normpath(p)) def which(program): import os @@ -1393,7 +1392,7 @@ class DLLComponent(Component): shutil.copy('%s.a' % os.path.join(build_path, self.dll_name), '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) -class PythonComponent(Component): +class PythonComponent(Component): def __init__(self, name, libz3Component): assert isinstance(libz3Component, DLLComponent) global PYTHON_ENABLED @@ -1418,7 +1417,7 @@ class PythonComponent(Component): def mk_makefile(self, out): return - + class PythonInstallComponent(Component): def __init__(self, name, libz3Component): assert isinstance(libz3Component, DLLComponent) @@ -1521,7 +1520,7 @@ class PythonInstallComponent(Component): os.path.join('python', 'z3', '*.pyc'), os.path.join(self.pythonPkgDir,'z3'), in_prefix=self.in_prefix_install) - + if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib(): out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR) @@ -1586,7 +1585,7 @@ class DotNetDLLComponent(Component): def mk_makefile(self, out): global DOTNET_KEY_FILE - + if not is_dotnet_enabled(): return cs_fp_files = [] @@ -1631,7 +1630,7 @@ class DotNetDLLComponent(Component): else: print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.key_file, self.dll_name)) self.key_file = None - + if not self.key_file is None: print("%s.dll will be signed using key '%s'." % (self.dll_name, self.key_file)) cscCmdLine.append('/keyfile:{}'.format(self.key_file)) @@ -1658,7 +1657,7 @@ class DotNetDLLComponent(Component): ) else: cscCmdLine.extend(['/optimize+']) - + if IS_WINDOWS: if VS_X64: cscCmdLine.extend(['/platform:x64']) @@ -1962,7 +1961,7 @@ class MLComponent(Component): OCAMLMKLIB = 'ocamlmklib' - LIBZ3 = '-L. -lz3' + LIBZ3 = '-L. -lz3' if is_cygwin() and not(is_cygwin_mingw()): LIBZ3 = 'libz3.dll' @@ -2214,7 +2213,7 @@ class PythonExampleComponent(ExampleComponent): def mk_win_dist(self, build_path, dist_path): full = os.path.join(EXAMPLE_DIR, self.path) py = 'example.py' - shutil.copyfile(os.path.join(full, py), + shutil.copyfile(os.path.join(full, py), os.path.join(dist_path, INSTALL_BIN_DIR, 'python', py)) def mk_unix_dist(self, build_path, dist_path): @@ -2263,7 +2262,7 @@ def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, man def add_python(libz3Component): name = 'python' reg_component(name, PythonComponent(name, libz3Component)) - + def add_python_install(libz3Component): name = 'python_install' reg_component(name, PythonInstallComponent(name, libz3Component)) @@ -2689,7 +2688,7 @@ def get_full_version_string(major, minor, build, revision): branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD', '--long']) res += " master " + check_output(['git', 'describe']) return '"' + res + '"' - + # Update files with the version number def mk_version_dot_h(major, minor, build, revision): c = get_component(UTIL_COMPONENT) diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 66f44426f..384e1d080 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -1,7 +1,7 @@ ############################################ # Copyright (c) 2012 Microsoft Corporation -# -# Scripts for automatically generating +# +# Scripts for automatically generating # Window distribution zip files. # # Author: Leonardo de Moura (leonardo) @@ -46,7 +46,7 @@ def mk_dir(d): def set_build_dir(path): global BUILD_DIR, BUILD_X86_DIR, BUILD_X64_DIR - BUILD_DIR = path + BUILD_DIR = mk_util.norm_path(path) BUILD_X86_DIR = os.path.join(path, 'x86') BUILD_X64_DIR = os.path.join(path, 'x64') mk_dir(BUILD_X86_DIR) @@ -74,7 +74,7 @@ def display_help(): def parse_options(): global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED, X86ONLY, X64ONLY path = BUILD_DIR - options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', + options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 'help', 'silent', 'force', @@ -102,7 +102,7 @@ def parse_options(): elif opt == '--nopython': PYTHON_ENABLED = False elif opt == '--dotnet-key': - DOTNET_KEY_FILE = arg + DOTNET_KEY_FILE = arg elif opt == '--nojava': JAVA_ENABLED = False elif opt == '--githash': @@ -139,7 +139,7 @@ def mk_build_dir(path, x64): opts.append('--python') if subprocess.call(opts) != 0: raise MKException("Failed to generate build directory at '%s'" % path) - + # Create build directories def mk_build_dirs(): mk_build_dir(BUILD_X86_DIR, False) @@ -176,7 +176,7 @@ def mk_z3(x64): cmds = [] if x64: cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" amd64') - cmds.append('cd %s' % BUILD_X64_DIR) + cmds.append('cd %s' % BUILD_X64_DIR) else: cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" x86') cmds.append('cd %s' % BUILD_X86_DIR) @@ -248,12 +248,12 @@ def mk_zips(): VS_RUNTIME_PATS = [re.compile('vcomp.*\.dll'), re.compile('msvcp.*\.dll'), re.compile('msvcr.*\.dll')] - + # Copy Visual Studio Runtime libraries -def cp_vs_runtime(x64): +def cp_vs_runtime(x64): if x64: platform = "x64" - + else: platform = "x86" vcdir = os.environ['VCINSTALLDIR'] @@ -261,7 +261,7 @@ def cp_vs_runtime(x64): VS_RUNTIME_FILES = [] for root, dirs, files in os.walk(path): for filename in files: - if fnmatch(filename, '*.dll'): + if fnmatch(filename, '*.dll'): for pat in VS_RUNTIME_PATS: if pat.match(filename): fname = os.path.join(root, filename) From dbdb0307dbd4d84920719e47abb1bd13b403154a Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 1 Mar 2017 15:22:15 +0100 Subject: [PATCH 16/18] Free allocated char arrays in JNI API Fixes #886 --- scripts/update_api.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/update_api.py b/scripts/update_api.py index 26f19cc1c..cc96bd425 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -710,6 +710,9 @@ def mk_java(java_dir, package_name): java_wrapper.write(' }\n') elif k == OUT_MANAGED_ARRAY: java_wrapper.write(' *(jlong**)a%s = (jlong*)_a%s;\n' % (i, i)) + + elif k == IN and param_type(param) == STRING: + java_wrapper.write(' jenv->ReleaseStringUTFChars(a%s, _a%s);\n' % (i, i)); i = i + 1 # return if result == STRING: From cac0283e7d2d77885911025b40c4042a0faebd49 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 2 Mar 2017 21:18:54 +0000 Subject: [PATCH 17/18] [CMake] For single configuration generators only allow `CMAKE_BUILD_TYPE` to be one of the pre-defined build configurations that we support. --- CMakeLists.txt | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 1ca94689e..87bd07f31 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -112,6 +112,13 @@ else() set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${available_build_types}) endif() message(STATUS "Build type: ${CMAKE_BUILD_TYPE}") + + # Check the selected build type is valid + list(FIND available_build_types "${CMAKE_BUILD_TYPE}" _build_type_index) + if ("${_build_type_index}" EQUAL "-1") + message(FATAL_ERROR "\"${CMAKE_BUILD_TYPE}\" is an invalid build type.\n" + "Use one of the following build types ${available_build_types}") + endif() endif() # CMAKE_BUILD_TYPE has no meaning for multi-configuration generators From ad0766898ca702950de72fc0a71b21df811cab20 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Sat, 4 Mar 2017 15:20:57 -0500 Subject: [PATCH 18/18] add boolean operators to zstring and fix ostream --- src/ast/seq_decl_plugin.cpp | 50 +++++++++++++++++++++++++++++++++++-- src/ast/seq_decl_plugin.h | 6 ++++- 2 files changed, 53 insertions(+), 3 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index d671694e3..9af4687d2 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -284,8 +284,54 @@ zstring zstring::operator+(zstring const& other) const { return result; } -std::ostream& zstring::operator<<(std::ostream& out) const { - return out << encode(); +bool zstring::operator==(const zstring& other) const { + // two strings are equal iff they have the same length and characters + if (length() != other.length()) { + return false; + } + for (unsigned i = 0; i < length(); ++i) { + unsigned Xi = m_buffer[i]; + unsigned Yi = other[i]; + if (Xi != Yi) { + return false; + } + } + + return true; +} + +bool zstring::operator!=(const zstring& other) const { + return !(*this == other); +} + +std::ostream& operator<<(std::ostream &os, const zstring &str) { + return os << str.encode(); +} + +bool operator<(const zstring& lhs, const zstring& rhs) { + // This has the same semantics as strcmp() + unsigned len = lhs.length(); + if (rhs.length() < len) { + len = rhs.length(); + } + for (unsigned i = 0; i < len; ++i) { + unsigned Li = lhs[i]; + unsigned Ri = rhs[i]; + if (Li < Ri) { + return true; + } else if (Li > Ri) { + return false; + } else { + continue; + } + } + // at this point, all compared characters are equal, + // so decide based on the relative lengths + if (lhs.length() < rhs.length()) { + return true; + } else { + return false; + } } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index b07e4d307..a7e534bbb 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -114,7 +114,11 @@ public: int indexof(zstring const& other, int offset) const; zstring extract(int lo, int hi) const; zstring operator+(zstring const& other) const; - std::ostream& operator<<(std::ostream& out) const; + bool operator==(const zstring& other) const; + bool operator!=(const zstring& other) const; + + friend std::ostream& operator<<(std::ostream &os, const zstring &str); + friend bool operator<(const zstring& lhs, const zstring& rhs); }; class seq_decl_plugin : public decl_plugin {