smtlib-backends

Low-level functions for SMT-LIB-based interaction with SMT solvers.

LTS Haskell 24.17:0.4@rev:2
Stackage Nightly 2025-10-31:0.4@rev:2
Latest on Hackage:0.4@rev:2

See all snapshots smtlib-backends appears in

MIT licensed by Quentin Aristote
Maintained by [email protected], [email protected], [email protected]
This version can be pinned in stack with:smtlib-backends-0.4@sha256:a662fecbc8908337b8f19d9bb7e1515a29f4dd992a5eb88f1fcb59e6ab1d0871,1258

Module documentation for 0.4

Depends on 2 packages(full list with versions):
base, bytestring

This library provides an extensible interface for interacting with SMT solvers using SMT-LIB. The smtlib-backends-process package provides a backend that runs solvers as external processes, and the smtlib-backends-z3 package provides a backend that uses inlined calls to Z3's C API.

Changes

Changelog

All notable changes to the smtlib-backends library will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to PVP versioning.

The same stands for the changelogs of smtlib-backends-tests, smtlib-backends-process and smtlib-backends-z3, except the version numbers simply follow that of smtlib-backends.

v0.4 (2024-05-28)

Changed

  • (breaking change) stop changing the default of the produce-models option.

v0.3 (2023-02-03)

Added

  • (breaking change) add a datatype Backends.QueuingFlag to set the queuing mode
    • the initSolver function now takes this datatype as argument instead of a boolean
  • (breaking change) add a send_ method to the Backends.Backend datatype for sending commands with no output
  • add a Backends.flushQueue function for forcing the content of the queue to be evaluated

Changed

  • (breaking change) make the queuing functions thread-unsafe but faster

v0.2 (2022-12-16)

Changed

  • split the Process module into its own library
  • rename SMTLIB.Backends’s ackCommand to command_
  • improve read-me

Removed

  • remove logging abilities
    • the user can always surround command or command_ with their own logging functions