mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-18 11:07:49 -07:00
commit b1d4f36c85
23 changed files with 480 additions and 74 deletions
Download patch file Download diff file Expand all files Collapse all files

94
.github/workflows/nightly-validation.yml vendored
View file

@ -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('<I', f.read(4))[0]
# Verify PE signature
f.seek(pe_offset)
if f.read(4) != b'PE\x00\x00':
print("ERROR: Missing PE\\0\\0 signature")
sys.exit(1)
# COFF Machine field is the 2 bytes immediately after the PE signature
machine = struct.unpack('<H', f.read(2))[0]
machine_names = {
0x0000: "Unknown/AnyCPU",
0x014C: "i386 (AnyCPU for managed assemblies)",
0x8664: "AMD64/x64",
0xAA64: "ARM64",
0x01C0: "ARM",
0x01C4: "ARM Thumb-2",
}
machine_name = machine_names.get(machine, f"0x{machine:04X}")
print(f"Machine field: 0x{machine:04X} = {machine_name}")
if machine == 0x8664:
print()
print("FAIL: Machine is AMD64 (0x8664).")
print("This prevents loading on arm64 .NET hosts even though the assembly")
print("contains only pure IL (CorFlags.ILONLY=True).")
print("The DLL must be built as AnyCPU (Machine=0x014C) so the CLR loader")
print("accepts it on every host architecture.")
print("See issue #9863 for details.")
sys.exit(1)
elif machine == 0xAA64:
print()
print("FAIL: Machine is ARM64 (0xAA64).")
print("This prevents loading on x64 .NET hosts.")
print("The DLL must be built as AnyCPU (Machine=0x014C).")
sys.exit(1)
elif machine in (0x014C, 0x0000):
print()
print("PASS: Machine field indicates AnyCPU.")
print("Microsoft.Z3.dll will load on any .NET host architecture.")
else:
print()
print(f"FAIL: Unexpected Machine field 0x{machine:04X}.")
print("Expected 0x014C (i386/AnyCPU) for a managed-only assembly.")
sys.exit(1)
EOF

17
BUILD.bazel
View file

@ -19,14 +19,23 @@ filegroup(
cmake(
name = "z3_dynamic",
generate_args = [
"-G Ninja",
"-G Ninja",
"-D Z3_EXPORTED_TARGETS=", # prevents installation, leaving symlinks between dylibs intact on copy
],
lib_source = ":all_files",
out_binaries = ["z3"],
out_shared_libs = select({
"@platforms//os:linux": ["libz3.so"],
# "@platforms//os:osx": ["libz3.dylib"], # FIXME: this is not working, libz3<version>.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",
],

1
scripts/mk_util.py
View file

@ -1804,6 +1804,7 @@ class DotNetDLLComponent(Component):
<Description>Z3 is a satisfiability modulo theories solver from Microsoft Research.</Description>
<Copyright>Copyright Microsoft Corporation. All rights reserved.</Copyright>
<PackageTags>smt constraint solver theorem prover</PackageTags>
<PlatformTarget>AnyCPU</PlatformTarget>
%s
</PropertyGroup>

1
src/api/dotnet/Microsoft.Z3.csproj.in
View file

@ -60,6 +60,7 @@
<Warn>4</Warn>
<GenerateDocumentationFile>true</GenerateDocumentationFile>
<DocumentationFile>$(OutputPath)\Microsoft.Z3.xml</DocumentationFile>
<PlatformTarget>AnyCPU</PlatformTarget>
</PropertyGroup>
<!-- Compilation items -->

34
src/api/js/package-lock.json generated
View file

@ -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"

3
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -768,9 +768,10 @@ void bit_blaster_tpl<Cfg>::mk_smod(unsigned sz, expr * const * a_bits, expr * co
template<typename Cfg>
void bit_blaster_tpl<Cfg>::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);
}

63
src/ast/rewriter/seq_rewriter.cpp
View file

@ -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;
}

21
src/ast/seq_decl_plugin.cpp
View file

@ -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));

2
src/ast/seq_decl_plugin.h
View file

@ -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); }

2
src/ast/simplifiers/dependent_expr_state.h
View file

@ -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;

2
src/model/func_interp.h
View file

@ -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);

1
src/smt/smt_context.cpp
View file

@ -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))

1
src/smt/theory_sls.h
View file

@ -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;

3
src/solver/parallel_tactical2.cpp
View file

@ -460,7 +460,6 @@ class parallel_solver {
};
unsigned id;
parallel_solver& p;
batch_manager& b;
ast_manager m; /* worker-local manager */
ref<solver> 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 */

5
src/tactic/arith/lia2card_tactic.cpp
View file

@ -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)

1
src/test/CMakeLists.txt
View file

@ -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

1
src/test/main.cpp
View file

@ -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) \

49
src/test/nlsat.cpp
View file

@ -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)

193
src/test/seq_rewriter.cpp Normal file
View file

@ -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 <iostream>
// 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";
}

16
src/util/obj_hashtable.h
View file

@ -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<Key*>& collisions) {
vector<key_data> 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);
}

12
src/util/obj_pair_hashtable.h
View file

@ -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) {

15
src/util/obj_triple_hashtable.h
View file

@ -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),

17
src/util/symbol_table.h
View file

@ -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});
}
}