Data.Integer.Presburger.Form

Documentation

check :: Form (Prop PosP) -> Bool

data Conn

Constructors

And

Or

Instances

Eq Conn

PP Conn

data Form p

Constructors

Node !Conn (Form p) (Form p)

Leaf !p

Ex Bool (Name, Integer) (Form p)

Instances

Functor Form

PP p => PP (Form p)

form_lcm :: Form (NormProp CVarP) -> Integer

form_scale :: Name -> Form (Prop PosP) -> Form (NormProp VarP)

a_b_sets :: (Integer, [Term], [Term]) -> NormProp VarP -> (Integer, [Term], [Term])

form_pos_inf :: Term -> Form (NormProp VarP) -> Form (Prop PosP)

form_neg_inf :: Term -> Form (NormProp VarP) -> Form (Prop PosP)

form_no_inf :: Term -> Form (NormProp VarP) -> Form (Prop PosP)

neg :: Form (Prop PosP) -> Form (Prop PosP)

simplify :: Form (Prop PosP) -> Form (Prop PosP)

ex_step :: Name -> Form (Prop PosP) -> Form (Prop PosP)

thm_as :: [Term] -> Name -> Form (NormProp VarP) -> Form (Prop PosP)

thm_bs :: [Term] -> Name -> Form (NormProp VarP) -> Form (Prop PosP)

form_bound :: Form (NormProp VarP) -> Integer

eval_form :: Form (Prop PosP) -> Env -> Bool

split_ands :: Form p -> [Form p]

split_divs :: Form (Prop PosP) -> ([DivCtr], Form (Prop PosP))

eval_conn :: Conn -> Bool -> Bool -> Bool

subst_form :: Name -> Integer -> Form (Prop PosP) -> Form (Prop PosP)

module Data.Integer.Presburger.Prop