From 367bfedab0f984ec7aefcb98cb1d6c088abf0dac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 May 2022 07:39:38 -0700 Subject: [PATCH] add min/max diff in final check Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 51 +++++++++++++++++++++---------- src/ast/seq_decl_plugin.h | 3 ++ src/sat/smt/array_axioms.cpp | 27 ++++++++++++++-- src/sat/smt/array_internalize.cpp | 2 ++ src/sat/smt/array_solver.cpp | 7 ++++- src/sat/smt/array_solver.h | 10 +++--- 6 files changed, 77 insertions(+), 23 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 77179a263..8b859d587 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -198,10 +198,6 @@ void seq_decl_plugin::init() { sort* boolT = m.mk_bool_sort(); sort* intT = arith_util(m).mk_int(); sort* predA = autil.mk_array_sort(A, boolT); - sort* arrAB = autil.mk_array_sort(A, B); - sort* arrIAB = autil.mk_array_sort(intT, A, B); - sort* arrBAB = autil.mk_array_sort(B, A, B); - sort* arrIBAB = autil.mk_array_sort(intT, B, A, B); sort* seqAseqAseqA[3] = { seqA, seqA, seqA }; sort* seqAreAseqA[3] = { seqA, reA, seqA }; sort* seqAseqA[2] = { seqA, seqA }; @@ -217,10 +213,6 @@ void seq_decl_plugin::init() { sort* str2TintT[3] = { strT, strT, intT }; sort* seqAintT[2] = { seqA, intT }; sort* seq3A[3] = { seqA, seqA, seqA }; - sort* arrABseqA[2] = { arrAB, seqA }; - sort* arrIABintTseqA[3] = { arrIAB, intT, seqA }; - sort* arrBAB_BseqA[3] = { arrBAB, B,seqA }; - sort* arrIBABintTBseqA[4] = { arrIBAB, intT, B, seqA }; m_sigs.resize(LAST_SEQ_OP); // TBD: have (par ..) construct and load parameterized signature from premable. @@ -239,10 +231,6 @@ void seq_decl_plugin::init() { m_sigs[OP_SEQ_NTH_I] = alloc(psig, m, "seq.nth_i", 1, 2, seqAintT, A); m_sigs[OP_SEQ_NTH_U] = alloc(psig, m, "seq.nth_u", 1, 2, seqAintT, A); m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq.len", 1, 1, &seqA, intT); - m_sigs[OP_SEQ_MAP] = alloc(psig, m, "seq.map", 2, 2, arrABseqA, seqB); - m_sigs[OP_SEQ_MAPI] = alloc(psig, m, "seq.mapi", 2, 3, arrIABintTseqA, seqB); - m_sigs[OP_SEQ_FOLDL] = alloc(psig, m, "seq.fold_left", 2, 3, arrBAB_BseqA, B); - m_sigs[OP_SEQ_FOLDLI] = alloc(psig, m, "seq.fold_leftli", 2, 4, arrIBABintTBseqA, B); m_sigs[OP_RE_PLUS] = alloc(psig, m, "re.+", 1, 1, &reA, reA); m_sigs[OP_RE_STAR] = alloc(psig, m, "re.*", 1, 1, &reA, reA); m_sigs[OP_RE_OPTION] = alloc(psig, m, "re.opt", 1, 1, &reA, reA); @@ -290,6 +278,7 @@ void seq_decl_plugin::init() { m_sigs[_OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT); } + sort* seq_decl_plugin::mk_reglan() { if (!m_reglan) { ast_manager& m = *m_manager; @@ -603,7 +592,8 @@ func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p case OP_SEQ_MAPI: case OP_SEQ_FOLDL: case OP_SEQ_FOLDLI: - return mk_str_fun(k, arity, domain, range, k); + add_map_sig(); + return mk_str_fun(k, arity, domain, range, k); case OP_SEQ_TO_RE: m_has_re = true; @@ -648,13 +638,42 @@ func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p } } +void seq_decl_plugin::add_map_sig() { + if (m_sigs[OP_SEQ_MAP]) + return; + ast_manager& m = *m_manager; + array_util autil(m); + sort* A = m.mk_uninterpreted_sort(symbol(0u)); + sort* B = m.mk_uninterpreted_sort(symbol(1u)); + parameter paramA(A); + parameter paramB(B); + sort* seqA = m.mk_sort(m_family_id, SEQ_SORT, 1, ¶mA); + sort* seqB = m.mk_sort(m_family_id, SEQ_SORT, 1, ¶mB); + sort* intT = arith_util(m).mk_int(); + sort* arrAB = autil.mk_array_sort(A, B); + sort* arrIAB = autil.mk_array_sort(intT, A, B); + sort* arrBAB = autil.mk_array_sort(B, A, B); + sort* arrIBAB = autil.mk_array_sort(intT, B, A, B); + sort* arrABseqA[2] = { arrAB, seqA }; + sort* arrIABintTseqA[3] = { arrIAB, intT, seqA }; + sort* arrBAB_BseqA[3] = { arrBAB, B,seqA }; + sort* arrIBABintTBseqA[4] = { arrIBAB, intT, B, seqA }; + m_sigs[OP_SEQ_MAP] = alloc(psig, m, "seq.map", 2, 2, arrABseqA, seqB); + m_sigs[OP_SEQ_MAPI] = alloc(psig, m, "seq.mapi", 2, 3, arrIABintTseqA, seqB); + m_sigs[OP_SEQ_FOLDL] = alloc(psig, m, "seq.fold_left", 2, 3, arrBAB_BseqA, B); + m_sigs[OP_SEQ_FOLDLI] = alloc(psig, m, "seq.fold_leftli", 2, 4, arrIBABintTBseqA, B); +} + void seq_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { init(); for (unsigned i = 0; i < m_sigs.size(); ++i) { - if (m_sigs[i]) { - op_names.push_back(builtin_name(m_sigs[i]->m_name.str(), i)); - } + if (m_sigs[i]) + op_names.push_back(builtin_name(m_sigs[i]->m_name.str(), i)); } + op_names.push_back(builtin_name("seq.map", OP_SEQ_MAP)); + op_names.push_back(builtin_name("seq.mapi", OP_SEQ_MAPI)); + op_names.push_back(builtin_name("seq.foldl", OP_SEQ_FOLDL)); + op_names.push_back(builtin_name("seq.foldli", OP_SEQ_FOLDLI)); op_names.push_back(builtin_name("str.in.re", _OP_STRING_IN_REGEXP)); op_names.push_back(builtin_name("str.in-re", _OP_STRING_IN_REGEXP)); op_names.push_back(builtin_name("str.to.re", _OP_STRING_TO_REGEXP)); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 03cfef033..29d7b08ef 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -140,6 +140,9 @@ class seq_decl_plugin : public decl_plugin { bool m_has_seq; char_decl_plugin* m_char_plugin { nullptr }; + + void add_map_sig(); + void match(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng); void match_assoc(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng); diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index 40be702b1..613d7a17c 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -68,6 +68,8 @@ namespace array { return assert_extensionality(r.n->get_expr(), r.select->get_expr()); case axiom_record::kind_t::is_diff: return assert_diff(r.n->get_app()); + case axiom_record::kind_t::is_diffselect: + return assert_diff_select(r.n->get_app(), r.select->get_app()); case axiom_record::kind_t::is_congruence: return assert_congruent_axiom(r.n->get_expr(), r.select->get_expr()); default: @@ -294,7 +296,7 @@ namespace array { * a = c and a[i] != b[i] => i <= md(b, c) or default(b) != default(c) * where ai = a[i], md = md(b, c) */ - bool solver::assert_diff_select(app* ai, app* md) { + bool solver::assert_diff_select(app* md, app* ai) { SASSERT(a.is_select(ai)); SASSERT(ai->get_num_args() == 2); expr* A = ai->get_arg(0); @@ -303,7 +305,7 @@ namespace array { expr* C = md->get_arg(1); literal eq_default = eq_internalize(a.mk_default(B), a.mk_default(C)); arith_util autil(m); - literal ineq = mk_literal(autil.mk_le(i, md)); + literal ineq = mk_literal(a.is_maxdiff(md) ? autil.mk_le(i, md) : autil.mk_le(md, i)); bool is_new = false; if (ctx.get_enode(A)->get_root() == ctx.get_enode(B)->get_root()) { literal eq_ab = eq_internalize(A, B); @@ -714,5 +716,26 @@ namespace array { return false; } + bool solver::add_diff_select_axioms() { + bool added = false; + + auto add_diff_select = [&](euf::enode* md, euf::enode* a) { + var_data const& d = get_var_data(find(get_th_var(a))); + for (euf::enode* select : d.m_parent_selects) { + if (assert_diff_select(md->get_app(), select->get_app())) + added = true; + } + }; + for (euf::enode* md : m_minmaxdiffs) { + euf::enode* a = md->get_arg(0); + euf::enode* b = md->get_arg(1); + add_diff_select(md, a); + add_diff_select(md, b); + } + return added; + } + + + } diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index a83bce1e9..030018088 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -118,6 +118,8 @@ namespace array { case OP_ARRAY_MINDIFF: case OP_ARRAY_MAXDIFF: push_axiom(diff_axiom(n)); + m_minmaxdiffs.push_back(n); + ctx.push(push_back_vector(m_minmaxdiffs)); break; case OP_ARRAY_DEFAULT: add_parent_default(find(n->get_arg(0)), n); diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp index f2836d9aa..eb8986098 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -101,9 +101,14 @@ namespace array { else if (!turn[idx] && add_interface_equalities()) return sat::check_result::CR_CONTINUE; } - if (m_delay_qhead < m_axiom_trail.size()) + + if (add_diff_select_axioms()) return sat::check_result::CR_CONTINUE; + if (m_delay_qhead < m_axiom_trail.size()) + return sat::check_result::CR_CONTINUE; + + // validate_check(); return sat::check_result::CR_DONE; } diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index 4ad27842b..239de0904 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -147,9 +147,9 @@ namespace array { axiom_record::eq m_eq; axiom_table_t m_axioms; svector m_axiom_trail; - unsigned m_qhead { 0 }; - unsigned m_delay_qhead { 0 }; - bool m_enable_delay { true }; + unsigned m_qhead = 0; + unsigned m_delay_qhead = 0; + bool m_enable_delay = true; struct reset_new; void push_axiom(axiom_record const& r); bool propagate_axiom(unsigned idx); @@ -166,7 +166,8 @@ namespace array { axiom_record extensionality_axiom(euf::enode* x, euf::enode* y) { return axiom_record(axiom_record::kind_t::is_extensionality, x, y); } axiom_record congruence_axiom(euf::enode* a, euf::enode* b) { return axiom_record(axiom_record::kind_t::is_congruence, a, b); } axiom_record diff_axiom(euf::enode* md) { return axiom_record(axiom_record::kind_t::is_diff, md); } - axiom_record diff_select_axiom(euf::enode* ai, euf::enode* md) { return axiom_record(axiom_record::kind_t::is_diffselect, ai, md); } + euf::enode_vector m_minmaxdiffs; + axiom_record diff_select_axiom(euf::enode* md, euf::enode* ai) { return axiom_record(axiom_record::kind_t::is_diffselect, md, ai); } scoped_ptr m_constraint; @@ -187,6 +188,7 @@ namespace array { bool assert_congruent_axiom(expr* e1, expr* e2); bool add_delayed_axioms(); bool add_as_array_eqs(euf::enode* n); + bool add_diff_select_axioms(); expr_ref apply_map(app* map, unsigned n, expr* const* args); bool is_map_combinator(expr* e) const;