diff --git a/RELEASE_NOTES b/RELEASE_NOTES index abc6fec1d..dac0367d2 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -10,8 +10,8 @@ Version 4.9.next - native word level bit-vector solving. - introduction of simple induction lemmas to handle a limited repertoire of induction proofs. -Version 4.9 -=========== +Version 4.9.0 +============= - API for incremental parsing of assertions. A description of the feature is given by example here: https://github.com/Z3Prover/z3/commit/815518dc026e900392bf0d08ed859e5ec42d1e43 It also allows incrementality at the level of adding assertions to the @@ -19,10 +19,21 @@ Version 4.9 - Fold/map for sequences: https://microsoft.github.io/rise4fun/docs/guide/Sequences#map-and-fold At this point these functions are only exposed over the SMTLIB2 interface (and not programmatic API) + maxdiff/mindiff on arrays are more likely to be deprecated - User Propagator: - Add functions and callbacks for external control over branching - A functioning dotnet API for the User Propagator https://github.com/Z3Prover/z3/blob/master/src/api/dotnet/UserPropagator.cs +- Java Script API + - higher level object wrappers are available thanks to Gibbons and Tomalka +- Totalizers and RC2 + - The MaxSAT engine now allows to run RC2 with totalizer encoding. + Totalizers are on by default as preliminary tests suggest this solves already 10% more problems on + standard benchmarks. The option rc2.totalizer (which by default is true) is used to control whether to use + totalizer encoding or built-in cardinality constraints. + The default engine is still maxres, so you have to set opt.maxsat_engine=rc2 to + enable the rc2 option at this point. The engines maxres-bin and rc2bin are experimental should not be used + (they are inferior to default options). Version 4.8.17 ============== diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index ca2e1584d..93e10f094 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -67,6 +67,30 @@ namespace recfun { m_decl = m.mk_func_decl(s, arity, domain, range, info); } + def* def::copy(util& dst, ast_translation& tr) { + SASSERT(&dst.m() == &tr.to()); + sort_ref_vector domain(tr.to()); + sort_ref range(tr(m_range.get()), tr.to()); + for (auto* s : m_domain) + domain.push_back(tr(s)); + family_id fid = dst.get_family_id(); + bool is_generated = m_decl->get_parameter(0).get_int() != 0; + def* r = alloc(def, tr.to(), fid, m_name, domain.size(), domain.data(), range, is_generated); + r->m_rhs = tr(m_rhs.get()); + for (auto* v : m_vars) + r->m_vars.push_back(tr(v)); + for (auto const& c1 : m_cases) { + r->m_cases.push_back(case_def(tr.to())); + auto& c2 = r->m_cases.back(); + c2.m_pred = tr(c1.m_pred.get()); + c2.m_guards = tr(c1.m_guards); + c2.m_rhs = tr(c1.m_rhs.get()); + c2.m_def = r; + c2.m_immediate = c1.m_immediate; + } + return r; + } + bool def::contains_def(util& u, expr * e) { struct def_find_p : public i_expr_pred { util& u; @@ -415,6 +439,19 @@ namespace recfun { return promise_def(&u(), d); } + void plugin::inherit(decl_plugin* other, ast_translation& tr) { + for (auto [k, v] : static_cast(other)->m_defs) { + func_decl_ref f(tr(k), tr.to()); + if (m_defs.contains(f)) + continue; + def* d = v->copy(u(), tr); + m_defs.insert(f, d); + for (case_def & c : d->get_cases()) + m_case_defs.insert(c.get_decl(), &c); + + } + } + promise_def plugin::ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated) { def* d = u().decl_fun(name, n, params, range, is_generated); erase_def(d->get_decl()); diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index 70447ff67..bbc4e5810 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -21,6 +21,7 @@ Revision History: #include "ast/ast.h" #include "ast/ast_pp.h" +#include "ast/ast_translation.h" #include "util/obj_hashtable.h" namespace recfun { @@ -62,6 +63,12 @@ namespace recfun { def * m_def; // const& solver::get_seq_args(enode* n) { + ptr_vector const& solver::get_seq_args(enode* n, enode*& sibling) { m_nodes.reset(); m_todo.reset(); auto add_todo = [&](enode* n) { @@ -515,9 +515,15 @@ namespace dt { m_todo.push_back(n); } }; - - for (enode* sib : euf::enode_class(n)) - add_todo(sib); + + for (enode* sib : euf::enode_class(n)) { + if (m_sutil.str.is_concat_of_units(sib->get_expr())) { + add_todo(sib); + sibling = sib; + break; + } + } + for (unsigned i = 0; i < m_todo.size(); ++i) { enode* n = m_todo[i]; @@ -551,10 +557,10 @@ namespace dt { // collect equalities on all children that may have been used. bool found = false; - auto add = [&](enode* arg) { - if (arg->get_root() == child->get_root()) { - if (arg != child) - m_used_eqs.push_back(enode_pair(arg, child)); + auto add = [&](enode* seq_arg) { + if (seq_arg->get_root() == child->get_root()) { + if (seq_arg != child) + m_used_eqs.push_back(enode_pair(seq_arg, child)); found = true; } }; @@ -564,11 +570,14 @@ namespace dt { if (m_autil.is_array(s) && dt.is_datatype(get_array_range(s))) for (enode* aarg : get_array_args(arg)) add(aarg); - } - sort* se; - if (m_sutil.is_seq(child->get_sort(), se) && dt.is_datatype(se)) { - for (enode* aarg : get_seq_args(child)) - add(aarg); + sort* se; + if (m_sutil.is_seq(arg->get_sort(), se) && dt.is_datatype(se)) { + enode* sibling = nullptr; + for (enode* seq_arg : get_seq_args(arg, sibling)) + add(seq_arg); + if (sibling && sibling != arg) + m_used_eqs.push_back(enode_pair(arg, sibling)); + } } VERIFY(found); @@ -636,12 +645,13 @@ namespace dt { // explore `arg` (with parent) expr* earg = arg->get_expr(); sort* s = earg->get_sort(), *se; + enode* sibling; if (dt.is_datatype(s)) { m_parent.insert(arg->get_root(), parent); oc_push_stack(arg); } else if (m_sutil.is_seq(s, se) && dt.is_datatype(se)) { - for (enode* sarg : get_seq_args(arg)) + for (enode* sarg : get_seq_args(arg, sibling)) if (process_arg(sarg)) return true; } diff --git a/src/sat/smt/dt_solver.h b/src/sat/smt/dt_solver.h index e0a076a2d..4e2524f6b 100644 --- a/src/sat/smt/dt_solver.h +++ b/src/sat/smt/dt_solver.h @@ -112,7 +112,7 @@ namespace dt { void oc_push_stack(enode * n); ptr_vector m_nodes, m_todo; ptr_vector const& get_array_args(enode* n); - ptr_vector const& get_seq_args(enode* n); + ptr_vector const& get_seq_args(enode* n, enode*& sibling); void pop_core(unsigned n) override;