Copyright | (c) 2014-2016 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
Desugar into SMTLIB Terminology
Documentation
desugarProp :: Prop -> IfExpr Prop Source
Assumes simplified, linear, defined.
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
variablex
must equal constantA
x = y
variablex
must equal variabley
x = A * y + B
(coming soon) variablex
is a linear function ofy
,A
andB
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
.