Module suggestion_solver 

Validity check + Quantifier Elimination. Used to make suggestions.

Structs

ConstraintGlobalEnv 🔒

ConstraintLocalEnv 🔒

Declarations active in a single constraint’s solver scope (as a string to send to Z3), and maps to decode its response back to T.

SuggestionSolver

Enums

SuggestionSolverError

Functions

application_head 🔒

atom_symbol 🔒

conjunction 🔒

exact_arg 🔒

prune_vacuous 🔒

substitute_sexp 🔒