Cryptol.TypeCheck.Solver.Numeric.SMT

Desugar into SMTLIB Terminology

Documentation

desugarProp :: Prop -> IfExpr Prop

Assumes simplified, linear, defined.

smtName :: Name -> String

The name of a variable in the SMT translation.

smtFinName :: Name -> String

The name of a boolean variable, representing `fin x`.

ifPropToSmtLib :: IfExpr Prop -> SExpr

cryImproveModel :: Solver -> Logger -> Map Name Nat' -> IO (Map Name Expr, [Prop])

Given a model, compute an improving substitution, implied by the model. The entries in the substitution look like this:

• x = A variable x must equal constant A
• x = y variable x must equal variable y
• x = A * y + B (coming soon) variable x is a linear function of y, A and B are natural numbers.

We are mostly interested in improving unification variables. However, it is also useful to improve skolem variables, as this could turn non-linear constraints into linear ones. For example, if we have a constraint x * y = z, and we can figure out that x must be 5, then we end up with a linear constraint 5 * y = z.

getVal :: Solver -> Name -> IO Nat'

Get the value for the given name. * Assumes that we are in a SAT state (i.e., there is a model) * Assumes that the name is in the model

getVals :: Solver -> [Name] -> IO (Map Name Nat')

Get the values for the given names.