cryptol-2.4.0: Cryptol: The Language of Cryptography

Cryptol.TypeCheck.Solver.Numeric.SMT

Description

Desugar into SMTLIB Terminology

Synopsis

# Documentation

Assumes simplified, linear, defined.

The name of a variable in the SMT translation.

The name of a boolean variable, representing fin x.

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.

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') Source #

Get the values for the given names.