Module BoolExp

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

bNot :: BoolExp -> BoolExp   

A Boolean negation.

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