From 51fa40ece5b52fef5d44ce16fad37e1e9d49bf1e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Dec 2021 10:23:37 -0800 Subject: [PATCH 001/209] fix spelling --- src/ast/rewriter/seq_rewriter.cpp | 62 +++++++++++++++---------------- src/ast/rewriter/seq_rewriter.h | 2 +- src/ast/seq_decl_plugin.cpp | 6 +-- src/ast/seq_decl_plugin.h | 8 ++-- 4 files changed, 39 insertions(+), 39 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 588979534..cb7b778ab 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -552,9 +552,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con st = mk_re_concat(args[0], args[1], result); } break; - case _OP_RE_ANTIMOROV_UNION: + case _OP_RE_ANTIMIROV_UNION: SASSERT(num_args == 2); - // Rewrite Antimorov union to real union + // Rewrite antimirov union to real union result = re().mk_union(args[0], args[1]); st = BR_REWRITE1; break; @@ -2723,7 +2723,7 @@ expr_ref seq_rewriter::is_nullable_rec(expr* r) { re().is_intersection(r, r1, r2)) { m_br.mk_and(is_nullable(r1), is_nullable(r2), result); } - else if (re().is_union(r, r1, r2) || re().is_antimorov_union(r, r1, r2)) { + else if (re().is_union(r, r1, r2) || re().is_antimirov_union(r, r1, r2)) { m_br.mk_or(is_nullable(r1), is_nullable(r2), result); } else if (re().is_diff(r, r1, r2)) { @@ -2908,7 +2908,7 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) { Once the derivative is built, we return BR_REWRITE_FULL so that any remaining possible simplification is performed from the bottom up. - Rewriting also replaces _OP_RE_ANTIMOROV_UNION, which is produced + Rewriting also replaces _OP_RE_antimirov_UNION, which is produced by is_derivative, with real union. */ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) { @@ -2924,16 +2924,16 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) { When computing derivatives recursively, we preserve the following BDD normal form: - - At the top level, the derivative is a union of Antimorov derivatives + - At the top level, the derivative is a union of antimirov derivatives (Conceptually each element of the union is a different derivative). We currently express this derivative using an internal op code: - _OP_RE_ANTIMOROV_UNION - - An Antimorov derivative is a nested if-then-else term. + _OP_RE_antimirov_UNION + - An antimirov derivative is a nested if-then-else term. if-then-elses are pushed outwards and sorted by condition ID (cond->get_id()), from largest on the outside to smallest on the inside. Duplicate nested conditions are eliminated. - The leaves of the if-then-else BDD can have unions themselves, - but these are interpreted as Regex union, not as separate Antimorov + but these are interpreted as Regex union, not as separate antimirov derivatives. To debug the normal form, call Z3 with -dbg:seq_regex: @@ -2962,7 +2962,7 @@ bool seq_rewriter::check_deriv_normal_form(expr* r, int level) { unsigned lo = 0, hi = 0; STRACE("seq_verbose", tout << " (level " << level << ")";); int new_level = 0; - if (re().is_antimorov_union(r)) { + if (re().is_antimirov_union(r)) { SASSERT(level >= 2); new_level = 2; } @@ -2975,7 +2975,7 @@ bool seq_rewriter::check_deriv_normal_form(expr* r, int level) { SASSERT(!re().is_opt(r)); SASSERT(!re().is_plus(r)); - if (re().is_antimorov_union(r, r1, r2) || + if (re().is_antimirov_union(r, r1, r2) || re().is_concat(r, r1, r2) || re().is_union(r, r1, r2) || re().is_intersection(r, r1, r2) || @@ -3410,8 +3410,8 @@ expr_ref seq_rewriter::simplify_path(expr* path) { } -expr_ref seq_rewriter::mk_der_antimorov_union(expr* r1, expr* r2) { - return mk_der_op(_OP_RE_ANTIMOROV_UNION, r1, r2); +expr_ref seq_rewriter::mk_der_antimirov_union(expr* r1, expr* r2) { + return mk_der_op(_OP_RE_ANTIMIROV_UNION, r1, r2); } expr_ref seq_rewriter::mk_der_union(expr* r1, expr* r2) { @@ -3512,7 +3512,7 @@ bool seq_rewriter::ite_bdds_compatabile(expr* a, expr* b) { OP_RE_INTERSECT OP_RE_UNION OP_RE_CONCAT - _OP_RE_ANTIMOROV_UNION + _OP_RE_antimirov_UNION - a and b are in normal form (check_deriv_normal_form) Postcondition: @@ -3542,44 +3542,44 @@ expr_ref seq_rewriter::mk_der_op_rec(decl_kind k, expr* a, expr* b) { }; // Choose when to lift a union to the top level, by converting - // it to an Antimorov union - // This implements a restricted form of Antimorov derivatives + // it to an antimirov union + // This implements a restricted form of antimirov derivatives if (k == OP_RE_UNION) { - if (re().is_antimorov_union(a) || re().is_antimorov_union(b)) { - k = _OP_RE_ANTIMOROV_UNION; + if (re().is_antimirov_union(a) || re().is_antimirov_union(b)) { + k = _OP_RE_ANTIMIROV_UNION; } #if 0 - // Disabled: eager Antimorov lifting unless BDDs are compatible + // Disabled: eager antimirov lifting unless BDDs are compatible // Note: the check for BDD compatibility could be made more - // sophisticated: in an Antimorov union of n terms, we really + // sophisticated: in an antimirov union of n terms, we really // want to check if any pair of them is compatible. else if (m().is_ite(a) && m().is_ite(b) && !ite_bdds_compatabile(a, b)) { - k = _OP_RE_ANTIMOROV_UNION; + k = _OP_RE_ANTIMIROV_UNION; } #endif } - if (k == _OP_RE_ANTIMOROV_UNION) { - result = re().mk_antimorov_union(a, b); + if (k == _OP_RE_ANTIMIROV_UNION) { + result = re().mk_antimirov_union(a, b); return result; } - if (re().is_antimorov_union(a, a1, a2)) { + if (re().is_antimirov_union(a, a1, a2)) { expr_ref r1(m()), r2(m()); r1 = mk_der_op(k, a1, b); r2 = mk_der_op(k, a2, b); - result = re().mk_antimorov_union(r1, r2); + result = re().mk_antimirov_union(r1, r2); return result; } - if (re().is_antimorov_union(b, b1, b2)) { + if (re().is_antimirov_union(b, b1, b2)) { expr_ref r1(m()), r2(m()); r1 = mk_der_op(k, a, b1); r2 = mk_der_op(k, a, b2); - result = re().mk_antimorov_union(r1, r2); + result = re().mk_antimirov_union(r1, r2); return result; } // Remaining non-union case: combine two if-then-else BDDs - // (underneath top-level Antimorov unions) + // (underneath top-level antimirov unions) if (m().is_ite(a, ca, a1, a2)) { expr_ref r1(m()), r2(m()); expr_ref notca(m().mk_not(ca), m()); @@ -3688,9 +3688,9 @@ expr_ref seq_rewriter::mk_der_compl(expr* r) { expr_ref result(m_op_cache.find(OP_RE_COMPLEMENT, r, nullptr, nullptr), m()); if (!result) { expr* c = nullptr, * r1 = nullptr, * r2 = nullptr; - if (re().is_antimorov_union(r, r1, r2)) { + if (re().is_antimirov_union(r, r1, r2)) { // Convert union to intersection - // Result: Antimorov union at top level is lost, pushed inside ITEs + // Result: antimirov union at top level is lost, pushed inside ITEs expr_ref res1(m()), res2(m()); res1 = mk_der_compl(r1); res2 = mk_der_compl(r2); @@ -3796,11 +3796,11 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { return result; } else { - // Instead of mk_der_union here, we use mk_der_antimorov_union to + // Instead of mk_der_union here, we use mk_der_antimirov_union to // force the two cases to be considered separately and lifted to // the top level. This avoids blowup in cases where determinization // is expensive. - return mk_der_antimorov_union(result, mk_der_concat(is_n, dr2)); + return mk_der_antimirov_union(result, mk_der_concat(is_n, dr2)); } } else if (re().is_star(r, r1)) { diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 20978c279..5cba15fc8 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -200,7 +200,7 @@ class seq_rewriter { expr_ref mk_der_inter(expr* a, expr* b); expr_ref mk_der_compl(expr* a); expr_ref mk_der_cond(expr* cond, expr* ele, sort* seq_sort); - expr_ref mk_der_antimorov_union(expr* r1, expr* r2); + expr_ref mk_der_antimirov_union(expr* r1, expr* r2); bool ite_bdds_compatabile(expr* a, expr* b); /* if r has the form deriv(en..deriv(e1,to_re(s))..) returns 's = [e1..en]' else returns '() in r'*/ expr_ref is_nullable_symbolic_regex(expr* r, sort* seq_sort); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 0829aa09f..8be046fd9 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -243,7 +243,7 @@ void seq_decl_plugin::init() { m_sigs[OP_RE_OF_PRED] = alloc(psig, m, "re.of.pred", 1, 1, &predA, reA); m_sigs[OP_RE_REVERSE] = alloc(psig, m, "re.reverse", 1, 1, &reA, reA); m_sigs[OP_RE_DERIVATIVE] = alloc(psig, m, "re.derivative", 1, 2, AreA, reA); - m_sigs[_OP_RE_ANTIMOROV_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, reA); + m_sigs[_OP_RE_ANTIMIROV_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, reA); m_sigs[OP_SEQ_TO_RE] = alloc(psig, m, "seq.to.re", 1, 1, &seqA, reA); m_sigs[OP_SEQ_IN_RE] = alloc(psig, m, "seq.in.re", 1, 2, seqAreA, boolT); m_sigs[OP_SEQ_REPLACE_RE_ALL] = alloc(psig, m, "str.replace_re_all", 1, 3, seqAreAseqA, seqA); @@ -414,7 +414,7 @@ func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p case OP_RE_COMPLEMENT: case OP_RE_REVERSE: case OP_RE_DERIVATIVE: - case _OP_RE_ANTIMOROV_UNION: + case _OP_RE_ANTIMIROV_UNION: m_has_re = true; // fall-through case OP_SEQ_UNIT: @@ -1283,7 +1283,7 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const { print(out, r1); print(out, r2); } - else if (re.is_antimorov_union(e, r1, r2) || re.is_union(e, r1, r2)) { + else if (re.is_antimirov_union(e, r1, r2) || re.is_union(e, r1, r2)) { out << "("; print(out, r1); out << (html_encode ? "⋃" : "|"); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 09a10ee9a..1db05b722 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -103,7 +103,7 @@ enum seq_op_kind { _OP_REGEXP_EMPTY, _OP_REGEXP_FULL_CHAR, _OP_RE_IS_NULLABLE, - _OP_RE_ANTIMOROV_UNION, // Lifted union for antimorov-style derivatives + _OP_RE_ANTIMIROV_UNION, // Lifted union for antimirov-style derivatives _OP_SEQ_SKOLEM, LAST_SEQ_OP }; @@ -525,7 +525,7 @@ public: app* mk_of_pred(expr* p); app* mk_reverse(expr* r) { return m.mk_app(m_fid, OP_RE_REVERSE, r); } app* mk_derivative(expr* ele, expr* r) { return m.mk_app(m_fid, OP_RE_DERIVATIVE, ele, r); } - app* mk_antimorov_union(expr* r1, expr* r2) { return m.mk_app(m_fid, _OP_RE_ANTIMOROV_UNION, r1, r2); } + app* mk_antimirov_union(expr* r1, expr* r2) { return m.mk_app(m_fid, _OP_RE_ANTIMIROV_UNION, r1, r2); } bool is_to_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); } bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_RE_CONCAT); } @@ -557,7 +557,7 @@ public: bool is_of_pred(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OF_PRED); } bool is_reverse(expr const* n) const { return is_app_of(n, m_fid, OP_RE_REVERSE); } bool is_derivative(expr const* n) const { return is_app_of(n, m_fid, OP_RE_DERIVATIVE); } - bool is_antimorov_union(expr const* n) const { return is_app_of(n, m_fid, _OP_RE_ANTIMOROV_UNION); } + bool is_antimirov_union(expr const* n) const { return is_app_of(n, m_fid, _OP_RE_ANTIMIROV_UNION); } MATCH_UNARY(is_to_re); MATCH_BINARY(is_concat); MATCH_BINARY(is_union); @@ -571,7 +571,7 @@ public: MATCH_UNARY(is_of_pred); MATCH_UNARY(is_reverse); MATCH_BINARY(is_derivative); - MATCH_BINARY(is_antimorov_union); + MATCH_BINARY(is_antimirov_union); bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) const; bool is_loop(expr const* n, expr*& body, unsigned& lo) const; bool is_loop(expr const* n, expr*& body, expr*& lo, expr*& hi) const; From 0405a597d4b7c3997fa0aa2e670c808710093974 Mon Sep 17 00:00:00 2001 From: Calvin Loncaric Date: Thu, 9 Dec 2021 14:39:38 -0800 Subject: [PATCH 002/209] Fix return type of as_int64 (#5703) --- src/api/c++/z3++.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 95c09e47a..6af9beae7 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -834,7 +834,7 @@ namespace z3 { double as_double() const { double d = 0; is_numeral(d); return d; } uint64_t as_uint64() const { uint64_t r = 0; is_numeral_u64(r); return r; } - uint64_t as_int64() const { int64_t r = 0; is_numeral_i64(r); return r; } + int64_t as_int64() const { int64_t r = 0; is_numeral_i64(r); return r; } /** From 96e871c826fe7708ca8cd0061d38599bdcbe5bed Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Dec 2021 12:31:15 -0800 Subject: [PATCH 003/209] add stub for testing updates to scoped_timer Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 3 ++- src/test/CMakeLists.txt | 1 + src/test/main.cpp | 1 + src/test/scoped_timer.cpp | 9 +++++++++ 4 files changed, 13 insertions(+), 1 deletion(-) create mode 100644 src/test/scoped_timer.cpp diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 8be046fd9..1e87e1402 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -416,7 +416,7 @@ func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p case OP_RE_DERIVATIVE: case _OP_RE_ANTIMIROV_UNION: m_has_re = true; - // fall-through + Z3_fallthrough; case OP_SEQ_UNIT: case OP_STRING_ITOS: case OP_STRING_STOI: @@ -516,6 +516,7 @@ func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p case OP_SEQ_REPLACE_RE_ALL: case OP_SEQ_REPLACE_RE: m_has_re = true; + Z3_fallthrough; case OP_SEQ_REPLACE_ALL: return mk_str_fun(k, arity, domain, range, k); diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index eb0e94173..500cb4258 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -101,6 +101,7 @@ add_executable(test-z3 sat_local_search.cpp sat_lookahead.cpp sat_user_scope.cpp + scoped_timer.cpp simple_parser.cpp simplex.cpp simplifier.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index 3e3f1d575..6272c2dee 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -259,6 +259,7 @@ int main(int argc, char ** argv) { TST(bdd); TST(pdd); TST(pdd_solver); + TST(scoped_timer); TST(solver_pool); //TST_ARGV(hs); TST(finder); diff --git a/src/test/scoped_timer.cpp b/src/test/scoped_timer.cpp new file mode 100644 index 000000000..c21e39cbe --- /dev/null +++ b/src/test/scoped_timer.cpp @@ -0,0 +1,9 @@ +// test driver for scoped timer. +// fixes are required to be fuzzed +// with single and multi-threaded mode and short timeouts. + +#include "util/scoped_timer.h" + +void tst_scoped_timer() { + +} From 0a7e003709ec46ddb8793f660c5f5bb6a1928d09 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Dec 2021 17:51:05 -0800 Subject: [PATCH 004/209] this one is for you Nuno - pull request might have new bugs given that build is broken. - this test doesn't expose race conditions under simple tests, yet. It is a starting point. - run under cuzz (app-verifier) should expose races, this is what it was made for. --- src/test/scoped_timer.cpp | 42 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/src/test/scoped_timer.cpp b/src/test/scoped_timer.cpp index c21e39cbe..d65034135 100644 --- a/src/test/scoped_timer.cpp +++ b/src/test/scoped_timer.cpp @@ -1,9 +1,51 @@ // test driver for scoped timer. // fixes are required to be fuzzed // with single and multi-threaded mode and short timeouts. +// run it with app-verifier (becuzz yes ...) #include "util/scoped_timer.h" +#include "util/util.h" +#include "util/vector.h" +#include "util/trace.h" +#include + +class test_scoped_eh : public event_handler { + std::atomic m_called = false; +public: + void operator()(event_handler_caller_t id) override { + m_caller_id = id; + m_called = true; + } + bool called() const { return m_called; } +}; + +static void worker_thread(unsigned tid) { + for (unsigned i = 0; i < 100; ++i) { + test_scoped_eh eh; + scoped_timer sc(1, &eh); + unsigned_vector v; + for (unsigned j = 0; j < (2 << 25); ++j) { + v.push_back(j); + if (eh.called()) { + // IF_VERBOSE(0, verbose_stream() << tid << " " << i << " " << j << "\n"); + break; + } + } + } +} void tst_scoped_timer() { + + std::cout << "sequential test\n"; + worker_thread(0); + + std::cout << "thread test\n"; + unsigned num_threads = 3; + vector threads(num_threads); + for (unsigned i = 0; i < num_threads; ++i) + threads[i] = std::thread([&, i]() { worker_thread(i); }); + + for (auto& th : threads) + th.join(); } From b85f2f7e865828ba2f52efd37c1b399bcc2208ab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Dec 2021 21:10:07 -0800 Subject: [PATCH 005/209] #5704 --- src/api/python/z3/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 8e6a86cf1..ae29a0b01 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -4809,7 +4809,7 @@ def Ext(a, b): """ ctx = a.ctx if z3_debug(): - _z3_assert(is_array_sort(a) and is_array(b), "arguments must be arrays") + _z3_assert(is_array_sort(a) and (is_array(b) or b.is_lambda()), "arguments must be arrays") return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx) From fcdf8d49485c63e8c8ecda3d0a488f92c62055da Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Dec 2021 11:40:45 -0800 Subject: [PATCH 006/209] include atomic Signed-off-by: Nikolaj Bjorner --- src/test/scoped_timer.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/test/scoped_timer.cpp b/src/test/scoped_timer.cpp index d65034135..ff9d52b06 100644 --- a/src/test/scoped_timer.cpp +++ b/src/test/scoped_timer.cpp @@ -8,6 +8,7 @@ #include "util/vector.h" #include "util/trace.h" #include +#include class test_scoped_eh : public event_handler { std::atomic m_called = false; From 9ec0f94ab9b1ecb6e5cf95b0bc0e010bc28b86f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Dec 2021 14:25:05 -0800 Subject: [PATCH 007/209] hoisting out blocker for empty #5693 --- src/smt/seq_regex.cpp | 49 +++++++++++++++++++++++++++---------------- src/smt/seq_regex.h | 2 ++ 2 files changed, 33 insertions(+), 18 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index aa1faa131..3fedd68e8 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -235,6 +235,31 @@ namespace smt { } + bool seq_regex::block_if_empty(expr* r, literal lit) { + auto info = re().get_info(r); + + //if the minlength of the regex is UINT_MAX then the regex is a deadend + if (re().is_empty(r) || info.min_length == UINT_MAX) { + STRACE("seq_regex_brief", tout << "(empty) ";); + th.add_axiom(~lit); + return true; + } + + if (info.interpreted) { + std::cout << "recur: " << r->get_id() << "\n"; + std::cout << mk_pp(r, m) << "\n"; + update_state_graph(r); + + if (m_state_graph.is_dead(get_state_id(r))) { + STRACE("seq_regex_brief", tout << "(dead) ";); + th.add_axiom(~lit); + return true; + } + } + return false; + } + + /** * Propagate the atom (accept s i r) * @@ -271,24 +296,8 @@ namespace smt { << "PA(" << mk_pp(s, m) << "@" << idx << "," << state_str(r) << ") ";); - auto info = re().get_info(r); - - //if the minlength of the regex is UINT_MAX then the regex is a deadend - if (re().is_empty(r) || info.min_length == UINT_MAX) { - STRACE("seq_regex_brief", tout << "(empty) ";); - th.add_axiom(~lit); + if (block_if_empty(r, lit)) return; - } - - if (info.interpreted) { - update_state_graph(r); - - if (m_state_graph.is_dead(get_state_id(r))) { - STRACE("seq_regex_brief", tout << "(dead) ";); - th.add_axiom(~lit); - return; - } - } if (block_unfolding(lit, idx)) { STRACE("seq_regex_brief", tout << "(blocked) ";); @@ -544,6 +553,10 @@ namespace smt { expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr, *n = nullptr; VERIFY(sk().is_is_non_empty(e, r, u, n)); + if (block_if_empty(r, lit)) + return; + + TRACE("seq_regex", tout << "propagate nonempty: " << mk_pp(e, m) << std::endl;); STRACE("seq_regex_brief", tout << std::endl << "PNE(" << expr_id_str(e) << "," << state_str(r) @@ -553,6 +566,7 @@ namespace smt { if (m.is_true(is_nullable)) return; + literal null_lit = th.mk_literal(is_nullable); expr_ref hd = mk_first(r, n); expr_ref d(m); @@ -845,7 +859,6 @@ namespace smt { return m_state_to_expr.get(id - 1); } - bool seq_regex::can_be_in_cycle(expr *r1, expr *r2) { // TBD: This can be used to optimize the state graph: // return false here if it is known that r1 -> r2 can never be diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index dcf81dbc3..01dd6e4a2 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -184,6 +184,8 @@ namespace smt { } } + bool block_if_empty(expr* r, literal lit); + public: seq_regex(theory_seq& th); From b2af7ea68fced2ced3bd9f23fbcbe7160f920cae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Dec 2021 15:19:29 -0800 Subject: [PATCH 008/209] stdout Signed-off-by: Nikolaj Bjorner --- src/smt/seq_regex.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 3fedd68e8..a6ce1884d 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -246,8 +246,6 @@ namespace smt { } if (info.interpreted) { - std::cout << "recur: " << r->get_id() << "\n"; - std::cout << mk_pp(r, m) << "\n"; update_state_graph(r); if (m_state_graph.is_dead(get_state_id(r))) { From f40becf0999b6a61d8f41edc4548bcc4c61ac20d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Dec 2021 18:17:40 -0800 Subject: [PATCH 009/209] remove case for non-emptiness to combine with standard membership as part of revising engine for addressing #5693 --- src/ast/rewriter/seq_skolem.cpp | 1 - src/ast/rewriter/seq_skolem.h | 7 +--- src/smt/seq_regex.cpp | 70 +++------------------------------ src/smt/seq_regex.h | 4 +- src/smt/theory_seq.cpp | 4 -- 5 files changed, 8 insertions(+), 78 deletions(-) diff --git a/src/ast/rewriter/seq_skolem.cpp b/src/ast/rewriter/seq_skolem.cpp index c2e948216..ff67ff0bd 100644 --- a/src/ast/rewriter/seq_skolem.cpp +++ b/src/ast/rewriter/seq_skolem.cpp @@ -38,7 +38,6 @@ skolem::skolem(ast_manager& m, th_rewriter& rw): m_max_unfolding = "seq.max_unfolding"; m_length_limit = "seq.length_limit"; m_is_empty = "re.is_empty"; - m_is_non_empty = "re.is_non_empty"; } expr_ref skolem::mk(symbol const& s, expr* e1, expr* e2, expr* e3, expr* e4, sort* range, bool rw) { diff --git a/src/ast/rewriter/seq_skolem.h b/src/ast/rewriter/seq_skolem.h index 913942b8a..799b5ca07 100644 --- a/src/ast/rewriter/seq_skolem.h +++ b/src/ast/rewriter/seq_skolem.h @@ -36,7 +36,7 @@ namespace seq { symbol m_indexof_left, m_indexof_right; // inverse of indexof: (indexof_left s t) + s + (indexof_right s t) = t, for s in t. symbol m_aut_step; // regex unfolding state symbol m_accept; // regex - symbol m_is_empty, m_is_non_empty; // regex emptiness check + symbol m_is_empty; // regex emptiness check symbol m_pre, m_post; // inverse of at: (pre s i) + (at s i) + (post s i) = s if 0 <= i < (len s) symbol m_postp; symbol m_eq; // equality atom @@ -73,7 +73,6 @@ namespace seq { } expr_ref mk_accept(expr_ref_vector const& args) { return expr_ref(seq.mk_skolem(m_accept, args.size(), args.data(), m.mk_bool_sort()), m); } expr_ref mk_accept(expr* s, expr* i, expr* r) { return mk(m_accept, s, i, r, nullptr, m.mk_bool_sort()); } - expr_ref mk_is_non_empty(expr* r, expr* u, expr* n) { return mk(m_is_non_empty, r, u, n, m.mk_bool_sort(), false); } expr_ref mk_is_empty(expr* r, expr* u, expr* n) { return mk(m_is_empty, r, u, n, m.mk_bool_sort(), false); } expr_ref mk_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_left, t, s, offset); } @@ -153,13 +152,9 @@ namespace seq { bool is_length_limit(expr* e) const { return is_skolem(m_length_limit, e); } bool is_length_limit(expr* p, unsigned& lim, expr*& s) const; bool is_is_empty(expr* e) const { return is_skolem(m_is_empty, e); } - bool is_is_non_empty(expr* e) const { return is_skolem(m_is_non_empty, e); } bool is_is_empty(expr* e, expr*& r, expr*& u, expr*& n) const { return is_skolem(m_is_empty, e) && (r = to_app(e)->get_arg(0), u = to_app(e)->get_arg(1), n = to_app(e)->get_arg(2), true); } - bool is_is_non_empty(expr* e, expr*& r, expr*& u, expr*& n) const { - return is_skolem(m_is_non_empty, e) && (r = to_app(e)->get_arg(0), u = to_app(e)->get_arg(1), n = to_app(e)->get_arg(2), true); - } void decompose(expr* e, expr_ref& head, expr_ref& tail); diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index a6ce1884d..79bddf83e 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -246,8 +246,7 @@ namespace smt { } if (info.interpreted) { - update_state_graph(r); - + update_state_graph(r); if (m_state_graph.is_dead(get_state_id(r))) { STRACE("seq_regex_brief", tout << "(dead) ";); th.add_axiom(~lit); @@ -519,15 +518,12 @@ namespace smt { void seq_regex::propagate_ne(expr* r1, expr* r2) { TRACE("seq_regex", tout << "propagate NEQ: " << mk_pp(r1, m) << ", " << mk_pp(r2, m) << std::endl;); STRACE("seq_regex_brief", tout << "PNEQ ";); - // TBD: rewrite to use state_graph - // why is is_non_empty even needed, why not just not(in_empty) sort* seq_sort = nullptr; VERIFY(u().is_re(r1, seq_sort)); expr_ref r = symmetric_diff(r1, r2); - expr_ref emp(re().mk_empty(r->get_sort()), m); - expr_ref n(m.mk_fresh_const("re.char", seq_sort), m); - expr_ref is_non_empty = sk().mk_is_non_empty(r, r, n); - th.add_axiom(th.mk_eq(r1, r2, false), th.mk_literal(is_non_empty)); + expr_ref s(m.mk_fresh_const("re.member", seq_sort), m); + expr_ref is_member(re().mk_in_re(s, r), m); + th.add_axiom(th.mk_eq(r1, r2, false), th.mk_literal(is_member)); } bool seq_regex::is_member(expr* r, expr* u) { @@ -537,62 +533,7 @@ namespace smt { return true; } return r == u; - } - - /** - * is_non_empty(r, u) => nullable or \/_i (c_i and is_non_empty(r_i, u union r)) - * - * for each (c_i, r_i) in cofactors (min-terms) - * - * is_non_empty(r_i, u union r) := false if r_i in u - * - */ - void seq_regex::propagate_is_non_empty(literal lit) { - expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr, *n = nullptr; - VERIFY(sk().is_is_non_empty(e, r, u, n)); - - if (block_if_empty(r, lit)) - return; - - - TRACE("seq_regex", tout << "propagate nonempty: " << mk_pp(e, m) << std::endl;); - STRACE("seq_regex_brief", tout - << std::endl << "PNE(" << expr_id_str(e) << "," << state_str(r) - << "," << expr_id_str(u) << "," << expr_id_str(n) << ") ";); - - expr_ref is_nullable = is_nullable_wrapper(r); - if (m.is_true(is_nullable)) - return; - - - literal null_lit = th.mk_literal(is_nullable); - expr_ref hd = mk_first(r, n); - expr_ref d(m); - d = mk_derivative_wrapper(hd, r); - - literal_vector lits; - lits.push_back(~lit); - if (null_lit != false_literal) - lits.push_back(null_lit); - - expr_ref_pair_vector cofactors(m); - get_cofactors(d, cofactors); - for (auto const& p : cofactors) { - if (is_member(p.second, u)) - continue; - expr_ref cond(p.first, m); - seq_rw().elim_condition(hd, cond); - rewrite(cond); - if (m.is_false(cond)) - continue; - expr_ref next_non_empty = sk().mk_is_non_empty(p.second, re().mk_union(u, p.second), n); - if (!m.is_true(cond)) - next_non_empty = m.mk_and(cond, next_non_empty); - lits.push_back(th.mk_literal(next_non_empty)); - } - - th.add_axiom(lits); - } + } /* Given a string s, index i, and a derivative r, return an @@ -915,6 +856,7 @@ namespace smt { } m_state_graph.mark_done(r_id); } + STRACE("seq_regex", m_state_graph.display(tout);); STRACE("seq_regex_brief", tout << std::endl;); STRACE("seq_regex_brief", m_state_graph.display(tout);); diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index 01dd6e4a2..8b6a39782 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -203,9 +203,7 @@ namespace smt { void propagate_eq(expr* r1, expr* r2); - void propagate_ne(expr* r1, expr* r2); - - void propagate_is_non_empty(literal lit); + void propagate_ne(expr* r1, expr* r2); void propagate_is_empty(literal lit); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index fe0d116ef..842798bab 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3014,10 +3014,6 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { if (is_true) m_regex.propagate_is_empty(lit); } - else if (m_sk.is_is_non_empty(e)) { - if (is_true) - m_regex.propagate_is_non_empty(lit); - } else if (m_sk.is_eq(e, e1, e2)) { if (is_true) { propagate_eq(lit, e1, e2, true); From 5348af3c4c1828c682071cc54e388a43a8360189 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Dec 2021 10:01:53 -0800 Subject: [PATCH 010/209] fix co-factoring Signed-off-by: Nikolaj Bjorner --- src/smt/seq_regex.cpp | 120 ++++++++++++++++++++++++++++++++---------- src/smt/seq_regex.h | 4 +- 2 files changed, 95 insertions(+), 29 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 79bddf83e..8ac66ec97 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -19,6 +19,9 @@ Author: #include "smt/seq_regex.h" #include "smt/theory_seq.h" #include "ast/expr_abstract.h" +#include "ast/ast_util.h" +#include "ast/for_each_expr.h" +#include namespace smt { @@ -533,7 +536,62 @@ namespace smt { return true; } return r == u; - } + } + + /** + * is_non_empty(r, u) => nullable or \/_i (c_i and is_non_empty(r_i, u union r)) + * + * for each (c_i, r_i) in cofactors (min-terms) + * + * is_non_empty(r_i, u union r) := false if r_i in u + * + */ + void seq_regex::propagate_is_non_empty(literal lit) { + expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr, *n = nullptr; + VERIFY(sk().is_is_non_empty(e, r, u, n)); + + if (block_if_empty(r, lit)) + return; + + + TRACE("seq_regex", tout << "propagate nonempty: " << mk_pp(e, m) << std::endl;); + STRACE("seq_regex_brief", tout + << std::endl << "PNE(" << expr_id_str(e) << "," << state_str(r) + << "," << expr_id_str(u) << "," << expr_id_str(n) << ") ";); + + expr_ref is_nullable = is_nullable_wrapper(r); + if (m.is_true(is_nullable)) + return; + + + literal null_lit = th.mk_literal(is_nullable); + expr_ref hd = mk_first(r, n); + expr_ref d(m); + d = mk_derivative_wrapper(hd, r); + + literal_vector lits; + lits.push_back(~lit); + if (null_lit != false_literal) + lits.push_back(null_lit); + + expr_ref_pair_vector cofactors(m); + get_cofactors(d, cofactors); + for (auto const& p : cofactors) { + if (is_member(p.second, u)) + continue; + expr_ref cond(p.first, m); + seq_rw().elim_condition(hd, cond); + rewrite(cond); + if (m.is_false(cond)) + continue; + expr_ref next_non_empty = sk().mk_is_non_empty(p.second, re().mk_union(u, p.second), n); + if (!m.is_true(cond)) + next_non_empty = m.mk_and(cond, next_non_empty); + lits.push_back(th.mk_literal(next_non_empty)); + } + + th.add_axiom(lits); + } /* Given a string s, index i, and a derivative r, return an @@ -681,39 +739,47 @@ namespace smt { Return a list of all (cond, leaf) pairs in a given derivative expression r. - Note: this recursive implementation is inefficient, since if nodes - are repeated often in the expression DAG, they may be visited - many times. For this reason, prefer mk_deriv_accept and - get_all_derivatives when possible. + Note: this implementation is inefficient: it simply collects all expressions under an if and + iterates over all combinations. This method is still used by: propagate_is_empty propagate_is_non_empty */ void seq_regex::get_cofactors(expr* r, expr_ref_pair_vector& result) { - expr_ref_vector conds(m); - get_cofactors_rec(r, conds, result); - STRACE("seq_regex", tout << "Number of derivatives: " - << result.size() << std::endl;); - STRACE("seq_regex_brief", tout << "#derivs=" << result.size() << " ";); - } - void seq_regex::get_cofactors_rec(expr* r, expr_ref_vector& conds, - expr_ref_pair_vector& result) { - expr* cond = nullptr, *r1 = nullptr, *r2 = nullptr; - if (m.is_ite(r, cond, r1, r2)) { - conds.push_back(cond); - get_cofactors_rec(r1, conds, result); - conds.pop_back(); - conds.push_back(mk_not(m, cond)); - get_cofactors_rec(r2, conds, result); - conds.pop_back(); + obj_hashtable ifs; + expr* cond = nullptr, * r1 = nullptr, * r2 = nullptr; + for (expr* e : subterms::ground(expr_ref(r, m))) + if (m.is_ite(e, cond, r1, r2)) + ifs.insert(cond); + + expr_ref_vector rs(m); + vector conds; + conds.push_back(expr_ref_vector(m)); + rs.push_back(r); + for (expr* c : ifs) { + unsigned sz = conds.size(); + expr_safe_replace rep1(m); + expr_safe_replace rep2(m); + rep1.insert(c, m.mk_true()); + rep2.insert(c, m.mk_false()); + expr_ref r2(m); + for (unsigned i = 0; i < sz; ++i) { + expr_ref_vector cs = conds[i]; + cs.push_back(mk_not(m, c)); + conds.push_back(cs); + conds[i].push_back(c); + expr_ref r1(rs.get(i), m); + rep1(r1, r2); + rs[i] = r2; + rep2(r1, r2); + rs.push_back(r2); + } } - else if (re().is_union(r, r1, r2)) { - get_cofactors_rec(r1, conds, result); - get_cofactors_rec(r2, conds, result); - } - else { - expr_ref conj = mk_and(conds); + for (unsigned i = 0; i < conds.size(); ++i) { + expr_ref conj = mk_and(conds[i]); + expr_ref r(rs.get(i), m); + ctx.get_rewriter()(r); if (!m.is_false(conj) && !re().is_empty(r)) result.push_back(conj, r); } diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index 8b6a39782..201369d2c 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -165,8 +165,6 @@ namespace smt { expr_ref mk_deriv_accept(expr* s, unsigned i, expr* r); void get_derivative_targets(expr* r, expr_ref_vector& targets); void get_cofactors(expr* r, expr_ref_pair_vector& result); - void get_cofactors_rec(expr* r, expr_ref_vector& conds, - expr_ref_pair_vector& result); /* Pretty print the regex of the state id to the out stream, @@ -186,6 +184,8 @@ namespace smt { bool block_if_empty(expr* r, literal lit); + void propagate_is_non_empty(literal lit); + public: seq_regex(theory_seq& th); From b1d167de5bd0aea754ecf881ad8cb85329d03e6c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Dec 2021 10:12:38 -0800 Subject: [PATCH 011/209] fix co-factoring' Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_skolem.cpp | 1 + src/ast/rewriter/seq_skolem.h | 6 ++++++ src/smt/seq_regex.cpp | 7 ++++--- src/smt/seq_regex.h | 4 ++-- src/smt/theory_seq.cpp | 4 ++++ 5 files changed, 17 insertions(+), 5 deletions(-) diff --git a/src/ast/rewriter/seq_skolem.cpp b/src/ast/rewriter/seq_skolem.cpp index ff67ff0bd..c2e948216 100644 --- a/src/ast/rewriter/seq_skolem.cpp +++ b/src/ast/rewriter/seq_skolem.cpp @@ -38,6 +38,7 @@ skolem::skolem(ast_manager& m, th_rewriter& rw): m_max_unfolding = "seq.max_unfolding"; m_length_limit = "seq.length_limit"; m_is_empty = "re.is_empty"; + m_is_non_empty = "re.is_non_empty"; } expr_ref skolem::mk(symbol const& s, expr* e1, expr* e2, expr* e3, expr* e4, sort* range, bool rw) { diff --git a/src/ast/rewriter/seq_skolem.h b/src/ast/rewriter/seq_skolem.h index 799b5ca07..088a00eeb 100644 --- a/src/ast/rewriter/seq_skolem.h +++ b/src/ast/rewriter/seq_skolem.h @@ -37,6 +37,7 @@ namespace seq { symbol m_aut_step; // regex unfolding state symbol m_accept; // regex symbol m_is_empty; // regex emptiness check + symbol m_is_non_empty; symbol m_pre, m_post; // inverse of at: (pre s i) + (at s i) + (post s i) = s if 0 <= i < (len s) symbol m_postp; symbol m_eq; // equality atom @@ -74,6 +75,7 @@ namespace seq { expr_ref mk_accept(expr_ref_vector const& args) { return expr_ref(seq.mk_skolem(m_accept, args.size(), args.data(), m.mk_bool_sort()), m); } expr_ref mk_accept(expr* s, expr* i, expr* r) { return mk(m_accept, s, i, r, nullptr, m.mk_bool_sort()); } expr_ref mk_is_empty(expr* r, expr* u, expr* n) { return mk(m_is_empty, r, u, n, m.mk_bool_sort(), false); } + expr_ref mk_is_non_empty(expr* r, expr* u, expr* n) { return mk(m_is_non_empty, r, u, n, m.mk_bool_sort(), false); } expr_ref mk_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_left, t, s, offset); } expr_ref mk_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_right, t, s, offset); } @@ -155,6 +157,10 @@ namespace seq { bool is_is_empty(expr* e, expr*& r, expr*& u, expr*& n) const { return is_skolem(m_is_empty, e) && (r = to_app(e)->get_arg(0), u = to_app(e)->get_arg(1), n = to_app(e)->get_arg(2), true); } + bool is_is_non_empty(expr* e) const { return is_skolem(m_is_non_empty, e); } + bool is_is_non_empty(expr* e, expr*& r, expr*& u, expr*& n) const { + return is_skolem(m_is_non_empty, e) && (r = to_app(e)->get_arg(0), u = to_app(e)->get_arg(1), n = to_app(e)->get_arg(2), true); + } void decompose(expr* e, expr_ref& head, expr_ref& tail); diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 8ac66ec97..fe716c20d 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -524,9 +524,10 @@ namespace smt { sort* seq_sort = nullptr; VERIFY(u().is_re(r1, seq_sort)); expr_ref r = symmetric_diff(r1, r2); - expr_ref s(m.mk_fresh_const("re.member", seq_sort), m); - expr_ref is_member(re().mk_in_re(s, r), m); - th.add_axiom(th.mk_eq(r1, r2, false), th.mk_literal(is_member)); + expr_ref emp(re().mk_empty(r->get_sort()), m); + expr_ref n(m.mk_fresh_const("re.char", seq_sort), m); + expr_ref is_non_empty = sk().mk_is_non_empty(r, r, n); + th.add_axiom(th.mk_eq(r1, r2, false), th.mk_literal(is_non_empty)); } bool seq_regex::is_member(expr* r, expr* u) { diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index 201369d2c..5c3fddd25 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -184,8 +184,6 @@ namespace smt { bool block_if_empty(expr* r, literal lit); - void propagate_is_non_empty(literal lit); - public: seq_regex(theory_seq& th); @@ -206,6 +204,8 @@ namespace smt { void propagate_ne(expr* r1, expr* r2); void propagate_is_empty(literal lit); + + void propagate_is_non_empty(literal lit); }; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 842798bab..369adccc1 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3033,6 +3033,10 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { propagate_length_limit(e); } } + else if (m_sk.is_is_non_empty(e)) { + if (is_true) + m_regex.propagate_is_non_empty(lit); + } else if (m_util.str.is_lt(e) || m_util.str.is_le(e)) { m_lts.push_back(e); } From 03b5380a204179b479799c28f648abc4c3c707e2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Dec 2021 13:39:52 -0800 Subject: [PATCH 012/209] na --- src/ast/rewriter/var_subst.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ast/rewriter/var_subst.h b/src/ast/rewriter/var_subst.h index 84318c9b5..e9d39740d 100644 --- a/src/ast/rewriter/var_subst.h +++ b/src/ast/rewriter/var_subst.h @@ -48,6 +48,7 @@ public: Otherwise, (VAR 0) is stored in the first position, (VAR 1) in the second, and so on. */ expr_ref operator()(expr * n, unsigned num_args, expr * const * args); + inline expr_ref operator()(expr* n, expr* arg) { return (*this)(n, 1, &arg); } inline expr_ref operator()(expr * n, expr_ref_vector const& args) { return (*this)(n, args.size(), args.data()); } inline expr_ref operator()(expr * n, var_ref_vector const& args) { return (*this)(n, args.size(), (expr*const*)args.data()); } inline expr_ref operator()(expr * n, app_ref_vector const& args) { return (*this)(n, args.size(), (expr*const*)args.data()); } From 3b58f548f73f56830e75ea5ed8586b30893201f2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Dec 2021 13:42:52 -0800 Subject: [PATCH 013/209] remove dead code --- src/smt/seq_regex.cpp | 67 ++----------------------------------------- 1 file changed, 2 insertions(+), 65 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index fe716c20d..55c3d7edd 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -147,38 +147,6 @@ namespace smt { } } - /* - //if r is uninterpreted then taking a derivative may diverge try to obtain the - //value from equations providing r a definition - if (is_uninterp(r)) { - if (m_const_to_expr.contains(r)) { - proof* _not_used = nullptr; - m_const_to_expr.get(r, r, _not_used); - if (is_uninterp(r)) { - if (m_const_to_expr.contains(r)) { - m_const_to_expr.get(r, r, _not_used); - } - } - } - else { - //add the literal back - expr_ref r_alias(m.mk_fresh_const(symbol(r->get_id()), r->get_sort(), false), m); - expr_ref s_in_r_alias(re().mk_in_re(s, r_alias), m); - literal s_in_r_alias_lit = th.mk_literal(s_in_r_alias); - m_const_to_expr.insert(r_alias, r, nullptr); - th.add_axiom(s_in_r_alias_lit); - return; - } - } - */ - - /* - if (is_uninterp(r)) { - th.add_unhandled_expr(e); - return; - } - */ - expr_ref zero(a().mk_int(0), m); expr_ref acc(sk().mk_accept(s, zero, r), m); literal acc_lit = th.mk_literal(acc); @@ -468,13 +436,10 @@ namespace smt { STRACE("seq_regex", tout << "derivative(" << mk_pp(ele, m) << "): " << mk_pp(r, m) << std::endl;); // Uses canonical variable (:var 0) for the derivative element - expr_ref der(seq_rw().mk_derivative(r), m); - // Substitute (:var 0) with the actual element + expr_ref der = seq_rw().mk_derivative(r); var_subst subst(m); - expr_ref_vector sub(m); - sub.push_back(ele); - der = subst(der, sub); + der = subst(der, ele); STRACE("seq_regex", tout << "derivative result: " << mk_pp(der, m) << std::endl;); STRACE("seq_regex_brief", tout << "d(" << state_str(r) << ")=" @@ -489,17 +454,6 @@ namespace smt { TRACE("seq_regex", tout << "propagate EQ: " << mk_pp(r1, m) << ", " << mk_pp(r2, m) << std::endl;); STRACE("seq_regex_brief", tout << "PEQ ";); - /* - if (is_uninterp(r1) || is_uninterp(r2)) { - th.add_axiom(th.mk_eq(r1, r2, false)); - if (is_uninterp(r1)) - m_const_to_expr.insert(r1, r2, nullptr); - else - m_const_to_expr.insert(r2, r1, nullptr); - - } - */ - sort* seq_sort = nullptr; VERIFY(u().is_re(r1, seq_sort)); expr_ref r = symmetric_diff(r1, r2); @@ -653,23 +607,6 @@ namespace smt { // s[i..] in .* <==> true, also: s[i..] in .+ <==> true when |s|>i re_to_accept.find(e) = m.mk_true(); } - /* - else if (re().is_epsilon(e)) - { - expr* one = a().mk_int(1); - _temp_bool_owner.push_back(one); - //the substring starting after position i must be empty - expr* s_end = str().mk_substr(s, i_int, one); - expr* s_end_is_epsilon = m.mk_eq(s_end, str().mk_empty(m.get_sort(s))); - - _temp_bool_owner.push_back(s_end_is_epsilon); - re_to_accept.find(e) = s_end_is_epsilon; - - STRACE("seq_regex_verbose", tout - << "added empty sequence leaf: " - << mk_pp(s_end_is_epsilon, m) << std::endl;); - } - */ else if (re().is_union(e, e1, e2)) { expr* b1 = re_to_accept.find(e1); expr* b2 = re_to_accept.find(e2); From 2be93870c86761dd5bd3df93a8b92f1ddf94bf24 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Wed, 15 Dec 2021 10:59:34 -0800 Subject: [PATCH 014/209] Cleanup regex info and some fixes in Derivative code (#5709) * removed unused regex info fields * cleanup of info and fixes in antimirov derivatives * removed extra qualification on operator --- src/ast/rewriter/seq_rewriter.cpp | 128 ++++++++++++++++++++---------- src/ast/rewriter/seq_rewriter.h | 7 +- src/ast/seq_decl_plugin.cpp | 105 ++++++++---------------- src/ast/seq_decl_plugin.h | 35 ++------ 4 files changed, 132 insertions(+), 143 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index cb7b778ab..d399df1e6 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3115,8 +3115,8 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref result = mk_antimirov_deriv_union(c1, re().mk_ite_simplify(r1nullable, mk_antimirov_deriv(e, r2, path), nothing())); } else if (m().is_ite(r, c, r1, r2)) { - c1 = simplify_path(m().mk_and(c, path)); - c2 = simplify_path(m().mk_and(m().mk_not(c), path)); + c1 = simplify_path(e, m().mk_and(c, path)); + c2 = simplify_path(e, m().mk_and(m().mk_not(c), path)); if (m().is_false(c1)) result = mk_antimirov_deriv(e, r2, c2); else if (m().is_false(c2)) @@ -3131,8 +3131,8 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref SASSERT(u().is_char(c1)); SASSERT(u().is_char(c2)); // case: c1 <= e <= c2 - range = simplify_path(m().mk_and(u().mk_le(c1, e), u().mk_le(e, c2))); - psi = simplify_path(m().mk_and(path, range)); + range = simplify_path(e, m().mk_and(u().mk_le(c1, e), u().mk_le(e, c2))); + psi = simplify_path(e, m().mk_and(path, range)); } else if (!str().is_string(r1) && str().is_unit_string(r2, c2)) { SASSERT(u().is_char(c2)); @@ -3141,8 +3141,8 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref expr_ref zero(m_autil.mk_int(0), m()); expr_ref r1_length_eq_one(m().mk_eq(str().mk_length(r1), one), m()); expr_ref r1_0(str().mk_nth_i(r1, zero), m()); - range = simplify_path(m().mk_and(r1_length_eq_one, m().mk_and(u().mk_le(r1_0, e), u().mk_le(e, c2)))); - psi = simplify_path(m().mk_and(path, range)); + range = simplify_path(e, m().mk_and(r1_length_eq_one, m().mk_and(u().mk_le(r1_0, e), u().mk_le(e, c2)))); + psi = simplify_path(e, m().mk_and(path, range)); } else if (!str().is_string(r2) && str().is_unit_string(r1, c1)) { SASSERT(u().is_char(c1)); @@ -3151,8 +3151,8 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref expr_ref zero(m_autil.mk_int(0), m()); expr_ref r2_length_eq_one(m().mk_eq(str().mk_length(r2), one), m()); expr_ref r2_0(str().mk_nth_i(r2, zero), m()); - range = simplify_path(m().mk_and(r2_length_eq_one, m().mk_and(u().mk_le(c1, e), u().mk_le(e, r2_0)))); - psi = simplify_path(m().mk_and(path, range)); + range = simplify_path(e, m().mk_and(r2_length_eq_one, m().mk_and(u().mk_le(c1, e), u().mk_le(e, r2_0)))); + psi = simplify_path(e, m().mk_and(path, range)); } else if (!str().is_string(r1) && !str().is_string(r2)) { // both r1 and r2 nonground: |r1|=1 & |r2|=1 & r1[0] <= e <= r2[0] @@ -3162,8 +3162,8 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref expr_ref r1_0(str().mk_nth_i(r1, zero), m()); expr_ref r2_length_eq_one(m().mk_eq(str().mk_length(r2), one), m()); expr_ref r2_0(str().mk_nth_i(r2, zero), m()); - range = simplify_path(m().mk_and(r1_length_eq_one, m().mk_and(r2_length_eq_one, m().mk_and(u().mk_le(r1_0, e), u().mk_le(e, r2_0))))); - psi = simplify_path(m().mk_and(path, range)); + range = simplify_path(e, m().mk_and(r1_length_eq_one, m().mk_and(r2_length_eq_one, m().mk_and(u().mk_le(r1_0, e), u().mk_le(e, r2_0))))); + psi = simplify_path(e, m().mk_and(path, range)); } if (m().is_false(psi)) result = nothing(); @@ -3173,7 +3173,7 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref else if (re().is_union(r, r1, r2)) result = mk_antimirov_deriv_union(mk_antimirov_deriv(e, r1, path), mk_antimirov_deriv(e, r2, path)); else if (re().is_intersection(r, r1, r2)) - result = mk_antimirov_deriv_intersection( + result = mk_antimirov_deriv_intersection(e, mk_antimirov_deriv(e, r1, path), mk_antimirov_deriv(e, r2, path), m().mk_true()); else if (re().is_star(r, r1) || re().is_plus(r, r1) || (re().is_loop(r, r1, lo) && 0 <= lo && lo <= 1)) @@ -3190,11 +3190,11 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref result = mk_antimirov_deriv(e, r1, path); else if (re().is_complement(r, r1)) // D(e,~r1) = ~D(e,r1) - result = mk_antimirov_deriv_negate(mk_antimirov_deriv(e, r1, path)); + result = mk_antimirov_deriv_negate(e, mk_antimirov_deriv(e, r1, path)); else if (re().is_diff(r, r1, r2)) - result = mk_antimirov_deriv_intersection( + result = mk_antimirov_deriv_intersection(e, mk_antimirov_deriv(e, r1, path), - mk_antimirov_deriv_negate(mk_antimirov_deriv(e, r2, path)), m().mk_true()); + mk_antimirov_deriv_negate(e, mk_antimirov_deriv(e, r2, path)), m().mk_true()); else if (re().is_of_pred(r, r1)) { array_util array(m()); expr* args[2] = { r1, e }; @@ -3207,36 +3207,47 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref result = re().mk_derivative(e, r); } -expr_ref seq_rewriter::mk_antimirov_deriv_intersection(expr* d1, expr* d2, expr* path) { +expr_ref seq_rewriter::mk_antimirov_deriv_intersection(expr* e, expr* d1, expr* d2, expr* path) { sort* seq_sort = nullptr, * ele_sort = nullptr; VERIFY(m_util.is_re(d1, seq_sort)); VERIFY(m_util.is_seq(seq_sort, ele_sort)); expr_ref result(m()); expr* c, * a, * b; - if (d1 == d2 || re().is_full_seq(d2) || re().is_empty(d1)) + //if (d1 == d2 || re().is_full_seq(d2) || re().is_empty(d1)) + // result = d1; + //else if (re().is_full_seq(d1) || re().is_empty(d2)) + // result = d2; + //else + if (re().is_empty(d1)) result = d1; - else if (re().is_full_seq(d1) || re().is_empty(d2)) + else if (re().is_empty(d2)) result = d2; else if (m().is_ite(d1, c, a, b)) { - expr_ref path_and_c(simplify_path(m().mk_and(path, c)), m()); - expr_ref path_and_notc(simplify_path(m().mk_and(path, m().mk_not(c))), m()); + expr_ref path_and_c(simplify_path(e, m().mk_and(path, c)), m()); + expr_ref path_and_notc(simplify_path(e, m().mk_and(path, m().mk_not(c))), m()); if (m().is_false(path_and_c)) - result = mk_antimirov_deriv_intersection(b, d2, path); + result = mk_antimirov_deriv_intersection(e, b, d2, path); else if (m().is_false(path_and_notc)) - result = mk_antimirov_deriv_intersection(a, d2, path); + result = mk_antimirov_deriv_intersection(e, a, d2, path); else - result = m().mk_ite(c, mk_antimirov_deriv_intersection(a, d2, path_and_c), - mk_antimirov_deriv_intersection(b, d2, path_and_notc)); + result = m().mk_ite(c, mk_antimirov_deriv_intersection(e, a, d2, path_and_c), + mk_antimirov_deriv_intersection(e, b, d2, path_and_notc)); } else if (m().is_ite(d2)) // swap d1 and d2 - result = mk_antimirov_deriv_intersection(d2, d1, path); + result = mk_antimirov_deriv_intersection(e, d2, d1, path); + else if (d1 == d2 || re().is_full_seq(d2)) + result = mk_antimirov_deriv_restrict(e, d1, path); + else if (re().is_full_seq(d1)) + result = mk_antimirov_deriv_restrict(e, d2, path); else if (re().is_union(d1, a, b)) // distribute intersection over the union in d1 - result = mk_antimirov_deriv_union(mk_antimirov_deriv_intersection(a, d2, path), mk_antimirov_deriv_intersection(b, d2, path)); + result = mk_antimirov_deriv_union(mk_antimirov_deriv_intersection(e, a, d2, path), + mk_antimirov_deriv_intersection(e, b, d2, path)); else if (re().is_union(d2, a, b)) // distribute intersection over the union in d2 - result = mk_antimirov_deriv_union(mk_antimirov_deriv_intersection(d1, a, path), mk_antimirov_deriv_intersection(d1, b, path)); + result = mk_antimirov_deriv_union(mk_antimirov_deriv_intersection(e, d1, a, path), + mk_antimirov_deriv_intersection(e, d1, b, path)); else // in all other cases create the intersection regex // TODO: flatten, order and merge d1 and d2 to maintain equality under similarity @@ -3258,7 +3269,7 @@ expr_ref seq_rewriter::mk_antimirov_deriv_concat(expr* d, expr* r) { return result; } -expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* d) { +expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* elem, expr* d) { sort* seq_sort = nullptr; VERIFY(m_util.is_re(d, seq_sort)); auto nothing = [&]() { return expr_ref(re().mk_empty(d->get_sort()), m()); }; @@ -3276,11 +3287,12 @@ expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* d) { else if (re().is_dot_plus(d)) result = epsilon(); else if (m().is_ite(d, c, t, e)) - result = m().mk_ite(c, mk_antimirov_deriv_negate(t), mk_antimirov_deriv_negate(e)); + result = m().mk_ite(c, mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e)); else if (re().is_union(d, t, e)) - result = re().mk_inter(mk_antimirov_deriv_negate(t), mk_antimirov_deriv_negate(e)); + //result = re().mk_inter(mk_antimirov_deriv_negate(t), mk_antimirov_deriv_negate(e)); + result = mk_antimirov_deriv_intersection(elem, mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e), m().mk_true()); else if (re().is_intersection(d, t, e)) - result = re().mk_union(mk_antimirov_deriv_negate(t), mk_antimirov_deriv_negate(e)); + result = re().mk_union(mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e)); else if (re().is_complement(d, t)) result = t; else @@ -3304,6 +3316,45 @@ expr_ref seq_rewriter::mk_antimirov_deriv_union(expr* d1, expr* d2) { return result; } +// restrict the guards of all conditionals id d and simplify the resulting derivative +// restrict(if(c, a, b), cond) = if(c, restrict(a, cond & c), restrict(b, cond & ~c)) +// restrict(a U b, cond) = restrict(a, cond) U restrict(b, cond) +// where {} U X = X, X U X = X +// restrict(R, cond) = R +// +// restrict(d, false) = [] +// +// it is already assumed that the restriction takes place witin a branch +// so the condition is not added explicitly but propagated down in order to eliminate +// infeasible cases +expr_ref seq_rewriter::mk_antimirov_deriv_restrict(expr* e, expr* d, expr* cond) { + expr_ref result(d, m()); + expr_ref _cond(cond, m()); + expr* c, * a, * b; + if (m().is_false(cond)) + result = re().mk_empty(d->get_sort()); + else if (re().is_empty(d) || m().is_true(cond)) + result = d; + else if (m().is_ite(d, c, a, b)) { + expr_ref path_and_c(simplify_path(e, m().mk_and(cond, c)), m()); + expr_ref path_and_notc(simplify_path(e, m().mk_and(cond, m().mk_not(c))), m()); + result = re().mk_ite_simplify(c, mk_antimirov_deriv_restrict(e, a, path_and_c), + mk_antimirov_deriv_restrict(e, b, path_and_notc)); + } + else if (re().is_union(d, a, b)) { + expr_ref a1(mk_antimirov_deriv_restrict(e, a, cond), m()); + expr_ref b1(mk_antimirov_deriv_restrict(e, b, cond), m()); + if (a1 == b1 || re().is_empty(b1) || re().is_full_seq(a1)) + result = a1; + else if (re().is_empty(a1) || re().is_full_seq(b1)) + result = b1; + else + //TODO: merge + result = (a1->get_id() <= b1->get_id() ? re().mk_union(a1, b1) : re().mk_union(b1, a1)); + } + return result; +} + expr_ref seq_rewriter::mk_regex_reverse(expr* r) { expr* r1 = nullptr, * r2 = nullptr, * c = nullptr; unsigned lo = 0, hi = 0; @@ -3390,21 +3441,18 @@ expr_ref seq_rewriter::mk_in_antimirov_rec(expr* s, expr* d) { } /* -path is typically a conjunction of (negated) character equations or constraints that can potentially be simplified -the first element of each equation is assumed to be the element parameter, for example x = (:var 0), -for example a constraint x='a' & x='b' is simplified to false +* calls elim_condition */ -expr_ref seq_rewriter::simplify_path(expr* path) { - //TODO: more systematic simplifications +expr_ref seq_rewriter::simplify_path(expr* elem, expr* path) { expr_ref result(path, m()); - expr* h = nullptr, * t = nullptr, * lhs = nullptr, * rhs = nullptr, * h1 = nullptr; + expr* h = nullptr, * t = nullptr; if (m().is_and(path, h, t)) { if (m().is_true(h)) - result = simplify_path(t); + result = simplify_path(elem, t); else if (m().is_true(t)) - result = simplify_path(h); - else if (m().is_eq(h, lhs, rhs) || (m().is_not(h, h1) && m().is_eq(h1, lhs, rhs))) - elim_condition(lhs, result); + result = simplify_path(elem, h); + else + elim_condition(elem, result); } return result; } diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 5cba15fc8..9687797a0 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -214,14 +214,15 @@ class seq_rewriter { expr_ref mk_in_antimirov_rec(expr* s, expr* d); expr_ref mk_in_antimirov(expr* s, expr* d); - expr_ref mk_antimirov_deriv_intersection(expr* d1, expr* d2, expr* path); + expr_ref mk_antimirov_deriv_intersection(expr* elem, expr* d1, expr* d2, expr* path); expr_ref mk_antimirov_deriv_concat(expr* d, expr* r); - expr_ref mk_antimirov_deriv_negate(expr* d); + expr_ref mk_antimirov_deriv_negate(expr* elem, expr* d); expr_ref mk_antimirov_deriv_union(expr* d1, expr* d2); + expr_ref mk_antimirov_deriv_restrict(expr* elem, expr* d1, expr* cond); expr_ref mk_regex_reverse(expr* r); expr_ref mk_regex_concat(expr* r1, expr* r2); - expr_ref simplify_path(expr* path); + expr_ref simplify_path(expr* elem, expr* path); bool lt_char(expr* ch1, expr* ch2); bool eq_char(expr* ch1, expr* ch2); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 1e87e1402..2044590aa 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1503,9 +1503,9 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { if (e->get_family_id() == u.get_family_id()) { switch (e->get_decl()->get_decl_kind()) { case OP_RE_EMPTY_SET: - return info(true, true, true, true, true, true, false, l_false, UINT_MAX, 0); + return info(true, l_false, UINT_MAX); case OP_RE_FULL_SEQ_SET: - return info(true, true, true, true, true, true, false, l_true, 0, 1); + return info(true, l_true, 0); case OP_RE_STAR: i1 = get_info_rec(e->get_arg(0)); return i1.star(); @@ -1517,7 +1517,7 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { case OP_RE_OF_PRED: //TBD: check if the character predicate contains uninterpreted symbols or is nonground or is unsat //TBD: check if the range is unsat - return info(true, true, true, true, true, true, true, l_false, 1, 0); + return info(true, l_false, 1); case OP_RE_CONCAT: i1 = get_info_rec(e->get_arg(0)); i2 = get_info_rec(e->get_arg(1)); @@ -1534,7 +1534,7 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { min_length = u.str.min_length(e->get_arg(0)); is_value = m.is_value(e->get_arg(0)); nullable = (is_value && min_length == 0 ? l_true : (min_length > 0 ? l_false : l_undef)); - return info(true, true, is_value, true, true, true, (min_length == 1 && u.str.max_length(e->get_arg(0)) == 1), nullable, min_length, 0); + return info(is_value, nullable, min_length); case OP_RE_REVERSE: return get_info_rec(e->get_arg(0)); case OP_RE_PLUS: @@ -1570,14 +1570,7 @@ std::ostream& seq_util::rex::info::display(std::ostream& out) const { if (is_known()) { out << "info(" << "nullable=" << (nullable == l_true ? "T" : (nullable == l_false ? "F" : "U")) << ", " - << "classical=" << (classical ? "T" : "F") << ", " - << "standard=" << (standard ? "T" : "F") << ", " - << "nonbranching=" << (nonbranching ? "T" : "F") << ", " - << "normalized=" << (normalized ? "T" : "F") << ", " - << "monadic=" << (monadic ? "T" : "F") << ", " - << "singleton=" << (singleton ? "T" : "F") << ", " - << "min_length=" << min_length << ", " - << "star_height=" << star_height << ")"; + << "min_length=" << min_length << ")"; } else if (is_valid()) out << "UNKNOWN"; @@ -1597,13 +1590,13 @@ std::string seq_util::rex::info::str() const { seq_util::rex::info seq_util::rex::info::star() const { //if is_known() is false then all mentioned properties will remain false - return seq_util::rex::info(classical, classical, interpreted, nonbranching, normalized, monadic, false, l_true, 0, star_height + 1); + return seq_util::rex::info(interpreted, l_true, 0); } seq_util::rex::info seq_util::rex::info::plus() const { if (is_known()) { //plus never occurs in a normalized regex - return info(classical, classical, interpreted, nonbranching, false, monadic, false, nullable, min_length, star_height + 1); + return info(interpreted, nullable, min_length); } else return *this; @@ -1612,14 +1605,14 @@ seq_util::rex::info seq_util::rex::info::plus() const { seq_util::rex::info seq_util::rex::info::opt() const { // if is_known() is false then all mentioned properties will remain false // optional construct never occurs in a normalized regex - return seq_util::rex::info(classical, classical, interpreted, nonbranching, false, monadic, false, l_true, 0, star_height); + return seq_util::rex::info(interpreted, l_true, 0); } seq_util::rex::info seq_util::rex::info::complement() const { if (is_known()) { lbool compl_nullable = (nullable == l_true ? l_false : (nullable == l_false ? l_true : l_undef)); unsigned compl_min_length = (compl_nullable == l_false ? 1 : 0); - return info(false, standard, interpreted, nonbranching, normalized, monadic, false, compl_nullable, compl_min_length, star_height); + return info(interpreted, compl_nullable, compl_min_length); } else return *this; @@ -1631,16 +1624,9 @@ seq_util::rex::info seq_util::rex::info::concat(seq_util::rex::info const& rhs, unsigned m = min_length + rhs.min_length; if (m < min_length || m < rhs.min_length) m = UINT_MAX; - return info(classical & rhs.classical, - classical && rhs.classical, //both args of concat must be classical for it to be standard - interpreted && rhs.interpreted, - nonbranching && rhs.nonbranching, - (normalized && !lhs_is_concat && rhs.normalized), - monadic && rhs.monadic, - false, + return info(interpreted && rhs.interpreted, ((nullable == l_false || rhs.nullable == l_false) ? l_false : ((nullable == l_true && rhs.nullable == l_true) ? l_true : l_undef)), - m, - std::max(star_height, rhs.star_height)); + m); } else return rhs; @@ -1652,16 +1638,9 @@ seq_util::rex::info seq_util::rex::info::concat(seq_util::rex::info const& rhs, seq_util::rex::info seq_util::rex::info::disj(seq_util::rex::info const& rhs) const { if (is_known() || rhs.is_known()) { //works correctly if one of the arguments is unknown - return info(classical & rhs.classical, - standard && rhs.standard, - interpreted && rhs.interpreted, - nonbranching && rhs.nonbranching, - normalized && rhs.normalized, - monadic && rhs.monadic, - singleton && rhs.singleton, + return info(interpreted && rhs.interpreted, ((nullable == l_true || rhs.nullable == l_true) ? l_true : ((nullable == l_false && rhs.nullable == l_false) ? l_false : l_undef)), - std::min(min_length, rhs.min_length), - std::max(star_height, rhs.star_height)); + std::min(min_length, rhs.min_length)); } else return rhs; @@ -1670,16 +1649,9 @@ seq_util::rex::info seq_util::rex::info::disj(seq_util::rex::info const& rhs) co seq_util::rex::info seq_util::rex::info::conj(seq_util::rex::info const& rhs) const { if (is_known()) { if (rhs.is_known()) { - return info(false, - standard && rhs.standard, - interpreted && rhs.interpreted, - nonbranching && rhs.nonbranching, - normalized && rhs.normalized, - monadic && rhs.monadic, - singleton && rhs.singleton, + return info(interpreted && rhs.interpreted, ((nullable == l_true && rhs.nullable == l_true) ? l_true : ((nullable == l_false || rhs.nullable == l_false) ? l_false : l_undef)), - std::max(min_length, rhs.min_length), - std::max(star_height, rhs.star_height)); + std::max(min_length, rhs.min_length)); } else return rhs; @@ -1691,16 +1663,9 @@ seq_util::rex::info seq_util::rex::info::conj(seq_util::rex::info const& rhs) co seq_util::rex::info seq_util::rex::info::diff(seq_util::rex::info const& rhs) const { if (is_known()) { if (rhs.is_known()) { - return info(false, - standard & rhs.standard, - interpreted & rhs.interpreted, - nonbranching & rhs.nonbranching, - normalized & rhs.normalized, - monadic & rhs.monadic, - false, + return info(interpreted & rhs.interpreted, ((nullable == l_true && rhs.nullable == l_false) ? l_true : ((nullable == l_false || rhs.nullable == l_false) ? l_false : l_undef)), - std::max(min_length, rhs.min_length), - std::max(star_height, rhs.star_height)); + std::max(min_length, rhs.min_length)); } else return rhs; @@ -1715,13 +1680,9 @@ seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) co // unsigned ite_min_length = std::min(min_length, i.min_length); // lbool ite_nullable = (nullable == i.nullable ? nullable : l_undef); // TBD: whether ite is interpreted or not depends on whether the condition is interpreted and both branches are interpreted - return info(false, false, false, false, - normalized && i.normalized, - monadic && i.monadic, - singleton && i.singleton, + return info(false, ((nullable == l_true && i.nullable == l_true) ? l_true : ((nullable == l_false && i.nullable == l_false) ? l_false : l_undef)), - std::min(min_length, i.min_length), - std::max(star_height, i.star_height)); + std::min(min_length, i.min_length)); } else return i; @@ -1737,24 +1698,22 @@ seq_util::rex::info seq_util::rex::info::loop(unsigned lower, unsigned upper) co if (m > 0 && (m < min_length || m < lower)) m = UINT_MAX; lbool loop_nullable = (nullable == l_true || lower == 0 ? l_true : nullable); - if (upper == UINT_MAX) { - // this means the loop is r{lower,*} and is therefore not normalized - // normalized regex would be r{lower,lower}r* and would in particular not use r{0,} for r* - return info(classical, classical, interpreted, nonbranching, false, singleton, false, loop_nullable, m, star_height + 1); - } - else { - bool loop_normalized = normalized; - // r{lower,upper} is not normalized if r is nullable but lower > 0 - // r{0,1} is not normalized: it should be ()|r - // r{1,1} is not normalized: it should be r - // r{lower,upper} is not normalized if lower > upper it should then be [] (empty) - if ((nullable == l_true && lower > 0) || upper == 1 || lower > upper) - loop_normalized = false; - return info(classical, classical, interpreted, nonbranching, loop_normalized, singleton, false, loop_nullable, m, star_height); - } + return info(interpreted, loop_nullable, m); } else return *this; } +seq_util::rex::info& seq_util::rex::info::operator=(info const& other) { + if (this == &other) { + return *this; + } + + known = other.known; + interpreted = other.interpreted; + nullable = other.nullable; + min_length = other.min_length; + return *this; +} + diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 1db05b722..d6a1a0f29 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -411,26 +411,11 @@ public: struct info { /* Value is either undefined (known=l_undef) or defined and known (l_true) or defined but unknown (l_false)*/ lbool known { l_undef }; - /* No complement, no intersection, no difference, and no if-then-else is used. Reverse is allowed. */ - bool classical { false }; - /* Boolean-reverse combination of classical regexes (using reverse, union, complement, intersection or difference). */ - bool standard { false }; - /* There are no uninterpreted symbols. */ bool interpreted { false }; - /* No if-then-else is used. */ - bool nonbranching { false }; - /* Concatenations are right associative and if a loop body is nullable then the lower bound is zero. */ - bool normalized { false }; - /* All bounded loops have a body that is a singleton. */ - bool monadic { false }; - /* Positive Boolean combination of ranges or predicates or singleton sequences. */ - bool singleton { false }; /* If l_true then empty word is accepted, if l_false then empty word is not accepted. */ lbool nullable { l_undef }; /* Lower bound on the length of all accepted words. */ unsigned min_length { 0 }; - /* Maximum nesting depth of Kleene stars. */ - unsigned star_height { 0 }; /* Default constructor of invalid info. @@ -445,19 +430,13 @@ public: /* General info constructor. */ - info(bool is_classical, - bool is_standard, - bool is_interpreted, - bool is_nonbranching, - bool is_normalized, - bool is_monadic, - bool is_singleton, + info(bool is_interpreted, lbool is_nullable, - unsigned min_l, - unsigned star_h) : - known(l_true), classical(is_classical), standard(is_standard), interpreted(is_interpreted), nonbranching(is_nonbranching), - normalized(is_normalized), monadic(is_monadic), singleton(is_singleton), nullable(is_nullable), - min_length(min_l), star_height(star_h) {} + unsigned min_l) : + known(l_true), + interpreted(is_interpreted), + nullable(is_nullable), + min_length(min_l) {} /* Appends a string representation of the info into the stream. @@ -483,6 +462,8 @@ public: info diff(info const& rhs) const; info orelse(info const& rhs) const; info loop(unsigned lower, unsigned upper) const; + + info& operator=(info const& other); }; private: seq_util& u; From 2caa7e6e454fdb01236421b66b08561b5ab60029 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Dec 2021 03:22:54 -0800 Subject: [PATCH 015/209] remove EnumToNative as it drops reference counts, fixes #5713 --- src/api/dotnet/Context.cs | 33 ++++++++++++++++++++------------- src/api/dotnet/Z3Object.cs | 16 +--------------- 2 files changed, 21 insertions(+), 28 deletions(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 07759b1fa..c06f58cbd 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -980,7 +980,8 @@ namespace Microsoft.Z3 Debug.Assert(t != null); Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); - return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.EnumToNative(t))); + var ands = t.ToArray(); + return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.ArrayToNative(ands))); } /// @@ -1005,7 +1006,8 @@ namespace Microsoft.Z3 Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); - return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Count(), AST.EnumToNative(t))); + var ts = t.ToArray(); + return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)ts.Length, AST.ArrayToNative(ts))); } #endregion @@ -1032,7 +1034,8 @@ namespace Microsoft.Z3 Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Count(), AST.EnumToNative(t))); + var ts = t.ToArray(); + return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)ts.Length, AST.ArrayToNative(ts))); } /// @@ -1044,7 +1047,8 @@ namespace Microsoft.Z3 Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t))); + var ts = t.ToArray(); + return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts))); } /// @@ -1056,7 +1060,8 @@ namespace Microsoft.Z3 Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); - return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t))); + var ts = t.ToArray(); + return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts))); } /// @@ -2749,10 +2754,11 @@ namespace Microsoft.Z3 /// public BoolExpr MkAtMost(IEnumerable args, uint k) { - Debug.Assert(args != null); - CheckContextMatch(args); - return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Count(), - AST.EnumToNative(args), k)); + Debug.Assert(args != null); + CheckContextMatch(args); + var ts = args.ToArray(); + return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) ts.Length, + AST.ArrayToNative(ts), k)); } /// @@ -2760,10 +2766,11 @@ namespace Microsoft.Z3 /// public BoolExpr MkAtLeast(IEnumerable args, uint k) { - Debug.Assert(args != null); - CheckContextMatch(args); - return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint) args.Count(), - AST.EnumToNative(args), k)); + Debug.Assert(args != null); + CheckContextMatch(args); + var ts = args.ToArray(); + return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint) ts.Length, + AST.ArrayToNative(ts), k)); } /// diff --git a/src/api/dotnet/Z3Object.cs b/src/api/dotnet/Z3Object.cs index 9a61a0119..d25dfc25a 100644 --- a/src/api/dotnet/Z3Object.cs +++ b/src/api/dotnet/Z3Object.cs @@ -131,24 +131,10 @@ namespace Microsoft.Z3 return an; } - internal static IntPtr[] EnumToNative(IEnumerable a) where T : Z3Object - { - - if (a == null) return null; - IntPtr[] an = new IntPtr[a.Count()]; - int i = 0; - foreach (var ai in a) - { - if (ai != null) an[i] = ai.NativeObject; - ++i; - } - return an; - } - internal static uint ArrayLength(Z3Object[] a) { return (a == null)?0:(uint)a.Length; } - #endregion +#endregion } } From dd6a11b526426579133d5920d9c9ed0c34ec3632 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Dec 2021 09:35:54 -0800 Subject: [PATCH 016/209] fix #5715 --- src/smt/theory_seq.cpp | 32 +++++++++++++++++++++----------- src/smt/theory_seq.h | 6 +++--- 2 files changed, 24 insertions(+), 14 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 369adccc1..5ef415d6a 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -349,7 +349,7 @@ final_check_status theory_seq::final_check_eh() { TRACEFIN("propagate_contains"); return FC_CONTINUE; } - if (fixed_length(true)) { + if (check_fixed_length(true, false)) { ++m_stats.m_fixed_length; TRACEFIN("zero_length"); return FC_CONTINUE; @@ -359,7 +359,7 @@ final_check_status theory_seq::final_check_eh() { TRACEFIN("split_based_on_length"); return FC_CONTINUE; } - if (fixed_length()) { + if (check_fixed_length(false, false)) { ++m_stats.m_fixed_length; TRACEFIN("fixed_length"); return FC_CONTINUE; @@ -413,6 +413,11 @@ final_check_status theory_seq::final_check_eh() { TRACEFIN("branch_itos"); return FC_CONTINUE; } + if (check_fixed_length(false, true)) { + ++m_stats.m_fixed_length; + TRACEFIN("fixed_length"); + return FC_CONTINUE; + } if (m_unhandled_expr) { TRACEFIN("give_up"); TRACE("seq", tout << "unhandled: " << mk_pp(m_unhandled_expr, m) << "\n";); @@ -461,18 +466,18 @@ bool theory_seq::enforce_length(expr_ref_vector const& es, vector & le } -bool theory_seq::fixed_length(bool is_zero) { +bool theory_seq::check_fixed_length(bool is_zero, bool check_long_strings) { bool found = false; for (unsigned i = 0; i < m_length.size(); ++i) { expr* e = m_length.get(i); - if (fixed_length(e, is_zero)) { + if (fixed_length(e, is_zero, check_long_strings)) { found = true; } } return found; } -bool theory_seq::fixed_length(expr* len_e, bool is_zero) { +bool theory_seq::fixed_length(expr* len_e, bool is_zero, bool check_long_strings) { rational lo, hi; expr* e = nullptr; VERIFY(m_util.str.is_length(len_e, e)); @@ -493,12 +498,21 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) { expr_ref seq(e, m), head(m), tail(m); + + TRACE("seq", tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";); + literal a = mk_eq(len_e, m_autil.mk_numeral(lo, true), false); + if (ctx.get_assignment(a) == l_false) + return false; + + if (!check_long_strings && lo > 20 && !is_zero) + return false; + if (lo.is_zero()) { seq = m_util.str.mk_empty(e->get_sort()); } else if (!is_zero) { unsigned _lo = lo.get_unsigned(); - expr_ref_vector elems(m); + expr_ref_vector elems(m); for (unsigned j = 0; j < _lo; ++j) { m_sk.decompose(seq, head, tail); elems.push_back(head); @@ -506,10 +520,6 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) { } seq = mk_concat(elems.size(), elems.data()); } - TRACE("seq", tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";); - literal a = mk_eq(len_e, m_autil.mk_numeral(lo, true), false); - if (ctx.get_assignment(a) == l_false) - return false; literal b = mk_seq_eq(seq, e); if (ctx.get_assignment(b) == l_true) return false; @@ -2873,7 +2883,7 @@ void theory_seq::add_axiom(literal_vector & lits) { for (literal lit : lits) ctx.mark_as_relevant(lit); - IF_VERBOSE(10, verbose_stream() << "ax "; + IF_VERBOSE(10, verbose_stream() << "ax"; for (literal l : lits) ctx.display_literal_smt2(verbose_stream() << " ", l); verbose_stream() << "\n"); m_new_propagation = true; diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 68e9f3762..4b4c1d80b 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -243,7 +243,7 @@ namespace smt { replay_fixed_length(ast_manager& m, expr* e) : m_e(e, m) {} ~replay_fixed_length() override {} void operator()(theory_seq& th) override { - th.fixed_length(m_e); + th.fixed_length(m_e, false, false); m_e.reset(); } }; @@ -436,8 +436,8 @@ namespace smt { bool check_length_coherence(); bool check_length_coherence0(expr* e); bool check_length_coherence(expr* e); - bool fixed_length(bool is_zero = false); - bool fixed_length(expr* e, bool is_zero); + bool check_fixed_length(bool is_zero, bool check_long_strings); + bool fixed_length(expr* e, bool is_zero, bool check_long_strings); bool branch_variable_eq(depeq const& e); bool branch_binary_variable(depeq const& e); bool can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs); From a0999723543fab1efb1314b577e31752e5b95d3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Dec 2021 10:20:53 -0800 Subject: [PATCH 017/209] fix #5714 It is not unlike other fuzz bugs: it exercises some behavior that applications are unlikely to expose. In this case, a rule body expanded into a conjunction with more than 1M formulas (with a lot of repetition). The original rule representation assumed silently that the number of constraints in a body would fit within 20 bits, but reality allowed bodies with as many as 2^{32} - 1 constraints. So "minimizing" the bug as @agurfinkel asks for seems not to make too much sense. Just running the samples in debug mode points to the root cause. Since fuzz bugs are not from applications and fuzz tools have the potential for creating a large number of issues, I find it reasonable to push some basic pro-active asks on filers: - reproduce bug in debug builds to assess whether a debug assert triggers. - minimize or keep it simpler when possible (in this case it does not apply) - perform basic diagnostics/triage. I am basically asking to push this part of the work on to the fuzzer. Otherwise, addressing random bugs doesn't scale. Triaging should have pointed to the root cause. Now, there tends to be something to learn from bugs. In this case, the question was: "can we avoid constraints with duplications"? In particular, it points to a basic inefficiency of extracting conjunctions (and disjunctions). The function didn't deduplicate. So I added deduplication into this function. It is used throughout z3 code base so could expose latent issues. We will see. --- src/ast/ast_util.cpp | 46 ++++++++++++++++++++++++---------------- src/muz/base/dl_rule.cpp | 18 +++++++--------- src/muz/base/dl_rule.h | 13 ++++++------ 3 files changed, 42 insertions(+), 35 deletions(-) diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp index 993831d64..bec80240f 100644 --- a/src/ast/ast_util.cpp +++ b/src/ast/ast_util.cpp @@ -260,39 +260,44 @@ expr_ref mk_distinct(expr_ref_vector const& args) { void flatten_and(expr_ref_vector& result) { ast_manager& m = result.get_manager(); expr* e1, *e2, *e3; + expr_fast_mark1 seen; for (unsigned i = 0; i < result.size(); ++i) { - if (m.is_and(result.get(i))) { - app* a = to_app(result.get(i)); + expr* e = result.get(i); + if (seen.is_marked(e)) + continue; + seen.mark(e); + if (m.is_and(e)) { + app* a = to_app(e); for (expr* arg : *a) result.push_back(arg); result[i] = result.back(); result.pop_back(); --i; } - else if (m.is_not(result.get(i), e1) && m.is_not(e1, e2)) { + else if (m.is_not(e, e1) && m.is_not(e1, e2)) { result[i] = e2; --i; } - else if (m.is_not(result.get(i), e1) && m.is_or(e1)) { + else if (m.is_not(e, e1) && m.is_or(e1)) { app* a = to_app(e1); for (expr* arg : *a) result.push_back(m.mk_not(arg)); result[i] = result.back(); result.pop_back(); --i; } - else if (m.is_not(result.get(i), e1) && m.is_implies(e1,e2,e3)) { + else if (m.is_not(e, e1) && m.is_implies(e1, e2, e3)) { result.push_back(e2); result[i] = m.mk_not(e3); --i; } - else if (m.is_true(result.get(i)) || - (m.is_not(result.get(i), e1) && + else if (m.is_true(e) || + (m.is_not(e, e1) && m.is_false(e1))) { result[i] = result.back(); result.pop_back(); --i; } - else if (m.is_false(result.get(i)) || - (m.is_not(result.get(i), e1) && + else if (m.is_false(e) || + (m.is_not(e, e1) && m.is_true(e1))) { result.reset(); result.push_back(m.mk_false()); @@ -317,39 +322,44 @@ void flatten_and(expr_ref& fml) { void flatten_or(expr_ref_vector& result) { ast_manager& m = result.get_manager(); expr* e1, *e2, *e3; + expr_fast_mark1 seen; for (unsigned i = 0; i < result.size(); ++i) { - if (m.is_or(result.get(i))) { - app* a = to_app(result.get(i)); + expr* e = result.get(i); + if (seen.is_marked(e)) + continue; + seen.mark(e); + if (m.is_or(e)) { + app* a = to_app(e); for (expr* arg : *a) result.push_back(arg); result[i] = result.back(); result.pop_back(); --i; } - else if (m.is_not(result.get(i), e1) && m.is_not(e1, e2)) { + else if (m.is_not(e, e1) && m.is_not(e1, e2)) { result[i] = e2; --i; } - else if (m.is_not(result.get(i), e1) && m.is_and(e1)) { + else if (m.is_not(e, e1) && m.is_and(e1)) { app* a = to_app(e1); for (expr* arg : *a) result.push_back(m.mk_not(arg)); result[i] = result.back(); result.pop_back(); --i; } - else if (m.is_implies(result.get(i),e2,e3)) { + else if (m.is_implies(e,e2,e3)) { result.push_back(e3); result[i] = m.mk_not(e2); --i; } - else if (m.is_false(result.get(i)) || - (m.is_not(result.get(i), e1) && + else if (m.is_false(e) || + (m.is_not(e, e1) && m.is_true(e1))) { result[i] = result.back(); result.pop_back(); --i; } - else if (m.is_true(result.get(i)) || - (m.is_not(result.get(i), e1) && + else if (m.is_true(e) || + (m.is_not(e, e1) && m.is_false(e1))) { result.reset(); result.push_back(m.mk_true()); diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 2baaf57b9..9bd7a7adf 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -178,7 +178,7 @@ namespace datalog { m_ctx.register_predicate(m_hnf.get_fresh_predicates()[i], false); } for (unsigned i = 0; i < fmls.size(); ++i) { - mk_horn_rule(fmls[i].get(), prs[i].get(), rules, name); + mk_horn_rule(fmls.get(i), prs.get(i), rules, name); } } @@ -190,12 +190,10 @@ namespace datalog { hoist_compound_predicates(index, m_head, m_body); TRACE("dl_rule", tout << mk_pp(m_head, m) << " :- "; - for (unsigned i = 0; i < m_body.size(); ++i) { - tout << mk_pp(m_body[i].get(), m) << " "; - } + for (expr* b : m_body) + tout << mk_pp(b, m) << " "; tout << "\n";); - mk_negations(m_body, m_neg); check_valid_rule(m_head, m_body.size(), m_body.data()); @@ -241,9 +239,8 @@ namespace datalog { m_args.reset(); head = ensure_app(e2); flatten_and(e1, m_args); - for (unsigned i = 0; i < m_args.size(); ++i) { - body.push_back(ensure_app(m_args[i].get())); - } + for (expr* a : m_args) + body.push_back(ensure_app(a)); } else { head = ensure_app(fml); @@ -255,7 +252,7 @@ namespace datalog { unsigned sz = body.size(); hoist_compound(index, head, body); for (unsigned i = 0; i < sz; ++i) { - app_ref b(body[i].get(), m); + app_ref b(body.get(i), m); hoist_compound(index, b, body); body[i] = b; } @@ -949,7 +946,8 @@ namespace datalog { } bool rule::has_negation() const { - for (unsigned i = 0; i < get_uninterpreted_tail_size(); ++i) { + unsigned sz = get_uninterpreted_tail_size(); + for (unsigned i = 0; i < sz; ++i) { if (is_neg_tail(i)) { return true; } diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index 044260f12..02d13c1ca 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -287,13 +287,12 @@ namespace datalog { class rule : public accounted_object { friend class rule_manager; - app* m_head{ nullptr }; - proof* m_proof{ nullptr }; - unsigned m_tail_size:20; - // unsigned m_reserve:12; - unsigned m_ref_cnt{ 0 }; - unsigned m_positive_cnt{ 0 }; - unsigned m_uninterp_cnt{ 0 }; + app* m_head = nullptr; + proof* m_proof = nullptr; + unsigned m_tail_size = 0; + unsigned m_ref_cnt = 0; + unsigned m_positive_cnt = 0; + unsigned m_uninterp_cnt = 0; symbol m_name; /** The following field is an array of tagged pointers. From 122b0fec0f873c69db421a6ec0ed935dbaf82069 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Dec 2021 12:30:29 -0800 Subject: [PATCH 018/209] fix #5710 --- src/opt/opt_solver.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index c1a4c68a9..39a7bb032 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -342,6 +342,11 @@ namespace opt { } void opt_solver::get_model_core(model_ref & m) { + if (m_last_model.get()) { + m = m_last_model.get(); + return; + } + for (unsigned i = m_models.size(); i-- > 0; ) { auto* mdl = m_models[i]; if (mdl) { From 4641a20f4fea6f23dc25be0d463615052d3cc13d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Dec 2021 13:50:31 -0800 Subject: [PATCH 019/209] #5700 - Add download x86 as part of release NuGet x86 is part of nightly NuGet but was not added to the release pipeline. --- scripts/release.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/scripts/release.yml b/scripts/release.yml index 9a1982744..78a58de59 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -171,6 +171,10 @@ stages: inputs: artifact: 'WindowsBuild-x64' path: $(Agent.TempDirectory)\package + displayName: 'Download Win32 Build' + inputs: + artifact: 'WindowsBuild-x86' + path: $(Agent.TempDirectory)\package - task: DownloadPipelineArtifact@2 displayName: 'Download Ubuntu Build' inputs: From db62038845213e31d36f18172499d0fa42d52b3b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Dec 2021 14:20:40 -0800 Subject: [PATCH 020/209] Update nightly.yaml see if this gets us past the upload to GitHub issue --- scripts/nightly.yaml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index d26f77934..5509c374b 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -1,5 +1,5 @@ variables: - ReleaseVersion: '4.8.13' + ReleaseVersion: '4.8.14' stages: - stage: Build @@ -287,6 +287,8 @@ stages: jobs: - job: Deploy displayName: "Deploy into GitHub" + pool: + vmImage: "ubuntu-latest" steps: - task: DownloadPipelineArtifact@2 displayName: "Download windows32" From a288f9048ad48275cb78ccf87412bb1fc3c06638 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Thu, 16 Dec 2021 19:19:36 -0800 Subject: [PATCH 021/209] Update regex union and intersection to maintain ANF (#5717) * added merge for unions and intersections * added normalization rules to ensure ANF * fixing PR comments related to merge --- src/ast/rewriter/seq_rewriter.cpp | 286 +++++++++++++++++++++++++----- src/ast/rewriter/seq_rewriter.h | 10 +- 2 files changed, 255 insertions(+), 41 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index d399df1e6..045642019 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3112,7 +3112,7 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref else // D(e,r1)r2|(ite (r1nullable) (D(e,r2)) []) // observe that (mk_ite_simplify(true, D(e,r2), []) = D(e,r2) - result = mk_antimirov_deriv_union(c1, re().mk_ite_simplify(r1nullable, mk_antimirov_deriv(e, r2, path), nothing())); + result = mk_regex_union_normalize(c1, re().mk_ite_simplify(r1nullable, mk_antimirov_deriv(e, r2, path), nothing())); } else if (m().is_ite(r, c, r1, r2)) { c1 = simplify_path(e, m().mk_and(c, path)); @@ -3171,7 +3171,7 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref result = re().mk_ite_simplify(range, epsilon(), nothing()); } else if (re().is_union(r, r1, r2)) - result = mk_antimirov_deriv_union(mk_antimirov_deriv(e, r1, path), mk_antimirov_deriv(e, r2, path)); + result = mk_regex_union_normalize(mk_antimirov_deriv(e, r1, path), mk_antimirov_deriv(e, r2, path)); else if (re().is_intersection(r, r1, r2)) result = mk_antimirov_deriv_intersection(e, mk_antimirov_deriv(e, r1, path), @@ -3213,11 +3213,6 @@ expr_ref seq_rewriter::mk_antimirov_deriv_intersection(expr* e, expr* d1, expr* VERIFY(m_util.is_seq(seq_sort, ele_sort)); expr_ref result(m()); expr* c, * a, * b; - //if (d1 == d2 || re().is_full_seq(d2) || re().is_empty(d1)) - // result = d1; - //else if (re().is_full_seq(d1) || re().is_empty(d2)) - // result = d2; - //else if (re().is_empty(d1)) result = d1; else if (re().is_empty(d2)) @@ -3242,16 +3237,14 @@ expr_ref seq_rewriter::mk_antimirov_deriv_intersection(expr* e, expr* d1, expr* result = mk_antimirov_deriv_restrict(e, d2, path); else if (re().is_union(d1, a, b)) // distribute intersection over the union in d1 - result = mk_antimirov_deriv_union(mk_antimirov_deriv_intersection(e, a, d2, path), + result = mk_regex_union_normalize(mk_antimirov_deriv_intersection(e, a, d2, path), mk_antimirov_deriv_intersection(e, b, d2, path)); else if (re().is_union(d2, a, b)) // distribute intersection over the union in d2 - result = mk_antimirov_deriv_union(mk_antimirov_deriv_intersection(e, d1, a, path), + result = mk_regex_union_normalize(mk_antimirov_deriv_intersection(e, d1, a, path), mk_antimirov_deriv_intersection(e, d1, b, path)); else - // in all other cases create the intersection regex - // TODO: flatten, order and merge d1 and d2 to maintain equality under similarity - result = (d1->get_id() <= d2->get_id() ? re().mk_inter(d1, d2) : re().mk_inter(d2, d1)); + result = mk_regex_inter_normalize(d1, d2); return result; } @@ -3263,7 +3256,7 @@ expr_ref seq_rewriter::mk_antimirov_deriv_concat(expr* d, expr* r) { if (m().is_ite(d, c, t, e)) result = m().mk_ite(c, mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r)); else if (re().is_union(d, t, e)) - result = re().mk_union(mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r)); + result = mk_regex_union_normalize(mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r)); else result = mk_re_append(d, r); return result; @@ -3289,10 +3282,9 @@ expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* elem, expr* d) { else if (m().is_ite(d, c, t, e)) result = m().mk_ite(c, mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e)); else if (re().is_union(d, t, e)) - //result = re().mk_inter(mk_antimirov_deriv_negate(t), mk_antimirov_deriv_negate(e)); result = mk_antimirov_deriv_intersection(elem, mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e), m().mk_true()); else if (re().is_intersection(d, t, e)) - result = re().mk_union(mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e)); + result = mk_regex_union_normalize(mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e)); else if (re().is_complement(d, t)) result = t; else @@ -3300,22 +3292,6 @@ expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* elem, expr* d) { return result; } -expr_ref seq_rewriter::mk_antimirov_deriv_union(expr* d1, expr* d2) { - expr_ref result(m()); - if (re().is_empty(d1) || re().is_full_seq(d2)) - result = d2; - else if (re().is_empty(d2) || re().is_full_seq(d1)) - result = d1; - else if (re().is_dot_plus(d1) && re().get_info(d2).min_length > 0) - result = d1; - else if (re().is_dot_plus(d2) && re().get_info(d1).min_length > 0) - result = d2; - else - // TODO: flatten, order and merge d1 and d2 to maintain equality under similarity - result = (d1->get_id() <= d2->get_id() ? re().mk_union(d1, d2) : re().mk_union(d2, d1)); - return result; -} - // restrict the guards of all conditionals id d and simplify the resulting derivative // restrict(if(c, a, b), cond) = if(c, restrict(a, cond & c), restrict(b, cond & ~c)) // restrict(a U b, cond) = restrict(a, cond) U restrict(b, cond) @@ -3344,17 +3320,212 @@ expr_ref seq_rewriter::mk_antimirov_deriv_restrict(expr* e, expr* d, expr* cond) else if (re().is_union(d, a, b)) { expr_ref a1(mk_antimirov_deriv_restrict(e, a, cond), m()); expr_ref b1(mk_antimirov_deriv_restrict(e, b, cond), m()); - if (a1 == b1 || re().is_empty(b1) || re().is_full_seq(a1)) - result = a1; - else if (re().is_empty(a1) || re().is_full_seq(b1)) - result = b1; - else - //TODO: merge - result = (a1->get_id() <= b1->get_id() ? re().mk_union(a1, b1) : re().mk_union(b1, a1)); + result = mk_regex_union_normalize(a1, b1); } return result; } +expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) { + VERIFY(m_util.is_re(r1)); + VERIFY(m_util.is_re(r2)); + expr_ref result(m()); + std::function test = [&](expr* t, expr*& a, expr*& b) { return re().is_union(t, a, b); }; + std::function compose = [&](expr* r1, expr* r2) { return re().mk_union(r1, r2); }; + if (r1 == r2 || re().is_empty(r2) || re().is_full_seq(r1)) + result = r1; + else if (re().is_empty(r1) || re().is_full_seq(r2)) + result = r2; + else if (re().is_dot_plus(r1) && re().get_info(r2).min_length > 0) + result = r1; + else if (re().is_dot_plus(r2) && re().get_info(r1).min_length > 0) + result = r2; + else + result = merge_regex_sets(r1, r2, re().mk_full_seq(r1->get_sort()), test, compose); + return result; +} + +expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) { + VERIFY(m_util.is_re(r1)); + VERIFY(m_util.is_re(r2)); + expr_ref result(m()); + std::function test = [&](expr* t, expr*& a, expr*& b) { return re().is_intersection(t, a, b); }; + std::function compose = [&](expr* r1, expr* r2) { return re().mk_inter(r1, r2); }; + if (r1 == r2 || re().is_empty(r1) || re().is_full_seq(r2)) + result = r1; + else if (re().is_empty(r2) || re().is_full_seq(r1)) + result = r2; + else if (re().is_epsilon(r1)) { + if (re().get_info(r2).nullable == l_true) + result = r1; + else if (re().get_info(r2).nullable == l_false) + result = re().mk_empty(r1->get_sort()); + else + result = merge_regex_sets(r1, r2, re().mk_empty(r1->get_sort()), test, compose); + } + else if (re().is_dot_plus(r1) && re().get_info(r2).min_length > 0) + result = r2; + else if (re().is_dot_plus(r2) && re().get_info(r1).min_length > 0) + result = r1; + else { + result = merge_regex_sets(r1, r2, re().mk_empty(r1->get_sort()), test, compose); + } + return result; +} + +expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit, + std::function& test, + std::function& compose) { + sort* seq_sort; + expr_ref result(unit, m()); + expr_ref_vector prefix(m()); + expr* a, * ar, * ar1, * b, * br, * br1; + VERIFY(m_util.is_re(r1, seq_sort)); + VERIFY(m_util.is_re(r2)); + SASSERT(r2->get_sort() == r1->get_sort()); + // Ordering of expressions used by merging, 0 means unordered, -1 means e1 < e2, 1 means e2 < e1 + auto compare = [&](expr* x, expr* y) { + expr* z; + unsigned int xid, yid; + // TODO: consider also the case of A{0,l}++B having the same id as A*++B + // in which case return 0 + if (x == y) + return 0; + + xid = (re().is_complement(x, z) ? z->get_id() : x->get_id()); + yid = (re().is_complement(y, z) ? z->get_id() : y->get_id()); + VERIFY(xid != yid); + return (xid < yid ? -1 : 1); + }; + auto composeresult = [&](expr* suffix) { + result = suffix; + while (!prefix.empty()) { + result = compose(prefix.back(), result); + prefix.pop_back(); + } + }; + if (r1 == r2) + result = r1; + else if (are_complements(r1, r2)) + // TODO: loops + result = unit; + else { + signed int k; + ar = r1; + br = r2; + while (true) {; + if (test(ar, a, ar1)) { + if (test(br, b, br1)) { + if (a == b) { + prefix.push_back(a); + ar = ar1; + br = br1; + } + else if (are_complements(a, b)) { + result = unit; + break; + } + else { + k = compare(a, b); + if (k == -1) { + // a < b + prefix.push_back(a); + ar = ar1; + } + else { + // b < a + prefix.push_back(b); + br = br1; + } + } + } + else { + // br is not decomposable + if (a == br) { + // result = prefix ++ ar + composeresult(ar); + break; + } + else if (are_complements(a, br)) { + result = unit; + break; + } + else { + k = compare(a, br); + if (k == -1) { + // a < br + prefix.push_back(a); + ar = ar1; + } + else { + // br < a, result = prefix ++ (br) ++ ar + prefix.push_back(br); + composeresult(ar); + break; + } + } + } + } + else { + // ar is not decomposable + if (test(br, b, br1)) { + if (ar == b) { + // result = prefix ++ br + composeresult(br); + break; + } + else if (are_complements(ar, b)) { + result = unit; + break; + } + else { + k = compare(ar, b); + if (k == -1) { + // ar < b, result = prefix ++ (ar) ++ br + prefix.push_back(ar); + composeresult(br); + break; + } + else { + // b < ar + prefix.push_back(b); + br = br1; + } + } + } + else { + // neither ar nor br is decomposable + if (ar == br) { + // result = prefix ++ ar + composeresult(ar); + break; + } + else if (are_complements(ar, br)) { + result = unit; + break; + } + else { + k = compare(ar, br); + if (k == -1) { + // ar < br, result = prefix ++ (ar) ++ (br) + prefix.push_back(ar); + composeresult(br); + break; + } + else { + // br < ar, result = prefix ++ (br) ++ (ar) + prefix.push_back(br); + composeresult(ar); + break; + } + } + } + } + } + } + return result; +} + + expr_ref seq_rewriter::mk_regex_reverse(expr* r) { expr* r1 = nullptr, * r2 = nullptr, * c = nullptr; unsigned lo = 0, hi = 0; @@ -4344,6 +4515,7 @@ br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) { r ++ [] -> [] r ++ "" -> r "" ++ r -> r + . ++ .* -> .+ to_re and star: (str.to_re s1) ++ (str.to_re s2) -> (str.to_re (s1 ++ s2)) @@ -4371,6 +4543,14 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) { result = a; return BR_DONE; } + if (re().is_full_char(a) && re().is_full_seq(b)) { + result = re().mk_plus(a); + return BR_DONE; + } + if (re().is_full_char(b) && re().is_full_seq(a)) { + result = re().mk_plus(b); + return BR_DONE; + } expr_ref a_str(m()); expr_ref b_str(m()); if (lift_str_from_to_re(a, a_str) && lift_str_from_to_re(b, b_str)) { @@ -4515,6 +4695,11 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) { result = mk_full(); return BR_DONE; } + + //just keep the union normalized + result = mk_regex_union_normalize(a, b); + return BR_DONE; + expr* a1 = nullptr, *a2 = nullptr; expr* b1 = nullptr, *b2 = nullptr; @@ -4643,9 +4828,17 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { result = mk_empty(); return BR_DONE; } + + // intersect and normalize + result = mk_regex_inter_normalize(a, b); + return BR_DONE; + expr* a1 = nullptr, *a2 = nullptr; expr* b1 = nullptr, *b2 = nullptr; + // the following rewrite rules do not seem to + // do the right thing when it comes to normalizing + // ensure intersection is right-associative // and swap-sort entries if (re().is_intersection(a, a1, a2)) { @@ -4696,7 +4889,7 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { } br_status seq_rewriter::mk_re_diff(expr* a, expr* b, expr_ref& result) { - result = re().mk_inter(a, re().mk_complement(b)); + result = mk_regex_inter_normalize(a, re().mk_complement(b)); return BR_REWRITE2; } @@ -4939,7 +5132,7 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) { flatten_and(cond, conds); expr* lhs = nullptr, *rhs = nullptr, *e1 = nullptr; if (u().is_char(elem)) { - unsigned ch = 0; + unsigned ch = 0, ch2 = 0; svector> ranges, ranges1; ranges.push_back(std::make_pair(0, u().max_char())); auto exclude_char = [&](unsigned ch) { @@ -4991,6 +5184,19 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) { else intersect(0, ch-1, ranges); } + else if (m().is_true(e) || (m().is_eq(e, lhs, rhs) && lhs == rhs)) { + // trivially true + continue; + } + else if (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch != ch2) { + // trivially true + continue; + } + else if (m().is_false(e) || (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && lhs == rhs)) { + // trivially false + cond = m().mk_false(); + return; + } else { all_ranges = false; break; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 9687797a0..c944e8f77 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -217,11 +217,19 @@ class seq_rewriter { expr_ref mk_antimirov_deriv_intersection(expr* elem, expr* d1, expr* d2, expr* path); expr_ref mk_antimirov_deriv_concat(expr* d, expr* r); expr_ref mk_antimirov_deriv_negate(expr* elem, expr* d); - expr_ref mk_antimirov_deriv_union(expr* d1, expr* d2); expr_ref mk_antimirov_deriv_restrict(expr* elem, expr* d1, expr* cond); expr_ref mk_regex_reverse(expr* r); expr_ref mk_regex_concat(expr* r1, expr* r2); + expr_ref merge_regex_sets(expr* r1, expr* r2, expr* unit, std::function& decompose, std::function& compose); + + // Apply simplifications and keep the representation normalized + // Assuming r1 and r2 are normalized + expr_ref mk_regex_union_normalize(expr* r1, expr* r2); + expr_ref mk_regex_inter_normalize(expr* r1, expr* r2); + + // elem is (:var 0) and path a condition that may have (:var 0) as a free variable + // simplify path, e.g., (:var 0) = 'a' & (:var 0) = 'b' is simplified to false expr_ref simplify_path(expr* elem, expr* path); bool lt_char(expr* ch1, expr* ch2); From 6cc9aa356296f594a7d79463dd21b563f81c199f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Dec 2021 19:36:18 -0800 Subject: [PATCH 022/209] prepare user propagator declared functions for likely Clemens use case --- src/muz/base/dl_rule.cpp | 2 +- src/smt/smt_context.h | 12 +++++++ src/smt/smt_kernel.cpp | 18 ++++++++++- src/smt/smt_kernel.h | 7 ++--- src/smt/theory_user_propagator.cpp | 20 ++++++++++++ src/smt/theory_user_propagator.h | 8 +++-- src/tactic/core/elim_uncnstr_tactic.cpp | 26 ++++++++++----- src/tactic/user_propagator_base.h | 42 +++++++++++++++++++++++++ 8 files changed, 120 insertions(+), 15 deletions(-) diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 9bd7a7adf..d0c872c3c 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -778,7 +778,7 @@ namespace datalog { tail_neg.push_back(false); } - SASSERT(tail.size()==tail_neg.size()); + SASSERT(tail.size() == tail_neg.size()); rule_ref old_r = r; r = mk(head, tail.size(), tail.data(), tail_neg.data(), old_r->name()); r->set_accounting_parent_object(m_ctx, old_r); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 700c2f211..fe9fe2054 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1728,6 +1728,18 @@ namespace smt { throw default_exception("user propagator must be initialized"); return m_user_propagator->add_expr(e); } + + void user_propagate_register_declared(user_propagator::register_created_eh_t& r) { + if (!m_user_propagator) + throw default_exception("user propagator must be initialized"); + m_user_propagator->register_declared(r); + } + + func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { + if (!m_user_propagator) + throw default_exception("user propagator must be initialized"); + return m_user_propagator->declare(name, n, domain, range); + } bool watches_fixed(enode* n) const; diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 4b321fd4a..1e97fa465 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -248,6 +248,14 @@ namespace smt { unsigned user_propagate_register(expr* e) { return m_kernel.user_propagate_register(e); } + + void user_propagate_register_declared(user_propagator::register_created_eh_t& r) { + m_kernel.user_propagate_register_declared(r); + } + + func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { + return m_kernel.user_propagate_declare(name, n, domain, range); + } }; @@ -477,4 +485,12 @@ namespace smt { return m_imp->user_propagate_register(e); } -}; + void kernel::user_propagate_register_declared(user_propagator::register_created_eh_t& r) { + m_imp->user_propagate_register_declared(r); + } + + func_decl* kernel::user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { + return m_imp->user_propagate_declare(name, n, domain, range); + } + +}; \ No newline at end of file diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 2259dd997..7af8f2fe6 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -301,12 +301,11 @@ namespace smt { void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh); - - /** - \brief register an expression to be tracked fro user propagation. - */ unsigned user_propagate_register(expr* e); + void user_propagate_register_declared(user_propagator::register_created_eh_t& r); + + func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range); /** \brief Return a reference to smt::context. diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index 2b50e07ab..75983b490 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -173,6 +173,26 @@ void theory_user_propagator::propagate() { m_qhead = qhead; } +func_decl* theory_user_propagator::declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { + if (!m_created_eh) + throw default_exception("event handler for dynamic expressions has to be registered before functions can be created"); + // ensure that declaration plugin is registered with m. + if (!m.has_plugin(get_id())) + m.register_plugin(get_id(), alloc(user_propagator::plugin)); + + func_decl_info info(get_id(), user_propagator::plugin::kind_t::OP_USER_PROPAGATE); + return m.mk_func_decl(name, n, domain, range, info); +} + +bool theory_user_propagator::internalize_atom(app* atom, bool gate_ctx) { + return internalize_term(atom); +} + +bool theory_user_propagator::internalize_term(app* term) { + NOT_IMPLEMENTED_YET(); + return false; +} + void theory_user_propagator::collect_statistics(::statistics & st) const { st.update("user-propagations", m_stats.m_num_propagations); st.update("user-watched", get_num_vars()); diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h index d007de6a0..0c5cdeef8 100644 --- a/src/smt/theory_user_propagator.h +++ b/src/smt/theory_user_propagator.h @@ -56,6 +56,8 @@ namespace smt { user_propagator::fixed_eh_t m_fixed_eh; user_propagator::eq_eh_t m_eq_eh; user_propagator::eq_eh_t m_diseq_eh; + user_propagator::register_created_eh_t m_created_eh; + user_propagator::context_obj* m_api_context = nullptr; unsigned m_qhead = 0; uint_set m_fixed; @@ -94,6 +96,8 @@ namespace smt { void register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; } void register_eq(user_propagator::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; } void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; } + void register_declared(user_propagator::register_created_eh_t& created_eh) { m_created_eh = created_eh; } + func_decl* declare(symbol const& name, unsigned n, sort* const* domain, sort* range); bool has_fixed() const { return (bool)m_fixed_eh; } @@ -103,8 +107,8 @@ namespace smt { void new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits); theory * mk_fresh(context * new_ctx) override; - bool internalize_atom(app * atom, bool gate_ctx) override { UNREACHABLE(); return false; } - bool internalize_term(app * term) override { UNREACHABLE(); return false; } + bool internalize_atom(app* atom, bool gate_ctx) override; + bool internalize_term(app* term) override; void new_eq_eh(theory_var v1, theory_var v2) override { if (m_eq_eh) m_eq_eh(m_user_context, this, v1, v2); } void new_diseq_eh(theory_var v1, theory_var v2) override { if (m_diseq_eh) m_diseq_eh(m_user_context, this, v1, v2); } bool use_diseqs() const override { return ((bool)m_diseq_eh); } diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 915a0f3c0..a5cbea932 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -38,6 +38,7 @@ class elim_uncnstr_tactic : public tactic { struct rw_cfg : public default_rewriter_cfg { bool m_produce_proofs; obj_hashtable & m_vars; + obj_hashtable& m_nonvars; ref m_mc; arith_util m_a_util; bv_util m_bv_util; @@ -49,10 +50,11 @@ class elim_uncnstr_tactic : public tactic { unsigned long long m_max_memory; unsigned m_max_steps; - rw_cfg(ast_manager & m, bool produce_proofs, obj_hashtable & vars, mc * _m, - unsigned long long max_memory, unsigned max_steps): + rw_cfg(ast_manager & m, bool produce_proofs, obj_hashtable & vars, obj_hashtable & nonvars, mc * _m, + unsigned long long max_memory, unsigned max_steps): m_produce_proofs(produce_proofs), m_vars(vars), + m_nonvars(nonvars), m_mc(_m), m_a_util(m), m_bv_util(m), @@ -73,7 +75,7 @@ class elim_uncnstr_tactic : public tactic { } bool uncnstr(expr * arg) const { - return m_vars.contains(arg); + return m_vars.contains(arg) && !m_nonvars.contains(arg); } bool uncnstr(unsigned num, expr * const * args) const { @@ -749,16 +751,17 @@ class elim_uncnstr_tactic : public tactic { class rw : public rewriter_tpl { rw_cfg m_cfg; public: - rw(ast_manager & m, bool produce_proofs, obj_hashtable & vars, mc * _m, + rw(ast_manager & m, bool produce_proofs, obj_hashtable & vars, obj_hashtable& nonvars, mc * _m, unsigned long long max_memory, unsigned max_steps): rewriter_tpl(m, produce_proofs, m_cfg), - m_cfg(m, produce_proofs, vars, _m, max_memory, max_steps) { + m_cfg(m, produce_proofs, vars, nonvars, _m, max_memory, max_steps) { } }; ast_manager & m_manager; ref m_mc; obj_hashtable m_vars; + obj_hashtable m_nonvars; scoped_ptr m_rw; unsigned m_num_elim_apps = 0; unsigned long long m_max_memory; @@ -774,12 +777,11 @@ class elim_uncnstr_tactic : public tactic { } void init_rw(bool produce_proofs) { - m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps); + m_rw = alloc(rw, m(), produce_proofs, m_vars, m_nonvars, m_mc.get(), m_max_memory, m_max_steps); } void run(goal_ref const & g, goal_ref_buffer & result) { bool produce_proofs = g->proofs_enabled(); - TRACE("goal", g->display(tout);); tactic_report report("elim-uncnstr", *g); m_vars.reset(); @@ -890,6 +892,16 @@ public: m_num_elim_apps = 0; } + unsigned user_propagate_register(expr* e) override { + m_nonvars.insert(e); + return 0; + } + + void user_propagate_clear() override { + m_nonvars.reset(); + } + + }; } diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h index 899722c2a..e5a2d282f 100644 --- a/src/tactic/user_propagator_base.h +++ b/src/tactic/user_propagator_base.h @@ -23,8 +23,33 @@ namespace user_propagator { typedef std::function fresh_eh_t; typedef std::function push_eh_t; typedef std::function pop_eh_t; + typedef std::function register_created_eh_t; + class plugin : public decl_plugin { + public: + + enum kind_t { OP_USER_PROPAGATE }; + + virtual ~plugin() {} + + virtual decl_plugin* mk_fresh() { return alloc(plugin); } + + family_id get_family_id() const { return m_family_id; } + + sort* mk_sort(decl_kind k, unsigned num_parameters, parameter const* parameters) override { + UNREACHABLE(); + return nullptr; + } + + func_decl* mk_func_decl(decl_kind k, unsigned num_parameters, parameter const* parameters, + unsigned arity, sort* const* domain, sort* range) { + UNREACHABLE(); + return nullptr; + } + + }; + class core { public: @@ -58,8 +83,25 @@ namespace user_propagator { throw default_exception("user-propagators are only supported on the SMT solver"); } + /** + * Create uninterpreted function for the user propagator. + * When expressions using the function are assigned values, generate a callback + * into a register_declared_eh(user_ctx, solver_ctx, declared_expr, declare_id) with arguments + * 1. context and callback context + * 2. declared_expr: expression using function that was declared at top. + * 3. declared_id: a unique identifier (unique within the current scope) to track the expression. + */ + virtual func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { + throw default_exception("user-propagators are only supported on the SMT solver"); + } + + virtual void user_propagate_register_created(register_created_eh_t& r) { + throw default_exception("user-propagators are only supported on the SMT solver"); + } + virtual void user_propagate_clear() { } + }; From 4e82a9af5fadb984aa18e0da885f631275a71bc5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Dec 2021 19:41:32 -0800 Subject: [PATCH 023/209] pin expressions --- src/ast/rewriter/seq_rewriter.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 045642019..e4d6ac7cd 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3326,8 +3326,9 @@ expr_ref seq_rewriter::mk_antimirov_deriv_restrict(expr* e, expr* d, expr* cond) } expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) { - VERIFY(m_util.is_re(r1)); - VERIFY(m_util.is_re(r2)); + expr_ref _r1(r1, m), _r2(r2, m); + ASSERT(m_util.is_re(r1)); + ASSERT(m_util.is_re(r2)); expr_ref result(m()); std::function test = [&](expr* t, expr*& a, expr*& b) { return re().is_union(t, a, b); }; std::function compose = [&](expr* r1, expr* r2) { return re().mk_union(r1, r2); }; @@ -3345,8 +3346,9 @@ expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) { } expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) { - VERIFY(m_util.is_re(r1)); - VERIFY(m_util.is_re(r2)); + expr_ref _r1(r1, m), _r2(r2, m); + ASSERT(m_util.is_re(r1)); + ASSERT(m_util.is_re(r2)); expr_ref result(m()); std::function test = [&](expr* t, expr*& a, expr*& b) { return re().is_intersection(t, a, b); }; std::function compose = [&](expr* r1, expr* r2) { return re().mk_inter(r1, r2); }; @@ -3380,7 +3382,7 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit, expr_ref_vector prefix(m()); expr* a, * ar, * ar1, * b, * br, * br1; VERIFY(m_util.is_re(r1, seq_sort)); - VERIFY(m_util.is_re(r2)); + ASSERT(m_util.is_re(r2)); SASSERT(r2->get_sort() == r1->get_sort()); // Ordering of expressions used by merging, 0 means unordered, -1 means e1 < e2, 1 means e2 < e1 auto compare = [&](expr* x, expr* y) { @@ -3393,7 +3395,7 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit, xid = (re().is_complement(x, z) ? z->get_id() : x->get_id()); yid = (re().is_complement(y, z) ? z->get_id() : y->get_id()); - VERIFY(xid != yid); + ASSERT(xid != yid); return (xid < yid ? -1 : 1); }; auto composeresult = [&](expr* suffix) { @@ -3942,7 +3944,7 @@ expr_ref seq_rewriter::mk_der_compl(expr* r) { */ expr_ref seq_rewriter::mk_der_cond(expr* cond, expr* ele, sort* seq_sort) { STRACE("seq_verbose", tout << "mk_der_cond: " - << mk_pp(cond, m()) << ", " << mk_pp(ele, m()) << std::endl;); + << mk_pp(cond, m()) << ", " << mk_pp(ele, m()) << std::endl;); sort *ele_sort = nullptr; VERIFY(u().is_seq(seq_sort, ele_sort)); SASSERT(ele_sort == ele->get_sort()); From 59742004448c83343923040c06c7e1ed41e45614 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Dec 2021 20:06:49 -0800 Subject: [PATCH 024/209] fixes to previous push and streamlining --- src/ast/rewriter/seq_rewriter.cpp | 184 ++++++++++++------------------ 1 file changed, 70 insertions(+), 114 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index e4d6ac7cd..16c2e57c8 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3326,9 +3326,9 @@ expr_ref seq_rewriter::mk_antimirov_deriv_restrict(expr* e, expr* d, expr* cond) } expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) { - expr_ref _r1(r1, m), _r2(r2, m); - ASSERT(m_util.is_re(r1)); - ASSERT(m_util.is_re(r2)); + expr_ref _r1(r1, m()), _r2(r2, m()); + SASSERT(m_util.is_re(r1)); + SASSERT(m_util.is_re(r2)); expr_ref result(m()); std::function test = [&](expr* t, expr*& a, expr*& b) { return re().is_union(t, a, b); }; std::function compose = [&](expr* r1, expr* r2) { return re().mk_union(r1, r2); }; @@ -3346,9 +3346,9 @@ expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) { } expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) { - expr_ref _r1(r1, m), _r2(r2, m); - ASSERT(m_util.is_re(r1)); - ASSERT(m_util.is_re(r2)); + expr_ref _r1(r1, m()), _r2(r2, m()); + SASSERT(m_util.is_re(r1)); + SASSERT(m_util.is_re(r2)); expr_ref result(m()); std::function test = [&](expr* t, expr*& a, expr*& b) { return re().is_intersection(t, a, b); }; std::function compose = [&](expr* r1, expr* r2) { return re().mk_inter(r1, r2); }; @@ -3382,7 +3382,7 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit, expr_ref_vector prefix(m()); expr* a, * ar, * ar1, * b, * br, * br1; VERIFY(m_util.is_re(r1, seq_sort)); - ASSERT(m_util.is_re(r2)); + SASSERT(m_util.is_re(r2)); SASSERT(r2->get_sort() == r1->get_sort()); // Ordering of expressions used by merging, 0 means unordered, -1 means e1 < e2, 1 means e2 < e1 auto compare = [&](expr* x, expr* y) { @@ -3395,7 +3395,7 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit, xid = (re().is_complement(x, z) ? z->get_id() : x->get_id()); yid = (re().is_complement(y, z) ? z->get_id() : y->get_id()); - ASSERT(xid != yid); + SASSERT(xid != yid); return (xid < yid ? -1 : 1); }; auto composeresult = [&](expr* suffix) { @@ -3404,124 +3404,80 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit, result = compose(prefix.back(), result); prefix.pop_back(); } + return result; }; if (r1 == r2) result = r1; else if (are_complements(r1, r2)) // TODO: loops - result = unit; + return expr_ref(unit, m()); else { - signed int k; ar = r1; br = r2; while (true) {; + if (ar == br) + return composeresult(ar); + + if (are_complements(ar, br)) + return expr_ref(unit, m()); + + if (test(br, b, br1) && !test(ar, a, ar1)) + std::swap(ar, br); + + if (test(br, b, br1)) { + VERIFY(test(ar, a, ar1)); + if (are_complements(a, b)) + return expr_ref(unit, m()); + switch (compare(a, b)) { + case 0: + // a == b + prefix.push_back(a); + ar = ar1; + br = br1; + break; + case -1: + // a < b + prefix.push_back(a); + ar = ar1; + break; + default: + // b < a + prefix.push_back(b); + br = br1; + break; + } + continue; + } + if (test(ar, a, ar1)) { - if (test(br, b, br1)) { - if (a == b) { - prefix.push_back(a); - ar = ar1; - br = br1; - } - else if (are_complements(a, b)) { - result = unit; - break; - } - else { - k = compare(a, b); - if (k == -1) { - // a < b - prefix.push_back(a); - ar = ar1; - } - else { - // b < a - prefix.push_back(b); - br = br1; - } - } - } - else { - // br is not decomposable - if (a == br) { - // result = prefix ++ ar - composeresult(ar); - break; - } - else if (are_complements(a, br)) { - result = unit; - break; - } - else { - k = compare(a, br); - if (k == -1) { - // a < br - prefix.push_back(a); - ar = ar1; - } - else { - // br < a, result = prefix ++ (br) ++ ar - prefix.push_back(br); - composeresult(ar); - break; - } - } - } - } - else { - // ar is not decomposable - if (test(br, b, br1)) { - if (ar == b) { - // result = prefix ++ br - composeresult(br); - break; - } - else if (are_complements(ar, b)) { - result = unit; - break; - } - else { - k = compare(ar, b); - if (k == -1) { - // ar < b, result = prefix ++ (ar) ++ br - prefix.push_back(ar); - composeresult(br); - break; - } - else { - // b < ar - prefix.push_back(b); - br = br1; - } - } - } - else { - // neither ar nor br is decomposable - if (ar == br) { - // result = prefix ++ ar - composeresult(ar); - break; - } - else if (are_complements(ar, br)) { - result = unit; - break; - } - else { - k = compare(ar, br); - if (k == -1) { - // ar < br, result = prefix ++ (ar) ++ (br) - prefix.push_back(ar); - composeresult(br); - break; - } - else { - // br < ar, result = prefix ++ (br) ++ (ar) - prefix.push_back(br); - composeresult(ar); - break; - } - } + // br is not decomposable + if (are_complements(a, br)) + return expr_ref(unit, m()); + switch (compare(a, br)) { + case 0: + // result = prefix ++ ar + return composeresult(ar); + case -1: + // a < br + prefix.push_back(a); + ar = ar1; + break; + case 1: + // br < a, result = prefix ++ (br) ++ ar + prefix.push_back(br); + return composeresult(ar); + default: + UNREACHABLE(); } + continue; } + + // neither ar nor br is decomposable + if (compare(ar, br) == -1) + std::swap(ar, br); + // br < ar, result = prefix ++ (br) ++ (ar) + prefix.push_back(br); + return composeresult(ar); } } return result; From 696345170410c79640f347948bc7126c41081ce4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Dec 2021 20:13:29 -0800 Subject: [PATCH 025/209] na --- src/ast/rewriter/seq_rewriter.cpp | 153 ++++++++++++++---------------- 1 file changed, 73 insertions(+), 80 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 16c2e57c8..12b5449eb 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3380,21 +3380,20 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit, sort* seq_sort; expr_ref result(unit, m()); expr_ref_vector prefix(m()); - expr* a, * ar, * ar1, * b, * br, * br1; + expr* a, * ar1, * b, * br1; VERIFY(m_util.is_re(r1, seq_sort)); SASSERT(m_util.is_re(r2)); SASSERT(r2->get_sort() == r1->get_sort()); // Ordering of expressions used by merging, 0 means unordered, -1 means e1 < e2, 1 means e2 < e1 auto compare = [&](expr* x, expr* y) { - expr* z; - unsigned int xid, yid; + expr* z = nullptr; // TODO: consider also the case of A{0,l}++B having the same id as A*++B // in which case return 0 if (x == y) return 0; - xid = (re().is_complement(x, z) ? z->get_id() : x->get_id()); - yid = (re().is_complement(y, z) ? z->get_id() : y->get_id()); + unsigned xid = (re().is_complement(x, z) ? z->get_id() : x->get_id()); + unsigned yid = (re().is_complement(y, z) ? z->get_id() : y->get_id()); SASSERT(xid != yid); return (xid < yid ? -1 : 1); }; @@ -3406,83 +3405,77 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit, } return result; }; - if (r1 == r2) - result = r1; - else if (are_complements(r1, r2)) - // TODO: loops - return expr_ref(unit, m()); - else { - ar = r1; - br = r2; - while (true) {; - if (ar == br) - return composeresult(ar); - - if (are_complements(ar, br)) - return expr_ref(unit, m()); - - if (test(br, b, br1) && !test(ar, a, ar1)) - std::swap(ar, br); - - if (test(br, b, br1)) { - VERIFY(test(ar, a, ar1)); - if (are_complements(a, b)) - return expr_ref(unit, m()); - switch (compare(a, b)) { - case 0: - // a == b - prefix.push_back(a); - ar = ar1; - br = br1; - break; - case -1: - // a < b - prefix.push_back(a); - ar = ar1; - break; - default: - // b < a - prefix.push_back(b); - br = br1; - break; - } - continue; - } - - if (test(ar, a, ar1)) { - // br is not decomposable - if (are_complements(a, br)) - return expr_ref(unit, m()); - switch (compare(a, br)) { - case 0: - // result = prefix ++ ar - return composeresult(ar); - case -1: - // a < br - prefix.push_back(a); - ar = ar1; - break; - case 1: - // br < a, result = prefix ++ (br) ++ ar - prefix.push_back(br); - return composeresult(ar); - default: - UNREACHABLE(); - } - continue; - } - - // neither ar nor br is decomposable - if (compare(ar, br) == -1) - std::swap(ar, br); - // br < ar, result = prefix ++ (br) ++ (ar) - prefix.push_back(br); + expr* ar = r1; + expr* br = r2; + while (true) { + if (ar == br) return composeresult(ar); - } - } - return result; -} + if (are_complements(ar, br)) + return expr_ref(unit, m()); + + if (test(br, b, br1) && !test(ar, a, ar1)) + std::swap(ar, br); + + // both ar, br are decomposable + if (test(br, b, br1)) { + VERIFY(test(ar, a, ar1)); + if (are_complements(a, b)) + return expr_ref(unit, m()); + switch (compare(a, b)) { + case 0: + // a == b + prefix.push_back(a); + ar = ar1; + br = br1; + break; + case -1: + // a < b + prefix.push_back(a); + ar = ar1; + break; + case 1: + // b < a + prefix.push_back(b); + br = br1; + break; + default: + UNREACHABLE(); + } + continue; + } + + // ar is decomposable, br is not decomposable + if (test(ar, a, ar1)) { + if (are_complements(a, br)) + return expr_ref(unit, m()); + switch (compare(a, br)) { + case 0: + // result = prefix ++ ar + return composeresult(ar); + case -1: + // a < br + prefix.push_back(a); + ar = ar1; + break; + case 1: + // br < a, result = prefix ++ (br) ++ ar + prefix.push_back(br); + return composeresult(ar); + default: + UNREACHABLE(); + } + continue; + } + + // neither ar nor br is decomposable + if (compare(ar, br) == -1) + std::swap(ar, br); + // br < ar, result = prefix ++ (br) ++ (ar) + prefix.push_back(br); + return composeresult(ar); + } +} expr_ref seq_rewriter::mk_regex_reverse(expr* r) { expr* r1 = nullptr, * r2 = nullptr, * c = nullptr; From 9c8800bdde04044edfce8d43e00693d5f3cd7d6e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Dec 2021 10:45:59 -0800 Subject: [PATCH 026/209] adding a new toy for Clemens Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.h | 4 +-- src/smt/smt_kernel.cpp | 9 +++--- src/smt/smt_kernel.h | 2 +- src/smt/smt_solver.cpp | 8 ++++++ src/smt/tactic/smt_tactic_core.cpp | 46 ++++++++++++++++++++++++++++-- src/smt/theory_user_propagator.cpp | 8 ++++-- src/smt/theory_user_propagator.h | 2 +- src/tactic/tactical.cpp | 8 ++++++ 8 files changed, 74 insertions(+), 13 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index fe9fe2054..ba8005484 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1729,10 +1729,10 @@ namespace smt { return m_user_propagator->add_expr(e); } - void user_propagate_register_declared(user_propagator::register_created_eh_t& r) { + void user_propagate_register_created(user_propagator::register_created_eh_t& r) { if (!m_user_propagator) throw default_exception("user propagator must be initialized"); - m_user_propagator->register_declared(r); + m_user_propagator->register_created(r); } func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 1e97fa465..13f7da7dc 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -249,8 +249,8 @@ namespace smt { return m_kernel.user_propagate_register(e); } - void user_propagate_register_declared(user_propagator::register_created_eh_t& r) { - m_kernel.user_propagate_register_declared(r); + void user_propagate_register_created(user_propagator::register_created_eh_t& r) { + m_kernel.user_propagate_register_created(r); } func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { @@ -305,7 +305,6 @@ namespace smt { return m_imp->get_formula(i); } - void kernel::push() { m_imp->push(); } @@ -485,8 +484,8 @@ namespace smt { return m_imp->user_propagate_register(e); } - void kernel::user_propagate_register_declared(user_propagator::register_created_eh_t& r) { - m_imp->user_propagate_register_declared(r); + void kernel::user_propagate_register_created(user_propagator::register_created_eh_t& r) { + m_imp->user_propagate_register_created(r); } func_decl* kernel::user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 7af8f2fe6..e8fdbc648 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -303,7 +303,7 @@ namespace smt { unsigned user_propagate_register(expr* e); - void user_propagate_register_declared(user_propagator::register_created_eh_t& r); + void user_propagate_register_created(user_propagator::register_created_eh_t& r); func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 9352e33f4..a755fe5ae 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -241,6 +241,14 @@ namespace { return m_context.user_propagate_register(e); } + void user_propagate_register_created(user_propagator::register_created_eh_t& c) override { + m_context.user_propagate_register_created(c); + } + + func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { + return m_context.user_propagate_declare(name, n, domain, range); + } + struct scoped_minimize_core { smt_solver& s; expr_ref_vector m_assumptions; diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp index 5cbe469fd..93ce81976 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -319,15 +319,21 @@ public: user_propagator::final_eh_t m_final_eh; user_propagator::eq_eh_t m_eq_eh; user_propagator::eq_eh_t m_diseq_eh; + user_propagator::register_created_eh_t m_created_eh; + expr_ref_vector m_vars; unsigned_vector m_var2internal; unsigned_vector m_internal2var; + unsigned_vector m_limit; + + user_propagator::push_eh_t i_push_eh; + user_propagator::pop_eh_t i_pop_eh; user_propagator::fixed_eh_t i_fixed_eh; user_propagator::final_eh_t i_final_eh; user_propagator::eq_eh_t i_eq_eh; user_propagator::eq_eh_t i_diseq_eh; - + user_propagator::register_created_eh_t i_created_eh; struct callback : public user_propagator::callback { @@ -403,15 +409,43 @@ public: m_ctx->user_propagate_register_diseq(i_diseq_eh); } + void init_i_created_eh() { + if (!m_created_eh) + return; + i_created_eh = [this](void* ctx, user_propagator::callback* cb, expr* e, unsigned i) { + unsigned j = m_vars.size(); + m_vars.push_back(e); + m_internal2var.setx(i, j, 0); + m_var2internal.setx(j, i, 0); + }; + m_ctx->user_propagate_register_created(i_created_eh); + } + + void init_i_push_pop() { + i_push_eh = [this](void* ctx) { + m_limit.push_back(m_vars.size()); + m_push_eh(ctx); + }; + i_pop_eh = [this](void* ctx, unsigned n) { + unsigned old_sz = m_limit.size() - n; + unsigned num_vars = m_limit[old_sz]; + m_vars.shrink(num_vars); + m_limit.shrink(old_sz); + m_pop_eh(ctx, n); + }; + } + void user_propagate_delay_init() { if (!m_user_ctx) return; - m_ctx->user_propagate_init(m_user_ctx, m_push_eh, m_pop_eh, m_fresh_eh); + init_i_push_pop(); + m_ctx->user_propagate_init(m_user_ctx, i_push_eh, i_pop_eh, m_fresh_eh); init_i_fixed_eh(); init_i_final_eh(); init_i_eq_eh(); init_i_diseq_eh(); + init_i_created_eh(); unsigned i = 0; for (expr* v : m_vars) { @@ -463,6 +497,14 @@ public: m_vars.push_back(e); return m_vars.size() - 1; } + + func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) override { + return m_ctx->user_propagate_declare(name, n, domain, range); + } + + void user_propagate_register_created(user_propagator::register_created_eh_t& created_eh) override { + m_ctx->user_propagate_register_created(created_eh); + } }; static tactic * mk_seq_smt_tactic(ast_manager& m, params_ref const & p) { diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index 75983b490..ac7968d45 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -189,8 +189,12 @@ bool theory_user_propagator::internalize_atom(app* atom, bool gate_ctx) { } bool theory_user_propagator::internalize_term(app* term) { - NOT_IMPLEMENTED_YET(); - return false; + for (auto arg : *term) + ensure_enode(arg); + unsigned v = add_expr(term); + if (m_created_eh) + m_created_eh(m_user_context, this, term, v); + return true; } void theory_user_propagator::collect_statistics(::statistics & st) const { diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h index 0c5cdeef8..a9b340d4a 100644 --- a/src/smt/theory_user_propagator.h +++ b/src/smt/theory_user_propagator.h @@ -96,7 +96,7 @@ namespace smt { void register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; } void register_eq(user_propagator::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; } void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; } - void register_declared(user_propagator::register_created_eh_t& created_eh) { m_created_eh = created_eh; } + void register_created(user_propagator::register_created_eh_t& created_eh) { m_created_eh = created_eh; } func_decl* declare(symbol const& name, unsigned n, sort* const* domain, sort* range); bool has_fixed() const { return (bool)m_fixed_eh; } diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 19009aa44..171a8314d 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -200,6 +200,14 @@ public: m_t2->user_propagate_clear(); } + void user_propagate_register_created(user_propagator::register_created_eh_t& created_eh) override { + m_t2->user_propagate_register_created(created_eh); + } + + func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) override { + return m_t2->user_propagate_declare(name, n, domain, range); + } + }; tactic * and_then(tactic * t1, tactic * t2) { From e1ffaa7faf1cdcde8e5a42769c5205121fc09e65 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Dec 2021 11:34:54 -0800 Subject: [PATCH 027/209] na Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 12b5449eb..13d8ef4fb 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3368,9 +3368,8 @@ expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) { result = r2; else if (re().is_dot_plus(r2) && re().get_info(r1).min_length > 0) result = r1; - else { - result = merge_regex_sets(r1, r2, re().mk_empty(r1->get_sort()), test, compose); - } + else + result = merge_regex_sets(r1, r2, re().mk_empty(r1->get_sort()), test, compose); return result; } @@ -3380,7 +3379,6 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit, sort* seq_sort; expr_ref result(unit, m()); expr_ref_vector prefix(m()); - expr* a, * ar1, * b, * br1; VERIFY(m_util.is_re(r1, seq_sort)); SASSERT(m_util.is_re(r2)); SASSERT(r2->get_sort() == r1->get_sort()); @@ -3414,6 +3412,7 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit, if (are_complements(ar, br)) return expr_ref(unit, m()); + expr* a, * ar1, * b, * br1; if (test(br, b, br1) && !test(ar, a, ar1)) std::swap(ar, br); From 8ca023d541b3a80fc1fcd8384dcb3ed9f71990fe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Dec 2021 16:12:47 -0800 Subject: [PATCH 028/209] expose propagate created --- src/api/api_solver.cpp | 19 +++++++++++++++++++ src/api/z3_api.h | 15 +++++++++++++++ src/ast/ast.h | 2 +- src/ast/recfun_decl_plugin.h | 2 +- src/ast/rewriter/maximize_ac_sharing.h | 2 +- src/smt/params/preprocessor_params.cpp | 4 ++-- src/smt/params/preprocessor_params.h | 6 +++--- src/smt/smt_setup.cpp | 8 ++++---- src/solver/assertions/asserted_formulas.cpp | 14 +++++++------- src/solver/assertions/asserted_formulas.h | 6 +++--- src/util/zstring.cpp | 8 ++++---- src/util/zstring.h | 14 +++++++------- 12 files changed, 67 insertions(+), 33 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index ea009b1bc..bb5ab9752 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -964,4 +964,23 @@ extern "C" { Z3_CATCH; } + void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh) { + Z3_TRY; + RESET_ERROR_CODE(); + user_propagator::register_created_eh_t c = (void(*)(void*, user_propagator::callback*, expr*, unsigned))created_eh; + to_solver_ref(s)->user_propagate_register_created(c); + Z3_CATCH; + } + + Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_solver s, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range) { + Z3_TRY; + LOG_Z3_solver_propagate_declare(c, s, name, n, domain, range); + RESET_ERROR_CODE(); + func_decl* f = to_solver_ref(s)->user_propagate_declare(to_symbol(name), n, to_sorts(domain), to_sort(range)); + mk_c(c)->save_ast_trail(f); + RETURN_Z3(of_func_decl(f)); + Z3_CATCH_RETURN(nullptr); + } + + }; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 767eebc43..899a5e7d1 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1430,6 +1430,7 @@ typedef void* Z3_fresh_eh(void* ctx, Z3_context new_context); typedef void Z3_fixed_eh(void* ctx, Z3_solver_callback cb, unsigned id, Z3_ast value); typedef void Z3_eq_eh(void* ctx, Z3_solver_callback cb, unsigned x, unsigned y); typedef void Z3_final_eh(void* ctx, Z3_solver_callback cb); +typedef void Z3_created_eh(void* ctx, Z3_solver_callback cb, Z3_ast e, unsigned id); /** @@ -6676,6 +6677,20 @@ extern "C" { */ void Z3_API Z3_solver_propagate_diseq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh); + /** + * \brief register a callback when a new expression with a registered function is used by the solver + * The registered function appears at the top level and is created using \c Z3_solver_declare. + */ + void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh); + + /** + \brief Create a registered function. Expressions used by the solver \c s that uses the registered function + at top level cause the callback propagate_created to be invoked. + + def_API('Z3_solver_propagate_declare', FUNC_DECL, (_in(CONTEXT), _in(SOLVER), _in(SYMBOL), _in(UINT), _in_array(3, SORT), _in(SORT))) + */ + Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_solver s, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range); + /** \brief register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Vector can be registered for propagation. diff --git a/src/ast/ast.h b/src/ast/ast.h index b04e67003..13898c2a6 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -845,7 +845,7 @@ class quantifier : public expr { char m_patterns_decls[0]; static unsigned get_obj_size(unsigned num_decls, unsigned num_patterns, unsigned num_no_patterns) { - return sizeof(quantifier) + num_decls * (sizeof(sort *) + sizeof(symbol)) + (num_patterns + num_no_patterns) * sizeof(expr*); + return (unsigned)(sizeof(quantifier) + num_decls * (sizeof(sort *) + sizeof(symbol)) + (num_patterns + num_no_patterns) * sizeof(expr*)); } quantifier(quantifier_kind k, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, sort* s, diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index 1146b7aaf..dd07e8baf 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -305,7 +305,7 @@ namespace recfun { m_pred(pred), m_cdef(&d), m_args(args) {} body_expansion(body_expansion const & from): m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(from.m_args) {} - body_expansion(body_expansion && from) : + body_expansion(body_expansion && from) noexcept : m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {} std::ostream& display(std::ostream& out) const; diff --git a/src/ast/rewriter/maximize_ac_sharing.h b/src/ast/rewriter/maximize_ac_sharing.h index 53e102b74..a2741aa89 100644 --- a/src/ast/rewriter/maximize_ac_sharing.h +++ b/src/ast/rewriter/maximize_ac_sharing.h @@ -46,7 +46,7 @@ class maximize_ac_sharing : public default_rewriter_cfg { entry(func_decl * d = nullptr, expr * arg1 = nullptr, expr * arg2 = nullptr):m_decl(d), m_arg1(arg1), m_arg2(arg2) { SASSERT((d == 0 && arg1 == 0 && arg2 == 0) || (d != 0 && arg1 != 0 && arg2 != 0)); - if (arg1->get_id() > arg2->get_id()) + if (arg1 && arg2 && arg1->get_id() > arg2->get_id()) std::swap(m_arg1, m_arg2); } diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp index a87d4959d..9fcb09843 100644 --- a/src/smt/params/preprocessor_params.cpp +++ b/src/smt/params/preprocessor_params.cpp @@ -40,8 +40,8 @@ void preprocessor_params::display(std::ostream & out) const { pattern_inference_params::display(out); bit_blaster_params::display(out); - DISPLAY_PARAM(m_lift_ite); - DISPLAY_PARAM(m_ng_lift_ite); + DISPLAY_PARAM((int)m_lift_ite); + DISPLAY_PARAM((int)m_ng_lift_ite); DISPLAY_PARAM(m_pull_cheap_ite); DISPLAY_PARAM(m_pull_nested_quantifiers); DISPLAY_PARAM(m_eliminate_term_ite); diff --git a/src/smt/params/preprocessor_params.h b/src/smt/params/preprocessor_params.h index a0d56182a..53568c366 100644 --- a/src/smt/params/preprocessor_params.h +++ b/src/smt/params/preprocessor_params.h @@ -21,7 +21,7 @@ Revision History: #include "params/pattern_inference_params.h" #include "params/bit_blaster_params.h" -enum lift_ite_kind { +enum class lift_ite_kind { LI_NONE, LI_CONSERVATIVE, LI_FULL @@ -50,8 +50,8 @@ struct preprocessor_params : public pattern_inference_params, public: preprocessor_params(params_ref const & p = params_ref()): - m_lift_ite(LI_NONE), - m_ng_lift_ite(LI_NONE), + m_lift_ite(lift_ite_kind::LI_NONE), + m_ng_lift_ite(lift_ite_kind::LI_NONE), m_pull_cheap_ite(false), m_pull_nested_quantifiers(false), m_eliminate_term_ite(false), diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index ba601272d..2d131c6ab 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -643,8 +643,8 @@ namespace smt { // It destroys the existing patterns. // m_params.m_macro_finder = true; - if (m_params.m_ng_lift_ite == LI_NONE) - m_params.m_ng_lift_ite = LI_CONSERVATIVE; + if (m_params.m_ng_lift_ite == lift_ite_kind::LI_NONE) + m_params.m_ng_lift_ite = lift_ite_kind::LI_CONSERVATIVE; TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";); m_context.register_plugin(alloc(smt::theory_i_arith, m_context)); setup_arrays(); @@ -668,8 +668,8 @@ namespace smt { m_params.m_qi_lazy_threshold = 20; // m_params.m_macro_finder = true; - if (m_params.m_ng_lift_ite == LI_NONE) - m_params.m_ng_lift_ite = LI_CONSERVATIVE; + if (m_params.m_ng_lift_ite == lift_ite_kind::LI_NONE) + m_params.m_ng_lift_ite = lift_ite_kind::LI_CONSERVATIVE; m_params.m_pi_max_multi_patterns = 10; //<< it was used for SMT-COMP m_params.m_array_lazy_ieq = true; m_params.m_array_lazy_ieq_delay = 4; diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index b3be7e8ab..1b8bfe9dd 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -71,12 +71,12 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_re void asserted_formulas::setup() { switch (m_smt_params.m_lift_ite) { - case LI_FULL: - m_smt_params.m_ng_lift_ite = LI_NONE; + case lift_ite_kind::LI_FULL: + m_smt_params.m_ng_lift_ite = lift_ite_kind::LI_NONE; break; - case LI_CONSERVATIVE: - if (m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE) - m_smt_params.m_ng_lift_ite = LI_NONE; + case lift_ite_kind::LI_CONSERVATIVE: + if (m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE) + m_smt_params.m_ng_lift_ite = lift_ite_kind::LI_NONE; break; default: break; @@ -281,8 +281,8 @@ void asserted_formulas::reduce() { if (!invoke(m_reduce_asserted_formulas)) return; if (!invoke(m_pull_nested_quantifiers)) return; if (!invoke(m_lift_ite)) return; - m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == LI_CONSERVATIVE); - m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE); + m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == lift_ite_kind::LI_CONSERVATIVE); + m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE); if (!invoke(m_ng_lift_ite)) return; if (!invoke(m_elim_term_ite)) return; if (!invoke(m_refine_inj_axiom)) return; diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h index 95848133c..23a4f5a0a 100644 --- a/src/solver/assertions/asserted_formulas.h +++ b/src/solver/assertions/asserted_formulas.h @@ -154,7 +154,7 @@ class asserted_formulas { public: elim_term_ite_fn(asserted_formulas& af): simplify_fmls(af, "elim-term-ite"), m_elim(af.m, af.m_defined_names) {} void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_elim(j.get_fml(), n, p); } - bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != LI_FULL; } + bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != lift_ite_kind::LI_FULL; } void post_op() override { af.m_formulas.append(m_elim.new_defs()); af.reduce_and_solve(); m_elim.reset(); } void push() { m_elim.push(); } void pop(unsigned n) { m_elim.pop(n); } @@ -187,8 +187,8 @@ class asserted_formulas { MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_smt_params.m_eliminate_bounds && af.has_quantifiers(), true); MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_smt_params.m_bb_quantifiers, true); MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_smt_params.m_simplify_bit2int, true); - MK_SIMPLIFIERF(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != LI_NONE, true); - MK_SIMPLIFIERF(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != LI_NONE, true); + MK_SIMPLIFIERF(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != lift_ite_kind::LI_NONE, true); + MK_SIMPLIFIERF(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != lift_ite_kind::LI_NONE, true); reduce_asserted_formulas_fn m_reduce_asserted_formulas; diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp index 534999606..e73c4cd52 100644 --- a/src/util/zstring.cpp +++ b/src/util/zstring.cpp @@ -87,12 +87,12 @@ zstring::zstring(char const* s) { string_encoding zstring::get_encoding() { if (gparams::get_value("encoding") == "unicode") - return unicode; + return string_encoding::unicode; if (gparams::get_value("encoding") == "bmp") - return bmp; + return string_encoding::bmp; if (gparams::get_value("encoding") == "ascii") - return ascii; - return unicode; + return string_encoding::ascii; + return string_encoding::unicode; } bool zstring::well_formed() const { diff --git a/src/util/zstring.h b/src/util/zstring.h index c5606b267..cb462238a 100644 --- a/src/util/zstring.h +++ b/src/util/zstring.h @@ -21,7 +21,7 @@ Author: #include "util/buffer.h" #include "util/rational.h" -enum string_encoding { +enum class string_encoding { ascii, // exactly 8 bits unicode, bmp // basic multilingual plane; exactly 16 bits @@ -41,22 +41,22 @@ public: static unsigned ascii_num_bits() { return 8; } static unsigned max_char() { switch (get_encoding()) { - case unicode: + case string_encoding::unicode: return unicode_max_char(); - case bmp: + case string_encoding::bmp: return bmp_max_char(); - case ascii: + case string_encoding::ascii: return ascii_max_char(); } return unicode_max_char(); } static unsigned num_bits() { switch (get_encoding()) { - case unicode: + case string_encoding::unicode: return unicode_num_bits(); - case bmp: + case string_encoding::bmp: return bmp_num_bits(); - case ascii: + case string_encoding::ascii: return ascii_num_bits(); } return unicode_num_bits(); From 4856581b68d63929d8913240c9ce25360c0fba8f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Dec 2021 16:40:19 -0800 Subject: [PATCH 029/209] na --- src/api/api_solver.cpp | 2 +- src/ast/recfun_decl_plugin.h | 2 +- src/cmd_context/pdecl.cpp | 24 ++++++++++++------------ src/cmd_context/pdecl.h | 16 ++++++++-------- src/smt/smt_context.h | 2 +- src/smt/smt_kernel.cpp | 4 ++-- src/smt/smt_kernel.h | 2 +- src/smt/smt_solver.cpp | 3 +-- src/smt/tactic/smt_tactic_core.cpp | 6 +++--- src/smt/theory_user_propagator.h | 6 +++--- src/tactic/tactical.cpp | 2 +- src/tactic/user_propagator_base.h | 4 ++-- 12 files changed, 36 insertions(+), 37 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index bb5ab9752..222fe7061 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -967,7 +967,7 @@ extern "C" { void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh) { Z3_TRY; RESET_ERROR_CODE(); - user_propagator::register_created_eh_t c = (void(*)(void*, user_propagator::callback*, expr*, unsigned))created_eh; + user_propagator::created_eh_t c = (void(*)(void*, user_propagator::callback*, expr*, unsigned))created_eh; to_solver_ref(s)->user_propagate_register_created(c); Z3_CATCH; } diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index dd07e8baf..70447ff67 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -305,7 +305,7 @@ namespace recfun { m_pred(pred), m_cdef(&d), m_args(args) {} body_expansion(body_expansion const & from): m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(from.m_args) {} - body_expansion(body_expansion && from) noexcept : + body_expansion(body_expansion && from) noexcept : m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {} std::ostream& display(std::ostream& out) const; diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index e34c7e38a..7a93382e9 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -416,9 +416,9 @@ void psort_builtin_decl::display(std::ostream & out) const { void ptype::display(std::ostream & out, pdatatype_decl const * const * dts) const { switch (kind()) { - case PTR_PSORT: get_psort()->display(out); break; - case PTR_REC_REF: out << dts[get_idx()]->get_name(); break; - case PTR_MISSING_REF: out << get_missing_ref(); break; + case ptype_kind::PTR_PSORT: get_psort()->display(out); break; + case ptype_kind::PTR_REC_REF: out << dts[get_idx()]->get_name(); break; + case ptype_kind::PTR_MISSING_REF: out << get_missing_ref(); break; } } @@ -426,19 +426,19 @@ paccessor_decl::paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & pdecl(id, num_params), m_name(n), m_type(r) { - if (m_type.kind() == PTR_PSORT) { + if (m_type.kind() == ptype_kind::PTR_PSORT) { m.inc_ref(r.get_psort()); } } void paccessor_decl::finalize(pdecl_manager & m) { - if (m_type.kind() == PTR_PSORT) { + if (m_type.kind() == ptype_kind::PTR_PSORT) { m.lazy_dec_ref(m_type.get_psort()); } } bool paccessor_decl::has_missing_refs(symbol & missing) const { - if (m_type.kind() == PTR_MISSING_REF) { + if (m_type.kind() == ptype_kind::PTR_MISSING_REF) { missing = m_type.get_missing_ref(); return true; } @@ -446,14 +446,14 @@ bool paccessor_decl::has_missing_refs(symbol & missing) const { } bool paccessor_decl::fix_missing_refs(dictionary const & symbol2idx, symbol & missing) { - TRACE("fix_missing_refs", tout << "m_type.kind(): " << m_type.kind() << "\n"; - if (m_type.kind() == PTR_MISSING_REF) tout << m_type.get_missing_ref() << "\n";); - if (m_type.kind() != PTR_MISSING_REF) + TRACE("fix_missing_refs", tout << "m_type.kind(): " << (int)m_type.kind() << "\n"; + if (m_type.kind() == ptype_kind::PTR_MISSING_REF) tout << m_type.get_missing_ref() << "\n";); + if (m_type.kind() != ptype_kind::PTR_MISSING_REF) return true; int idx; if (symbol2idx.find(m_type.get_missing_ref(), idx)) { m_type = ptype(idx); - SASSERT(m_type.kind() == PTR_REC_REF); + SASSERT(m_type.kind() == ptype_kind::PTR_REC_REF); return true; } missing = m_type.get_missing_ref(); @@ -462,8 +462,8 @@ bool paccessor_decl::fix_missing_refs(dictionary const & symbol2idx, symbol accessor_decl * paccessor_decl::instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s) { switch (m_type.kind()) { - case PTR_REC_REF: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_idx())); - case PTR_PSORT: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_psort()->instantiate(m, n, s))); + case ptype_kind::PTR_REC_REF: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_idx())); + case ptype_kind::PTR_PSORT: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_psort()->instantiate(m, n, s))); default: // missing refs must have been eliminated. UNREACHABLE(); diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index e5b630902..3a1db06c1 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -157,7 +157,7 @@ class pdatatype_decl; class pconstructor_decl; class paccessor_decl; -enum ptype_kind { +enum class ptype_kind { PTR_PSORT, // psort PTR_REC_REF, // recursive reference PTR_MISSING_REF // a symbol, it is useful for building parsers. @@ -171,14 +171,14 @@ class ptype { }; symbol m_missing_ref; public: - ptype():m_kind(PTR_PSORT), m_sort(nullptr) {} - ptype(int idx):m_kind(PTR_REC_REF), m_idx(idx) {} - ptype(psort * s):m_kind(PTR_PSORT), m_sort(s) {} - ptype(symbol const & s):m_kind(PTR_MISSING_REF), m_missing_ref(s) {} + ptype():m_kind(ptype_kind::PTR_PSORT), m_sort(nullptr) {} + ptype(int idx):m_kind(ptype_kind::PTR_REC_REF), m_idx(idx) {} + ptype(psort * s):m_kind(ptype_kind::PTR_PSORT), m_sort(s) {} + ptype(symbol const & s):m_kind(ptype_kind::PTR_MISSING_REF), m_sort(nullptr), m_missing_ref(s) {} ptype_kind kind() const { return m_kind; } - psort * get_psort() const { SASSERT(kind() == PTR_PSORT); return m_sort; } - int get_idx() const { SASSERT(kind() == PTR_REC_REF); return m_idx; } - symbol const & get_missing_ref() const { SASSERT(kind() == PTR_MISSING_REF); return m_missing_ref; } + psort * get_psort() const { SASSERT(kind() == ptype_kind::PTR_PSORT); return m_sort; } + int get_idx() const { SASSERT(kind() == ptype_kind::PTR_REC_REF); return m_idx; } + symbol const & get_missing_ref() const { SASSERT(kind() == ptype_kind::PTR_MISSING_REF); return m_missing_ref; } void display(std::ostream & out, pdatatype_decl const * const * dts) const; }; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index ba8005484..85f59d26c 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1729,7 +1729,7 @@ namespace smt { return m_user_propagator->add_expr(e); } - void user_propagate_register_created(user_propagator::register_created_eh_t& r) { + void user_propagate_register_created(user_propagator::created_eh_t& r) { if (!m_user_propagator) throw default_exception("user propagator must be initialized"); m_user_propagator->register_created(r); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 13f7da7dc..b26823291 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -249,7 +249,7 @@ namespace smt { return m_kernel.user_propagate_register(e); } - void user_propagate_register_created(user_propagator::register_created_eh_t& r) { + void user_propagate_register_created(user_propagator::created_eh_t& r) { m_kernel.user_propagate_register_created(r); } @@ -484,7 +484,7 @@ namespace smt { return m_imp->user_propagate_register(e); } - void kernel::user_propagate_register_created(user_propagator::register_created_eh_t& r) { + void kernel::user_propagate_register_created(user_propagator::created_eh_t& r) { m_imp->user_propagate_register_created(r); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index e8fdbc648..0296c29a6 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -303,7 +303,7 @@ namespace smt { unsigned user_propagate_register(expr* e); - void user_propagate_register_created(user_propagator::register_created_eh_t& r); + void user_propagate_register_created(user_propagator::created_eh_t& r); func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index a755fe5ae..fe4aec944 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -200,7 +200,6 @@ namespace { return m_context.check(num_assumptions, assumptions); } - lbool check_sat_cc_core(expr_ref_vector const& cube, vector const& clauses) override { return m_context.check(cube, clauses); } @@ -241,7 +240,7 @@ namespace { return m_context.user_propagate_register(e); } - void user_propagate_register_created(user_propagator::register_created_eh_t& c) override { + void user_propagate_register_created(user_propagator::created_eh_t& c) override { m_context.user_propagate_register_created(c); } diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp index 93ce81976..d67e430e2 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -319,7 +319,7 @@ public: user_propagator::final_eh_t m_final_eh; user_propagator::eq_eh_t m_eq_eh; user_propagator::eq_eh_t m_diseq_eh; - user_propagator::register_created_eh_t m_created_eh; + user_propagator::created_eh_t m_created_eh; expr_ref_vector m_vars; unsigned_vector m_var2internal; @@ -333,7 +333,7 @@ public: user_propagator::final_eh_t i_final_eh; user_propagator::eq_eh_t i_eq_eh; user_propagator::eq_eh_t i_diseq_eh; - user_propagator::register_created_eh_t i_created_eh; + user_propagator::created_eh_t i_created_eh; struct callback : public user_propagator::callback { @@ -502,7 +502,7 @@ public: return m_ctx->user_propagate_declare(name, n, domain, range); } - void user_propagate_register_created(user_propagator::register_created_eh_t& created_eh) override { + void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override { m_ctx->user_propagate_register_created(created_eh); } }; diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h index a9b340d4a..0189b13cb 100644 --- a/src/smt/theory_user_propagator.h +++ b/src/smt/theory_user_propagator.h @@ -56,7 +56,7 @@ namespace smt { user_propagator::fixed_eh_t m_fixed_eh; user_propagator::eq_eh_t m_eq_eh; user_propagator::eq_eh_t m_diseq_eh; - user_propagator::register_created_eh_t m_created_eh; + user_propagator::created_eh_t m_created_eh; user_propagator::context_obj* m_api_context = nullptr; unsigned m_qhead = 0; @@ -96,7 +96,7 @@ namespace smt { void register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; } void register_eq(user_propagator::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; } void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; } - void register_created(user_propagator::register_created_eh_t& created_eh) { m_created_eh = created_eh; } + void register_created(user_propagator::created_eh_t& created_eh) { m_created_eh = created_eh; } func_decl* declare(symbol const& name, unsigned n, sort* const* domain, sort* range); bool has_fixed() const { return (bool)m_fixed_eh; } @@ -123,7 +123,7 @@ namespace smt { void collect_statistics(::statistics & st) const override; model_value_proc * mk_value(enode * n, model_generator & mg) override { return nullptr; } void init_model(model_generator & m) override {} - bool include_func_interp(func_decl* f) override { return false; } + bool include_func_interp(func_decl* f) override { return true; } bool can_propagate() override; void propagate() override; void display(std::ostream& out) const override {} diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 171a8314d..07fc88b37 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -200,7 +200,7 @@ public: m_t2->user_propagate_clear(); } - void user_propagate_register_created(user_propagator::register_created_eh_t& created_eh) override { + void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override { m_t2->user_propagate_register_created(created_eh); } diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h index e5a2d282f..db9ca88fd 100644 --- a/src/tactic/user_propagator_base.h +++ b/src/tactic/user_propagator_base.h @@ -23,7 +23,7 @@ namespace user_propagator { typedef std::function fresh_eh_t; typedef std::function push_eh_t; typedef std::function pop_eh_t; - typedef std::function register_created_eh_t; + typedef std::function created_eh_t; class plugin : public decl_plugin { @@ -95,7 +95,7 @@ namespace user_propagator { throw default_exception("user-propagators are only supported on the SMT solver"); } - virtual void user_propagate_register_created(register_created_eh_t& r) { + virtual void user_propagate_register_created(created_eh_t& r) { throw default_exception("user-propagators are only supported on the SMT solver"); } From f0740bdf607520ae1d687e45534421e7a7a5ce1e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 18 Dec 2021 10:56:42 -0800 Subject: [PATCH 030/209] move user propagte declare to context level declaration of user propagate functions are declared at context level instead of at solver scope. --- src/api/api_solver.cpp | 13 +- src/api/z3_api.h | 14 +- src/sat/sat_solver/inc_sat_solver.cpp | 4 +- src/sat/smt/euf_solver.h | 2 +- src/smt/smt_context.h | 8 +- src/smt/smt_kernel.cpp | 302 ++++-------------------- src/smt/smt_kernel.h | 4 +- src/smt/smt_solver.cpp | 8 +- src/smt/tactic/smt_tactic_core.cpp | 8 +- src/smt/theory_user_propagator.cpp | 12 +- src/smt/theory_user_propagator.h | 1 - src/solver/tactic2solver.cpp | 4 +- src/tactic/core/elim_uncnstr_tactic.cpp | 2 +- src/tactic/core/reduce_args_tactic.cpp | 4 +- src/tactic/tactic.h | 2 +- src/tactic/tactical.cpp | 12 +- src/tactic/user_propagator_base.h | 16 +- 17 files changed, 92 insertions(+), 324 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 222fe7061..8e8360cd3 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -944,7 +944,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_propagate_register(c, s, e); RESET_ERROR_CODE(); - return to_solver_ref(s)->user_propagate_register(to_expr(e)); + return to_solver_ref(s)->user_propagate_register_expr(to_expr(e)); Z3_CATCH_RETURN(0); } @@ -972,11 +972,16 @@ extern "C" { Z3_CATCH; } - Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_solver s, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range) { + Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range) { Z3_TRY; - LOG_Z3_solver_propagate_declare(c, s, name, n, domain, range); + LOG_Z3_solver_propagate_declare(c, name, n, domain, range); RESET_ERROR_CODE(); - func_decl* f = to_solver_ref(s)->user_propagate_declare(to_symbol(name), n, to_sorts(domain), to_sort(range)); + ast_manager& m = mk_c(c)->m(); + family_id fid = m.mk_family_id(user_propagator::plugin::name()); + if (!m.has_plugin(fid)) + m.register_plugin(fid, alloc(user_propagator::plugin)); + func_decl_info info(fid, user_propagator::plugin::kind_t::OP_USER_PROPAGATE); + func_decl* f = m.mk_func_decl(to_symbol(name), n, to_sorts(domain), to_sort(range), info); mk_c(c)->save_ast_trail(f); RETURN_Z3(of_func_decl(f)); Z3_CATCH_RETURN(nullptr); diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 899a5e7d1..0ac70ee98 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6679,17 +6679,21 @@ extern "C" { /** * \brief register a callback when a new expression with a registered function is used by the solver - * The registered function appears at the top level and is created using \c Z3_solver_declare. + * The registered function appears at the top level and is created using \ref Z3_propagate_solver_declare. */ void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh); /** - \brief Create a registered function. Expressions used by the solver \c s that uses the registered function - at top level cause the callback propagate_created to be invoked. + Create uninterpreted function declaration for the user propagator. + When expressions using the function are created by the solver invoke a callback + to \ref \Z3_solver_progate_created with arguments + 1. context and callback solve + 2. declared_expr: expression using function that was used as the top-level symbol + 3. declared_id: a unique identifier (unique within the current scope) to track the expression. - def_API('Z3_solver_propagate_declare', FUNC_DECL, (_in(CONTEXT), _in(SOLVER), _in(SYMBOL), _in(UINT), _in_array(3, SORT), _in(SORT))) + def_API('Z3_solver_propagate_declare', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT))) */ - Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_solver s, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range); + Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range); /** \brief register an expression to propagate on with the solver. diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index ea81f0c4d..97a319382 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -683,8 +683,8 @@ public: ensure_euf()->user_propagate_register_diseq(diseq_eh); } - unsigned user_propagate_register(expr* e) override { - return ensure_euf()->user_propagate_register(e); + unsigned user_propagate_register_expr(expr* e) override { + return ensure_euf()->user_propagate_register_expr(e); } private: diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index d70206d11..384e15822 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -425,7 +425,7 @@ namespace euf { check_for_user_propagator(); m_user_propagator->register_diseq(diseq_eh); } - unsigned user_propagate_register(expr* e) { + unsigned user_propagate_register_expr(expr* e) { check_for_user_propagator(); return m_user_propagator->add_expr(e); } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 85f59d26c..4a764e975 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1723,7 +1723,7 @@ namespace smt { m_user_propagator->register_diseq(diseq_eh); } - unsigned user_propagate_register(expr* e) { + unsigned user_propagate_register_expr(expr* e) { if (!m_user_propagator) throw default_exception("user propagator must be initialized"); return m_user_propagator->add_expr(e); @@ -1735,12 +1735,6 @@ namespace smt { m_user_propagator->register_created(r); } - func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { - if (!m_user_propagator) - throw default_exception("user propagator must be initialized"); - return m_user_propagator->declare(name, n, domain, range); - } - bool watches_fixed(enode* n) const; void assign_fixed(enode* n, expr* val, unsigned sz, literal const* explain); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index b26823291..fdfbbb97a 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -49,14 +49,6 @@ namespace smt { return m_kernel.get_manager(); } - bool set_logic(symbol logic) { - return m_kernel.set_logic(logic); - } - - void set_progress_callback(progress_callback * callback) { - return m_kernel.set_progress_callback(callback); - } - void display(std::ostream & out) const { // m_kernel.display(out); <<< for external users it is just junk // TODO: it will be replaced with assertion_stack.display @@ -67,195 +59,7 @@ namespace smt { out << "\n " << mk_ismt2_pp(f, m(), 2); } out << ")"; - } - - void assert_expr(expr * e) { - TRACE("smt_kernel", tout << "assert:\n" << mk_ismt2_pp(e, m()) << "\n";); - m_kernel.assert_expr(e); - } - - void assert_expr(expr * e, proof * pr) { - m_kernel.assert_expr(e, pr); - } - - unsigned size() const { - return m_kernel.get_num_asserted_formulas(); - } - - void get_formulas(ptr_vector& fmls) const { - m_kernel.get_asserted_formulas(fmls); - } - - expr* get_formula(unsigned i) const { - return m_kernel.get_asserted_formula(i); - } - - void push() { - TRACE("smt_kernel", tout << "push()\n";); - m_kernel.push(); - } - - void pop(unsigned num_scopes) { - TRACE("smt_kernel", tout << "pop()\n";); - m_kernel.pop(num_scopes); - } - - unsigned get_scope_level() const { - return m_kernel.get_scope_level(); - } - - lbool setup_and_check() { - return m_kernel.setup_and_check(); - } - - bool inconsistent() { - return m_kernel.inconsistent(); - } - - lbool check(unsigned num_assumptions, expr * const * assumptions) { - return m_kernel.check(num_assumptions, assumptions); - } - - lbool check(expr_ref_vector const& cube, vector const& clause) { - return m_kernel.check(cube, clause); - } - - lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) { - return m_kernel.get_consequences(assumptions, vars, conseq, unfixed); - } - - lbool preferred_sat(expr_ref_vector const& asms, vector& cores) { - return m_kernel.preferred_sat(asms, cores); - } - - lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { - return m_kernel.find_mutexes(vars, mutexes); - } - - void get_model(model_ref & m) { - m_kernel.get_model(m); - } - - proof * get_proof() { - return m_kernel.get_proof(); - } - - unsigned get_unsat_core_size() const { - return m_kernel.get_unsat_core_size(); - } - - expr * get_unsat_core_expr(unsigned idx) const { - return m_kernel.get_unsat_core_expr(idx); - } - - void get_levels(ptr_vector const& vars, unsigned_vector& depth) { - m_kernel.get_levels(vars, depth); - } - - expr_ref_vector get_trail() { - return m_kernel.get_trail(); - } - - failure last_failure() const { - return m_kernel.get_last_search_failure(); - } - - std::string last_failure_as_string() const { - return m_kernel.last_failure_as_string(); - } - - void set_reason_unknown(char const* msg) { - m_kernel.set_reason_unknown(msg); - } - - void get_assignments(expr_ref_vector & result) { - m_kernel.get_assignments(result); - } - - void get_relevant_labels(expr * cnstr, buffer & result) { - m_kernel.get_relevant_labels(cnstr, result); - } - - void get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) { - m_kernel.get_relevant_labeled_literals(at_lbls, result); - } - - void get_relevant_literals(expr_ref_vector & result) { - m_kernel.get_relevant_literals(result); - } - - void get_guessed_literals(expr_ref_vector & result) { - m_kernel.get_guessed_literals(result); - } - - expr_ref next_cube() { - lookahead lh(m_kernel); - return lh.choose(); - } - - expr_ref_vector cubes(unsigned depth) { - lookahead lh(m_kernel); - return lh.choose_rec(depth); - } - - void collect_statistics(::statistics & st) const { - m_kernel.collect_statistics(st); - } - - void reset_statistics() { - } - - void display_statistics(std::ostream & out) const { - m_kernel.display_statistics(out); - } - - void display_istatistics(std::ostream & out) const { - m_kernel.display_istatistics(out); - } - - bool canceled() { - return m_kernel.get_cancel_flag(); - } - - void updt_params(params_ref const & p) { - m_kernel.updt_params(p); - } - - void user_propagate_init( - void* ctx, - user_propagator::push_eh_t& push_eh, - user_propagator::pop_eh_t& pop_eh, - user_propagator::fresh_eh_t& fresh_eh) { - m_kernel.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); - } - - void user_propagate_register_final(user_propagator::final_eh_t& final_eh) { - m_kernel.user_propagate_register_final(final_eh); - } - - void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) { - m_kernel.user_propagate_register_fixed(fixed_eh); - } - - void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) { - m_kernel.user_propagate_register_eq(eq_eh); - } - - void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) { - m_kernel.user_propagate_register_diseq(diseq_eh); - } - - unsigned user_propagate_register(expr* e) { - return m_kernel.user_propagate_register(e); - } - - void user_propagate_register_created(user_propagator::created_eh_t& r) { - m_kernel.user_propagate_register_created(r); - } - - func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { - return m_kernel.user_propagate_declare(name, n, domain, range); - } + } }; @@ -268,7 +72,7 @@ namespace smt { } ast_manager & kernel::m() const { - return m_imp->m(); + return m_imp->m_kernel.get_manager(); } void kernel::copy(kernel& src, kernel& dst) { @@ -276,45 +80,44 @@ namespace smt { } bool kernel::set_logic(symbol logic) { - return m_imp->set_logic(logic); + return m_imp->m_kernel.set_logic(logic); } void kernel::set_progress_callback(progress_callback * callback) { - m_imp->set_progress_callback(callback); + m_imp->m_kernel.set_progress_callback(callback); } void kernel::assert_expr(expr * e) { - m_imp->assert_expr(e); + m_imp->m_kernel.assert_expr(e); } void kernel::assert_expr(expr_ref_vector const& es) { - for (unsigned i = 0; i < es.size(); ++i) { - m_imp->assert_expr(es[i]); - } + for (unsigned i = 0; i < es.size(); ++i) + m_imp->m_kernel.assert_expr(es[i]); } void kernel::assert_expr(expr * e, proof * pr) { - m_imp->assert_expr(e, pr); + m_imp->m_kernel.assert_expr(e, pr); } unsigned kernel::size() const { - return m_imp->size(); + return m_imp->m_kernel.get_num_asserted_formulas(); } expr* kernel::get_formula(unsigned i) const { - return m_imp->get_formula(i); + return m_imp->m_kernel.get_asserted_formula(i); } void kernel::push() { - m_imp->push(); + m_imp->m_kernel.push(); } void kernel::pop(unsigned num_scopes) { - m_imp->pop(num_scopes); + m_imp->m_kernel.pop(num_scopes); } unsigned kernel::get_scope_level() const { - return m_imp->get_scope_level(); + return m_imp->m_kernel.get_scope_level(); } void kernel::reset() { @@ -326,89 +129,91 @@ namespace smt { } bool kernel::inconsistent() { - return m_imp->inconsistent(); + return m_imp->m_kernel.inconsistent(); } lbool kernel::setup_and_check() { - return m_imp->setup_and_check(); + return m_imp->m_kernel.setup_and_check(); } lbool kernel::check(unsigned num_assumptions, expr * const * assumptions) { - lbool r = m_imp->check(num_assumptions, assumptions); + lbool r = m_imp->m_kernel.check(num_assumptions, assumptions); TRACE("smt_kernel", tout << "check result: " << r << "\n";); return r; } lbool kernel::check(expr_ref_vector const& cube, vector const& clauses) { - return m_imp->check(cube, clauses); + return m_imp->m_kernel.check(cube, clauses); } lbool kernel::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed) { - return m_imp->get_consequences(assumptions, vars, conseq, unfixed); + return m_imp->m_kernel.get_consequences(assumptions, vars, conseq, unfixed); } lbool kernel::preferred_sat(expr_ref_vector const& asms, vector& cores) { - return m_imp->preferred_sat(asms, cores); + return m_imp->m_kernel.preferred_sat(asms, cores); } lbool kernel::find_mutexes(expr_ref_vector const& vars, vector& mutexes) { - return m_imp->find_mutexes(vars, mutexes); + return m_imp->m_kernel.find_mutexes(vars, mutexes); } void kernel::get_model(model_ref & m) { - m_imp->get_model(m); + m_imp->m_kernel.get_model(m); } proof * kernel::get_proof() { - return m_imp->get_proof(); + return m_imp->m_kernel.get_proof(); } unsigned kernel::get_unsat_core_size() const { - return m_imp->get_unsat_core_size(); + return m_imp->m_kernel.get_unsat_core_size(); } expr * kernel::get_unsat_core_expr(unsigned idx) const { - return m_imp->get_unsat_core_expr(idx); + return m_imp->m_kernel.get_unsat_core_expr(idx); } failure kernel::last_failure() const { - return m_imp->last_failure(); + return m_imp->m_kernel.get_last_search_failure(); } std::string kernel::last_failure_as_string() const { - return m_imp->last_failure_as_string(); + return m_imp->m_kernel.last_failure_as_string(); } void kernel::set_reason_unknown(char const* msg) { - m_imp->set_reason_unknown(msg); + m_imp->m_kernel.set_reason_unknown(msg); } void kernel::get_assignments(expr_ref_vector & result) { - m_imp->get_assignments(result); + m_imp->m_kernel.get_assignments(result); } void kernel::get_relevant_labels(expr * cnstr, buffer & result) { - m_imp->get_relevant_labels(cnstr, result); + m_imp->m_kernel.get_relevant_labels(cnstr, result); } void kernel::get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) { - m_imp->get_relevant_labeled_literals(at_lbls, result); + m_imp->m_kernel.get_relevant_labeled_literals(at_lbls, result); } void kernel::get_relevant_literals(expr_ref_vector & result) { - m_imp->get_relevant_literals(result); + m_imp->m_kernel.get_relevant_literals(result); } void kernel::get_guessed_literals(expr_ref_vector & result) { - m_imp->get_guessed_literals(result); + m_imp->m_kernel.get_guessed_literals(result); } expr_ref kernel::next_cube() { - return m_imp->next_cube(); + lookahead lh(m_imp->m_kernel); + return lh.choose(); } expr_ref_vector kernel::cubes(unsigned depth) { - return m_imp->cubes(depth); + lookahead lh(m_imp->m_kernel); + return lh.choose_rec(depth); } std::ostream& kernel::display(std::ostream & out) const { @@ -417,27 +222,26 @@ namespace smt { } void kernel::collect_statistics(::statistics & st) const { - m_imp->collect_statistics(st); + m_imp->m_kernel.collect_statistics(st); } void kernel::reset_statistics() { - m_imp->reset_statistics(); } void kernel::display_statistics(std::ostream & out) const { - m_imp->display_statistics(out); + m_imp->m_kernel.display_statistics(out); } void kernel::display_istatistics(std::ostream & out) const { - m_imp->display_istatistics(out); + m_imp->m_kernel.display_istatistics(out); } bool kernel::canceled() const { - return m_imp->canceled(); + return m_imp->m_kernel.get_cancel_flag(); } void kernel::updt_params(params_ref const & p) { - return m_imp->updt_params(p); + return m_imp->m_kernel.updt_params(p); } void kernel::collect_param_descrs(param_descrs & d) { @@ -449,11 +253,11 @@ namespace smt { } void kernel::get_levels(ptr_vector const& vars, unsigned_vector& depth) { - m_imp->get_levels(vars, depth); + m_imp->m_kernel.get_levels(vars, depth); } expr_ref_vector kernel::get_trail() { - return m_imp->get_trail(); + return m_imp->m_kernel.get_trail(); } void kernel::user_propagate_init( @@ -461,35 +265,31 @@ namespace smt { user_propagator::push_eh_t& push_eh, user_propagator::pop_eh_t& pop_eh, user_propagator::fresh_eh_t& fresh_eh) { - m_imp->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); + m_imp->m_kernel.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); } void kernel::user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) { - m_imp->user_propagate_register_fixed(fixed_eh); + m_imp->m_kernel.user_propagate_register_fixed(fixed_eh); } void kernel::user_propagate_register_final(user_propagator::final_eh_t& final_eh) { - m_imp->user_propagate_register_final(final_eh); + m_imp->m_kernel.user_propagate_register_final(final_eh); } void kernel::user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) { - m_imp->user_propagate_register_eq(eq_eh); + m_imp->m_kernel.user_propagate_register_eq(eq_eh); } void kernel::user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) { - m_imp->user_propagate_register_diseq(diseq_eh); + m_imp->m_kernel.user_propagate_register_diseq(diseq_eh); } - unsigned kernel::user_propagate_register(expr* e) { - return m_imp->user_propagate_register(e); + unsigned kernel::user_propagate_register_expr(expr* e) { + return m_imp->m_kernel.user_propagate_register_expr(e); } void kernel::user_propagate_register_created(user_propagator::created_eh_t& r) { - m_imp->user_propagate_register_created(r); - } - - func_decl* kernel::user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { - return m_imp->user_propagate_declare(name, n, domain, range); + m_imp->m_kernel.user_propagate_register_created(r); } }; \ No newline at end of file diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 0296c29a6..5c28d52fd 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -301,12 +301,10 @@ namespace smt { void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh); - unsigned user_propagate_register(expr* e); + unsigned user_propagate_register_expr(expr* e); void user_propagate_register_created(user_propagator::created_eh_t& r); - func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range); - /** \brief Return a reference to smt::context. This is a temporary hack to support user theories. diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index fe4aec944..f9ab54327 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -236,18 +236,14 @@ namespace { m_context.user_propagate_register_diseq(diseq_eh); } - unsigned user_propagate_register(expr* e) override { - return m_context.user_propagate_register(e); + unsigned user_propagate_register_expr(expr* e) override { + return m_context.user_propagate_register_expr(e); } void user_propagate_register_created(user_propagator::created_eh_t& c) override { m_context.user_propagate_register_created(c); } - func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { - return m_context.user_propagate_declare(name, n, domain, range); - } - struct scoped_minimize_core { smt_solver& s; expr_ref_vector m_assumptions; diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp index d67e430e2..c99e50393 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -449,7 +449,7 @@ public: unsigned i = 0; for (expr* v : m_vars) { - unsigned j = m_ctx->user_propagate_register(v); + unsigned j = m_ctx->user_propagate_register_expr(v); m_var2internal.setx(i, j, 0); m_internal2var.setx(j, i, 0); ++i; @@ -493,15 +493,11 @@ public: m_diseq_eh = diseq_eh; } - unsigned user_propagate_register(expr* e) override { + unsigned user_propagate_register_expr(expr* e) override { m_vars.push_back(e); return m_vars.size() - 1; } - func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) override { - return m_ctx->user_propagate_declare(name, n, domain, range); - } - void user_propagate_register_created(user_propagator::created_eh_t& created_eh) override { m_ctx->user_propagate_register_created(created_eh); } diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index ac7968d45..200d9b946 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -23,7 +23,7 @@ Author: using namespace smt; theory_user_propagator::theory_user_propagator(context& ctx): - theory(ctx, ctx.get_manager().mk_family_id("user_propagator")) + theory(ctx, ctx.get_manager().mk_family_id(user_propagator::plugin::name())) {} theory_user_propagator::~theory_user_propagator() { @@ -173,16 +173,6 @@ void theory_user_propagator::propagate() { m_qhead = qhead; } -func_decl* theory_user_propagator::declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { - if (!m_created_eh) - throw default_exception("event handler for dynamic expressions has to be registered before functions can be created"); - // ensure that declaration plugin is registered with m. - if (!m.has_plugin(get_id())) - m.register_plugin(get_id(), alloc(user_propagator::plugin)); - - func_decl_info info(get_id(), user_propagator::plugin::kind_t::OP_USER_PROPAGATE); - return m.mk_func_decl(name, n, domain, range, info); -} bool theory_user_propagator::internalize_atom(app* atom, bool gate_ctx) { return internalize_term(atom); diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h index 0189b13cb..0589a87a5 100644 --- a/src/smt/theory_user_propagator.h +++ b/src/smt/theory_user_propagator.h @@ -97,7 +97,6 @@ namespace smt { void register_eq(user_propagator::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; } void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; } void register_created(user_propagator::created_eh_t& created_eh) { m_created_eh = created_eh; } - func_decl* declare(symbol const& name, unsigned n, sort* const* domain, sort* range); bool has_fixed() const { return (bool)m_fixed_eh; } diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 94f7fb336..15c9cab82 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -108,8 +108,8 @@ public: m_tactic->user_propagate_register_diseq(diseq_eh); } - unsigned user_propagate_register(expr* e) override { - return m_tactic->user_propagate_register(e); + unsigned user_propagate_register_expr(expr* e) override { + return m_tactic->user_propagate_register_expr(e); } void user_propagate_clear() override { diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index a5cbea932..a9f5ffcf8 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -892,7 +892,7 @@ public: m_num_elim_apps = 0; } - unsigned user_propagate_register(expr* e) override { + unsigned user_propagate_register_expr(expr* e) override { m_nonvars.insert(e); return 0; } diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index 436ee3272..607928f64 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -78,7 +78,7 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result) override; void cleanup() override; - unsigned user_propagate_register(expr* e) override; + unsigned user_propagate_register_expr(expr* e) override; void user_propagate_clear() override; }; @@ -502,7 +502,7 @@ void reduce_args_tactic::cleanup() { m_imp->m_vars.append(vars); } -unsigned reduce_args_tactic::user_propagate_register(expr* e) { +unsigned reduce_args_tactic::user_propagate_register_expr(expr* e) { m_imp->m_vars.push_back(e); return 0; } diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index 4c4b9358d..437c7f804 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -85,7 +85,7 @@ public: throw default_exception("tactic does not support user propagation"); } - unsigned user_propagate_register(expr* e) override { return 0; } + unsigned user_propagate_register_expr(expr* e) override { return 0; } virtual char const* name() const = 0; protected: diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 07fc88b37..fca2f8481 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -190,9 +190,9 @@ public: m_t2->user_propagate_register_diseq(diseq_eh); } - unsigned user_propagate_register(expr* e) override { - m_t1->user_propagate_register(e); - return m_t2->user_propagate_register(e); + unsigned user_propagate_register_expr(expr* e) override { + m_t1->user_propagate_register_expr(e); + return m_t2->user_propagate_register_expr(e); } void user_propagate_clear() override { @@ -204,10 +204,6 @@ public: m_t2->user_propagate_register_created(created_eh); } - func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) override { - return m_t2->user_propagate_declare(name, n, domain, range); - } - }; tactic * and_then(tactic * t1, tactic * t2) { @@ -833,7 +829,7 @@ public: void reset() override { m_t->reset(); } void set_logic(symbol const& l) override { m_t->set_logic(l); } void set_progress_callback(progress_callback * callback) override { m_t->set_progress_callback(callback); } - unsigned user_propagate_register(expr* e) override { return m_t->user_propagate_register(e); } + unsigned user_propagate_register_expr(expr* e) override { return m_t->user_propagate_register_expr(e); } void user_propagate_clear() override { m_t->user_propagate_clear(); } protected: diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h index db9ca88fd..534b9dbc0 100644 --- a/src/tactic/user_propagator_base.h +++ b/src/tactic/user_propagator_base.h @@ -29,6 +29,8 @@ namespace user_propagator { class plugin : public decl_plugin { public: + static symbol name() { return symbol("user_propagator"); } + enum kind_t { OP_USER_PROPAGATE }; virtual ~plugin() {} @@ -79,19 +81,7 @@ namespace user_propagator { throw default_exception("user-propagators are only supported on the SMT solver"); } - virtual unsigned user_propagate_register(expr* e) { - throw default_exception("user-propagators are only supported on the SMT solver"); - } - - /** - * Create uninterpreted function for the user propagator. - * When expressions using the function are assigned values, generate a callback - * into a register_declared_eh(user_ctx, solver_ctx, declared_expr, declare_id) with arguments - * 1. context and callback context - * 2. declared_expr: expression using function that was declared at top. - * 3. declared_id: a unique identifier (unique within the current scope) to track the expression. - */ - virtual func_decl* user_propagate_declare(symbol const& name, unsigned n, sort* const* domain, sort* range) { + virtual unsigned user_propagate_register_expr(expr* e) { throw default_exception("user-propagators are only supported on the SMT solver"); } From 85e362277c251a2421452c29199b568d126ef52f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 18 Dec 2021 11:56:05 -0800 Subject: [PATCH 031/209] Update z3++.h with bindings for user propagate functions --- src/api/c++/z3++.h | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 6af9beae7..747244ca7 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -334,6 +334,7 @@ namespace z3 { func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range); void recdef(func_decl, expr_vector const& args, expr const& body); + func_decl user_propagate_function(symbol const& name, unsigned arity, sort const* domain, sort const& range); expr constant(symbol const & name, sort const & s); expr constant(char const * name, sort const & s); @@ -3424,6 +3425,17 @@ namespace z3 { Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body); } + inline func_decl context::user_propagate_function(symbol const& name, unsigned arity, sort const* domain, sort const& range) { + array args(arity); + for (unsigned i = 0; i < arity; i++) { + check_context(domain[i], range); + args[i] = domain[i]; + } + Z3_func_decl f = Z3_user_propagate_declare(m_ctx, name, arity, args.ptr(), range); + check_error(); + return func_decl(*this, f); + } + inline expr context::constant(symbol const & name, sort const & s) { Z3_ast r = Z3_mk_const(m_ctx, name, s); check_error(); @@ -3877,10 +3889,12 @@ namespace z3 { typedef std::function fixed_eh_t; typedef std::function final_eh_t; typedef std::function eq_eh_t; + typedef std::function created_eh_t; final_eh_t m_final_eh; eq_eh_t m_eq_eh; fixed_eh_t m_fixed_eh; + created_eh_t m_created_eh; solver* s; Z3_context c; Z3_solver_callback cb { nullptr }; @@ -3929,6 +3943,14 @@ namespace z3 { static_cast(p)->m_final_eh(); } + static void created_eh(void* p, Z3_solver_callback cb, unsigned id, Z3_ast _e) { + user_propagator_base* p = static_cast(_p); + scoped_cb _cb(p, cb); + scoped_context ctx(p->ctx()); + expr e(ctx(), _e); + static_cast(p)->m_created_eh(id, e); + } + public: user_propagator_base(Z3_context c) : s(nullptr), c(c) {} @@ -4008,6 +4030,18 @@ namespace z3 { Z3_solver_propagate_final(ctx(), *s, final_eh); } + void register_created(created_eh_t& c) { + assert(s); + m_created_eh = c; + Z3_solver_propagate_created(c, *s, created_eh); + } + + void register_created() { + m_created_eh = [this](unsigned id, expr const& e) { + created(id, e); + }; + Z3_solver_propagate_created(c, *s, created_eh); + } virtual void fixed(unsigned /*id*/, expr const& /*e*/) { } @@ -4015,6 +4049,8 @@ namespace z3 { virtual void final() { } + virtual void created(unsigned /*id*/, expr const& /*e*/) {} + /** \brief tracks \c e by a unique identifier that is returned by the call. From 7441bd706b89021f733fe7cb3dc6107badbc2a58 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Dec 2021 10:57:42 -0800 Subject: [PATCH 032/209] na --- src/api/c++/z3++.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 747244ca7..941f7cc0b 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -4033,14 +4033,14 @@ namespace z3 { void register_created(created_eh_t& c) { assert(s); m_created_eh = c; - Z3_solver_propagate_created(c, *s, created_eh); + Z3_solver_propagate_created(ctx(), *s, created_eh); } void register_created() { m_created_eh = [this](unsigned id, expr const& e) { created(id, e); }; - Z3_solver_propagate_created(c, *s, created_eh); + Z3_solver_propagate_created(ctx(), *s, created_eh); } virtual void fixed(unsigned /*id*/, expr const& /*e*/) { } From bee742111a822151c3f47ef8b1c0fb1f19f2b189 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Dec 2021 11:05:19 -0800 Subject: [PATCH 033/209] na --- src/api/c++/z3++.h | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 941f7cc0b..1d44467f1 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -334,7 +334,7 @@ namespace z3 { func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range); void recdef(func_decl, expr_vector const& args, expr const& body); - func_decl user_propagate_function(symbol const& name, unsigned arity, sort const* domain, sort const& range); + func_decl user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range); expr constant(symbol const & name, sort const & s); expr constant(char const * name, sort const & s); @@ -3425,13 +3425,13 @@ namespace z3 { Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body); } - inline func_decl context::user_propagate_function(symbol const& name, unsigned arity, sort const* domain, sort const& range) { - array args(arity); - for (unsigned i = 0; i < arity; i++) { + inline func_decl context::user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range) { + array args(domain.size()); + for (unsigned i = 0; i < domain.size(); i++) { check_context(domain[i], range); args[i] = domain[i]; } - Z3_func_decl f = Z3_user_propagate_declare(m_ctx, name, arity, args.ptr(), range); + Z3_func_decl f = Z3_solver_propagate_declare(range.ctx(), name, args.size(), args.ptr(), range); check_error(); return func_decl(*this, f); } @@ -3943,7 +3943,7 @@ namespace z3 { static_cast(p)->m_final_eh(); } - static void created_eh(void* p, Z3_solver_callback cb, unsigned id, Z3_ast _e) { + static void created_eh(void* _p, Z3_solver_callback cb, Z3_ast _e, unsigned id) { user_propagator_base* p = static_cast(_p); scoped_cb _cb(p, cb); scoped_context ctx(p->ctx()); From a7b1db611c62fd64aa7aeb1e108b2962f6611933 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Sun, 19 Dec 2021 11:09:55 -0800 Subject: [PATCH 034/209] State graph dgml update and fixes in condition simplifier (#5721) * improved generated dgml graph * fixed simplification of negated ranges and did some code cleanup * do not make loops with lower=upper=0, this is epsilon * do not add loops with lower=upper=1 * bug fix in normalization: forgotten eps case --- src/ast/rewriter/seq_rewriter.cpp | 295 +++++++++--------------------- src/ast/rewriter/seq_rewriter.h | 10 +- src/ast/seq_decl_plugin.cpp | 50 +++++ src/ast/seq_decl_plugin.h | 7 + src/util/state_graph.cpp | 26 ++- 5 files changed, 168 insertions(+), 220 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 13d8ef4fb..aef5eeacd 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2857,7 +2857,7 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) { return BR_REWRITE2; } else if (re().is_loop(r, r1, lo, hi)) { - result = re().mk_loop(re().mk_reverse(r1), lo, hi); + result = re().mk_loop_proper(re().mk_reverse(r1), lo, hi); return BR_REWRITE2; } else if (re().is_reverse(r, r1)) { @@ -3184,7 +3184,7 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref if ((lo == 0 && hi == 0) || hi < lo) result = nothing(); else - result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop(r1, (lo == 0 ? 0 : lo - 1), hi - 1)); + result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop_proper(r1, (lo == 0 ? 0 : lo - 1), hi - 1)); } else if (re().is_opt(r, r1)) result = mk_antimirov_deriv(e, r1, path); @@ -3350,6 +3350,8 @@ expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) { SASSERT(m_util.is_re(r1)); SASSERT(m_util.is_re(r2)); expr_ref result(m()); + if (re().is_epsilon(r2)) + std::swap(r1, r2); std::function test = [&](expr* t, expr*& a, expr*& b) { return re().is_intersection(t, a, b); }; std::function compose = [&](expr* r1, expr* r2) { return re().mk_inter(r1, r2); }; if (r1 == r2 || re().is_empty(r1) || re().is_full_seq(r2)) @@ -3504,7 +3506,7 @@ expr_ref seq_rewriter::mk_regex_reverse(expr* r) { else if (re().is_loop(r, r1, lo)) result = re().mk_loop(mk_regex_reverse(r1), lo); else if (re().is_loop(r, r1, lo, hi)) - result = re().mk_loop(mk_regex_reverse(r1), lo, hi); + result = re().mk_loop_proper(mk_regex_reverse(r1), lo, hi); else if (re().is_opt(r, r1)) result = re().mk_opt(mk_regex_reverse(r1)); else if (re().is_complement(r, r1)) @@ -3517,8 +3519,9 @@ expr_ref seq_rewriter::mk_regex_reverse(expr* r) { } expr_ref seq_rewriter::mk_regex_concat(expr* r, expr* s) { - sort* seq_sort = nullptr; + sort* seq_sort = nullptr, * ele_sort = nullptr; VERIFY(m_util.is_re(r, seq_sort)); + VERIFY(u().is_seq(seq_sort, ele_sort)); SASSERT(r->get_sort() == s->get_sort()); expr_ref result(m()); expr* r1, * r2; @@ -3528,11 +3531,30 @@ expr_ref seq_rewriter::mk_regex_concat(expr* r, expr* s) { result = r; else if (re().is_full_seq(r) && re().is_full_seq(s)) result = r; + else if (re().is_full_char(r) && re().is_full_seq(s)) + // ..* = .+ + result = re().mk_plus(re().mk_full_char(ele_sort)); + else if (re().is_full_seq(r) && re().is_full_char(s)) + // .*. = .+ + result = re().mk_plus(re().mk_full_char(ele_sort)); else if (re().is_concat(r, r1, r2)) - //create the resulting concatenation in right-associative form + // create the resulting concatenation in right-associative form except for the following case + // TODO: maintain the followig invariant for A ++ B{m,n} + C + // concat(concat(A, B{m,n}), C) (if A != () and C != ()) + // concat(B{m,n}, C) (if A == () and C != ()) + // where A, B, C are regexes + // Using & below for Intersection and | for Union + // In other words, do not make A ++ B{m,n} into right-assoc form, but keep B{m,n} at the top + // This will help to identify this situation in the merge routine: + // concat(concat(A, B{0,m}), C) | concat(concat(A, B{0,n}), C) + // simplies to + // concat(concat(A, B{0,max(m,n)}), C) + // analogously: + // concat(concat(A, B{0,m}), C) & concat(concat(A, B{0,n}), C) + // simplies to + // concat(concat(A, B{0,min(m,n)}), C) result = mk_regex_concat(r1, mk_regex_concat(r2, s)); else { - //TODO: perhaps simplifiy some further cases such as .*. = ..* = .*.+ = .+.* = .+ result = re().mk_concat(r, s); } return result; @@ -3566,15 +3588,7 @@ expr_ref seq_rewriter::mk_in_antimirov_rec(expr* s, expr* d) { */ expr_ref seq_rewriter::simplify_path(expr* elem, expr* path) { expr_ref result(path, m()); - expr* h = nullptr, * t = nullptr; - if (m().is_and(path, h, t)) { - if (m().is_true(h)) - result = simplify_path(elem, t); - else if (m().is_true(t)) - result = simplify_path(elem, h); - else - elim_condition(elem, result); - } + elim_condition(elem, result); return result; } @@ -4027,7 +4041,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { return result; } else { - return mk_der_concat(result, re().mk_loop(r1, lo, hi)); + return mk_der_concat(result, re().mk_loop_proper(r1, lo, hi)); } } else if (re().is_full_seq(r) || @@ -4523,7 +4537,7 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) { unsigned lo1, hi1, lo2, hi2; if (re().is_loop(a, a1, lo1, hi1) && lo1 <= hi1 && re().is_loop(b, b1, lo2, hi2) && lo2 <= hi2 && a1 == b1) { - result = re().mk_loop(a1, lo1 + lo2, hi1 + hi2); + result = re().mk_loop_proper(a1, lo1 + lo2, hi1 + hi2); return BR_DONE; } if (re().is_loop(a, a1, lo1) && re().is_loop(b, b1, lo2) && a1 == b1) { @@ -4631,79 +4645,13 @@ br_status seq_rewriter::mk_re_union0(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } -/* - (a + a) = a - (a + eps) = a - (eps + a) = a -*/ +/* Creates a normalized union. */ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) { - br_status st = mk_re_union0(a, b, result); - if (st != BR_FAILED) - return st; - auto mk_full = [&]() { return re().mk_full_seq(a->get_sort()); }; - if (are_complements(a, b)) { - result = mk_full(); - return BR_DONE; - } - - //just keep the union normalized result = mk_regex_union_normalize(a, b); return BR_DONE; - - - expr* a1 = nullptr, *a2 = nullptr; - expr* b1 = nullptr, *b2 = nullptr; - // ensure union is right-associative - // and swap-sort entries - if (re().is_union(a, a1, a2)) { - result = re().mk_union(a1, re().mk_union(a2, b)); - return BR_REWRITE2; - } - - auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); }; - if (re().is_union(b, b1, b2)) { - if (is_subset(a, b1)) { - result = b; - return BR_DONE; - } - if (is_subset(b1, a)) { - result = re().mk_union(a, b2); - return BR_REWRITE1; - } - if (are_complements(a, b1)) { - result = mk_full(); - return BR_DONE; - } - if (get_id(a) > get_id(b1)) { - result = re().mk_union(b1, re().mk_union(a, b2)); - return BR_REWRITE2; - } - } - else { - if (is_subset(a, b)) { - result = b; - return BR_DONE; - } - if (is_subset(b, a)) { - result = a; - return BR_DONE; - } - if (get_id(a) > get_id(b)) { - result = re().mk_union(b, a); - return BR_DONE; - } - } - return BR_FAILED; } -/* - comp(intersect e1 e2) -> union comp(e1) comp(e2) - comp(union e1 e2) -> intersect comp(e1) comp(e2) - comp(none) -> all - comp(all) -> none - comp(comp(e1)) -> e1 - comp(epsilon) -> .+ -*/ +/* Creates a normalized complement */ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) { expr *e1 = nullptr, *e2 = nullptr; if (re().is_intersection(a, e1, e2)) { @@ -4758,84 +4706,10 @@ br_status seq_rewriter::mk_re_inter0(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } -/** - (r n r) = r - (emp n r) = emp - (r n emp) = emp - (all n r) = r - (r n all) = r - (r n comp(r)) = emp - (comp(r) n r) = emp - (r n to_re(s)) = ite (s in r) to_re(s) emp - (to_re(s) n r) = " - */ +/* Creates a normalized intersection. */ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { - br_status st = mk_re_inter0(a, b, result); - if (st != BR_FAILED) - return st; - auto mk_empty = [&]() { return re().mk_empty(a->get_sort()); }; - if (are_complements(a, b)) { - result = mk_empty(); - return BR_DONE; - } - - // intersect and normalize result = mk_regex_inter_normalize(a, b); return BR_DONE; - - expr* a1 = nullptr, *a2 = nullptr; - expr* b1 = nullptr, *b2 = nullptr; - - // the following rewrite rules do not seem to - // do the right thing when it comes to normalizing - - // ensure intersection is right-associative - // and swap-sort entries - if (re().is_intersection(a, a1, a2)) { - result = re().mk_inter(a1, re().mk_inter(a2, b)); - return BR_REWRITE2; - } - auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); }; - if (re().is_intersection(b, b1, b2)) { - if (is_subset(b1, a)) { - result = b; - return BR_DONE; - } - if (is_subset(a, b1)) { - result = re().mk_inter(a, b2); - return BR_REWRITE1; - } - if (are_complements(a, b1)) { - result = mk_empty(); - return BR_DONE; - } - if (get_id(a) > get_id(b1)) { - result = re().mk_inter(b1, re().mk_inter(a, b2)); - return BR_REWRITE2; - } - } - else { - if (get_id(a) > get_id(b)) { - result = re().mk_inter(b, a); - return BR_DONE; - } - if (is_subset(a, b)) { - result = a; - return BR_DONE; - } - if (is_subset(b, a)) { - result = b; - return BR_DONE; - } - } - if (re().is_to_re(b)) - std::swap(a, b); - expr* s = nullptr; - if (re().is_to_re(a, s)) { - result = m().mk_ite(re().mk_in_re(s, b), a, re().mk_empty(a->get_sort())); - return BR_REWRITE2; - } - return BR_FAILED; } br_status seq_rewriter::mk_re_diff(expr* a, expr* b, expr_ref& result) { @@ -4873,7 +4747,7 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* } // (loop (loop a l l) h h) = (loop a l*h l*h) if (re().is_loop(args[0], a, lo, hi) && np == 2 && lo == hi && lo2 == hi2) { - result = re().mk_loop(a, lo2 * lo, hi2 * hi); + result = re().mk_loop_proper(a, lo2 * lo, hi2 * hi); return BR_REWRITE1; } // (loop a 1 1) = a @@ -4900,7 +4774,7 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* case 3: if (m_autil.is_numeral(args[1], n1) && n1.is_unsigned() && m_autil.is_numeral(args[2], n2) && n2.is_unsigned()) { - result = re().mk_loop(args[0], n1.get_unsigned(), n2.get_unsigned()); + result = re().mk_loop_proper(args[0], n1.get_unsigned(), n2.get_unsigned()); return BR_REWRITE1; } break; @@ -4912,7 +4786,7 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* br_status seq_rewriter::mk_re_power(func_decl* f, expr* a, expr_ref& result) { unsigned p = f->get_parameter(0).get_int(); - result = re().mk_loop(a, p, p); + result = re().mk_loop_proper(a, p, p); return BR_REWRITE1; } @@ -5079,74 +4953,67 @@ void seq_rewriter::intersect(unsigned lo, unsigned hi, svector> ranges, ranges1; ranges.push_back(std::make_pair(0, u().max_char())); - auto exclude_char = [&](unsigned ch) { - if (ch == 0) { - intersect(1, u().max_char(), ranges); - } - else if (ch == u().max_char()) { - intersect(0, ch-1, ranges); + auto exclude_range = [&](unsigned lower, unsigned upper) { + SASSERT(lower <= upper); + if (lower == 0) { + if (upper == u().max_char()) + ranges.reset(); + else + intersect(upper + 1, u().max_char(), ranges); } + else if (upper == u().max_char()) + intersect(0, lower - 1, ranges); else { + // not(lower <= e <= upper) iff ((0 <= e <= lower-1) or (upper+1 <= e <= max)) + // Note that this transformation is correct only when lower <= upper ranges1.reset(); ranges1.append(ranges); - intersect(0, ch - 1, ranges); - intersect(ch + 1, u().max_char(), ranges1); + intersect(0, lower - 1, ranges); + intersect(upper + 1, u().max_char(), ranges1); ranges.append(ranges1); } }; bool all_ranges = true; + bool negated = false; for (expr* e : conds) { - if (m().is_eq(e, lhs, rhs) && elem == lhs && u().is_const_char(rhs, ch)) { - intersect(ch, ch, ranges); + if (u().is_char_const_range(elem, e, ch, ch2, negated)) { + if (ch > ch2) { + if (negated) + // !(ch <= elem <= ch2) is trivially true + continue; + else + // (ch <= elem <= ch2) is trivially false + ranges.reset(); + } + else if (negated) + exclude_range(ch, ch2); + else + intersect(ch, ch2, ranges); + conds_range.push_back(e); } - else if (m().is_eq(e, lhs, rhs) && elem == rhs && u().is_const_char(lhs, ch)) { - intersect(ch, ch, ranges); - } - else if (u().is_char_le(e, lhs, rhs) && elem == lhs && u().is_const_char(rhs, ch)) { - intersect(0, ch, ranges); - } - else if (u().is_char_le(e, lhs, rhs) && elem == rhs && u().is_const_char(lhs, ch)) { - intersect(ch, u().max_char(), ranges); - } - else if (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && elem == lhs && u().is_const_char(rhs, ch)) { - exclude_char(ch); - } - else if (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && elem == rhs && u().is_const_char(lhs, ch)) { - exclude_char(ch); - } - else if (m().is_not(e, e1) && u().is_char_le(e1, lhs, rhs) && elem == lhs && u().is_const_char(rhs, ch)) { - // not (e <= ch) - if (ch == u().max_char()) - ranges.reset(); - else - intersect(ch+1, u().max_char(), ranges); - } - else if (m().is_not(e, e1) && u().is_char_le(e1, lhs, rhs) && elem == rhs && u().is_const_char(lhs, ch)) { - // not (ch <= e) - if (ch == 0) - ranges.reset(); - else - intersect(0, ch-1, ranges); - } - else if (m().is_true(e) || (m().is_eq(e, lhs, rhs) && lhs == rhs)) { - // trivially true + // trivially true conditions + else if (m().is_true(e) || (m().is_eq(e, lhs, rhs) && lhs == rhs)) continue; - } - else if (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch != ch2) { - // trivially true + else if (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch != ch2) continue; - } - else if (m().is_false(e) || (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && lhs == rhs)) { - // trivially false - cond = m().mk_false(); - return; - } + else if (u().is_char_le(e, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch <= ch2) + continue; + else if (m().is_not(e, e1) && u().is_char_le(e1, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch > ch2) + continue; + // trivially false conditions + else if (m().is_false(e) || (m().is_not(e, e1) && m().is_eq(e1, lhs, rhs) && lhs == rhs)) + ranges.reset(); + else if (u().is_char_le(e, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch > ch2) + ranges.reset(); + else if (m().is_not(e, e1) && u().is_char_le(e1, lhs, rhs) && u().is_const_char(lhs, ch) && u().is_const_char(rhs, ch2) && ch <= ch2) + ranges.reset(); else { all_ranges = false; break; @@ -5163,6 +5030,8 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) { cond = m().mk_true(); return; } + // removes all the trivially true conditions from conds + conds.set(conds_range); } } diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index c944e8f77..9357a2be8 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -223,11 +223,6 @@ class seq_rewriter { expr_ref merge_regex_sets(expr* r1, expr* r2, expr* unit, std::function& decompose, std::function& compose); - // Apply simplifications and keep the representation normalized - // Assuming r1 and r2 are normalized - expr_ref mk_regex_union_normalize(expr* r1, expr* r2); - expr_ref mk_regex_inter_normalize(expr* r1, expr* r2); - // elem is (:var 0) and path a condition that may have (:var 0) as a free variable // simplify path, e.g., (:var 0) = 'a' & (:var 0) = 'b' is simplified to false expr_ref simplify_path(expr* elem, expr* path); @@ -423,5 +418,10 @@ public: // heuristic elimination of element from condition that comes form a derivative. // special case optimization for conjunctions of equalities, disequalities and ranges. void elim_condition(expr* elem, expr_ref& cond); + + /* Apply simplifications to the union to keep the union normalized (r1 and r2 are not normalized)*/ + expr_ref mk_regex_union_normalize(expr* r1, expr* r2); + /* Apply simplifications to the intersection to keep it normalized (r1 and r2 are not normalized)*/ + expr_ref mk_regex_inter_normalize(expr* r1, expr* r2); }; diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 2044590aa..98a77c6b8 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -831,6 +831,39 @@ app* seq_util::mk_lt(expr* ch1, expr* ch2) const { return m.mk_not(mk_le(ch2, ch1)); } +bool seq_util::is_char_const_range(expr const* x, expr* e, unsigned& l, unsigned& u, bool& negated) const { + expr* a, * b, * e1, * e2, * lb, * ub; + e1 = e; + negated = (m.is_not(e, e1)) ? true : false; + if (m.is_eq(e1, a, b) && (a == x && is_const_char(b, l))) { + u = l; + return true; + } + if (is_char_le(e1, a, b) && a == x && is_const_char(b, u)) { + // (x <= u) + l = 0; + return true; + } + if (is_char_le(e1, a, b) && b == x && is_const_char(a, l)) { + // (l <= x) + u = max_char(); + return true; + } + if (m.is_and(e1, e1, e2) && is_char_le(e1, lb, a) && a == x && is_const_char(lb, l) && + is_char_le(e2, b, ub) && b == x && is_const_char(ub, u)) + // (l <= x) & (x <= u) + return true; + if (m.is_eq(e1, a, b) && b == x && is_const_char(a, l)) { + u = l; + return true; + } + if (m.is_and(e1, e2, e1) && is_char_le(e1, lb, a) && a == x && is_const_char(lb, l) && + is_char_le(e2, b, ub) && b == x && is_const_char(ub, u)) + // (x <= u) & (l <= x) + return true; + return false; +} + bool seq_util::str::is_string(func_decl const* f, zstring& s) const { if (is_string(f)) { s = f->get_parameter(0).get_zstring(); @@ -1030,6 +1063,23 @@ app* seq_util::rex::mk_loop(expr* r, unsigned lo, unsigned hi) { return m.mk_app(m_fid, OP_RE_LOOP, 2, params, 1, &r); } +expr* seq_util::rex::mk_loop_proper(expr* r, unsigned lo, unsigned hi) +{ + if (lo == 0 && hi == 0) { + sort* seq_sort = nullptr; + VERIFY(u.is_re(r, seq_sort)); + // avoid creating a loop with both bounds 0 + // such an expression is invalid as a loop + // it is BY DEFINITION = epsilon + return mk_epsilon(seq_sort); + } + if (lo == 1 && hi == 1) + // do not create a loop unless it actually is a loop + return r; + parameter params[2] = { parameter(lo), parameter(hi) }; + return m.mk_app(m_fid, OP_RE_LOOP, 2, params, 1, &r); +} + app* seq_util::rex::mk_loop(expr* r, expr* lo) { expr* rs[2] = { r, lo }; return m.mk_app(m_fid, OP_RE_LOOP, 0, nullptr, 2, rs); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index d6a1a0f29..9c76298b0 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -252,6 +252,12 @@ public: unsigned max_char() const { return seq.max_char(); } unsigned num_bits() const { return seq.num_bits(); } + /* + e has a form that is equivalent to l <= x <= u (then negated = false) + or e is equivalent to !(l <= x <= u) (then negated = true) + */ + bool is_char_const_range(expr const* x, expr * e, unsigned& l, unsigned& u, bool& negated) const; + app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range); bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); } @@ -498,6 +504,7 @@ public: app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); } app* mk_loop(expr* r, unsigned lo); app* mk_loop(expr* r, unsigned lo, unsigned hi); + expr* mk_loop_proper(expr* r, unsigned lo, unsigned hi); app* mk_loop(expr* r, expr* lo); app* mk_loop(expr* r, expr* lo, expr* hi); app* mk_full_char(sort* s); diff --git a/src/util/state_graph.cpp b/src/util/state_graph.cpp index 2cc4158c7..55de6d515 100644 --- a/src/util/state_graph.cpp +++ b/src/util/state_graph.cpp @@ -445,7 +445,7 @@ bool state_graph::write_dgml() { } r = m_state_ufind.next(r); } while (r != s); - dgml << " Category=\"State\">" << std::endl; + dgml << " Category=\"State\" Group=\"Collapsed\">" << std::endl; if (m_dead.contains(s)) dgml << "" << std::endl; if (m_live.contains(s)) @@ -453,18 +453,35 @@ bool state_graph::write_dgml() { if (m_unexplored.contains(s)) dgml << "" << std::endl; dgml << "" << std::endl; + dgml << "" << std::endl; + dgml << "" << std::endl; } } dgml << "" << std::endl; dgml << "" << std::endl; for (auto s : m_seen) { - if (m_state_ufind.is_root(s)) + if (m_state_ufind.is_root(s)) { for (auto t : m_targets[s]) { dgml << "" << std::endl; if (!m_sources_maybecycle[t].contains(s)) dgml << "" << std::endl; dgml << "" << std::endl; } + dgml << "" << std::endl; + dgml << "" << std::endl; + } } dgml << "" << std::endl; dgml << "" << std::endl @@ -494,6 +511,11 @@ bool state_graph::write_dgml() { << "" << std::endl << "" << std::endl << "" << std::endl + << "" << std::endl + << "" << std::endl + << "" << std::endl << "