| Safe Haskell | Safe-Inferred |
|---|
FirstOrderTheory.Theory
- class FirstOrderTheory t where
- theoryName :: t -> String
- sorts :: t -> Set Sort
- predicates :: t -> Set PredicateDecl
- functions :: t -> Set FunctionDecl
- decideSat :: t -> Set Literal -> (Bool, Set Literal)
- data PredicateDecl
- data FunctionDecl
- nnfLit :: Literal -> NNFFormula
- nnfCon :: NNFFormula -> NNFFormula -> NNFFormula
- nnfDis :: NNFFormula -> NNFFormula -> NNFFormula
- predicateDecl :: Name -> Arity -> [Sort] -> PredicateDecl
- functionDecl :: Name -> Arity -> [Sort] -> Sort -> FunctionDecl
Documentation
class FirstOrderTheory t where
Description of a decidable first order theory
Methods
theoryName :: t -> String
predicates :: t -> Set PredicateDecl
functions :: t -> Set FunctionDecl
data PredicateDecl
Instances
data FunctionDecl
Instances
nnfLit :: Literal -> NNFFormula
Returns a NNF Formula consisting of only the input literal
nnfCon :: NNFFormula -> NNFFormula -> NNFFormula
Returns the conjunction of two NNF formulas
nnfDis :: NNFFormula -> NNFFormula -> NNFFormula
Return the disjunction of two NNF formulas
predicateDecl :: Name -> Arity -> [Sort] -> PredicateDecl
Specify a new predicate declaration
functionDecl :: Name -> Arity -> [Sort] -> Sort -> FunctionDecl
Specify a new function declaration