Initial Solution (from Qualifiers and WF constraints) ---------------------

Update Solution

update s kqs sets in s each KVar in kqs to the corresponding QBind.

Yields a pair (b, s') where b is true if the mapping of any KVar was changed.

Precondition: kqs contains no duplicate KVars.

applyInSortedReft applies the solution to a single sorted reft

Predicate corresponding to LHS of constraint in current solution

Simplifies existential expressions with unused or inconsequential bindings.

Simplification is helpful for human readability of solutions. It makes easier reporting errors. Sometimes it can be useful for debugging if run on queries sent to the SMT solver. We don't do that by default because some benchmarks show a slowdown in some cases.

For instance, in the following example, "x" is not used at all.

simplifyKVar "exists x y. y == z && y == C"
  ==
"exists y. y == z && y == C"

And in the following example, x is used but in a way that doesn't contribute any useful knowledge.

simplifyKVar "exists x y. x == C && y == z && y == C"
  ==
"exists y. y == z && y == C"

Therefore we eliminate variables that appear in equalities via substitutions.

simplifyKVar "exists x y. x == C && P && Q y"
  ==
"exists y. (P && Q y)[x:=C]"

The first parameter is the set of symbols that can appear free in the input expression. At the moment, this only needs to include the free variables that start with the subst$ prefix.

Determine if two expressions are alpha-equivalent.

Takes as first parameter the set of variables that might appear free in the expressions to compare.

Doesn't handle all cases, just enough for simplifying KVars which requires alpha-equivalence checking of existentially quantified expressions.