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 b170aa0..30b5a2f 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -17,6 +17,15 @@ 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). +- 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 === 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..d57d6a2 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,45 @@ 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`). The first alternative consumes a +# quoted string that is not a value, so `:key value` text inside it is never +# read as a pair; such a match has no captures. +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] + 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, ":") + 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 +2334,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 +2347,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..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,34 +27,37 @@ 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_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 - ctx = SMTContext() - declare_const(ctx, :a, :Int) + @testset "build_script includes check-sat and get-model" begin + ctx = SMTContext(solver=script_only) + 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 - ctx = SMTContext() - @test_throws Exception declare_const(ctx, :z, :UnknownSort123) + # A Julia type with no SMT-LIB sort mapping has no `smt_type` method + ctx = SMTContext(solver=script_only) + @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..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,13 +35,13 @@ using SMTLib @testset "Invariant: SMTContext assert! count matches calls" begin for _ in 1:30 - ctx = SMTContext() - declare_const(ctx, :x, :Int) + ctx = SMTContext(solver=script_only) + 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 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