From 6604a9ceea4451a3254ba00180d6a839908bfc8c Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 9 Oct 2026 10:05:44 +0100 Subject: [PATCH 1/3] fix: make the test suite pass (12 failures from #47) Four root causes, all fixed at the source rather than by loosening tests. 1. parse_statistics (3 fail + 3 error, runtests.jl:876-881). Its regex accepted only a single-pair list "(:key value)", closed immediately. Real solver statistics are one list holding many pairs, and Z3 spreads it over several lines: "(:time 0.01 :memory 12.5 :conflicts 0)". It now finds each "(:" keyword list (quoted strings are consumed first, so text inside an error message is never read as a list) and reads every ":key value" pair in it. Checked against real Z3 4.13.3 "(get-info :all-statistics)" output: 13 entries. 2. evaluate (2 fail, runtests.jl:931-932). Julia parses `p && q` and `p || q` as Expr(:&&) / Expr(:||), not as calls, so the `:call` branch never ran and the substituted Expr came back. Those heads are now computed once every operand is a Bool. 3. Unsat core (1 fail, runtests.jl:1153, Z3 only). Two defects: set_option!(ctx, :produce_unsat_cores, true) emitted the option name with underscores, which is not the SMT-LIB name (cvc5 answers "unsupported"); the Symbol method now maps '_' to '-'. And plain check_sat(ctx) never sent (get-unsat-core) even with the option on; get_unsat_core now defaults to the context's produce-unsat-cores option. Explicit get_unsat_core=true/false behaves as before. 4. declare_const / to_smtlib_script (3 errors, e2e_test.jl:23,41 and property_test.jl:31). These tests are provably wrong: they call two functions that have never existed in src/ (both were introduced only as callers in ed8eff1). The exported, documented API is declare(ctx, name, sort) (README "declare(ctx, name, sort)") and build_script(ctx, get_model), which runtests.jl's "Script Building" testset already uses. The tests and benches/benchmarks.jl (same commit, same calls) now use them. No assertion is weakened: - "unknown sort raises an error" passed vacuously before (the UndefVarError for declare_const satisfied @test_throws Exception); it now asserts a MethodError from an unmapped type (Vector{Int}) and that no declaration was recorded. - the pipeline test now also checks that exactly three asserts are emitted, as its comment says. CHANGELOG.adoc gains a Fixed section. Pkg.test, z3 4.13.3 and cvc5 1.1.2 on PATH: Julia 1.12.6 before 818 pass / 6 fail / 6 error (830) after 864 pass Julia 1.10.10 before 818 pass / 6 fail / 6 error (830) after 864 pass Julia 1.11 is not installed on this machine, so it was not run. The count rises because the property test now runs all 30 iterations instead of erroring on the first. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_016XJoh8YA2sCWQmq93CF8RX --- CHANGELOG.adoc | 7 ++++ benches/benchmarks.jl | 6 ++-- src/SMTLib.jl | 75 +++++++++++++++++++++++++++++++++++-------- test/e2e_test.jl | 17 ++++++---- test/property_test.jl | 4 +-- 5 files changed, 84 insertions(+), 25 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index b170aa0..da7fa87 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -17,6 +17,13 @@ The format is based on Keep a Changelog and this project follows Semantic Versio - Roadmap rewritten to a concrete Must/Intend/Like delivery model. - `.machine_readable/STATE.scm` aligned with package version and current roadmap intent. +=== Fixed +- `parse_statistics` reads every `:key value` pair of a multi-pair keyword list, including Z3's multi-line `(get-info :all-statistics)` block; it previously matched only single-pair `(:key value)` lists (#47). +- `evaluate` computes `a && b` and `a || b`, which Julia parses as `Expr(:&&)` / `Expr(:||)` rather than calls (#47). +- `set_option!` with a `Symbol` key translates `_` to `-`, so `:produce_unsat_cores` emits the SMT-LIB option `:produce-unsat-cores` (#47). +- `check_sat` requests the unsat core by default when the context has `produce-unsat-cores` set (#47). +- The e2e and property tests and the benchmarks called `declare_const` and `to_smtlib_script`, which never existed; they now use `declare` and `build_script` (#47). + == [0.1.0] - 2026-01-25 === Added diff --git a/benches/benchmarks.jl b/benches/benchmarks.jl index 0d48427..a87d8b8 100644 --- a/benches/benchmarks.jl +++ b/benches/benchmarks.jl @@ -24,17 +24,17 @@ SUITE["context"]["create"] = @benchmarkable SMTContext() SUITE["context"]["declare_assert_script_10"] = @benchmarkable begin ctx = SMTContext() - declare_const(ctx, :x, :Int) + declare(ctx, :x, Int) for i in 1:10 assert!(ctx, :(x > 0)) end - to_smtlib_script(ctx) + SMTLib.build_script(ctx, false) end SUITE["context"]["declare_10_consts"] = @benchmarkable begin ctx = SMTContext() for i in 1:10 - declare_const(ctx, Symbol("v$i"), :Int) + declare(ctx, Symbol("v$i"), Int) end end diff --git a/src/SMTLib.jl b/src/SMTLib.jl index 6c1b360..ca14761 100644 --- a/src/SMTLib.jl +++ b/src/SMTLib.jl @@ -969,10 +969,27 @@ function set_option!(ctx::SMTContext, key::String, value::String) nothing end +""" + set_option!(ctx::SMTContext, key::Symbol, value) + +Set a solver option from a Julia `Symbol` key and any value. + +SMT-LIB2 option names are hyphenated (`:produce-unsat-cores`), but a Julia +symbol literal cannot contain `-`, so underscores in `key` are translated to +hyphens: `set_option!(ctx, :produce_unsat_cores, true)` emits +`(set-option :produce-unsat-cores true)`. The value is stringified. Use the +`String`-key method to pass an option name verbatim. +""" function set_option!(ctx::SMTContext, key::Symbol, value::Any) - set_option!(ctx, string(key), string(value)) + set_option!(ctx, replace(string(key), '_' => '-'), string(value)) end +""" + set_option!(ctx::SMTContext, key::String, value) + +Set a solver option with a verbatim option name and any value, which is +stringified (e.g. `set_option!(ctx, "random-seed", 42)`). +""" function set_option!(ctx::SMTContext, key::String, value::Any) set_option!(ctx, key, string(value)) end @@ -982,7 +999,7 @@ end # ============================================================================ """ - check_sat(ctx::SMTContext; get_model=true, get_unsat_core=false) -> SMTResult + check_sat(ctx::SMTContext; get_model=true, get_unsat_core=) -> SMTResult Check satisfiability of the current context assertions. @@ -993,7 +1010,9 @@ parses the model. If `get_unsat_core` is true, requests the unsat core. # Arguments - `ctx::SMTContext`: The solving context. - `get_model::Bool`: Request model on sat (default `true`). -- `get_unsat_core::Bool`: Request unsat core on unsat (default `false`). +- `get_unsat_core::Bool`: Request unsat core on unsat. Defaults to `true` when + the context already has `produce-unsat-cores` set to `true` (for example via + `set_option!(ctx, :produce_unsat_cores, true)`), otherwise `false`. # Returns An `SMTResult` with status, model, unsat core, statistics, and raw output. @@ -1004,7 +1023,8 @@ result = check_sat(ctx) result = check_sat(ctx; get_model=true, get_unsat_core=true) ``` """ -function check_sat(ctx::SMTContext; get_model::Bool=true, get_unsat_core::Bool=false) +function check_sat(ctx::SMTContext; get_model::Bool=true, + get_unsat_core::Bool=get(ctx.solver_options, "produce-unsat-cores", "false") == "true") # If unsat core requested, ensure the option is set if get_unsat_core ctx.solver_options["produce-unsat-cores"] = "true" @@ -1234,23 +1254,42 @@ function parse_result(output::String) SMTResult(status, model, unsat_core, stats, output) end +# A keyword list `(:key value :key value ...)` as printed by `get-info`: it may +# span several lines and hold quoted strings (which may contain parentheses), +# but no nested parenthesised values. The first alternative consumes a quoted +# string on its own, so text inside a string (e.g. an error message) is never +# read as a list. +const STATISTICS_LIST_REGEX = r"\"(?:[^\"]|\"\")*\"|\(:(?:[^()\"]|\"(?:[^\"]|\"\")*\")*\)" + +# One `:key value` pair inside such a list. The key must start a token (it +# follows `(` or whitespace); the value is a quoted string or a single atom, +# optionally itself a keyword (`:key :value`). +const STATISTICS_PAIR_REGEX = r"(? Dict{String, Any} Parse SMT-LIB2 statistics output (e.g. from `(get-info :all-statistics)`). + +Every keyword list in `output`, such as Z3's multi-line +`(:time 0.01 :memory 12.5 :conflicts 0)`, contributes one entry per +`:key value` pair. Values are converted with `parse_smt_value`, so numbers +become `Int` or `Float64`; a keyword value (`:key :value`) is stored without +its leading colon. Lists whose values are nested S-expressions are skipped. """ function parse_statistics(output::String) stats = Dict{String, Any}() - # Support both (:key value) and (:key :value) - # Match (:key followed by value until next ) or end of line - for m in eachmatch(r"\(:([a-zA-Z0-9\._-]+)\s+((?:\d+\.\d+)|\d+|:?[a-zA-Z0-9\._-]+)\)", output) - key = m.captures[1] - val_str = m.captures[2] - # Strip leading : from value if present - if startswith(val_str, ":") - val_str = val_str[2:end] + for list in eachmatch(STATISTICS_LIST_REGEX, output) + startswith(list.match, '"') && continue # a string literal, not a list + for m in eachmatch(STATISTICS_PAIR_REGEX, list.match) + key = m.captures[1] + val_str = m.captures[2] + # Strip leading : from a keyword value + if startswith(val_str, ":") + val_str = val_str[2:end] + end + stats[key] = parse_smt_value(val_str) end - stats[key] = parse_smt_value(val_str) end stats end @@ -2292,6 +2331,12 @@ end Evaluate a Julia expression against a model dictionary. Replaces variables in `expr` with their values from `model` and evaluates. + +Function calls on known operators are computed once their arguments are +values. The short-circuit forms `a && b` and `a || b`, which Julia parses as +`Expr(:&&)` / `Expr(:||)` rather than calls, are computed once every operand +is a `Bool`. Anything that cannot be computed is returned as a substituted +`Expr`. """ function evaluate(model::Dict{Symbol, Any}, expr) if expr isa Symbol @@ -2299,6 +2344,10 @@ function evaluate(model::Dict{Symbol, Any}, expr) elseif expr isa Expr # Recursively evaluate args new_args = [evaluate(model, a) for a in expr.args] + # `&&` and `||` are syntax (their own Expr heads), not calls + if expr.head in (:&&, :||) && all(a -> a isa Bool, new_args) + return expr.head == :&& ? all(new_args) : any(new_args) + end # Attempt to evaluate the expression if all arguments are literals if expr.head == :call func = new_args[1] diff --git a/test/e2e_test.jl b/test/e2e_test.jl index b8e2a60..5ecea17 100644 --- a/test/e2e_test.jl +++ b/test/e2e_test.jl @@ -25,31 +25,34 @@ using SMTLib ctx = SMTContext() @test ctx isa SMTContext - declare_const(ctx, :x, :Int) - declare_const(ctx, :y, :Int) + declare(ctx, :x, Int) + declare(ctx, :y, Int) assert!(ctx, :(x > 0)) assert!(ctx, :(y < 10)) assert!(ctx, :(x + y == 5)) # Script should contain all three assertions - script = to_smtlib_script(ctx) + script = SMTLib.build_script(ctx, false) @test script isa String @test occursin("declare-const", script) @test occursin("assert", script) + @test length(collect(eachmatch(r"\(assert", script))) == 3 end - @testset "to_smtlib_script includes check-sat and get-model" begin + @testset "build_script includes check-sat and get-model" begin ctx = SMTContext() - declare_const(ctx, :a, :Int) + declare(ctx, :a, Int) assert!(ctx, :(a > 100)) - script = to_smtlib_script(ctx; check_sat=true, get_model=true) + script = SMTLib.build_script(ctx, true) @test occursin("check-sat", script) @test occursin("get-model", script) end @testset "Error handling: unknown sort raises an error" begin + # A Julia type with no SMT-LIB sort mapping has no `smt_type` method ctx = SMTContext() - @test_throws Exception declare_const(ctx, :z, :UnknownSort123) + @test_throws MethodError declare(ctx, :z, Vector{Int}) + @test isempty(ctx.declarations) end end diff --git a/test/property_test.jl b/test/property_test.jl index d25cc07..a009bbd 100644 --- a/test/property_test.jl +++ b/test/property_test.jl @@ -31,12 +31,12 @@ using SMTLib @testset "Invariant: SMTContext assert! count matches calls" begin for _ in 1:30 ctx = SMTContext() - declare_const(ctx, :x, :Int) + declare(ctx, :x, Int) n = rand(1:10) for i in 1:n assert!(ctx, :(x > 0)) end - script = to_smtlib_script(ctx) + script = SMTLib.build_script(ctx, false) # Count occurrences of "assert" in the script count = length(collect(eachmatch(r"\(assert", script))) @test count == n From 318efef8fd08b0b768067ee87f4ca04ea6665356 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 9 Oct 2026 10:22:21 +0100 Subject: [PATCH 2/3] fix(parse_statistics): never read pairs from inside a stray string CodeRabbit review on #49: text inside a quoted string must not be read as a ":key value" pair. A string that is a pair's value was already consumed whole, but a string that is not a value was not: "(:a 1 \"stray :time 99\")" produced a false time => 99 (reproduced before this change). The pair regex now consumes any quoted string on its own first, and such a match (no captures) is skipped, as the list regex already does. Tests added to "Statistics Parsing": Z3's multi-line layout, quoted values containing parentheses and ":key value" text, the stray-string case, an error message containing "(:foo bar)", and a keyword value. The tautology "isempty(stats) || !isempty(stats)" in "Empty output" now asserts isempty(stats), which holds for "sat\n". Pkg.test, z3 4.13.3 and cvc5 1.1.2 on PATH: 873 pass on Julia 1.12.6 and on Julia 1.10.10 (864 + 9 new). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_016XJoh8YA2sCWQmq93CF8RX --- src/SMTLib.jl | 7 +++++-- test/runtests.jl | 22 +++++++++++++++++++++- 2 files changed, 26 insertions(+), 3 deletions(-) diff --git a/src/SMTLib.jl b/src/SMTLib.jl index ca14761..d57d6a2 100644 --- a/src/SMTLib.jl +++ b/src/SMTLib.jl @@ -1263,8 +1263,10 @@ const STATISTICS_LIST_REGEX = r"\"(?:[^\"]|\"\")*\"|\(:(?:[^()\"]|\"(?:[^\"]|\"\ # One `:key value` pair inside such a list. The key must start a token (it # follows `(` or whitespace); the value is a quoted string or a single atom, -# optionally itself a keyword (`:key :value`). -const STATISTICS_PAIR_REGEX = r"(? Dict{String, Any} @@ -1283,6 +1285,7 @@ function parse_statistics(output::String) startswith(list.match, '"') && continue # a string literal, not a list for m in eachmatch(STATISTICS_PAIR_REGEX, list.match) key = m.captures[1] + key === nothing && continue # a stray string literal, not a pair val_str = m.captures[2] # Strip leading : from a keyword value if startswith(val_str, ":") diff --git a/test/runtests.jl b/test/runtests.jl index ffff888..e6dc127 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -893,7 +893,27 @@ using SMTLib result = SMTResult(:sat, Dict{Symbol,Any}(), Symbol[], Dict{String,Any}(), "sat\n") stats = get_statistics(result) - @test isempty(stats) || !isempty(stats) # May or may not find stats + @test isempty(stats) + end + + @testset "Multi-line keyword list (Z3 layout)" begin + output = "unsat\n(:conflicts 1\n :max-memory 17.82\n :num-allocs 35972\n :time 0.00)\n" + stats = SMTLib.parse_statistics(output) + @test stats["conflicts"] == 1 + @test stats["max-memory"] == 17.82 + @test stats["num-allocs"] == 35972 + @test stats["time"] == 0.0 + @test length(stats) == 4 + end + + @testset "Quoted strings are not read as pairs or lists" begin + stats = SMTLib.parse_statistics("(:name \"Z3 (x) :time 99\" :version \"4.13.3\")") + @test stats == Dict{String,Any}("name" => "Z3 (x) :time 99", "version" => "4.13.3") + stats = SMTLib.parse_statistics("(:a 1 \"stray :time 99\")") + @test stats == Dict{String,Any}("a" => 1) + @test isempty(SMTLib.parse_statistics("(error \"line 3: unknown (:foo bar)\")")) + @test SMTLib.parse_statistics("(:reason-unknown :incomplete)") == + Dict{String,Any}("reason-unknown" => "incomplete") end end From a6c6bc6effde7ddb5cd5b4f8d173bd671e69a4c4 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 9 Oct 2026 10:36:53 +0100 Subject: [PATCH 3/3] fix(ci): run the test matrix where no SMT solver is installed CI could not run a single test. Every `test (*)` job stopped at Build package with `expected package AcceleratorGate [59f742c7] to be registered`: julia-buildpkg adds only General, and AcceleratorGate is in hyperpolymath/julia-professional-registry. CI.yml now passes that registry to julia-buildpkg through its `localregistry` input. The test step reuses the same depot. CI also installs neither z3 nor cvc5. Four testsets in e2e_test.jl and property_test.jl only build SMT-LIB text, but they called `SMTContext()`, which looks a solver up on PATH and raises "No SMT solver found" when there is none. They now pass `SMTContext` a solver record that is never run. `declare`, `assert!` and `build_script` never read the context's solver; only `run_solver` does. Verified locally with Pkg.test() in a throwaway depot (General plus julia-professional-registry): - Julia 1.10.10, z3 and cvc5 removed from PATH: 757/757 pass. Before this commit: 718 pass, 4 errors. - Julia 1.12.6, z3 and cvc5 removed from PATH: 757/757 pass. - Julia 1.10.10, z3 4.13.3 and cvc5 1.1.2 on PATH: 873/873 pass, unchanged. Refs #47 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_016XJoh8YA2sCWQmq93CF8RX --- .github/workflows/CI.yml | 4 ++++ CHANGELOG.adoc | 2 ++ test/e2e_test.jl | 11 ++++++++--- test/property_test.jl | 7 ++++++- 4 files changed, 20 insertions(+), 4 deletions(-) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 48f4ad0..87fc335 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -25,8 +25,12 @@ jobs: version: ${{ matrix.julia-version }} - name: Cache Julia artifacts uses: julia-actions/cache@e32267b41e0fa7df82a3d53e8c7273620d52c586 # v3.4.0 + # AcceleratorGate is registered in the hyperpolymath registry, not in + # General. The registry is added to the depot that the test step reuses. - name: Build package uses: julia-actions/julia-buildpkg@e3eb439fad4f9aba7da2667e7510e4a46ebc46e1 # v1.7.0 + with: + localregistry: https://github.com/hyperpolymath/julia-professional-registry - name: Run tests uses: julia-actions/julia-runtest@d0c4f093badade621cd041bba567d1e832480ac2 # v1.10.0 - name: Process coverage diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index da7fa87..30b5a2f 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -23,6 +23,8 @@ The format is based on Keep a Changelog and this project follows Semantic Versio - `set_option!` with a `Symbol` key translates `_` to `-`, so `:produce_unsat_cores` emits the SMT-LIB option `:produce-unsat-cores` (#47). - `check_sat` requests the unsat core by default when the context has `produce-unsat-cores` set (#47). - The e2e and property tests and the benchmarks called `declare_const` and `to_smtlib_script`, which never existed; they now use `declare` and `build_script` (#47). +- The tests that only build SMT-LIB text give `SMTContext` a solver record that is never run, so they pass where no SMT solver is installed, as on CI (#47). +- CI adds `hyperpolymath/julia-professional-registry`, where AcceleratorGate is registered, so the `test` jobs can resolve the package (#47). == [0.1.0] - 2026-01-25 diff --git a/test/e2e_test.jl b/test/e2e_test.jl index 5ecea17..d767c51 100644 --- a/test/e2e_test.jl +++ b/test/e2e_test.jl @@ -7,6 +7,11 @@ using SMTLib @testset "E2E Pipeline Tests" begin + # These tests only build SMT-LIB text, which never runs the solver, so they + # use a solver record that is never executed. `SMTContext()` would look for + # z3 or cvc5 on PATH and fail on a machine that has neither, such as CI. + script_only = SMTSolver(:z3, "/nonexistent/z3", "never run") + @testset "Full SMT-LIB generation pipeline" begin # Nested arithmetic and logical expression round-trip through to_smtlib exprs = [ @@ -22,7 +27,7 @@ using SMTLib @testset "SMTContext declare → assert → check_sat pipeline (no solver)" begin # These operations must not error even without a solver installed - ctx = SMTContext() + ctx = SMTContext(solver=script_only) @test ctx isa SMTContext declare(ctx, :x, Int) @@ -40,7 +45,7 @@ using SMTLib end @testset "build_script includes check-sat and get-model" begin - ctx = SMTContext() + ctx = SMTContext(solver=script_only) declare(ctx, :a, Int) assert!(ctx, :(a > 100)) script = SMTLib.build_script(ctx, true) @@ -50,7 +55,7 @@ using SMTLib @testset "Error handling: unknown sort raises an error" begin # A Julia type with no SMT-LIB sort mapping has no `smt_type` method - ctx = SMTContext() + ctx = SMTContext(solver=script_only) @test_throws MethodError declare(ctx, :z, Vector{Int}) @test isempty(ctx.declarations) end diff --git a/test/property_test.jl b/test/property_test.jl index a009bbd..9c78ee4 100644 --- a/test/property_test.jl +++ b/test/property_test.jl @@ -7,6 +7,11 @@ using SMTLib @testset "Property-Based Tests" begin + # The SMTContext invariant below only builds SMT-LIB text, which never runs + # the solver, so it uses a solver record that is never executed. + # `SMTContext()` would fail on a machine with no z3 or cvc5, such as CI. + script_only = SMTSolver(:z3, "/nonexistent/z3", "never run") + @testset "Invariant: to_smtlib of integer literals is the decimal string" begin for _ in 1:50 n = rand(0:999) @@ -30,7 +35,7 @@ using SMTLib @testset "Invariant: SMTContext assert! count matches calls" begin for _ in 1:30 - ctx = SMTContext() + ctx = SMTContext(solver=script_only) declare(ctx, :x, Int) n = rand(1:10) for i in 1:n