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
Symbolic equality
Symbolic ordering
Arithmetic operations
Logical operations
Splitting, joining, and extending
Sign-casting
Indexed lookups
Word-level operations
Conditionals: Mergeable values
Uninterpreted sorts, constants, and functions
Properties, proofs, and satisfiability
Proving properties
Checking satisfiability
Proving properties using multiple solvers
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