API Reference

Constraints(constraints::Vector, solvertype="QF_NRA")

A collection of boolean constraints with an associated Z3 solver.

This type wraps a vector of SymbolicUtils boolean expressions and manages the corresponding Z3 solver context. Constraints are automatically converted to Z3 format and added to the solver upon construction.

Arguments

• constraints::Vector: Vector of boolean SymbolicUtils expressions
• solvertype::String="QF_NRA": Z3 solver type to use

Fields

• constraints::Vector: Original SymbolicUtils expressions
• solver::Z3.Solver: Z3 solver instance with constraints added
• context::Z3.Context: Z3 context associated with the solver

Examples

using SymbolicUtils, SymbolicSMT
@syms x::Real y::Real

# Single constraint
c1 = Constraints([x > 0])

# Multiple constraints
c2 = Constraints([x > 0, y > 0, x + y < 10])

# Specify solver type
c3 = Constraints([x > 0], "QF_LRA")

issatisfiable(expr, constraints::Constraints)

Check whether the given expression can be satisfied under the constraints.

Determines if there exists at least one assignment of variables that makes both the constraints and the expression true.

Arguments

• expr: Boolean expression to check for satisfiability
• constraints::Constraints: Constraints that must be satisfied

Returns

• true: The expression can be satisfied given the constraints
• false: The expression cannot be satisfied given the constraints
• nothing: The solver cannot determine satisfiability (unknown)

Examples

using SymbolicUtils, SymbolicSMT
@syms x::Real y::Real

constraints = Constraints([x > 0, y > 0])

# Can x be negative?
issatisfiable(x < 0, constraints)  # false

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

issatisfiable(expr::Bool, ::Constraints)

Handle satisfiability checking for boolean literals.

Boolean literals are trivially satisfiable based on their truth value.

Arguments

• expr::Bool: Boolean literal (true or false)
• ::Constraints: Constraints (ignored for boolean literals)

Returns

The boolean value itself.

issatisfiable(expr::Num, constraints::Constraints)

Check satisfiability of a Symbolics.jl Num expression.

This convenience method accepts Num expressions from Symbolics.jl, unwraps them to SymbolicUtils, and delegates to the core implementation.

Arguments

• expr::Num: Boolean expression to check for satisfiability
• constraints::Constraints: Constraints that must be satisfied

Returns

• true: The expression can be satisfied given the constraints
• false: The expression cannot be satisfied given the constraints
• nothing: The solver cannot determine satisfiability (unknown)

Examples

using Symbolics, SymbolicSMT

@variables x::Real y::Real
constraints = Constraints([x > 0, y > 0])

# Check with Symbolics.jl Num expressions
issatisfiable(x < 0, constraints)        # false
issatisfiable(x + y > 1, constraints)    # true

isprovable(expr, constraints::Constraints)

Check whether the given expression is provable (always true) under the constraints.

An expression is provable if it is true for all assignments of variables that satisfy the constraints. This is equivalent to checking that the negation of the expression is unsatisfiable under the constraints.

Arguments

• expr: Boolean expression to check for provability
• constraints::Constraints: Constraints under which to check provability

Returns

• true: The expression is provable (always true) given the constraints
• false: The expression is not provable given the constraints

Examples

using SymbolicUtils, SymbolicSMT
@syms x::Real y::Real

constraints = Constraints([x >= 0, y >= 0])

# Is x + y always non-negative?
isprovable(x + y >= 0, constraints)  # true

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

isprovable(expr::Num, constraints::Constraints)

Check provability of a Symbolics.jl Num expression.

This convenience method accepts Num expressions from Symbolics.jl, unwraps them to SymbolicUtils, and delegates to the core implementation.

Arguments

• expr::Num: Expression to check for provability
• constraints::Constraints: Constraints under which to check provability

Returns

• true: The expression is provably true under the constraints
• false: The expression can be false under the constraints

Examples

using Symbolics, SymbolicSMT

@variables x::Real y::Real
constraints = Constraints([x >= 0, y >= 0])

# Check provability with Symbolics.jl
isprovable(x >= 0, constraints)     # true
isprovable(x > y, constraints)      # false

resolve(expr, constraints::Constraints)

Attempt to resolve an expression to a boolean constant using the constraints.

Tries to determine if the expression is provably true or provably false under the given constraints. If neither can be proven, returns the original expression unchanged.

Arguments

• expr: Expression to resolve
• constraints::Constraints: Constraints to use for resolution

Returns

• true: If the expression is provably true
• false: If the expression is provably false
• expr: The original expression if it cannot be resolved

Examples

using SymbolicUtils, SymbolicSMT
@syms x::Real

constraints = Constraints([x > 5])

resolve(x > 0, constraints)   # true (provable)
resolve(x < 0, constraints)   # false (provable negation)
resolve(x > 10, constraints)  # x > 10 (cannot resolve)

resolve(expr::Num, constraints::Constraints)

Resolve a Symbolics.jl Num expression to a boolean constant if possible.

This convenience method accepts Num expressions from Symbolics.jl, unwraps them to SymbolicUtils, delegates to the core implementation, and wraps boolean results back to Num if needed.

Arguments

• expr::Num: Expression to resolve
• constraints::Constraints: Constraints to use for resolution

Returns

• true: If the expression is provably true
• false: If the expression is provably false
• Num: The wrapped original expression if it cannot be resolved

Examples

using Symbolics, SymbolicSMT

@variables x::Real
constraints = Constraints([x > 5])

resolve(x > 0, constraints)    # true
resolve(x < 0, constraints)    # false  
resolve(x > 10, constraints)   # x > 10 (as Num)