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:


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