Skip to content

jSMTLIB 0.15.0

Choose a tag to compare

@github-actions github-actions released this 15 Oct 17:04
cc9ccf9

Changes since the 0.14.0 release.

Pipelining (#129)

  • New --pipeline option (--no-pipeline is the default) and SMT.Configuration.pipeline,
    used by IScript.execute. Declarations, definitions, assertions, push/pop, check-sat,
    set-logic, set-info and reset are sent without waiting for each response; responses are
    read as they arrive and matched to their commands in order, so the output, including errors
    and their positions, is the same. Commands whose responses jSMTLIB needs (set-option, the
    get- commands) first wait for all earlier responses.
  • For a script of 2000 declarations and assertions this takes about 10-100x less time,
    depending on the solver. Terminal and --port input are never pipelined.
  • Library entry points: AbstractSolver.sendPipelined, executePipelined, readPipelined.

get-proof (#90)

  • get-proof answers are an IProofResponse holding the solver's proof as an s-expression,
    printed compactly, one step per line for step lists (cvc5).
  • API change: IProofResponse.proof() returns ISexpr (was Object), and
    IResponse.IFactory.get_proof_response takes the proof.
  • The s-expression parser and the proof printer are iterative, so deeply nested (z3) or very
    long (cvc5) proofs no longer overflow the stack or print in quadratic time.

Solver output

  • Diagnostic comment lines that z3 writes after some responses, when they arrive late or in
    pieces, are no longer taken as a later command's response (#99).
  • Solver text that is not SMT-LIB (e.g. bitwuzla's [error] ...) is reported as an error
    instead of failing with a ClassCastException (#118).

Executable lookup (#127)

  • A solver executable is resolved as a shell would: an absolute path as given; a relative path
    with a directory part from the current directory; a plain name in SMT_SOLVER_DIR, then on
    the PATH. Previously every relative path, including --exec's, was prefixed with
    SMT_SOLVER_DIR. SMT.resolveExecutablePath is public.

Tests, CI and documentation

  • New tests for pipelining (tests/pipeline/*.tst and five JUnit classes), proofs
    (ProofTests, ok_getProofSteps.tst), and the #99 and #118 fixes.
  • CI's macOS arm64 jobs run on macos-15. A draft release now targets the commit whose build it
    holds, so publishing it tags that commit.
  • The tutorial documents --pipeline and executable lookup.

Full suite: 12007 tests pass locally (macOS x86_64), plus the test added with the bitwuzla
follow-up; the suite passes in CI on Linux x86_64 and ARM64, macOS ARM64 and x86_64, and Windows
(release commit cc9ccf9).