Programming with symbolic values
Symbolic types
Abstract symbolic value type
Arrays of symbolic values
Creating a symbolic variable
Operations on symbolic values
Boolean literals
Integer literals
Float literals
Algebraic reals (only from rationals)
Symbolic equality
Constructing concrete lists
Symbolic ordering
Arithmetic operations
Logical operations
Splitting, joining, and extending
Sign-casting
Numeric conversions
Indexed lookups
Word-level operations
Conditionals: Mergeable values
Uninterpreted sorts, constants, and functions
Properties, proofs, and satisfiability
Proving properties
Checking satisfiability
Checking safety
Proving properties using multiple solvers
Quick-check
Model extraction
Inspecting proof results
Programmable model extraction
SMT Interface: Configurations and solvers
Symbolic computations
Getting SMT-Lib output (for offline analysis)
Code generation from symbolic programs
Setting code-generation options
Designating inputs
Designating outputs
Designating return values
Code generation with uninterpreted functions
Code generation with SInteger
and SReal
types
Compilation to C