Copyright | (c) 2014-2016 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
Separate Non-Linear Constraints When we spot a non-linear expression, we name it and add it to a map.
If we see the same expression multiple times, then we give it the same name.
The body of the non-linear expression is not processed further, so the resulting map should not contain any of the newly minted names.
Documentation
nonLinProp :: NonLinS -> Prop -> ([Prop], NonLinS) Source #
Factor-out non-linear terms, by naming them.
nonLinSubst :: NonLinS -> Subst Source #
Get the known non-linear terms.
initialNonLinS :: NonLinS Source #
The initial state for the linearization process.
apSubstNL :: Subst -> NonLinS -> Maybe (Subst, [Prop], NonLinS) Source #
Apply a substituin to the non-linear expression database.
Returns Nothing
if nothing was affected.
Otherwise returns Just
, and a substitution for non-linear expressions
that became linear.
The definitions of NL terms do not contain other named NL terms,
so it does not matter if the substitution contains bindings like _a = e
.
There should be no bindings that mention NL term names in the definitions
of the substition (i.e, things like x = _a
are NOT ok).