diff --git a/.github/workflows/nightly-validation.yml b/.github/workflows/nightly-validation.yml index f4daced79..bec816438 100644 --- a/.github/workflows/nightly-validation.yml +++ b/.github/workflows/nightly-validation.yml @@ -844,3 +844,97 @@ jobs: - name: Run build script unit tests run: python -m unittest discover -s scripts/tests -p "test_*.py" -v + + # ============================================================================ + # DOTNET MANAGED WRAPPER ARCHITECTURE VALIDATION + # ============================================================================ + + validate-dotnet-anycpu: + name: "Validate Microsoft.Z3.dll is AnyCPU (issue #9863)" + runs-on: ubuntu-latest + if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }} + timeout-minutes: 15 + steps: + - name: Checkout code + uses: actions/checkout@v6.0.3 + + - name: Download NuGet package from release + env: + GH_TOKEN: ${{ github.token }} + run: | + TAG="${{ github.event.inputs.release_tag }}" + if [ -z "$TAG" ]; then + TAG="Nightly" + fi + gh release download $TAG --pattern "*.nupkg" --dir nuget-packages + + - name: Extract managed DLL from NuGet package + run: | + # NuGet packages are ZIP archives; exclude the symbols package + NUPKG=$(ls nuget-packages/*.nupkg | grep -v '\.symbols\.' | grep -v '\.snupkg' | head -n 1) + echo "Checking package: $NUPKG" + unzip -q "$NUPKG" "lib/netstandard2.0/Microsoft.Z3.dll" -d nupkg-extracted + + - name: Check PE Machine field is AnyCPU (not architecture-specific) + run: | + python3 - <<'EOF' + import struct + import sys + + dll_path = "nupkg-extracted/lib/netstandard2.0/Microsoft.Z3.dll" + + with open(dll_path, 'rb') as f: + # Verify MZ magic + if f.read(2) != b'MZ': + print("ERROR: Not a valid PE file (missing MZ header)") + sys.exit(1) + + # Read PE header offset stored at 0x3C in the DOS stub + f.seek(0x3C) + pe_offset = struct.unpack('.dylib is not copied + # NOTE: These will need to be manually bumped along side the version in MODULE.bazel/VERSION.txt/CMake + "@platforms//os:linux": [ + "libz3.so", + "libz3.so.4.17", + "libz3.so.4.17.0.0", + ], + "@platforms//os:osx": [ + "libz3.dylib", + "libz3.4.17.dylib", + "libz3.4.17.0.0.dylib", + ], "@platforms//os:windows": ["libz3.dll"], "//conditions:default": ["@platforms//:incompatible"], }), @@ -36,7 +45,7 @@ cmake( cmake( name = "z3_static", generate_args = [ - "-G Ninja", + "-G Ninja", "-D BUILD_SHARED_LIBS=OFF", "-D Z3_BUILD_LIBZ3_SHARED=OFF", ], diff --git a/scripts/mk_util.py b/scripts/mk_util.py index ff04bfb68..89d82303a 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1804,6 +1804,7 @@ class DotNetDLLComponent(Component): Z3 is a satisfiability modulo theories solver from Microsoft Research. Copyright Microsoft Corporation. All rights reserved. smt constraint solver theorem prover + AnyCPU %s diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in index cf5aacf46..55cb100be 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj.in +++ b/src/api/dotnet/Microsoft.Z3.csproj.in @@ -60,6 +60,7 @@ 4 true $(OutputPath)\Microsoft.Z3.xml + AnyCPU diff --git a/src/api/js/package-lock.json b/src/api/js/package-lock.json index 5c11307f4..be3675354 100644 --- a/src/api/js/package-lock.json +++ b/src/api/js/package-lock.json @@ -5400,10 +5400,20 @@ "dev": true }, "node_modules/linkify-it": { - "version": "5.0.0", - "resolved": "https://registry.npmjs.org/linkify-it/-/linkify-it-5.0.0.tgz", - "integrity": "sha512-5aHCbzQRADcdP+ATqnDuhhJ/MRIqDkZX5pyjFHRRysS8vZ5AbqGEoFIb6pYHPZ+L/OC2Lc+xT8uHVVR5CAK/wQ==", + "version": "5.0.1", + "resolved": "https://registry.npmjs.org/linkify-it/-/linkify-it-5.0.1.tgz", + "integrity": "sha512-wVoTjP4Q6R0NW5hiZkVJaFZPWgtXfoGF+6LucL3/FtiNjmcHhYjEr5f1Kqjirc1nBW07J/ZuRFumqr2oqccEWg==", "dev": true, + "funding": [ + { + "type": "github", + "url": "https://github.com/sponsors/puzrin" + }, + { + "type": "github", + "url": "https://github.com/sponsors/markdown-it" + } + ], "license": "MIT", "dependencies": { "uc.micro": "^2.0.0" @@ -5501,15 +5511,25 @@ } }, "node_modules/markdown-it": { - "version": "14.1.0", - "resolved": "https://registry.npmjs.org/markdown-it/-/markdown-it-14.1.0.tgz", - "integrity": "sha512-a54IwgWPaeBCAAsv13YgmALOF1elABB08FxO9i+r4VFk5Vl4pKokRPeX8u5TCgSsPi6ec1otfLjdOpVcgbpshg==", + "version": "14.2.0", + "resolved": "https://registry.npmjs.org/markdown-it/-/markdown-it-14.2.0.tgz", + "integrity": "sha512-1TGiQiJVRQ3NPmZH6sx5Cfnmg6GQm9jvC1ch4TK511NjSJvjzKLzn5pPfZRNZkRPZP0HqCioSndqH8v2nRaWVQ==", "dev": true, + "funding": [ + { + "type": "github", + "url": "https://github.com/sponsors/puzrin" + }, + { + "type": "github", + "url": "https://github.com/sponsors/markdown-it" + } + ], "license": "MIT", "dependencies": { "argparse": "^2.0.1", "entities": "^4.4.0", - "linkify-it": "^5.0.0", + "linkify-it": "^5.0.1", "mdurl": "^2.0.0", "punycode.js": "^2.3.1", "uc.micro": "^2.1.0" diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 342ff5ed8..87785d8f8 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -768,9 +768,10 @@ void bit_blaster_tpl::mk_smod(unsigned sz, expr * const * a_bits, expr * co template void bit_blaster_tpl::mk_eq(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref & out) { expr_ref_vector out_bits(m()); + out_bits.resize(sz); for (unsigned i = 0; i < sz; ++i) { mk_iff(a_bits[i], b_bits[i], out); - out_bits.push_back(out); + out_bits[i] = out; } mk_and(out_bits.size(), out_bits.data(), out); } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index ac0261f61..2b9d738c0 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3344,9 +3344,20 @@ expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) { else if (false && re().is_intersection(r1, a1, a2) && re().is_intersection(r2, b1, b2) && is_complement(a1, b1) && is_complement(a2, b2)) { result = re().mk_xor(a1, re().mk_complement(a2)); - } - else - result = merge_regex_sets(r1, r2, re().mk_full_seq(r1->get_sort()), test, compose); + } + else { + // Range ∪ Range: [a,b] ∪ [c,d] = [min(a,c), max(b,d)] when overlapping or adjacent + unsigned lo1_v = 0, hi1_v = 0, lo2_v = 0, hi2_v = 0; + if (re().is_range(r1, lo1_v, hi1_v) && re().is_range(r2, lo2_v, hi2_v) && + lo2_v <= hi1_v + 1 && lo1_v <= hi2_v + 1) { + unsigned new_lo = std::min(lo1_v, lo2_v); + unsigned new_hi = std::max(hi1_v, hi2_v); + result = re().mk_range(r1->get_sort(), new_lo, new_hi); + } + else + result = merge_regex_sets(r1, r2, re().mk_full_seq(r1->get_sort()), test, compose); + } + return result; } @@ -3375,8 +3386,17 @@ 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 { + // Range ∩ Range: [a,b] ∩ [c,d] = [max(a,c), min(b,d)] or empty + unsigned lo1_v = 0, hi1_v = 0, lo2_v = 0, hi2_v = 0; + if (re().is_range(r1, lo1_v, hi1_v) && re().is_range(r2, lo2_v, hi2_v)) { + unsigned new_lo = std::max(lo1_v, lo2_v); + unsigned new_hi = std::min(hi1_v, hi2_v); + result = re().mk_range(r1->get_sort(), new_lo, new_hi); + } + else + result = merge_regex_sets(r1, r2, re().mk_empty(r1->get_sort()), test, compose); + } return result; } @@ -4805,6 +4825,34 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) { result = re().mk_plus(re().mk_full_char(a->get_sort())); return BR_DONE; } + // Range complement: comp([a,b]) → [0,a-1] ∪ [b+1,max] (or one half when a=0 or b=max) + unsigned lo_v = 0, hi_v = 0; + if (re().is_range(a, lo_v, hi_v)) { + unsigned max_c = u().max_char(); + sort* srt = a->get_sort(); + bool has_left = (lo_v > 0); + bool has_right = (hi_v < max_c); + if (!has_left && !has_right) { + // [0, max_c]: complement is empty + result = re().mk_empty(srt); + return BR_DONE; + } + if (!has_left) { + // [0, b]: complement is [b+1, max] + result = re().mk_range(srt, hi_v + 1, max_c); + return BR_REWRITE1; + } + if (!has_right) { + // [a, max]: complement is [0, a-1] + result = re().mk_range(srt, 0u, lo_v - 1); + return BR_REWRITE1; + } + // General: [a, b] → [0, a-1] ∪ [b+1, max] + auto left = re().mk_range(srt, 0u, lo_v - 1); + auto right = re().mk_range(srt, hi_v + 1, max_c); + result = re().mk_union(left, right); + return BR_REWRITE1; + } return BR_FAILED; } @@ -5102,6 +5150,11 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) { result = re().mk_empty(srt); return BR_DONE; } + // Singleton: re.range "a" "a" → str.to_re "a" + if (slo.length() == 1 && shi.length() == 1 && slo[0] == shi[0]) { + result = re().mk_to_re(lo); + return BR_DONE; + } return BR_FAILED; } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 59f5d046c..29949a151 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1208,6 +1208,15 @@ app* seq_util::rex::mk_of_pred(expr* p) { return m.mk_app(m_fid, OP_RE_OF_PRED, 0, nullptr, 1, &p); } +app* seq_util::rex::mk_range(sort* re_sort, unsigned lo, unsigned hi) { + if (lo > hi) + return mk_empty(re_sort); + app* lo_str = u.str.mk_string(zstring(lo)); + if (lo == hi) + return mk_to_re(lo_str); + return mk_range(lo_str, u.str.mk_string(zstring(hi))); +} + bool seq_util::rex::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) const { if (is_loop(n)) { app const* a = to_app(n); @@ -1671,11 +1680,19 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { case OP_RE_OPTION: i1 = get_info_rec(e->get_arg(0)); return i1.opt(); - case OP_RE_RANGE: + case OP_RE_RANGE: { + // A concrete range [lo, hi] with lo <= hi is non-empty and classical. + zstring slo, shi; + if (u.str.is_string(e->get_arg(0), slo) && slo.length() == 1 && + u.str.is_string(e->get_arg(1), shi) && shi.length() == 1 && + slo[0] <= shi[0]) + return info(true, l_false, 1, true); + // Symbolic or unknown: not classical + return info(true, l_false, 1, false); + } case OP_RE_FULL_CHAR_SET: 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, l_false, 1, false); case OP_RE_CONCAT: i1 = get_info_rec(e->get_arg(0)); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 75995ef7b..c643d8356 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -521,6 +521,8 @@ public: app* mk_to_re(expr* s) { return m.mk_app(m_fid, OP_SEQ_TO_RE, 1, &s); } app* mk_in_re(expr* s, expr* r) { return m.mk_app(m_fid, OP_SEQ_IN_RE, s, r); } app* mk_range(expr* s1, expr* s2) { return m.mk_app(m_fid, OP_RE_RANGE, s1, s2); } + // Smart constructor: returns re.empty / str.to_re / re.range based on lo vs hi. + app* mk_range(sort* re_sort, unsigned lo, unsigned hi); app* mk_concat(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_CONCAT, r1, r2); } app* mk_union(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_UNION, r1, r2); } app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); } diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index 504f67ad0..ed34d4a19 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -45,7 +45,7 @@ Author: class dependent_expr_state { unsigned m_qhead = 0; bool m_suffix_frozen = false; - unsigned m_num_recfun = 0, m_num_lambdas = 0; + unsigned m_num_recfun = 0; lbool m_has_quantifiers = l_undef; ast_mark m_frozen; func_decl_ref_vector m_frozen_trail; diff --git a/src/model/func_interp.h b/src/model/func_interp.h index e531e01cf..e3935e05e 100644 --- a/src/model/func_interp.h +++ b/src/model/func_interp.h @@ -40,7 +40,7 @@ class func_entry { // m_result and m_args[i] must be ground terms. expr * m_result; - expr * m_args[]; + expr * m_args[0]; static unsigned get_obj_size(unsigned arity) { return sizeof(func_entry) + arity * sizeof(expr*); } func_entry(ast_manager & m, unsigned arity, expr * const * args, expr * result); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 098240fc9..c23da2bba 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4672,7 +4672,6 @@ namespace smt { theory_id th_id = l->get_id(); for (enode * parent : enode::parents(n)) { - auto p = parent->get_expr(); family_id fid = parent->get_family_id(); if (fid != th_id && fid != m.get_basic_family_id()) { if (is_beta_redex(parent, n)) diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h index 2b65783b4..856f8f3d2 100644 --- a/src/smt/theory_sls.h +++ b/src/smt/theory_sls.h @@ -66,7 +66,6 @@ namespace smt { unsigned m_final_check_ls_steps = 30000; unsigned m_final_check_ls_steps_delta = 10000; unsigned m_final_check_ls_steps_min = 10000; - unsigned m_final_check_ls_steps_max = 30000; bool m_has_unassigned_clause_after_resolve = false; unsigned m_after_resolve_decide_gap = 4; unsigned m_after_resolve_decide_count = 0; diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index ebae4cb57..dffb5f15c 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -460,7 +460,6 @@ class parallel_solver { }; unsigned id; - parallel_solver& p; batch_manager& b; ast_manager m; /* worker-local manager */ ref s; /* translated solver copy */ @@ -579,7 +578,7 @@ class parallel_solver { worker(unsigned id, parallel_solver& p, solver& src, params_ref const& params, expr_ref_vector const& src_asms) - : id(id), p(p), b(p.m_batch_manager), + : id(id), b(p.m_batch_manager), asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) { /* create translated solver copy */ diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 17d8de908..b45457349 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -20,6 +20,7 @@ Notes: #include "ast/ast_ll_pp.h" #include "ast/pb_decl_plugin.h" #include "ast/arith_decl_plugin.h" +#include "ast/recfun_decl_plugin.h" #include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/expr_safe_replace.h" #include "ast/ast_util.h" @@ -185,6 +186,10 @@ public: expr_safe_replace rep(m); tactic_report report("lia2card", *g); + if (recfun::util(m).has_rec_defs()) { + result.push_back(g.get()); + return; + } bound_manager bounds(m); for (unsigned i = 0; i < g->size(); ++i) diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index ef5902c0c..d84892cd5 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -24,6 +24,7 @@ add_executable(test-z3 api_datalog.cpp parametric_datatype.cpp arith_rewriter.cpp + seq_rewriter.cpp arith_simplifier_plugin.cpp ast.cpp bdd.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index 4a5239f19..4eb66798f 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -113,6 +113,7 @@ X(api_bug) \ X(api_special_relations) \ X(arith_rewriter) \ + X(seq_rewriter) \ X(check_assumptions) \ X(smt_context) \ X(theory_dl) \ diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 9709a36bf..ab2749c3a 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -452,7 +452,7 @@ static void project(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned std::cout << "\n"; } -static void project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned num, nlsat::literal const* lits) { +static nlsat::scoped_literal_vector project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned num, nlsat::literal const* lits) { std::cout << "Project "; nlsat::scoped_literal_vector result(s); ex.compute_conflict_explanation(num, lits, result); @@ -464,6 +464,7 @@ static void project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsig s.display(std::cout << " ", ~lits[i]); } std::cout << ")\n"; + return result; } static nlsat::literal mk_gt(nlsat::solver& s, nlsat::poly* p) { @@ -490,6 +491,39 @@ static nlsat::literal mk_root_eq(nlsat::solver& s, nlsat::poly* p, nlsat::var x, return nlsat::literal(b, false); } +static bool contains_var(nlsat::var_vector const& vars, nlsat::var x) { + for (auto v : vars) { + if (v == x) + return true; + } + return false; +} + +static bool clause_contains_root_dependency( + nlsat::solver& s, + nlsat::scoped_literal_vector const& result, + nlsat::atom::kind kind, + nlsat::var target, + unsigned root_index, + nlsat::var dep1, + nlsat::var dep2, + nlsat::var dep3) { + nlsat::pmanager& pm = s.pm(); + nlsat::var_vector vars; + for (auto l : result) { + nlsat::atom* a = s.bool_var2atom(l.var()); + if (!a || !a->is_root_atom() || a->get_kind() != kind) + continue; + nlsat::root_atom* ra = nlsat::to_root_atom(a); + if (ra->x() != target || ra->i() != root_index || pm.max_var(ra->p()) != target) + continue; + s.vars(l, vars); + if (contains_var(vars, dep1) && contains_var(vars, dep2) && contains_var(vars, dep3)) + return true; + } + return false; +} + static void set_assignment_value(nlsat::assignment& as, anum_manager& am, nlsat::var v, rational const& val) { scoped_anum tmp(am); am.set(tmp, val.to_mpq()); @@ -1183,8 +1217,8 @@ static void tst_15() { auto cell = lws.single_cell(); } -// Test case for unsound lemma lws2380 - comparing standard projection vs levelwise -// The issue: x7 is unconstrained in levelwise output but affects the section polynomial +// Historical lws2380 regression test: both projection paths should preserve +// the x7-linked section/root constraints that witness the projected dependency. static void tst_16() { // enable_trace("nlsat_explain"); @@ -1283,8 +1317,9 @@ static void tst_16() { lits.push_back(mk_gt(s, p0.get())); // x13 > 0 lits.push_back(mk_gt(s, p1.get())); // p1 > 0 - project_fa(s, ex, x13, lits.size(), lits.data()); + auto result = project_fa(s, ex, x13, lits.size(), lits.data()); std::cout << "\n"; + ENSURE(clause_contains_root_dependency(s, result, nlsat::atom::ROOT_EQ, x11, 1, x7, x8, x10)); }; run_test(false); // Standard projection @@ -2144,11 +2179,11 @@ static void tst_22() { } } - if (all_false) { + if (all_false) std::cout << "*** ALL literals FALSE at counterexample - LEMMA IS UNSOUND! ***\n"; - } else { + else std::cout << "At least one literal is TRUE - lemma is sound at this point\n"; - } + ENSURE(!all_false); }; run_test(false); // lws=false (buggy) diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp new file mode 100644 index 000000000..b95008cde --- /dev/null +++ b/src/test/seq_rewriter.cpp @@ -0,0 +1,193 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Regression tests for seq_rewriter smart constructors for regex ranges. + +Tests: + 1. Empty range (lo > hi) → re.none + 2. Singleton range (lo == hi) → str.to_re lo + 3. Range ∩ Range → reduced range or re.none + 4. Range ∪ Range → merged range for overlapping/adjacent + 5. Complement of range → one or two ranges + 6. Downstream operators absorb empty ranges correctly +--*/ + +#include "ast/ast_pp.h" +#include "ast/reg_decl_plugins.h" +#include "ast/rewriter/th_rewriter.h" +#include "ast/seq_decl_plugin.h" +#include + +// Build a single-char string literal expression. +static expr_ref mk_str(ast_manager& m, seq_util& su, unsigned c) { + return expr_ref(su.str.mk_string(zstring(c)), m); +} + +void tst_seq_rewriter() { + ast_manager m; + reg_decl_plugins(m); + th_rewriter rw(m); + seq_util su(m); + + sort* str_sort = su.str.mk_string_sort(); + sort* re_sort = su.re.mk_re(str_sort); + + auto range = [&](unsigned lo, unsigned hi) -> expr_ref { + return expr_ref(su.re.mk_range(mk_str(m, su, lo), mk_str(m, su, hi)), m); + }; + + // Arbitrary regex variable for downstream tests. + app_ref R(m.mk_fresh_const("R", re_sort), m); + + // ----------------------------------------------------------------------- + // 1. Empty range (lo > hi) → re.none + // ----------------------------------------------------------------------- + { + expr_ref e = range('z', 'a'); + rw(e); + std::cout << "empty range lo>hi: " << mk_pp(e, m) << "\n"; + ENSURE(su.re.is_empty(e)); + } + + // ----------------------------------------------------------------------- + // 2. Singleton range (lo == hi) → str.to_re lo + // ----------------------------------------------------------------------- + { + expr_ref e = range('a', 'a'); + rw(e); + std::cout << "singleton range: " << mk_pp(e, m) << "\n"; + expr* inner = nullptr; + ENSURE(su.re.is_to_re(e, inner)); + } + + // ----------------------------------------------------------------------- + // 3. Range intersection: overlapping → smaller range + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_inter(range('a', 'z'), range('f', 'k')), m); + rw(e); + std::cout << "range inter overlapping: " << mk_pp(e, m) << "\n"; + unsigned lo = 0, hi = 0; + ENSURE(su.re.is_range(e, lo, hi) && lo == 'f' && hi == 'k'); + } + + // ----------------------------------------------------------------------- + // 4. Range intersection: disjoint → re.none + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_inter(range('a', 'f'), range('k', 'z')), m); + rw(e); + std::cout << "range inter disjoint: " << mk_pp(e, m) << "\n"; + ENSURE(su.re.is_empty(e)); + } + + // ----------------------------------------------------------------------- + // 5. Range intersection: touching at boundary → singleton (str.to_re "f") + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_inter(range('a', 'f'), range('f', 'z')), m); + rw(e); + std::cout << "range inter touching: " << mk_pp(e, m) << "\n"; + expr* inner = nullptr; + ENSURE(su.re.is_to_re(e, inner)); + } + + // ----------------------------------------------------------------------- + // 6. Range union: overlapping → merged range + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_union(range('a', 'f'), range('e', 'k')), m); + rw(e); + std::cout << "range union overlapping: " << mk_pp(e, m) << "\n"; + unsigned lo = 0, hi = 0; + ENSURE(su.re.is_range(e, lo, hi) && lo == 'a' && hi == 'k'); + } + + // ----------------------------------------------------------------------- + // 7. Range union: adjacent → merged range + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_union(range('a', 'f'), range('g', 'k')), m); + rw(e); + std::cout << "range union adjacent: " << mk_pp(e, m) << "\n"; + unsigned lo = 0, hi = 0; + ENSURE(su.re.is_range(e, lo, hi) && lo == 'a' && hi == 'k'); + } + + // ----------------------------------------------------------------------- + // 8. Range union: disjoint → stays as union + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_union(range('a', 'c'), range('m', 'z')), m); + rw(e); + std::cout << "range union disjoint (stays as union): " << mk_pp(e, m) << "\n"; + ENSURE(!su.re.is_range(e)); + } + + // ----------------------------------------------------------------------- + // 9. Range complement (general): no longer a complement node + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_complement(range('b', 'y')), m); + rw(e); + std::cout << "range comp general: " << mk_pp(e, m) << "\n"; + ENSURE(!su.re.is_complement(e)); + } + + // ----------------------------------------------------------------------- + // 10. Range complement (lo = 0): single range [hi+1, max] + // ----------------------------------------------------------------------- + { + expr_ref lo_str(su.str.mk_string(zstring(0u)), m); + expr_ref hi_str(su.str.mk_string(zstring((unsigned)'f')), m); + expr_ref e(su.re.mk_complement(su.re.mk_range(lo_str, hi_str)), m); + rw(e); + std::cout << "range comp lo=min: " << mk_pp(e, m) << "\n"; + ENSURE(!su.re.is_complement(e)); + ENSURE(su.re.is_range(e)); + } + + // ----------------------------------------------------------------------- + // 11. Downstream: (re.* (re.range "z" "a")) → str.to_re "" + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_star(range('z', 'a')), m); + rw(e); + std::cout << "star of empty range: " << mk_pp(e, m) << "\n"; + expr* inner = nullptr; + // star of empty → epsilon (str.to_re "") + ENSURE(su.re.is_to_re(e, inner) && su.str.is_empty(inner)); + } + + // ----------------------------------------------------------------------- + // 12. Downstream: concat absorbs empty range → re.none + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_concat(R, su.re.mk_concat(range('z', 'a'), R)), m); + rw(e); + std::cout << "concat absorbs empty range: " << mk_pp(e, m) << "\n"; + ENSURE(su.re.is_empty(e)); + } + + // ----------------------------------------------------------------------- + // 13. Downstream: union absorbs empty range → R + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_union(R, range('z', 'a')), m); + rw(e); + std::cout << "union absorbs empty range: " << mk_pp(e, m) << "\n"; + ENSURE(e.get() == R.get()); + } + + // ----------------------------------------------------------------------- + // 14. Downstream: inter absorbs empty range → re.none + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_inter(R, range('z', 'a')), m); + rw(e); + std::cout << "inter absorbs empty range: " << mk_pp(e, m) << "\n"; + ENSURE(su.re.is_empty(e)); + } + + std::cout << "tst_seq_rewriter: all tests passed\n"; +} diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 5020377e0..0b39163ea 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -62,10 +62,6 @@ public: struct key_data { Key * m_key = nullptr; Value m_value; - key_data() = default; - key_data(Key* k): m_key(k) {} - key_data(Key* k, Value const& v): m_key(k), m_value(v) {} - key_data(Key* k, Value&& v): m_key(k), m_value(std::move(v)) {} Value const & get_value() const { return m_value; } Key & get_key () const { return *m_key; } unsigned hash() const { return m_key->hash(); } @@ -136,15 +132,15 @@ public: } void insert(Key * const k, Value const & v) { - m_table.insert(key_data(k, v)); + m_table.insert(key_data{k, v}); } void insert(Key * const k, Value && v) { - m_table.insert(key_data(k, std::move(v))); + m_table.insert(key_data{k, std::move(v)}); } Value& insert_if_not_there(Key * k, Value const & v) { - return m_table.insert_if_not_there2(key_data(k, v))->get_data().m_value; + return m_table.insert_if_not_there2(key_data{k, v})->get_data().m_value; } Value& insert_if_not_there(Key * k, Value && v) { @@ -194,7 +190,7 @@ public: } iterator find_iterator(Key * k) const { - return m_table.find(key_data(k)); + return m_table.find(key_data{k}); } bool contains(Key * k) const { @@ -202,7 +198,7 @@ public: } void remove(Key * k) { - m_table.remove(key_data(k)); + m_table.remove(key_data{k}); } void erase(Key * k) { @@ -213,7 +209,7 @@ public: void get_collisions(Key * k, vector& collisions) { vector cs; - m_table.get_collisions(key_data(k), cs); + m_table.get_collisions(key_data{k}, cs); for (key_data const& kd : cs) { collisions.push_back(kd.m_key); } diff --git a/src/util/obj_pair_hashtable.h b/src/util/obj_pair_hashtable.h index e9d2e9bb5..78355b9bb 100644 --- a/src/util/obj_pair_hashtable.h +++ b/src/util/obj_pair_hashtable.h @@ -59,17 +59,13 @@ protected: class entry; public: class key_data { - Key1 * m_key1; - Key2 * m_key2; + Key1 * m_key1 = nullptr; + Key2 * m_key2 = nullptr; Value m_value; - unsigned m_hash; + unsigned m_hash = 0; friend class entry; public: - key_data(): - m_key1(nullptr), - m_key2(nullptr), - m_hash(0) { - } + key_data() = default; key_data(Key1 * k1, Key2 * k2): m_key1(k1), m_key2(k2) { diff --git a/src/util/obj_triple_hashtable.h b/src/util/obj_triple_hashtable.h index 7d75084fe..00a7a2845 100644 --- a/src/util/obj_triple_hashtable.h +++ b/src/util/obj_triple_hashtable.h @@ -60,19 +60,14 @@ protected: class entry; public: class key_data { - Key1 * m_key1; - Key2 * m_key2; - Key3 * m_key3; + Key1 * m_key1 = nullptr; + Key2 * m_key2 = nullptr; + Key3 * m_key3 = nullptr; Value m_value; - unsigned m_hash; + unsigned m_hash = 0; friend class entry; public: - key_data(): - m_key1(nullptr), - m_key2(nullptr), - m_key3(nullptr), - m_hash(0) { - } + key_data() = default; key_data(Key1 * k1, Key2 * k2, Key3 * k3): m_key1(k1), m_key2(k2), diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 5d2cce726..c6dbb9f82 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -30,17 +30,6 @@ class symbol_table { struct key_data { symbol m_key; T m_data; - - key_data() = default; - - explicit key_data(symbol k): - m_key(k) { - } - - key_data(symbol k, const T & d): - m_key(k), - m_data(d) { - } }; struct key_data_hash_proc { @@ -129,7 +118,7 @@ public: } bool contains(symbol key) const { - return m_sym_table.contains(key_data(key)); + return m_sym_table.contains(key_data{key}); } unsigned get_scope_level() const { @@ -148,11 +137,11 @@ public: m_trail_stack.push_back(dummy); key_data & new_entry = m_trail_stack.back(); new_entry.m_key = symbol::mark(new_entry.m_key); - m_sym_table.insert(key_data(key, data)); + m_sym_table.insert(key_data{key, data}); } } else { - m_sym_table.insert(key_data(key, data)); + m_sym_table.insert(key_data{key, data}); } }