cryptol-2.4.0: Cryptol: The Language of Cryptography

Cryptol.TypeCheck.Solver.Numeric.NonLin

Description

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.

Synopsis

# Documentation

nonLinProp :: NonLinS -> Prop -> ([Prop], NonLinS) Source #

Factor-out non-linear terms, by naming them.

data NonLinS Source #

Instances

 Source # MethodsshowList :: [NonLinS] -> ShowS #

Get the known non-linear terms.

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