Module BoolExp

This library defines a very simple structure for Boolean expressions

Summary of exported operations:

bTrue
                  :: BoolExp

A Boolean true.

bFalse
                  :: BoolExp

A Boolean false.

bEqu
                  :: BoolExp -> BoolExp -> BoolExp

An equality between two Boolean terms.

bEquVar
                  :: Int -> BoolExp -> BoolExp

An equality between a variable and a Boolean term.

bindingBE
                  :: String -> [(Int,BoolExp)] -> BoolExp -> BoolExp

A binding for a list of binding variables.

letBinding
                  :: [(Int,BoolExp)] -> BoolExp -> BoolExp

A "let" binding.

forallBinding
                  :: [(Int,BoolExp)] -> BoolExp -> BoolExp

A "forall" binding.

existsBinding
                  :: [(Int,BoolExp)] -> BoolExp -> BoolExp

An "exists" binding.

assertSMT
                  :: BoolExp -> BoolExp

An assertion of a Boolean expression.

allSymbolsOfBE
                  :: BoolExp -> [String]

simpBE
                  :: BoolExp -> BoolExp

showBoolExp
                  :: BoolExp -> String

smtBE
                  :: BoolExp -> String

asLisp
                  :: [String] -> String

prettyBE
                  :: BoolExp -> String

withBracket
                  :: String -> String

Exported datatypes:

BoolExp

Datatype for Boolean expressions.

Constructors:

BVar :: Int -> BoolExp
BTerm :: String -> [BoolExp] -> BoolExp
Conj :: [BoolExp] -> BoolExp
Disj :: [BoolExp] -> BoolExp
Not :: BoolExp -> BoolExp
Binding :: String -> [(Int,BoolExp)] -> BoolExp -> BoolExp

Exported operations:

bTrue :: BoolExp

A Boolean true.

Further infos:

solution complete, i.e., able to compute all solutions

bFalse :: BoolExp

A Boolean false.

Further infos:

solution complete, i.e., able to compute all solutions

bEqu :: BoolExp -> BoolExp -> BoolExp

An equality between two Boolean terms.

Further infos:

solution complete, i.e., able to compute all solutions

bEquVar :: Int -> BoolExp -> BoolExp

An equality between a variable and a Boolean term.

Further infos:

solution complete, i.e., able to compute all solutions

bindingBE :: String -> [(Int,BoolExp)] -> BoolExp -> BoolExp

A binding for a list of binding variables.

letBinding :: [(Int,BoolExp)] -> BoolExp -> BoolExp

A "let" binding.

forallBinding :: [(Int,BoolExp)] -> BoolExp -> BoolExp

A "forall" binding.

existsBinding :: [(Int,BoolExp)] -> BoolExp -> BoolExp

An "exists" binding.

assertSMT :: BoolExp -> BoolExp

An assertion of a Boolean expression.

Further infos:

solution complete, i.e., able to compute all solutions

allSymbolsOfBE :: BoolExp -> [String]

simpBE :: BoolExp -> BoolExp

showBoolExp :: BoolExp -> String

smtBE :: BoolExp -> String

asLisp :: [String] -> String

prettyBE :: BoolExp -> String

withBracket :: String -> String

Further infos:

solution complete, i.e., able to compute all solutions