From f7d1cce69a8dc1fc3a90bf325984a38329481b0f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 19 Jun 2021 22:12:52 -0700 Subject: [PATCH 01/35] #5336 Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_etable.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/euf/euf_etable.h b/src/ast/euf/euf_etable.h index 6274af142..f4e693e34 100644 --- a/src/ast/euf/euf_etable.h +++ b/src/ast/euf/euf_etable.h @@ -88,6 +88,9 @@ namespace euf { SASSERT(n1->num_args() == 2); SASSERT(n2->num_args() == 2); + if (n1->get_decl() != n2->get_decl()) + return false; + SASSERT(n1->get_decl() == n2->get_decl()); enode* c1_1 = get_root(n1, 0); enode* c1_2 = get_root(n1, 1); From 4a0a678e3f8c01dd8468133e594b71b2f9984512 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Jun 2021 13:18:19 -0700 Subject: [PATCH 02/35] #5336 --- src/sat/smt/q_clause.cpp | 10 +++++++--- src/sat/smt/q_clause.h | 2 ++ src/sat/smt/q_ematch.cpp | 20 ++++++++++++++------ src/util/dlist.h | 18 ++++++++++++++++++ 4 files changed, 41 insertions(+), 9 deletions(-) diff --git a/src/sat/smt/q_clause.cpp b/src/sat/smt/q_clause.cpp index 0d4049167..f7c200553 100644 --- a/src/sat/smt/q_clause.cpp +++ b/src/sat/smt/q_clause.cpp @@ -32,6 +32,12 @@ namespace q { << mk_bounded_pp(rhs, m, 2); } + std::ostream& binding::display(euf::solver& ctx, unsigned num_nodes, std::ostream& out) const { + for (unsigned i = 0; i < num_nodes; ++i) + out << ctx.bpp((*this)[i]) << " "; + return out; + } + std::ostream& clause::display(euf::solver& ctx, std::ostream& out) const { out << "clause:\n"; for (auto const& lit : m_lits) @@ -39,9 +45,7 @@ namespace q { binding* b = m_bindings; if (b) { do { - for (unsigned i = 0; i < num_decls(); ++i) - out << ctx.bpp((*b)[i]) << " "; - out << "\n"; + b->display(ctx, num_decls(), out) << " - " << b << "\n"; b = b->next(); } while (b != m_bindings); diff --git a/src/sat/smt/q_clause.h b/src/sat/smt/q_clause.h index 149b9ac94..7278d1db1 100644 --- a/src/sat/smt/q_clause.h +++ b/src/sat/smt/q_clause.h @@ -49,6 +49,8 @@ namespace q { euf::enode* const* nodes() { return m_nodes; } euf::enode* operator[](unsigned i) const { return m_nodes[i]; } + + std::ostream& display(euf::solver& ctx, unsigned num_nodes, std::ostream& out) const; }; struct clause { diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index 3dfa62422..da7e670c8 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -192,20 +192,26 @@ namespace q { } struct ematch::remove_binding : public trail { + euf::solver& ctx; clause& c; binding* b; - remove_binding(clause& c, binding* b): c(c), b(b) {} - void undo() override { + remove_binding(euf::solver& ctx, clause& c, binding* b): ctx(ctx), c(c), b(b) {} + void undo() override { + SASSERT(binding::contains(c.m_bindings, b)); binding::remove_from(c.m_bindings, b); + binding::detach(b); } }; struct ematch::insert_binding : public trail { + euf::solver& ctx; clause& c; binding* b; - insert_binding(clause& c, binding* b): c(c), b(b) {} - void undo() override { + insert_binding(euf::solver& ctx, clause& c, binding* b): ctx(ctx), c(c), b(b) {} + void undo() override { + SASSERT(!c.m_bindings || c.m_bindings->invariant()); binding::push_to_front(c.m_bindings, b); + SASSERT(!c.m_bindings || c.m_bindings->invariant()); } }; @@ -230,7 +236,7 @@ namespace q { for (unsigned i = 0; i < n; ++i) b->m_nodes[i] = _binding[i]; binding::push_to_front(c.m_bindings, b); - ctx.push(remove_binding(c, b)); + ctx.push(remove_binding(ctx, c, b)); } void ematch::on_binding(quantifier* q, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_gen, unsigned max_gen) { @@ -503,8 +509,10 @@ namespace q { while (b != c.m_bindings); for (auto* b : to_remove) { + SASSERT(binding::contains(c.m_bindings, b)); binding::remove_from(c.m_bindings, b); - ctx.push(insert_binding(c, b)); + binding::detach(b); + ctx.push(insert_binding(ctx, c, b)); } to_remove.reset(); } diff --git a/src/util/dlist.h b/src/util/dlist.h index 6248f34df..df28217c0 100644 --- a/src/util/dlist.h +++ b/src/util/dlist.h @@ -74,6 +74,10 @@ public: } } + static void detach(T* elem) { + elem->init(elem); + } + bool invariant() const { auto* e = this; do { @@ -84,6 +88,20 @@ public: while (e != this); return true; } + + + static bool contains(T* list, T* elem) { + if (!list) + return false; + T* first = list; + do { + if (list == elem) + return true; + list = list->m_next; + } + while (list != first); + return false; + } }; From 8d37495b7c83f749eec8a4c33b7c51b82c1b0e19 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 19 Jun 2021 22:22:41 -0700 Subject: [PATCH 03/35] merge Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_etable.h | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/ast/euf/euf_etable.h b/src/ast/euf/euf_etable.h index f4e693e34..68ae95cd2 100644 --- a/src/ast/euf/euf_etable.h +++ b/src/ast/euf/euf_etable.h @@ -87,11 +87,8 @@ namespace euf { bool operator()(enode * n1, enode * n2) const { SASSERT(n1->num_args() == 2); SASSERT(n2->num_args() == 2); - if (n1->get_decl() != n2->get_decl()) return false; - - SASSERT(n1->get_decl() == n2->get_decl()); enode* c1_1 = get_root(n1, 0); enode* c1_2 = get_root(n1, 1); enode* c2_1 = get_root(n2, 0); From 02644b5b7129f35df0d5ea7225e8711e1bd33fde Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Jun 2021 13:57:58 -0700 Subject: [PATCH 04/35] #5336 --- src/sat/smt/q_clause.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/smt/q_clause.cpp b/src/sat/smt/q_clause.cpp index f7c200553..7c8a260e5 100644 --- a/src/sat/smt/q_clause.cpp +++ b/src/sat/smt/q_clause.cpp @@ -45,7 +45,7 @@ namespace q { binding* b = m_bindings; if (b) { do { - b->display(ctx, num_decls(), out) << " - " << b << "\n"; + b->display(ctx, num_decls(), out) << "\n"; b = b->next(); } while (b != m_bindings); From ed9341e3b017973555f18dca4a2d218f8501efec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Jun 2021 17:45:13 -0700 Subject: [PATCH 05/35] #5336 --- src/ast/euf/euf_egraph.cpp | 2 +- src/sat/smt/arith_diagnostics.cpp | 2 +- src/sat/smt/arith_solver.h | 2 +- src/sat/smt/euf_internalize.cpp | 1 + src/sat/smt/euf_solver.h | 1 + src/sat/smt/q_mbi.cpp | 1 + 6 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 809cbe1f9..2bc9b1cde 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -745,7 +745,7 @@ namespace euf { out << "] "; } if (n->value() != l_undef) - out << "[v" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << "] "; + out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << "] "; if (n->has_th_vars()) { out << "[t"; for (auto v : enode_th_vars(n)) diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp index 770aeff98..b639c183f 100644 --- a/src/sat/smt/arith_diagnostics.cpp +++ b/src/sat/smt/arith_diagnostics.cpp @@ -50,7 +50,7 @@ namespace arith { scoped_anum an(m_nla->am()); m_nla->am().display(out << " = ", nl_value(v, an)); } - else if (can_get_value(v)) + else if (can_get_value(v) && !m_solver->has_changed_columns()) out << " = " << get_value(v); if (is_int(v)) out << ", int"; diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index 19164dff6..b449e049e 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -384,7 +384,7 @@ namespace arith { obj_map m_predicate2term; obj_map m_term2bound_info; - bool m_model_is_initialized{ false }; + bool m_model_is_initialized = false; unsigned small_lemma_size() const { return get_config().m_arith_small_lemma_size; } bool propagate_eqs() const { return get_config().m_arith_propagate_eqs && m_num_conflicts < get_config().m_arith_propagation_threshold; } diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 1eb9d6aef..0a7aa717f 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -278,6 +278,7 @@ namespace euf { } else { sat::bool_var v = si.to_bool_var(c); + s().set_external(v); VERIFY(v != sat::null_bool_var); VERIFY(s().is_external(v)); SASSERT(v != sat::null_bool_var); diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index ac8c41d59..73c44649c 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -352,6 +352,7 @@ namespace euf { sat::literal attach_lit(sat::literal lit, expr* e); void unhandled_function(func_decl* f); th_rewriter& get_rewriter() { return m_rewriter; } + void rewrite(expr_ref& e) { m_rewriter(e); } bool is_shared(euf::enode* n) const; // relevancy diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index bf44b5dd2..30c6c7e23 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -213,6 +213,7 @@ namespace q { sat::literal qlit = ctx.expr2literal(q); if (is_exists(q)) qlit.neg(); + ctx.rewrite(proj); TRACE("q", tout << "project: " << proj << "\n";); ++m_stats.m_num_instantiations; unsigned generation = ctx.get_max_generation(proj); From 45228bf8fb2c3bc07abade538b8f5d64f4a3a067 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Jun 2021 09:25:02 -0700 Subject: [PATCH 06/35] #5323 heap use after free Signed-off-by: Nikolaj Bjorner --- src/qe/mbp/mbp_arith.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index fb07ae450..ab13e0813 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -283,7 +283,8 @@ namespace mbp { unsigned j = 0; TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n"; for (expr* f : fmls) tout << mk_pp(f, m) << " := " << model(f) << "\n";); - for (expr* fml : fmls) { + for (unsigned i = 0; i < fmls.size(); ++i) { + expr* fml = fmls.get(i); if (!linearize(mbo, eval, fml, fmls, tids)) { TRACE("qe", tout << "could not linearize: " << mk_pp(fml, m) << "\n";); fmls[j++] = fml; From 161d38397bb5107d45d12c6d38c3475eea587c76 Mon Sep 17 00:00:00 2001 From: Robert Jacobson Date: Mon, 21 Jun 2021 17:40:31 -0400 Subject: [PATCH 07/35] In src/sat/sat_local_search.*: Changed the return type of `constraint_slack` to `int64_t` instead of `uint64_t` to match the `m_slack` member of the `constraint` struct, which has type `int64_t`. (#5360) --- src/sat/sat_local_search.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index e48d88924..e46d4b009 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -186,9 +186,9 @@ namespace sat { inline bool is_unit(literal l) const { return m_vars[l.var()].m_unit; } unsigned num_constraints() const { return m_constraints.size(); } // constraint index from 1 to num_constraint - - uint64_t constraint_slack(unsigned ci) const { return m_constraints[ci].m_slack; } - + + int64_t constraint_slack(unsigned ci) const { return m_constraints[ci].m_slack; } + void init(); void reinit(); void reinit_orig(); From f3737f68310ef101922fdc2e0ca607528612968b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Jun 2021 14:57:54 -0700 Subject: [PATCH 08/35] #5361 --- src/api/z3_fpa.h | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index ddf0fb1e5..fe85e702e 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -961,7 +961,8 @@ extern "C" { \param c logical context \param t a floating-point numeral - \param sgn sign + \param sgn the retrieved sign + \returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false Remarks: sets \c sgn to 0 if `t' is positive and to 1 otherwise, except for NaN, which is an invalid argument. @@ -975,6 +976,7 @@ extern "C" { \param c logical context \param t a floating-point numeral + \returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false Remarks: The significand \c s is always \ccode{0.0 <= s < 2.0}; the resulting string is long enough to represent the real significand precisely. @@ -1004,6 +1006,7 @@ extern "C" { \param c logical context \param t a floating-point numeral \param biased flag to indicate whether the result is in biased representation + \returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false Remarks: This function extracts the exponent in `t`, without normalization. NaN is an invalid argument. @@ -1019,6 +1022,7 @@ extern "C" { \param t a floating-point numeral \param n exponent \param biased flag to indicate whether the result is in biased representation + \returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false Remarks: This function extracts the exponent in `t`, without normalization. NaN is an invalid argument. From 55daa2424c192dcf19d05c955db1abc9ab6431fa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Jun 2021 12:26:27 -0700 Subject: [PATCH 09/35] fix #5362 --- src/math/lp/nla_core.cpp | 11 ++++++++--- src/math/lp/nla_core.h | 1 + 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 55a42c2f8..eedf46967 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -36,7 +36,7 @@ core::core(lp::lar_solver& s, reslimit & lim) : m_emons(m_evars), m_reslim(lim), m_use_nra_model(false), - m_nra(s, lim, *this) + m_nra(s, m_nra_lim, *this) { m_nlsat_delay = lp_settings().nlsat_delay(); } @@ -1563,10 +1563,15 @@ bool core::should_run_bounded_nlsat() { lbool core::bounded_nlsat() { params_ref p; + lbool ret; p.set_uint("max_conflicts", 100); - scoped_rlimit sr(m_reslim, 100000); m_nra.updt_params(p); - lbool ret = m_nra.check(); + { + scoped_limits sl(m_reslim); + sl.push_child(&m_nra_lim); + scoped_rlimit sr(m_nra_lim, 100000); + ret = m_nra.check(); + } p.set_uint("max_conflicts", UINT_MAX); m_nra.updt_params(p); m_stats.m_nra_calls++; diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 18baa0847..d0dc8d77d 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -175,6 +175,7 @@ private: svector m_add_buffer; mutable lp::u_set m_active_var_set; lp::u_set m_rows; + reslimit m_nra_lim; public: reslimit& m_reslim; bool m_use_nra_model; From d5c6abe14d3edc18667e5828144816ec756289fb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Jun 2021 16:24:00 -0700 Subject: [PATCH 10/35] #close 5363 Force in-lining auxiliary functions so that model values can be used by SPACER to retrieve counter-examples. This fixes the issue of terminating without a trace. It does not address inefficiency involved with invoking satisfiability checks to retrieve models during trace construction. --- src/model/func_interp.cpp | 10 ++++------ src/model/model.cpp | 41 ++++++++++++++++++++++----------------- src/model/model.h | 10 +++++----- 3 files changed, 32 insertions(+), 29 deletions(-) diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index 76b628dd3..22443ee1f 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -369,16 +369,14 @@ expr_ref func_interp::get_array_interp_core(func_decl * f) const { if (m_else == nullptr) return r; ptr_vector domain; - for (sort* s : *f) { - domain.push_back(s); - } + for (sort* s : *f) + domain.push_back(s); bool ground = is_ground(m_else); for (func_entry * curr : m_entries) { ground &= is_ground(curr->get_result()); - for (unsigned i = 0; i < m_arity; i++) { - ground &= is_ground(curr->get_arg(i)); - } + for (unsigned i = 0; i < m_arity; i++) + ground &= is_ground(curr->get_arg(i)); } if (!ground) { r = get_interp(); diff --git a/src/model/model.cpp b/src/model/model.cpp index 06ad4028d..f2861292f 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -224,7 +224,7 @@ struct model::top_sort : public ::top_sort { } }; -void model::compress() { +void model::compress(bool force_inline) { if (m_cleaned) return; // stratify m_finterp and m_decls in a topological sort @@ -238,7 +238,7 @@ void model::compress() { collect_deps(ts); ts.topological_sort(); for (func_decl * f : ts.top_sorted()) { - cleanup_interp(ts, f); + cleanup_interp(ts, f, force_inline); } func_decl_set removed; @@ -332,11 +332,11 @@ model::func_decl_set* model::collect_deps(top_sort& ts, func_interp * fi) { \brief Inline interpretations of skolem functions */ -void model::cleanup_interp(top_sort& ts, func_decl* f) { +void model::cleanup_interp(top_sort& ts, func_decl* f, bool force_inline) { unsigned pid = ts.partition_id(f); expr * e1 = get_const_interp(f); if (e1) { - expr_ref e2 = cleanup_expr(ts, e1, pid); + expr_ref e2 = cleanup_expr(ts, e1, pid, force_inline); if (e2 != e1) register_decl(f, e2); return; @@ -344,11 +344,11 @@ void model::cleanup_interp(top_sort& ts, func_decl* f) { func_interp* fi = get_func_interp(f); if (fi) { e1 = fi->get_else(); - expr_ref e2 = cleanup_expr(ts, e1, pid); + expr_ref e2 = cleanup_expr(ts, e1, pid, force_inline); if (e1 != e2) fi->set_else(e2); for (auto& fe : *fi) { - e2 = cleanup_expr(ts, fe->get_result(), pid); + e2 = cleanup_expr(ts, fe->get_result(), pid, force_inline); if (e2 != fe->get_result()) { fi->insert_entry(fe->get_args(), e2); } @@ -382,21 +382,26 @@ void model::collect_occs(top_sort& ts, expr* e) { for_each_ast(collector, e, true); } -bool model::can_inline_def(top_sort& ts, func_decl* f) { +bool model::can_inline_def(top_sort& ts, func_decl* f, bool force_inline) { if (ts.occur_count(f) <= 1) return true; func_interp* fi = get_func_interp(f); - if (!fi) return false; - if (fi->get_else() == nullptr) return false; - if (m_inline) return true; + if (!fi) + return false; + if (fi->get_else() == nullptr) + return false; + if (m_inline) + return true; expr* e = fi->get_else(); obj_hashtable subs; ptr_buffer todo; todo.push_back(e); while (!todo.empty()) { - if (fi->num_entries() + subs.size() > 8) return false; + if (!force_inline && fi->num_entries() + subs.size() > 8) + return false; expr* e = todo.back(); todo.pop_back(); - if (subs.contains(e)) continue; + if (subs.contains(e)) + continue; subs.insert(e); if (is_app(e)) { for (expr* arg : *to_app(e)) { @@ -411,7 +416,7 @@ bool model::can_inline_def(top_sort& ts, func_decl* f) { } -expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) { +expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition, bool force_inline) { if (!e) return expr_ref(nullptr, m); TRACE("model", tout << "cleaning up:\n" << mk_pp(e, m) << "\n";); @@ -455,7 +460,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) if (autil.is_as_array(a)) { func_decl* f = autil.get_as_array_func_decl(a); // only expand auxiliary definitions that occur once. - if (can_inline_def(ts, f)) { + if (can_inline_def(ts, f, force_inline)) { fi = get_func_interp(f); if (fi) { new_t = fi->get_array_interp(f); @@ -467,7 +472,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) if (new_t) { // noop } - else if (f->is_skolem() && can_inline_def(ts, f) && (fi = get_func_interp(f)) && + else if (f->is_skolem() && can_inline_def(ts, f, force_inline) && (fi = get_func_interp(f)) && fi->get_interp() && (!ts.partition_ids().find(f, pid) || pid != current_partition)) { var_subst vs(m, false); new_t = vs(fi->get_interp(), args.size(), args.data()); @@ -526,15 +531,15 @@ expr_ref model::unfold_as_array(expr* e) { } -expr_ref model::get_inlined_const_interp(func_decl* f) { +expr_ref model::get_inlined_const_interp(func_decl* f, bool force_inline) { expr* v = get_const_interp(f); if (!v) return expr_ref(nullptr, m); top_sort st(m); expr_ref result1(v, m); - expr_ref result2 = cleanup_expr(st, v, UINT_MAX); + expr_ref result2 = cleanup_expr(st, v, UINT_MAX, force_inline); while (result1 != result2) { result1 = result2; - result2 = cleanup_expr(st, result1, UINT_MAX); + result2 = cleanup_expr(st, result1, UINT_MAX, force_inline); } return result2; } diff --git a/src/model/model.h b/src/model/model.h index 8183c5a0e..822e4cff9 100644 --- a/src/model/model.h +++ b/src/model/model.h @@ -50,10 +50,10 @@ protected: void collect_deps(top_sort& ts); void collect_occs(top_sort& ts, func_decl* f); void collect_occs(top_sort& ts, expr* e); - void cleanup_interp(top_sort& ts, func_decl * f); - expr_ref cleanup_expr(top_sort& ts, expr* e, unsigned current_partition); + void cleanup_interp(top_sort& ts, func_decl * f, bool force_inline); + expr_ref cleanup_expr(top_sort& ts, expr* e, unsigned current_partition, bool force_inline); void remove_decls(ptr_vector & decls, func_decl_set const & s); - bool can_inline_def(top_sort& ts, func_decl* f); + bool can_inline_def(top_sort& ts, func_decl* f, bool force_inline); value_factory* get_factory(sort* s); public: @@ -78,7 +78,7 @@ public: sort * get_uninterpreted_sort(unsigned idx) const override; bool has_uninterpreted_sort(sort * s) const; - expr_ref get_inlined_const_interp(func_decl* f); + expr_ref get_inlined_const_interp(func_decl* f, bool force_inline); expr_ref unfold_as_array(expr* e); // @@ -90,7 +90,7 @@ public: // model * translate(ast_translation & translator) const; - void compress(); + void compress(bool force_inline = false); void set_model_completion(bool f) { m_mev.set_model_completion(f); } void updt_params(params_ref const & p); From 7255a2afd1cf5896dba2e49cd3a570760ad5fa71 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 Jul 2021 18:43:11 +0200 Subject: [PATCH 11/35] fix #5379 Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index d16295418..cf650a5fa 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4620,8 +4620,9 @@ extern "C" { /** \brief Return a hash code for the given AST. - The hash code is structural. You can use Z3_get_ast_id interchangeably with - this function. + The hash code is structural but two different AST objects can map to the same hash. + The result of \c Z3_get_ast_id returns an indentifier that is unique over the + set of live AST objects. def_API('Z3_get_ast_hash', UINT, (_in(CONTEXT), _in(AST))) */ From e5aa02b8f5edb862c7492ac93cee8d21f7f6ee2d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 Jul 2021 19:30:03 +0200 Subject: [PATCH 12/35] fix #5382 Signed-off-by: Nikolaj Bjorner --- src/ast/normal_forms/pull_quant.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp index e0e2de1f7..209772f3b 100644 --- a/src/ast/normal_forms/pull_quant.cpp +++ b/src/ast/normal_forms/pull_quant.cpp @@ -63,7 +63,7 @@ struct pull_quant::imp { for (unsigned i = 0; i < num_children; i++) { expr * child = children[i]; - if (is_quantifier(child)) { + if (is_quantifier(child) && !is_lambda(child)) { if (!found_quantifier && (is_forall(child) || is_exists(child))) { found_quantifier = true; @@ -184,11 +184,11 @@ struct pull_quant::imp { // Remark: patterns are ignored. // See comment in reduce1_app result = m.mk_forall(var_sorts.size(), - var_sorts.data(), - var_names.data(), - nested_q->get_expr(), - std::min(q->get_weight(), nested_q->get_weight()), - q->get_qid()); + var_sorts.data(), + var_names.data(), + nested_q->get_expr(), + std::min(q->get_weight(), nested_q->get_weight()), + m.is_lambda_def(q) ? symbol("pulled-lambda") : q->get_qid()); } void pull_quant1(quantifier * q, expr * new_expr, expr_ref & result) { From 2a8d00d8152a433b736d133fd599529c58d6e42f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Jul 2021 00:04:16 +0200 Subject: [PATCH 13/35] fix #5378 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_recfun.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 0a30202e1..e21eb2bc5 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -282,12 +282,14 @@ namespace smt { auto & vars = e.m_def->get_vars(); expr_ref lhs(e.m_lhs, m); unsigned depth = get_depth(e.m_lhs); - expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m); + expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m); literal lit = mk_eq_lit(lhs, rhs); std::function fn = [&]() { return lit; }; scoped_trace_stream _tr(*this, fn); ctx.mk_th_axiom(get_id(), 1, &lit); TRACEFN("macro expansion yields " << pp_lit(ctx, lit)); + if (has_quantifiers(rhs)) + throw default_exception("quantified formulas in recursive functions are not supported"); } /** @@ -392,6 +394,8 @@ namespace smt { std::function fn = [&]() { return clause; }; scoped_trace_stream _tr(*this, fn); ctx.mk_th_axiom(get_id(), clause); + if (has_quantifiers(rhs)) + throw default_exception("quantified formulas in recursive functions are not supported"); } final_check_status theory_recfun::final_check_eh() { From bdcfba1324ec834bd194d28f017798fdbb390322 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Jul 2021 10:19:17 +0200 Subject: [PATCH 14/35] use sort* not ast* #5386 --- src/ast/seq_decl_plugin.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 01f88112b..48d46923f 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -185,7 +185,7 @@ public: expr * get_some_value(sort * s) override; - bool is_char(ast* a) const { return a == m_char; } + bool is_char(sort* a) const { return a == m_char; } unsigned max_char() const { return get_char_plugin().max_char(); } unsigned num_bits() const { return get_char_plugin().num_bits(); } @@ -222,7 +222,7 @@ public: sort* mk_string_sort() const { return seq.string_sort(); } bool is_char(sort* s) const { return seq.is_char(s); } - bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); } + bool is_string(sort* s) const { return is_seq(s) && seq.is_char(to_sort(s->get_parameter(0).get_ast())); } bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); } bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); } bool is_re(sort* s, sort*& seq) const { return is_sort_of(s, m_fid, RE_SORT) && (seq = to_sort(s->get_parameter(0).get_ast()), true); } From 0c7625cd26fa14188f3d3300622c8aec4ecbf369 Mon Sep 17 00:00:00 2001 From: Gabriel Radanne Date: Tue, 6 Jul 2021 10:21:04 +0200 Subject: [PATCH 15/35] Remove size argument in OCaml's `Z3.mk_re_intersect` (#5383) * Remove size argument in OCaml's `Z3.mk_re_intersect` Passing the size as argument is unnecessary in OCaml, and that argument is abridged in all similar `Seq` functions. This applies the same pattern. * Enable the ocaml documentation in Seq. Turn all the comments into proper documentation comments. --- src/api/ml/z3.ml | 2 +- src/api/ml/z3.mli | 76 +++++++++++++++++++++++------------------------ 2 files changed, 39 insertions(+), 39 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 61a027cec..1448a9ea5 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1272,7 +1272,7 @@ struct let mk_re_concat ctx args = Z3native.mk_re_concat ctx (List.length args) args let mk_re_range = Z3native.mk_re_range let mk_re_loop = Z3native.mk_re_loop - let mk_re_intersect = Z3native.mk_re_intersect + let mk_re_intersect ctx args = Z3native.mk_re_intersect ctx (List.length args) args let mk_re_complement = Z3native.mk_re_complement let mk_re_empty = Z3native.mk_re_empty let mk_re_full = Z3native.mk_re_full diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index bbfed07d2..08e0a6747 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -1850,115 +1850,115 @@ end (** Sequences, Strings and Regular Expressions **) module Seq : sig - (* create a sequence sort *) + (** create a sequence sort *) val mk_seq_sort : context -> Sort.sort -> Sort.sort - (* test if sort is a sequence sort *) + (** test if sort is a sequence sort *) val is_seq_sort : context -> Sort.sort -> bool - (* create regular expression sorts over sequences of the argument sort *) + (** create regular expression sorts over sequences of the argument sort *) val mk_re_sort : context -> Sort.sort -> Sort.sort - (* test if sort is a regular expression sort *) + (** test if sort is a regular expression sort *) val is_re_sort : context -> Sort.sort -> bool - (* create string sort *) + (** create string sort *) val mk_string_sort : context -> Sort.sort - (* test if sort is a string sort (a sequence of 8-bit bit-vectors) *) + (** test if sort is a string sort (a sequence of 8-bit bit-vectors) *) val is_string_sort : context -> Sort.sort -> bool - (* create a string literal *) + (** create a string literal *) val mk_string : context -> string -> Expr.expr - (* test if expression is a string *) + (** test if expression is a string *) val is_string : context -> Expr.expr -> bool - (* retrieve string from string Expr.expr *) + (** retrieve string from string Expr.expr *) val get_string : context -> Expr.expr -> string - (* the empty sequence over base sort *) + (** the empty sequence over base sort *) val mk_seq_empty : context -> Sort.sort -> Expr.expr - (* a unit sequence *) + (** a unit sequence *) val mk_seq_unit : context -> Expr.expr -> Expr.expr - (* sequence concatenation *) + (** sequence concatenation *) val mk_seq_concat : context -> Expr.expr list -> Expr.expr - (* predicate if the first argument is a prefix of the second *) + (** predicate if the first argument is a prefix of the second *) val mk_seq_prefix : context -> Expr.expr -> Expr.expr -> Expr.expr - (* predicate if the first argument is a suffix of the second *) + (** predicate if the first argument is a suffix of the second *) val mk_seq_suffix : context -> Expr.expr -> Expr.expr -> Expr.expr - (* predicate if the first argument contains the second *) + (** predicate if the first argument contains the second *) val mk_seq_contains : context -> Expr.expr -> Expr.expr -> Expr.expr - (* extract sub-sequence starting at index given by second argument and of length provided by third argument *) + (** extract sub-sequence starting at index given by second argument and of length provided by third argument *) val mk_seq_extract : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr - (* replace first occurrence of second argument by third *) + (** replace first occurrence of second argument by third *) val mk_seq_replace : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr - (* a unit sequence at index provided by second argument *) + (** a unit sequence at index provided by second argument *) val mk_seq_at : context -> Expr.expr -> Expr.expr -> Expr.expr - (* length of a sequence *) + (** length of a sequence *) val mk_seq_length : context -> Expr.expr -> Expr.expr - (* index of the first occurrence of the second argument in the first *) + (** index of the first occurrence of the second argument in the first *) val mk_seq_index : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr - (* retrieve integer expression encoded in string *) + (** retrieve integer expression encoded in string *) val mk_str_to_int : context -> Expr.expr -> Expr.expr - (* compare strings less-than-or-equal *) + (** compare strings less-than-or-equal *) val mk_str_le : context -> Expr.expr -> Expr.expr -> Expr.expr - (* compare strings less-than *) + (** compare strings less-than *) val mk_str_lt : context -> Expr.expr -> Expr.expr -> Expr.expr - (* convert an integer expression to a string *) + (** convert an integer expression to a string *) val mk_int_to_str : context -> Expr.expr -> Expr.expr - (* create regular expression that accepts the argument sequence *) + (** create regular expression that accepts the argument sequence *) val mk_seq_to_re : context -> Expr.expr -> Expr.expr - (* regular expression membership predicate *) + (** regular expression membership predicate *) val mk_seq_in_re : context -> Expr.expr -> Expr.expr -> Expr.expr - (* regular expression plus *) + (** regular expression plus *) val mk_re_plus : context -> Expr.expr -> Expr.expr - (* regular expression star *) + (** regular expression star *) val mk_re_star : context -> Expr.expr -> Expr.expr - (* optional regular expression *) + (** optional regular expression *) val mk_re_option : context -> Expr.expr -> Expr.expr - (* union of regular expressions *) + (** union of regular expressions *) val mk_re_union : context -> Expr.expr list -> Expr.expr - (* concatenation of regular expressions *) + (** concatenation of regular expressions *) val mk_re_concat : context -> Expr.expr list -> Expr.expr - (* regular expression for the range between two characters *) + (** regular expression for the range between two characters *) val mk_re_range : context -> Expr.expr -> Expr.expr -> Expr.expr - (* bounded loop regular expression *) + (** bounded loop regular expression *) val mk_re_loop : context -> Expr.expr -> int -> int -> Expr.expr - (* intersection of regular expressions *) - val mk_re_intersect : context -> int -> Expr.expr list -> Expr.expr + (** intersection of regular expressions *) + val mk_re_intersect : context -> Expr.expr list -> Expr.expr - (* the regular expression complement *) + (** the regular expression complement *) val mk_re_complement : context -> Expr.expr -> Expr.expr - (* the regular expression that accepts no sequences *) + (** the regular expression that accepts no sequences *) val mk_re_empty : context -> Sort.sort -> Expr.expr - (* the regular expression that accepts all sequences *) + (** the regular expression that accepts all sequences *) val mk_re_full : context -> Sort.sort -> Expr.expr end From 8a33391708b282f93d0418ea0235f56a1e6fd265 Mon Sep 17 00:00:00 2001 From: Marc Mosko Date: Tue, 6 Jul 2021 01:22:00 -0700 Subject: [PATCH 16/35] Expose optimize.assertAndTrack to Java (#5387) Co-authored-by: Marc Mosko --- src/api/java/Optimize.java | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index 741dd08d9..c5a26b439 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -73,6 +73,28 @@ public class Optimize extends Z3Object { Assert(constraints); } + /** + * Assert a constraint into the optimizer, and track it (in the unsat) core + * using the Boolean constant p. + * + * Remarks: + * This API is an alternative to {@link #check} with assumptions for + * extracting unsat cores. + * Both APIs can be used in the same solver. The unsat core will contain a + * combination + * of the Boolean variables provided using {@link #assertAndTrack} + * and the Boolean literals + * provided using {@link #check} with assumptions. + */ + public void AssertAndTrack(Expr constraint, Expr p) + { + getContext().checkContextMatch(constraint); + getContext().checkContextMatch(p); + + Native.optimizeAssertAndTrack(getContext().nCtx(), getNativeObject(), + constraint.getNativeObject(), p.getNativeObject()); + } + /** * Handle to objectives returned by objective functions. **/ From ca05c668479d25cc5ae8496b068de16a988e3d91 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Jul 2021 14:20:03 +0200 Subject: [PATCH 17/35] #5376 --- src/smt/qi_queue.cpp | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 875c728a4..26beb883f 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -387,7 +387,7 @@ namespace smt { bool result = true; for (unsigned i = 0; i < sz; i++) { entry & e = m_delayed_entries[i]; - TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); + TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << " min-cost: " << min_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= min_cost) { TRACE("qi_queue", tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";); @@ -401,9 +401,11 @@ namespace smt { } bool result = true; + bool has_delayed = false; for (unsigned i = 0; i < m_delayed_entries.size(); i++) { entry & e = m_delayed_entries[i]; TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); + has_delayed |= !e.m_instantiated; if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) { TRACE("qi_queue", tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";); @@ -413,6 +415,20 @@ namespace smt { instantiate(e); } } + if (result && has_delayed) { + for (unsigned i = 0; i < m_delayed_entries.size(); i++) { + entry& e = m_delayed_entries[i]; + if (e.m_instantiated) + continue; + TRACE("qi_queue", + tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";); + result = false; + m_instantiated_trail.push_back(i); + m_stats.m_num_lazy_instances++; + instantiate(e); + break; + } + } return result; } From af5b2a417917e162086691b46bed37758f4f4ee8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Jul 2021 16:44:44 +0200 Subject: [PATCH 18/35] #5376 --- src/smt/qi_queue.cpp | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 26beb883f..f359136af 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -401,11 +401,9 @@ namespace smt { } bool result = true; - bool has_delayed = false; for (unsigned i = 0; i < m_delayed_entries.size(); i++) { entry & e = m_delayed_entries[i]; TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); - has_delayed |= !e.m_instantiated; if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) { TRACE("qi_queue", tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";); @@ -415,20 +413,6 @@ namespace smt { instantiate(e); } } - if (result && has_delayed) { - for (unsigned i = 0; i < m_delayed_entries.size(); i++) { - entry& e = m_delayed_entries[i]; - if (e.m_instantiated) - continue; - TRACE("qi_queue", - tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";); - result = false; - m_instantiated_trail.push_back(i); - m_stats.m_num_lazy_instances++; - instantiate(e); - break; - } - } return result; } From c2595b9bc80ef7b3d9c9d864541bf6c28f91989d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Jul 2021 18:58:27 +0200 Subject: [PATCH 19/35] #5379 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index c564acba3..6ef012836 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -559,10 +559,11 @@ unsigned get_node_hash(ast const * n) { return to_sort(n)->get_name().hash(); else return combine_hash(to_sort(n)->get_name().hash(), to_sort(n)->get_info()->hash()); - case AST_FUNC_DECL: + case AST_FUNC_DECL: { + unsigned h = combine_hash(to_func_decl(n)->get_name().hash(), to_func_decl(n)->get_range()->hash()); return ast_array_hash(to_func_decl(n)->get_domain(), to_func_decl(n)->get_arity(), - to_func_decl(n)->get_info() == nullptr ? - to_func_decl(n)->get_name().hash() : combine_hash(to_func_decl(n)->get_name().hash(), to_func_decl(n)->get_info()->hash())); + combine_hash(h, to_func_decl(n)->get_info() == nullptr ? 0 : to_func_decl(n)->get_info()->hash())); + } case AST_APP: return ast_array_hash(to_app(n)->get_args(), to_app(n)->get_num_args(), From 4f184b6aa9d42da757fba16cf7e5dd7882ed54aa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Jul 2021 19:20:35 +0200 Subject: [PATCH 20/35] fix #5376 --- src/smt/smt_model_checker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 4598a9a3f..9569ec3a8 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -218,7 +218,7 @@ namespace smt { TRACE("model_checker", tout << "Got some value " << sk_value << "\n";); if (use_inv) { - unsigned sk_term_gen; + unsigned sk_term_gen = 0; expr * sk_term = m_model_finder.get_inv(q, i, sk_value, sk_term_gen); if (sk_term != nullptr) { TRACE("model_checker", tout << "Found inverse " << mk_pp(sk_term, m) << "\n";); From 29c6d423806346b75724d94398e92bfe80730442 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 7 Jul 2021 08:20:31 +0200 Subject: [PATCH 21/35] is-char is overloaded #5389 Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 48d46923f..8ce0f7a4e 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -222,6 +222,7 @@ public: sort* mk_string_sort() const { return seq.string_sort(); } bool is_char(sort* s) const { return seq.is_char(s); } + bool is_char(expr* e) const { return is_char(e->get_sort()); } bool is_string(sort* s) const { return is_seq(s) && seq.is_char(to_sort(s->get_parameter(0).get_ast())); } bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); } bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); } @@ -230,7 +231,6 @@ public: bool is_seq(sort* s, sort*& seq) const { return is_seq(s) && (seq = to_sort(s->get_parameter(0).get_ast()), true); } bool is_re(expr* e) const { return is_re(e->get_sort()); } bool is_re(expr* e, sort*& seq) const { return is_re(e->get_sort(), seq); } - bool is_char(expr* e) const { return is_char(e->get_sort()); } bool is_const_char(expr* e, unsigned& c) const; bool is_const_char(expr* e) const { unsigned c; return is_const_char(e, c); } bool is_char_le(expr const* e) const; From 897cbf347bcf73ac986d50636b15f09968130880 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 7 Jul 2021 16:51:06 +0200 Subject: [PATCH 22/35] fix #5381 --- src/ast/rewriter/seq_eq_solver.cpp | 3 ++ src/smt/theory_seq.cpp | 50 ++++++++++++++++++++++++++++-- src/smt/theory_seq.h | 2 ++ 3 files changed, 52 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_eq_solver.cpp b/src/ast/rewriter/seq_eq_solver.cpp index 223372da1..2c595090e 100644 --- a/src/ast/rewriter/seq_eq_solver.cpp +++ b/src/ast/rewriter/seq_eq_solver.cpp @@ -148,6 +148,7 @@ namespace seq { expr_ref_vector const* _es = nullptr; if (!match_itos3(e, n, _es)) return false; + expr_ref_vector const& es = *_es; if (es.empty()) { @@ -183,6 +184,8 @@ namespace seq { expr_ref digit = m_ax.sk().mk_digit2int(u); add_consequence(m_ax.mk_ge(digit, 1)); } + expr_ref y(seq.str.mk_concat(e.rs, e.ls[0]->get_sort()), m); + ctx.add_solution(e.ls[0], y); return true; } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 89f224e2e..e4eec609f 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -402,8 +402,11 @@ final_check_status theory_seq::final_check_eh() { ++m_stats.m_branch_nqs; TRACEFIN("branch_ne"); return FC_CONTINUE; + } + if (branch_itos()) { + TRACEFIN("branch_itos"); + return FC_CONTINUE; } - if (m_unhandled_expr) { TRACEFIN("give_up"); TRACE("seq", tout << "unhandled: " << mk_pp(m_unhandled_expr, m) << "\n";); @@ -1539,14 +1542,55 @@ bool theory_seq::check_int_string() { bool theory_seq::check_int_string(expr* e) { expr* n = nullptr; if (ctx.inconsistent()) - return true; + return true; if (m_util.str.is_itos(e, n) && !m_util.str.is_stoi(n) && add_length_to_eqc(e)) return true; if (m_util.str.is_stoi(e, n) && !m_util.str.is_itos(n) && add_length_to_eqc(n)) return true; + return false; } - + +bool theory_seq::branch_itos() { + bool change = false; + for (expr * e : m_int_string) { + if (branch_itos(e)) + change = true; + } + return change; +} + +bool theory_seq::branch_itos(expr* e) { + expr* n = nullptr; + rational val; + if (ctx.inconsistent()) + return true; + if (!m_util.str.is_itos(e, n)) + return false; + if (!ctx.e_internalized(e)) + return false; + enode* r = ctx.get_enode(e)->get_root(); + if (m_util.str.is_string(r->get_expr())) + return false; + if (!get_num_value(n, val)) + return false; + if (val.is_neg()) + return false; + literal b = mk_eq(e, m_util.str.mk_string(val.to_string()), false); + if (ctx.get_assignment(b) == l_true) + return false; + if (ctx.get_assignment(b) == l_false) { + literal a = mk_eq(n, m_autil.mk_int(val), false); + add_axiom(~a, b); + } + else { + ctx.force_phase(b); + ctx.mark_as_relevant(b); + } + return true; +} + + void theory_seq::apply_sort_cnstr(enode* n, sort* s) { mk_var(n); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 5042fe14f..b7ea9517a 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -566,6 +566,8 @@ namespace smt { void add_int_string(expr* e); bool check_int_string(); bool check_int_string(expr* e); + bool branch_itos(); + bool branch_itos(expr* e); expr_ref add_elim_string_axiom(expr* n); void add_in_re_axiom(expr* n); From 2973d3bdc1fd01e710f312e15508445a9716ce3f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 7 Jul 2021 23:43:30 +0200 Subject: [PATCH 23/35] fix #5392 --- src/smt/smt_context_pp.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index b93d10e8e..3f826c2d1 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -608,14 +608,14 @@ namespace smt { clause * cls = j.get_clause(); out << "clause "; if (cls) out << literal_vector(cls->get_num_literals(), cls->begin()); - if (cls) display_literals_smt2(out << "\n", cls->get_num_literals(), cls->begin()); + // if (cls) display_literals_smt2(out << "\n", cls->get_num_literals(), cls->begin()); break; } case b_justification::JUSTIFICATION: { literal_vector lits; const_cast(*m_conflict_resolution).justification2literals(j.get_justification(), lits); out << "justification " << j.get_justification()->get_from_theory() << ": "; - display_literals_smt2(out, lits); + // display_literals_smt2(out, lits); break; } default: From 0f8d2d1d51b814edda853dacd8a7b88a45fad33a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Jul 2021 14:47:51 +0200 Subject: [PATCH 24/35] fix #5399 --- src/ast/rewriter/seq_rewriter.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 9049ad971..6e0d0f7b7 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1775,6 +1775,10 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu result = str().mk_concat(c, a); return BR_REWRITE1; } + if (str().is_empty(a) && str().is_empty(c)) { + result = a; + return BR_DONE; + } m_lhs.reset(); str().get_concat(a, m_lhs); From 34885562e0debe961b73935c6d02e71d6628238d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Jul 2021 15:20:56 +0200 Subject: [PATCH 25/35] try without #!/bin/env python #5397 --- scripts/mk_consts_files.py | 2 +- scripts/mk_def_file.py | 2 +- scripts/mk_gparams_register_modules_cpp.py | 2 +- scripts/mk_install_tactic_cpp.py | 2 +- scripts/mk_mem_initializer_cpp.py | 2 +- scripts/mk_pat_db.py | 2 +- scripts/pyg2hpp.py | 2 +- scripts/update_api.py | 2 +- 8 files changed, 8 insertions(+), 8 deletions(-) diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py index 39d4e9439..03c57770c 100755 --- a/scripts/mk_consts_files.py +++ b/scripts/mk_consts_files.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +# -- /usr/bin/env python """ Reads a list of Z3 API header files and generate the constant declarations need diff --git a/scripts/mk_def_file.py b/scripts/mk_def_file.py index 07418a975..c9b87a95d 100755 --- a/scripts/mk_def_file.py +++ b/scripts/mk_def_file.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +# - /usr/bin/env python """ Reads a list of Z3 API header files and generate a ``.def`` file to define the diff --git a/scripts/mk_gparams_register_modules_cpp.py b/scripts/mk_gparams_register_modules_cpp.py index 9614768ca..83a0bc91a 100755 --- a/scripts/mk_gparams_register_modules_cpp.py +++ b/scripts/mk_gparams_register_modules_cpp.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +# -- /usr/bin/env python """ Determines the available global parameters from a list of header files and generates a ``gparams_register_modules.cpp`` file in the destination directory diff --git a/scripts/mk_install_tactic_cpp.py b/scripts/mk_install_tactic_cpp.py index b82e71354..004e9bb96 100755 --- a/scripts/mk_install_tactic_cpp.py +++ b/scripts/mk_install_tactic_cpp.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +# -- /usr/bin/env python """ Determines the available tactics from a list of header files and generates a ``install_tactic.cpp`` file in the destination directory that defines a diff --git a/scripts/mk_mem_initializer_cpp.py b/scripts/mk_mem_initializer_cpp.py index 238595fa3..cd22e9045 100755 --- a/scripts/mk_mem_initializer_cpp.py +++ b/scripts/mk_mem_initializer_cpp.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +# -- /usr/bin/env python """ Scans the listed header files for memory initializers and finalizers and diff --git a/scripts/mk_pat_db.py b/scripts/mk_pat_db.py index 76dc7ba48..116aff67d 100755 --- a/scripts/mk_pat_db.py +++ b/scripts/mk_pat_db.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +# -- /usr/bin/env python """ Reads a pattern database and generates the corresponding header file. diff --git a/scripts/pyg2hpp.py b/scripts/pyg2hpp.py index b1af3edc9..97aa1d8a7 100755 --- a/scripts/pyg2hpp.py +++ b/scripts/pyg2hpp.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +# - /usr/bin/env python """ Reads a pyg file and emits the corresponding C++ header file into the specified destination diff --git a/scripts/update_api.py b/scripts/update_api.py index c973ff200..56ef503e9 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python +# - !/usr/bin/env python ############################################ # Copyright (c) 2012 Microsoft Corporation # From 66fc98015493d6506439e0e0217f353257e59cc2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Jul 2021 17:13:16 +0200 Subject: [PATCH 26/35] add helper axioms for int2bv #5396 --- src/smt/theory_bv.cpp | 34 +++++++++++++++++++++++----------- src/smt/theory_lra.cpp | 1 + 2 files changed, 24 insertions(+), 11 deletions(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 6efcc68c1..c714b17f3 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -646,9 +646,8 @@ namespace smt { ); ctx.mark_as_relevant(l); - if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var())); + scoped_trace_stream _ts(*this, l); ctx.mk_th_axiom(get_id(), 1, &l); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } void theory_bv::internalize_int2bv(app* n) { @@ -688,9 +687,10 @@ namespace smt { literal l(mk_eq(lhs, rhs, false)); ctx.mark_as_relevant(l); - if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var())); - ctx.mk_th_axiom(get_id(), 1, &l); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + { + scoped_trace_stream _ts(*this, l); + ctx.mk_th_axiom(get_id(), 1, &l); + } TRACE("bv", tout << mk_pp(lhs, m) << " == \n"; @@ -704,17 +704,29 @@ namespace smt { for (unsigned i = 0; i < sz; ++i) { numeral div = power(numeral(2), i); mod = numeral(2); - rhs = (i == 0) ? e : m_autil.mk_idiv(e, m_autil.mk_numeral(div, true)); - rhs = m_autil.mk_mod(rhs, m_autil.mk_numeral(mod, true)); + expr_ref div_rhs((i == 0) ? e : m_autil.mk_idiv(e, m_autil.mk_numeral(div, true)), m); + rhs = m_autil.mk_mod(div_rhs, m_autil.mk_numeral(mod, true)); rhs = ctx.mk_eq_atom(rhs, m_autil.mk_int(1)); lhs = n_bits.get(i); TRACE("bv", tout << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";); l = literal(mk_eq(lhs, rhs, false)); ctx.mark_as_relevant(l); - if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var())); - ctx.mk_th_axiom(get_id(), 1, &l); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - + { + scoped_trace_stream _st(*this, l); + ctx.mk_th_axiom(get_id(), 1, &l); + } + { + // 0 < e < 2^i => e div 2^i = 0 + expr_ref zero(m_autil.mk_int(0), m); + literal a = mk_literal(m_autil.mk_ge(e, m_autil.mk_int(div))); + literal b = mk_literal(m_autil.mk_ge(e, zero)); + literal c = mk_eq(div_rhs, zero, false); + ctx.mark_as_relevant(a); + ctx.mark_as_relevant(b); + ctx.mark_as_relevant(c); + // scoped_trace_stream _st(*this, a, ~b); + ctx.mk_th_axiom(get_id(), a, ~b, c); + } } } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 1187ead7a..30d9a8836 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1248,6 +1248,7 @@ public: mk_axiom(eq); mk_axiom(mk_literal(a.mk_ge(mod, zero))); mk_axiom(mk_literal(a.mk_le(mod, upper))); + { std::function log = [&,this]() { th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()))); From bc2e6ce037a947c449ae291788924a2b0ff41e1e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Jul 2021 22:42:02 +0200 Subject: [PATCH 27/35] Update release.yml for Azure Pipelines --- scripts/release.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/release.yml b/scripts/release.yml index 1e93d51c3..81f4fc897 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -325,7 +325,7 @@ stages: # Enable on release: - job: NuGetPublish - condition: eq(0,1) + condition: eq(1,1) displayName: "Publish to NuGet.org" steps: - task: DownloadPipelineArtifact@2 @@ -346,7 +346,7 @@ stages: # Enable on release: - job: PyPIPublish - condition: eq(0,1) + condition: eq(1,1) displayName: "Publish to PyPI" pool: vmImage: "ubuntu-latest" From 5fac396c2fb0ae8d9df350cb36cd3cbe00bc2947 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Jul 2021 19:25:04 +0200 Subject: [PATCH 28/35] simplify some verbose trace-stream --- src/smt/smt_theory.cpp | 12 ++++++++++++ src/smt/smt_theory.h | 8 ++++++++ src/smt/theory_lra.cpp | 25 +++++++------------------ 3 files changed, 27 insertions(+), 18 deletions(-) diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp index 5c3352ff4..60f8dc3ae 100644 --- a/src/smt/smt_theory.cpp +++ b/src/smt/smt_theory.cpp @@ -195,6 +195,18 @@ namespace smt { log_axiom_instantiation(mk_or(fmls)); } + + void theory::log_axiom_instantiation(literal_buffer const& ls) { + ast_manager& m = get_manager(); + expr_ref_vector fmls(m); + expr_ref tmp(m); + for (literal l : ls) { + ctx.literal2expr(l, tmp); + fmls.push_back(tmp); + } + log_axiom_instantiation(mk_or(fmls)); + } + void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, app * const * bindings, unsigned pattern_id, const vector> & used_enodes) { ast_manager & m = get_manager(); app_ref _r(r, m); diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index a77b4168c..7799acf24 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -124,6 +124,12 @@ namespace smt { } } + scoped_trace_stream(theory& th, literal_buffer const& lits) : m(th.get_manager()) { + if (m.has_trace_stream()) { + th.log_axiom_instantiation(lits); + } + } + scoped_trace_stream(theory& th, literal lit): m(th.get_manager()) { if (m.has_trace_stream()) { literal_vector lits; @@ -464,6 +470,8 @@ namespace smt { void log_axiom_instantiation(literal_vector const& ls); + void log_axiom_instantiation(literal_buffer const& ls); + void log_axiom_instantiation(app * r, unsigned num_blamed_enodes, enode ** blamed_enodes) { vector> used_enodes; for (unsigned i = 0; i < num_blamed_enodes; ++i) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 30d9a8836..fe7f4a5e8 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1321,13 +1321,8 @@ public: exprs.push_back(c.bool_var2expr(mod_j.var())); ctx().mark_as_relevant(mod_j); } - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_or(exprs.size(), exprs.data()); - th.log_axiom_instantiation(body); - } + scoped_trace_stream _st(th, lits); ctx().mk_th_axiom(get_id(), lits.size(), lits.begin()); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } } @@ -1750,20 +1745,14 @@ public: literal p_ge_r1 = mk_literal(a.mk_ge(p, a.mk_numeral(lo, true))); literal n_le_div = mk_literal(a.mk_le(n, a.mk_numeral(div_r, true))); literal n_ge_div = mk_literal(a.mk_ge(n, a.mk_numeral(div_r, true))); - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(ctx().bool_var2expr(p_le_r1.var()), ctx().bool_var2expr(n_le_div.var())); - th.log_axiom_instantiation(body); + { + scoped_trace_stream _sts(th, ~p_le_r1, n_le_div); + mk_axiom(~p_le_r1, n_le_div); } - mk_axiom(~p_le_r1, n_le_div); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_implies(ctx().bool_var2expr(p_ge_r1.var()), ctx().bool_var2expr(n_ge_div.var())); - th.log_axiom_instantiation(body); + { + scoped_trace_stream _sts(th, ~p_ge_r1, n_ge_div); + mk_axiom(~p_ge_r1, n_ge_div); } - mk_axiom(~p_ge_r1, n_ge_div); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; all_divs_valid = false; From e05f5ef6d14291a83a3f7df6afa04de6a6cc8033 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Jul 2021 06:15:20 +0200 Subject: [PATCH 29/35] na Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_internalize.cpp | 4 ++++ src/sat/smt/q_solver.cpp | 7 +++---- src/smt/theory_lra.cpp | 9 +++------ 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 0a7aa717f..caf12235c 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -139,6 +139,10 @@ namespace euf { sat::literal lit2 = literal(v, false); s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id())); s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id())); + if (relevancy_enabled()) { + add_root(~lit, lit2); + add_root(lit, ~lit2); + } lit = lit2; } diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index eebb4a721..b114e844f 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -41,7 +41,7 @@ namespace q { quantifier* q = to_quantifier(e); auto const& exp = expand(q); - if (exp.size() > 1 && is_forall(q)) { + if (exp.size() > 1 && is_forall(q) && !l.sign()) { for (expr* e : exp) { sat::literal lit = ctx.internalize(e, l.sign(), false, false); add_clause(~l, lit); @@ -50,14 +50,13 @@ namespace q { } return; } - if (exp.size() > 1 && is_exists(q)) { + if (exp.size() > 1 && is_exists(q) /* && l.sign() */) { sat::literal_vector lits; lits.push_back(~l); for (expr* e : exp) lits.push_back(ctx.internalize(e, l.sign(), false, false)); add_clause(lits); - if (ctx.relevancy_enabled()) - ctx.add_root(lits); + ctx.add_root(lits); return; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index fe7f4a5e8..abe10d0f3 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1170,14 +1170,11 @@ public: VERIFY(a.is_is_int(n, x)); literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false); literal is_int = ctx().get_literal(n); - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_iff(n, ctx().bool_var2expr(eq.var())); - th.log_axiom_instantiation(body); - } + scoped_trace_stream _sts1(th, ~is_int, eq); + scoped_trace_stream _sts2(th, is_int, ~eq); mk_axiom(~is_int, eq); mk_axiom(is_int, ~eq); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + } // create axiom for From 10ad5bae216e1f6df8d6d6a6206964afa1b7a469 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Jul 2021 06:17:58 +0200 Subject: [PATCH 30/35] increment version Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 2 +- RELEASE_NOTES | 1 + scripts/mk_project.py | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index fa2531670..d01004c36 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,7 +2,7 @@ cmake_minimum_required(VERSION 3.4) set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") -project(Z3 VERSION 4.8.11.0 LANGUAGES CXX) +project(Z3 VERSION 4.8.12.0 LANGUAGES CXX) ################################################################################ # Project version diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 4a423b536..89f839cae 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -10,6 +10,7 @@ Version 4.8.next option, but at this point does not translate into benefits. It is currently turned off by default. + Version 4.8.11 ============== - self-contained character theory, direct support for UTF8, Unicode character sets. diff --git a/scripts/mk_project.py b/scripts/mk_project.py index b5ed1a070..4e7c0e97b 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -8,7 +8,7 @@ from mk_util import * def init_version(): - set_version(4, 8, 11, 0) + set_version(4, 8, 12, 0) # Z3 Project definition def init_project_def(): From 18a76ab82c29a2777674499c3efdf0e71f477fa5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Jul 2021 06:42:27 +0200 Subject: [PATCH 31/35] #5336 Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_internalize.cpp | 4 ++-- src/sat/smt/q_solver.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index caf12235c..a7476bc5d 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -140,8 +140,8 @@ namespace euf { s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id())); s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id())); if (relevancy_enabled()) { - add_root(~lit, lit2); - add_root(lit, ~lit2); + add_aux(~lit, lit2); + add_aux(lit, ~lit2); } lit = lit2; } diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index b114e844f..af670297c 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -50,7 +50,7 @@ namespace q { } return; } - if (exp.size() > 1 && is_exists(q) /* && l.sign() */) { + if (exp.size() > 1 && is_exists(q) && l.sign()) { sat::literal_vector lits; lits.push_back(~l); for (expr* e : exp) From cab107651459ee74d7a7cf90cafcbb76bffaa2a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Jul 2021 21:00:58 +0200 Subject: [PATCH 32/35] #5336 --- src/math/simplex/model_based_opt.cpp | 37 +++++++++++++++++++--------- src/qe/mbp/mbp_arith.cpp | 4 ++- src/qe/mbp/mbp_plugin.cpp | 2 +- src/sat/smt/euf_solver.cpp | 8 ++++-- 4 files changed, 35 insertions(+), 16 deletions(-) diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index e785c33ed..6a05de93f 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -134,20 +134,29 @@ namespace opt { } void model_based_opt::def::normalize() { - if (m_div.is_one()) return; + SASSERT(m_div.is_int()); + if (m_div.is_neg()) { + for (var& v : m_vars) + v.m_coeff.neg(); + m_coeff.neg(); + m_div.neg(); + } + if (m_div.is_one()) + return; rational g(m_div); + if (!m_coeff.is_int()) + return; g = gcd(g, m_coeff); for (var const& v : m_vars) { + if (!v.m_coeff.is_int()) + return; g = gcd(g, abs(v.m_coeff)); - if (g.is_one()) break; - } - if (m_div.is_neg()) { - g.neg(); + if (g.is_one()) + break; } if (!g.is_one()) { - for (var& v : m_vars) { - v.m_coeff /= g; - } + for (var& v : m_vars) + v.m_coeff /= g; m_coeff /= g; m_div /= g; } @@ -1130,9 +1139,12 @@ namespace opt { } TRACE("opt1", display(tout << "tableau after replace x by y := v" << y << "\n");); def result = project(y, compute_def); - if (compute_def) - result = (result * D) + u; - SASSERT(!compute_def || eval(result) == eval(x)); + if (compute_def) { + result = (result * D) + u; + m_var2value[x] = eval(result); + } + TRACE("opt1", display(tout << "tableau after project y" << y << "\n");); + return result; } @@ -1181,7 +1193,7 @@ namespace opt { // 3 | -t & 21 | (-ct + 3s) & a-t <= 3u model_based_opt::def model_based_opt::solve_for(unsigned row_id1, unsigned x, bool compute_def) { - TRACE("opt", tout << "v" << x << "\n" << m_rows[row_id1] << "\n";); + TRACE("opt", tout << "v" << x << " := " << eval(x) << "\n" << m_rows[row_id1] << "\n";); rational a = get_coefficient(row_id1, x), b; ineq_type ty = m_rows[row_id1].m_type; SASSERT(!a.is_zero()); @@ -1231,6 +1243,7 @@ namespace opt { if (compute_def) { result = def(m_rows[row_id1], x); m_var2value[x] = eval(result); + TRACE("opt1", tout << "updated eval " << x << " := " << eval(x) << "\n";); } retire_row(row_id1); return result; diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index ab13e0813..a94984fbd 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -294,7 +294,9 @@ namespace mbp { } } fmls.shrink(j); - TRACE("qe", tout << "formulas\n" << fmls << "\n";); + TRACE("qe", tout << "formulas\n" << fmls << "\n"; + for (auto [e, id] : tids) + tout << mk_pp(e, m) << " -> " << id << "\n";); // fmls holds residue, // mbo holds linear inequalities that are in scope diff --git a/src/qe/mbp/mbp_plugin.cpp b/src/qe/mbp/mbp_plugin.cpp index af1043593..723ef26fa 100644 --- a/src/qe/mbp/mbp_plugin.cpp +++ b/src/qe/mbp/mbp_plugin.cpp @@ -102,7 +102,7 @@ namespace mbp { model_evaluator eval(model); eval.set_expand_array_equalities(true); TRACE("qe", tout << fmls << "\n";); - DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n";); SASSERT(!m.is_false(eval(fml))); }); + DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n" << model;); SASSERT(!m.is_false(eval(fml))); }); for (unsigned i = 0; i < fmls.size(); ++i) { expr* fml = fmls.get(i), * nfml, * f1, * f2, * f3; diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 66b373b6f..e8c9bb54f 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -302,13 +302,17 @@ namespace euf { size_t* c = to_ptr(l); SASSERT(is_literal(c)); SASSERT(l == get_literal(c)); - if (!sign && n->is_equality()) { + if (n->value_conflict()) { + euf::enode* nb = sign ? mk_false() : mk_true(); + m_egraph.merge(n, nb, c); + } + else if (!sign && n->is_equality()) { SASSERT(!m.is_iff(e)); euf::enode* na = n->get_arg(0); euf::enode* nb = n->get_arg(1); m_egraph.merge(na, nb, c); } - else if (n->merge_tf() || n->value_conflict()) { + else if (n->merge_tf()) { euf::enode* nb = sign ? mk_false() : mk_true(); m_egraph.merge(n, nb, c); } From a4f4975092030837f3e6bb2a8df162771dc6494c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Jul 2021 21:08:53 +0200 Subject: [PATCH 33/35] #5336 --- src/sat/smt/q_ematch.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index da7e670c8..e997476ed 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -401,7 +401,12 @@ namespace q { for (expr* arg : ors) { bool sign = m.is_not(arg, arg); expr* l, *r; - if (!m.is_eq(arg, l, r) || is_ground(arg)) { + if (m.is_distinct(arg) && to_app(arg)->get_num_args() == 2) { + l = to_app(arg)->get_arg(0); + r = to_app(arg)->get_arg(1); + sign = !sign; + } + else if (!m.is_eq(arg, l, r) || is_ground(arg)) { l = arg; r = sign ? m.mk_false() : m.mk_true(); sign = false; From 2ccfb1937de2bda061b2f869b61d1ac3ac5c9e71 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Jul 2021 23:20:19 +0200 Subject: [PATCH 34/35] na Signed-off-by: Nikolaj Bjorner --- src/qe/mbp/mbp_arith.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index a94984fbd..31329b3dd 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -281,7 +281,7 @@ namespace mbp { obj_map tids; expr_ref_vector pinned(m); unsigned j = 0; - TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n"; + TRACE("qe", tout << "vars: " << vars << "\n"; for (expr* f : fmls) tout << mk_pp(f, m) << " := " << model(f) << "\n";); for (unsigned i = 0; i < fmls.size(); ++i) { expr* fml = fmls.get(i); From 4c53655be7543555936bf6ded5a4c915a1c9c874 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Jul 2021 23:26:48 +0200 Subject: [PATCH 35/35] add z3doc build to release script Signed-off-by: Nikolaj Bjorner --- scripts/release.yml | 48 ++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 45 insertions(+), 3 deletions(-) diff --git a/scripts/release.yml b/scripts/release.yml index 81f4fc897..cc5946a91 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -72,6 +72,43 @@ stages: artifactName: 'UbuntuBuild' targetPath: $(Build.ArtifactStagingDirectory) + + - job: UbuntuDoc + displayName: "Ubuntu Doc build" + pool: + vmImage: "Ubuntu-18.04" + steps: + - script: sudo apt-get install ocaml opam libgmp-dev + - script: sudo apt-get install doxygen + - script: sudo apt-get install graphviz + - script: opam init -y + - script: eval `opam config env`; opam install zarith ocamlfind -y + - script: python scripts/mk_make.py --ml --staticlib + - script: | + set -e + cd build + eval `opam config env` + make -j3 + make -j3 examples + make -j3 test-z3 + ./ml_example + cd .. + - script: | + set -e + eval `opam config env` + cd doc + python mk_api_doc.py --mld --z3py-package-path=../build/python/z3 + mkdir api/html/ml + ocamldoc -html -d api/html/ml -sort -hide Z3 -I $( ocamlfind query zarith ) -I ../build/api/ml ../build/api/ml/z3enums.mli ../build/api/ml/z3.mli + cd .. + - script: zip -r z3doc.zip doc/api + - script: cp z3doc.zip $(Build.ArtifactStagingDirectory)/. + - task: PublishPipelineArtifact@0 + inputs: + artifactName: 'UbuntuDoc' + targetPath: $(Build.ArtifactStagingDirectory) + + - job: ManyLinuxBuild displayName: "ManyLinux build" pool: @@ -283,6 +320,11 @@ stages: inputs: artifact: 'UbuntuBuild' path: $(Agent.TempDirectory) + - task: DownloadPipelineArtifact@2 + displayName: "Download Doc" + inputs: + artifact: 'UbuntuDoc' + path: $(Agent.TempDirectory) - task: DownloadPipelineArtifact@2 displayName: 'Download macOS Build' inputs: @@ -307,7 +349,7 @@ stages: displayName: 'Download NuGet Package' inputs: artifact: 'NuGetPackage' - path: $(Agent.TempDirectory) + path: $(Agent.TempDirectory) - task: GitHubRelease@0 inputs: gitHubConnection: Z3GitHub @@ -323,9 +365,9 @@ stages: isDraft: true isPreRelease: false - # Enable on release: + # Enable on release (after fixing Nuget key) - job: NuGetPublish - condition: eq(1,1) + condition: eq(1,0) displayName: "Publish to NuGet.org" steps: - task: DownloadPipelineArtifact@2