Cryptol.TypeCheck.Solver.Numeric.NonLin

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)

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

data NonLinS

Instances

Show NonLinS

Methods

showsPrec :: Int -> NonLinS -> ShowS

show :: NonLinS -> String

showList :: [NonLinS] -> ShowS

nonLinSubst :: NonLinS -> Subst

Get the known non-linear terms.

initialNonLinS :: NonLinS

The initial state for the linearization process.

apSubstNL :: Subst -> NonLinS -> Maybe (Subst, [Prop], NonLinS)

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

lookupNL :: Name -> NonLinS -> Maybe Expr