fix: make the test suite pass (12 failures tracked by #47)

.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

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

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
 

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=<produce-unsat-cores option>) -> 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"\"(?:[^\"]|\"\")*\"|(?<![^\s(]):([^\s()\":]+)\s+(\"(?:[^\"]|\"\")*\"|:?[^\s()\"]+)"
+
 """
     parse_statistics(output::String) -> 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,13 +2334,23 @@ 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
         return get(model, expr, 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]

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

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

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