GitHub

SymbolicSMT.jl

Satisfiability solving for symbolic expressions

SymbolicSMT.jl provides an interface between SymbolicUtils.jl and Symbolics.jl symbolic expressions and the Z3 satisfiability modulo theories (SMT) solver. This allows you to check satisfiability and provability of symbolic boolean expressions containing arithmetic constraints.

Features

  • Symbolics.jl integration: Work with @variables and Num types from Symbolics.jl
  • SymbolicUtils.jl support: Direct compatibility with SymbolicUtils expressions
  • Z3 integration: Leverage the power of Microsoft Research's Z3 solver
  • Multiple theories: Support for linear and nonlinear real arithmetic
  • Satisfiability checking: Determine if constraints have solutions
  • Provability checking: Verify if statements are always true under constraints

Installation

using Pkg
Pkg.add("SymbolicSMT")

Quick Example with Symbolics.jl

using Symbolics, SymbolicSMT

# Create symbolic variables with Symbolics.jl
@variables x::Real y::Real

# Define constraints: both variables are positive
constraints = Constraints([x > 0, y > 0])

# Check satisfiability: Can x + y be greater than 1?
issatisfiable(x + y > 1, constraints)  # true

# Check provability: Is x + y always positive?
isprovable(x + y > 0, constraints)     # true

# Check provability: Is x always greater than y?
isprovable(x > y, constraints)         # false

# Resolve expressions to constants when possible
resolve(x > 0, constraints)     # true (always true)
resolve(x > 10, constraints)    # x > 10 (cannot determine)

Alternative: SymbolicUtils.jl Interface

SymbolicSMT.jl also supports the lower-level SymbolicUtils.jl interface:

using SymbolicUtils, SymbolicSMT

@syms x::Real y::Real
constraints = Constraints([x > 0, y > 0])
issatisfiable(x + y > 1, constraints)  # true

Package Ecosystem

SymbolicSMT.jl is part of the JuliaSymbolics ecosystem and works seamlessly with:

Getting Help

  • Documentation: Browse the manual and API reference in the sidebar
  • Examples: Check out the tutorials for practical usage patterns
  • Issues: Report bugs or request features on GitHub
  • Discussions: Join the community on the Julia Discourse