From 0ebd93c8b513d8b7552a99bda491a8d01f5eebcd Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 23 Feb 2017 20:57:19 -0500 Subject: [PATCH 01/19] 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 02/19] 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 03/19] 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 04/19] 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 05/19] 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 06/19] 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 07/19] 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 08/19] 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 09/19] 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 10/19] 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 11/19] 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 12/19] [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 13/19] 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 { From 8f14cfadd26051189f0c8356228047064d6d72bd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 7 Mar 2017 18:10:03 +0000 Subject: [PATCH 14/19] Tabs, whitespace --- src/ast/fpa_decl_plugin.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index d8bf70e80..e039bcbd9 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -836,7 +836,7 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_BVWRAP: - return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range); + return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_BV2RM: return mk_internal_bv2rm(k, num_parameters, parameters, arity, domain, range); @@ -915,7 +915,7 @@ void fpa_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("to_fp_unsigned", OP_FPA_TO_FP_UNSIGNED)); /* Extensions */ - op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV)); + op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV)); op_names.push_back(builtin_name("fp.to_ieee_bv", OP_FPA_TO_IEEE_BV)); } From 41e6fafc58f44e379a04e0650ddbb25c84350350 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Mar 2017 10:07:31 +0100 Subject: [PATCH 15/19] fix bug for bit-vector optimization. Issue #919 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index ebe56381a..d1a3ddb8a 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1002,7 +1002,8 @@ namespace opt { TRACE("opt", tout << "Term does not evaluate " << term << "\n";); return false; } - if (!m_arith.is_numeral(val, r)) { + unsigned bv_size; + if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bv_size)) { TRACE("opt", tout << "model does not evaluate objective to a value\n";); return false; } From 829519b83747992056953cd4d5a69163982e4aac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Mar 2017 10:19:35 +0100 Subject: [PATCH 16/19] fix bug for bit-vector optimization. Issue #928 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index d1a3ddb8a..cd40944b2 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1002,8 +1002,8 @@ namespace opt { TRACE("opt", tout << "Term does not evaluate " << term << "\n";); return false; } - unsigned bv_size; - if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bv_size)) { + unsigned bvsz; + if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bvsz)) { TRACE("opt", tout << "model does not evaluate objective to a value\n";); return false; } From fcda4cee9fde8fa129637d87a261d683ff3ca3a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Mar 2017 05:29:56 +0100 Subject: [PATCH 17/19] ensure evaluation of array equalities is enabled for external facing evaluator. Issue #917 Signed-off-by: Nikolaj Bjorner --- src/model/model_evaluator.cpp | 11 ++++++++++- src/model/model_evaluator.h | 1 + src/model/model_evaluator_params.pyg | 3 ++- src/smt/proto_model/proto_model.cpp | 1 + src/smt/smt_model_checker.cpp | 7 +++++-- src/tactic/extension_model_converter.cpp | 1 + 6 files changed, 20 insertions(+), 4 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index af2253801..61da4b3a0 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -50,6 +50,7 @@ struct evaluator_cfg : public default_rewriter_cfg { unsigned m_max_steps; bool m_model_completion; bool m_cache; + bool m_array_equalities; evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p): m_model(md), @@ -81,6 +82,7 @@ struct evaluator_cfg : public default_rewriter_cfg { m_max_steps = p.max_steps(); m_model_completion = p.completion(); m_cache = p.cache(); + m_array_equalities = p.array_equalities(); } ast_manager & m() const { return m_model.get_manager(); } @@ -264,11 +266,14 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status mk_array_eq(expr* a, expr* b, expr_ref& result) { - return BR_FAILED; if (a == b) { result = m().mk_true(); return BR_DONE; } + if (!m_array_equalities) { + return BR_FAILED; + } + // disabled until made more efficient vector stores1, stores2; bool args_are_unique1, args_are_unique2; @@ -508,6 +513,10 @@ void model_evaluator::set_model_completion(bool f) { m_imp->cfg().m_model_completion = f; } +void model_evaluator::set_expand_array_equalities(bool f) { + m_imp->cfg().m_array_equalities = f; +} + unsigned model_evaluator::get_num_steps() const { return m_imp->get_num_steps(); } diff --git a/src/model/model_evaluator.h b/src/model/model_evaluator.h index 3f4da5c96..ba55e96ba 100644 --- a/src/model/model_evaluator.h +++ b/src/model/model_evaluator.h @@ -35,6 +35,7 @@ public: ast_manager & m () const; void set_model_completion(bool f); + void set_expand_array_equalities(bool f); void updt_params(params_ref const & p); static void get_param_descrs(param_descrs & r); diff --git a/src/model/model_evaluator_params.pyg b/src/model/model_evaluator_params.pyg index b68d5c3ad..b6417f7fc 100644 --- a/src/model/model_evaluator_params.pyg +++ b/src/model/model_evaluator_params.pyg @@ -3,6 +3,7 @@ def_module_params('model_evaluator', params=(max_memory_param(), max_steps_param(), ('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model'), - ('cache', BOOL, True, 'cache intermediate results in the model evaluator') + ('cache', BOOL, True, 'cache intermediate results in the model evaluator'), + ('array_equalities', BOOL, True, 'evaluate array equalities') )) diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index a7875e99e..129bed87e 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -93,6 +93,7 @@ bool proto_model::is_select_of_model_value(expr* e) const { bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { m_eval.set_model_completion(model_completion); + m_eval.set_expand_array_equalities(false); try { m_eval(e, result); #if 0 diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 5329cd80f..093d215b6 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -290,7 +290,7 @@ namespace smt { while (true) { lbool r = m_aux_context->check(); - TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";); + TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";); if (r != l_true) break; model_ref cex; @@ -300,7 +300,7 @@ namespace smt { } num_new_instances++; if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) { - TRACE("model_checker", tout << "Add blocking clause failed\n";); + TRACE("model_checker", tout << "Add blocking clause failed new-instances: " << num_new_instances << " max-cex: " << m_max_cexs << "\n";); // add_blocking_clause failed... stop the search for new counter-examples... break; } @@ -407,6 +407,7 @@ namespace smt { found_relevant = true; if (m.is_rec_fun_def(q)) { if (!check_rec_fun(q)) { + TRACE("model_checker", tout << "checking recursive function failed\n";); num_failures++; } } @@ -414,6 +415,7 @@ namespace smt { if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) { verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n"; } + TRACE("model_checker", tout << "checking quantifier " << mk_pp(q, m) << " failed\n";); num_failures++; } } @@ -452,6 +454,7 @@ namespace smt { } bool model_checker::has_new_instances() { + TRACE("model_checker", tout << "instances: " << m_new_instances.size() << "\n";); return !m_new_instances.empty(); } diff --git a/src/tactic/extension_model_converter.cpp b/src/tactic/extension_model_converter.cpp index ee6b8f691..18b5b6288 100644 --- a/src/tactic/extension_model_converter.cpp +++ b/src/tactic/extension_model_converter.cpp @@ -49,6 +49,7 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) { TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md);); model_evaluator ev(*(md.get())); ev.set_model_completion(true); + ev.set_expand_array_equalities(false); expr_ref val(m()); unsigned i = m_vars.size(); while (i > 0) { From 29969648ba7b2f567b5b35ae2330cae5a4803454 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Mar 2017 05:52:46 +0100 Subject: [PATCH 18/19] check that formulas are in lira before invoking qsat. Issue #919 Signed-off-by: Nikolaj Bjorner --- src/tactic/smtlogics/quant_tactics.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index 044511c33..7d428b369 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -28,6 +28,7 @@ Revision History: #include"ctx_simplify_tactic.h" #include"smt_tactic.h" #include"elim_term_ite_tactic.h" +#include"probe_arith.h" static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = false) { params_ref pull_ite_p; @@ -107,8 +108,10 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) { tactic * st = and_then(mk_quant_preprocessor(m), mk_qe_lite_tactic(m, p), cond(mk_has_quantifier_probe(), - or_else(mk_qsat_tactic(m, p), - and_then(mk_qe_tactic(m), mk_smt_tactic())), + cond(mk_is_lira_probe(), + or_else(mk_qsat_tactic(m, p), + and_then(mk_qe_tactic(m), mk_smt_tactic())), + mk_smt_tactic()), mk_smt_tactic())); st->updt_params(p); return st; From e34996fa9d8dab9f90d66603f273c5767036c229 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Mar 2017 06:00:34 +0100 Subject: [PATCH 19/19] add notes to README based on feedback in #916 Signed-off-by: Nikolaj Bjorner --- README.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index e0821ac79..b03888e9d 100644 --- a/README.md +++ b/README.md @@ -168,7 +168,10 @@ python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/p If you do need to install to a non standard prefix a better approach is to use a [Python virtual environment](https://virtualenv.readthedocs.org/en/latest/) -and install Z3 there. +and install Z3 there. Python packages also work for Python3. +Under Windows, recall to build inside the Visual C++ native command build environment. +Note that the buit/python/z3 directory should be accessible from where python is used with Z3 +and it depends on libz3.dll to be in the path. ```bash virtualenv venv @@ -185,3 +188,10 @@ python -c 'import z3; print(z3.get_version_string())' ``` See [``examples/python``](examples/python) for examples. + + +Even though the build instruction says use python scripts/mk_make.py -x --python, this can build a package that works in python3. +The building should take place inside the Visual C++ 2015 x64 Native Build Tools Prompt`. +The z3.exe appears to be independent and can work anywhere, you can copy the built version wherever. The libz3.dll needs to be discoverable on the PATH. So you can copy both build/z3.exe and build/libz3.dll into somewhere on the PATH. +Then the build/python/z3 directory should be copied into the site-packages directory of Python. On Windows, this isn't done automatically, instead you have to find your Windows site-packages: like python3 -c 'import site; print(site.getsitepackages())', then copy the entire directory there. +Then to test if it finally all works run: \ No newline at end of file