Repository navigation
Multiple queries/API change #6
Description
Right now, the symbolic evaluator API simply permits only a single query to the SMT solver. Sometimes there is benefit in permitting multiple queries however. For example, if you have a query over two disjoint properties it is better to query separately. Splitting the query into two annotations might duplicate work in the evaluation, which is also problematic. Even worse, if we want to conditionally do more queries, we cannot... For example, if we want to increase a bound for iterative deepening.
The solution I propose for now would be through a monadic interface of the evaluator instead. That is, instead of boolean functions, we would expect a function of type Sym (). The Sym monad would have a few built-in functions it exposes:
- Query an SMT solver for satisfiability (or validity) of a given expression.
- Write a counterexample expression to a function definition Counterexample should not require search over entire module to be provided #5
- Optionally enable the fresh variable generation Fresh variable generation API #3
These functions thus should get very special meaning in the evaluator, but it would permit a much richer way to use the symbolic evaluator!
Activity
[-]Multiple queries[/-][+]Multiple queries/API change[/+]RobinWebbers commentedon Oct 16, 2026
Here's a few more that might make sense:
Regarding satisfiability/validity check, perhaps the most modular way to permit these is by having functions to catch
Unreachable,UndefinedBehaviourandRaise? The alternative is to bake these into the check.Note, we should btw error if we do not get a unit value at the end of eval.