SymbolicSAT.jl

For you with the good questions
Author JuliaSymbolics
Popularity
23 Stars
Updated Last
2 Years Ago
Started In
May 2020

SymbolicSAT

WARNING: This package is experimental! Use it only to find bugs.

This package extends SymbolicUtils expression simplification with a theorem prover.

It is a wrapper around a wrapper to The Z3 Theorem Prover.

Usage:

  1. using SymbolicUtils, SymbolicSAT
  2. Construct a Constraints([cs...]) where cs are boolean expressions
  3. Pass it as the second argument to simplify
julia> using SymbolicUtils, SymbolicSAT

julia> @syms a::Real b::Real
(a, b)

julia> constraints = Constraints([a^2 + b^2 < 4])
Constraints:
  ((a ^ 2) + (b ^ 2)) < 4

julia> simplify((a < 2) & (b < 2), Constraints([a^2 + b^2 < 4]))
true

Thanks to the author of Z3.jl for the Julia bindings and answering my questions!