Eval package:sbv
Monad for performing symbolic evaluation.
Evaluate a symbolic tree, obtaining a symbolic value. Note how we
structure this evaluation so we impose extra constraints on what
values square-root, divide etc. can take. This is the power of the
symbolic approach: We can put arbitrary symbolic constraints as we
evaluate the tree.
Given an expression, symbolically evaluate it
Symbolic evaluation function for
Term.
For crackNum: The surface representation of variables, if available
Extract the value of an objective
Validate optimization results. NB: Does NOT make sure the model is
optimal, just checks they satisfy the constraints.
Most generalized form of uninterpretation, this function should not be
needed by end-user-code, but is rather useful for the library
development.
A demonstration of the use of the
SymbolicT and
QueryT
transformers in the setting of symbolic program evaluation.
In this example, we perform symbolic evaluation across three steps:
- allocate free variables, so we can extract a model after
evaluation
- perform symbolic evaluation of a program and an associated
property
- querying the solver for whether it's possible to find a set of
program inputs that falsify the property. if there is, we extract a
model.
To simplify the example, our programs always have exactly two integer
inputs named
x and
y.
Runs symbolic evaluation, sending a
Term to a symbolic value
(or failing). Used for symbolic evaluation of programs and properties.
Performs symbolic evaluation of a
Program.
Performs symbolic evaluation of a t'Property.