cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright(c) 2014-2016 Galois, Inc.
Safe HaskellSafe



Desugar into SMTLIB Terminology



desugarProp :: Prop -> IfExpr Prop Source #

Assumes simplified, linear, defined.

smtName :: Name -> String Source #

The name of a variable in the SMT translation.

smtFinName :: Name -> String Source #

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

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

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

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.