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

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`

.