cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright | (c) 2014-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.TypeCheck.Solver.Numeric.SMT

Description

Desugar into SMTLIB Terminology

Synopsis

- desugarProp :: Prop -> IfExpr Prop
- smtName :: Name -> String
- smtFinName :: Name -> String
- ifPropToSmtLib :: IfExpr Prop -> SExpr
- cryImproveModel :: Solver -> Logger -> Map Name Nat' -> IO (Map Name Expr, [Prop])
- getVal :: Solver -> Name -> IO Nat'
- getVals :: Solver -> [Name] -> IO (Map Name Nat')

# Documentation

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`.

ifPropToSmtLib :: IfExpr Prop -> SExpr Source #

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.