GitHub

Symbolics.jl Interface

This page documents the Symbolics.jl frontend API for SymbolicSMT.jl, which provides a modern, user-friendly interface using @variables and Num types.

Overview

The Symbolics.jl interface wraps the core SymbolicUtils.jl backend with convenient dispatch methods that automatically handle conversion between Num and SymbolicUtils.Symbolic types.

Variable Creation

@variables Macro

The @variables macro is re-exported from Symbolics.jl for convenience. It creates symbolic variables with specified types:

using SymbolicSMT  # @variables is available directly

@variables x::Real y::Real z::Integer p::Bool

Constraint Construction

SymbolicSMT.Constraints — Method
Constraints(constraints::Vector{Num}, solvertype="QF_NRA")

Create constraints from Symbolics.jl Num expressions.

This is a convenience constructor that accepts Num types from Symbolics.jl, unwraps them to SymbolicUtils expressions, and creates the constraint set.

Arguments

  • constraints::Vector{Num}: Vector of boolean Symbolics.jl Num expressions
  • solvertype::String="QF_NRA": Z3 solver type to use

Examples

using Symbolics, SymbolicSMT

@variables x::Real y::Real

# Create constraints with Symbolics.jl syntax
constraints = Constraints([x > 0, y >= 0, x + y < 10])

# Use with standard SymbolicSMT functions
issatisfiable(x + y > 5, constraints)
source

Create constraints from Symbolics.jl Num expressions:

@variables x::Real y::Real

# Create constraints with Symbolics.jl syntax
constraints = Constraints([x > 0, y >= 0, x + y < 10])

Satisfiability Checking

SymbolicSMT.issatisfiable — Method
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
source

Check if a Num expression can be satisfied:

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

issatisfiable(x < 0, constraints)        # false
issatisfiable(x + y > 1, constraints)    # true

Provability Checking

SymbolicSMT.isprovable — Method
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
source

Check if a Num expression is always true:

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

isprovable(x >= 0, constraints)     # true
isprovable(x > y, constraints)      # false

Expression Resolution

SymbolicSMT.resolve — Method
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)
source

Resolve Num expressions to constants when possible:

@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)

Type Handling

Variable Types

The Symbolics.jl interface supports all standard variable types:

# Real numbers (continuous)
@variables position::Real velocity::Real

# Integers (discrete)  
@variables count::Integer index::Integer

# Booleans (logical)
@variables active::Bool valid::Bool

Expression Types

All expression types are automatically handled:

Arithmetic Expressions

@variables x::Real y::Real

expr1 = x + y
expr2 = 2*x - 3*y  
expr3 = x^2 + y^2
expr4 = -x + 5

Comparison Expressions

comp1 = x > y
comp2 = x >= 0
comp3 = x == 5
comp4 = x <= 10
comp5 = x < y + 1

Boolean Expressions

@variables p::Bool q::Bool

bool1 = p & q
bool2 = p | q
bool3 = !p
bool4 = (p & q) | (!p & !q)

Mixed Expressions

@variables x::Real p::Bool

mixed1 = (x > 0) & p
mixed2 = p | (x < 5)
mixed3 = p => (x >= 0)

Conversion Details

Automatic Unwrapping

Num expressions are automatically unwrapped to SymbolicUtils.Symbolic:

@variables x::Real
num_expr = x > 0                    # Symbolics.Num
symbolic_expr = unwrap(num_expr)    # SymbolicUtils.BasicSymbolic{Bool}

Automatic Wrapping

Results are wrapped back to Num when appropriate:

result = resolve(x > 10, constraints)
# If cannot resolve: returns Num
# If resolves to bool: returns Bool

Type Preservation

The interface preserves semantic meaning:

# Input: Num expression
# Processing: SymbolicUtils backend
# Output: Appropriate type (Bool for constants, Num for expressions)

Usage Patterns

Basic Workflow

using Symbolics, SymbolicSMT

# 1. Create variables
@variables x::Real y::Real

# 2. Define constraints  
constraints = Constraints([x >= 0, y >= 0])

# 3. Query system
result1 = issatisfiable(x + y > 5, constraints)  
result2 = isprovable(x >= 0, constraints)
result3 = resolve(x > 10, constraints)

Advanced Usage

# Mixed variable types
@variables pos::Real vel::Real gear::Integer active::Bool

# Complex constraint set
constraints = Constraints([
    pos >= 0,                           # Real constraint
    vel >= 0, vel <= 120,              # Real bounds
    gear >= 1, gear <= 5,              # Integer constraint
    active,                             # Boolean constraint
    active => (vel > 0),               # Conditional constraint
    (gear > 3) => (vel > 50)          # Gear-speed relationship
])

# Complex queries
can_be_stationary = issatisfiable(vel == 0, constraints)
always_moving = isprovable(vel > 0, constraints)  
high_gear_fast = isprovable((gear > 3) => (vel > 50), constraints)

Comparison with SymbolicUtils Interface

Symbolics.jl Interface (Recommended)

using Symbolics, SymbolicSMT

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

Benefits:

  • Modern Julia ecosystem standard
  • Clean @variables syntax
  • Automatic type handling
  • Better integration with other packages

SymbolicUtils.jl Interface

using SymbolicUtils, SymbolicSMT

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

When to use:

  • Advanced symbolic manipulation
  • Custom symbolic operations
  • Lower-level control
  • Existing SymbolicUtils.jl codebase

Mixed Usage

Both interfaces can be used together:

using Symbolics, SymbolicUtils, SymbolicSMT

# Mix Symbolics and SymbolicUtils variables
@variables x::Real          # Symbolics.Num
@syms y::Real              # SymbolicUtils.Symbolic

# Both work in the same constraint set
constraints = Constraints([x > 0, y > 0])
issatisfiable(x + y > 1, constraints)  # Works seamlessly

Error Handling

The Symbolics.jl interface provides the same error handling as the SymbolicUtils backend:

Conversion Errors

# If expressions cannot be converted to Z3
try
    constraints = Constraints([unsupported_expr])
catch e
    # Detailed error message about conversion failure
    println(e)
end

Type Mismatches

# Type mismatches are caught during unwrapping
@variables x::Real

# This would cause an error if x is used in boolean context incorrectly
# The error message will indicate the type mismatch

Performance Notes

Zero Overhead Design

The Symbolics.jl interface adds minimal overhead:

  • Dispatch cost: Single method lookup
  • Conversion cost: Simple unwrap/wrap operations
  • Backend unchanged: Same optimized SymbolicUtils processing

Memory Usage

  • Shared backend: No duplication of solver state
  • Minimal wrappers: Num types are lightweight wrappers
  • Efficient conversion: Direct delegation without copying

Recommendations

For best performance:

  1. Batch constraint creation rather than creating many small sets
  2. Use appropriate variable types for your problem domain
  3. Prefer the Symbolics interface for new code (better ecosystem integration)
  4. Mix interfaces judiciously - conversion has minimal but non-zero cost