| 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
- 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
predicateDecl :: Name -> Arity -> [Sort] -> PredicateDecl
Specify a new predicate declaration
functionDecl :: Name -> Arity -> [Sort] -> Sort -> FunctionDecl
Specify a new function declaration