Cryptol.TypeCheck.Solver.Numeric

Solver code that does not depend on the type inference monad.

Documentation

numericStep :: OrdFacts -> Goal -> Solved

Try to perform a single step of simplification for a numeric goal. We assume that the substitution has been applied to the goal.

simpFin :: OrdFacts -> Prop -> Maybe [Prop]

goalOrderModel :: OrdFacts -> [Goal] -> (OrdFacts, [Goal], [Goal])

Collect fin and <= constraints in the ord model Returns (new model, bad goals, other goals). "bad goals" are goals that are incompatible with the model "other goals" are ones that are not "<=" or "fin"