-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A theory solver for conjunctions of literals in the theory of uninterpreted functions with equality
--   
--   A theory solver for conjunctions of literals in the theory of
--   uninterpreted functions with equality
@package EqualitySolver
@version 0.1.0.2

module EqualitySolver.Solver
data EqFormula
data EqLiteral
data EqTerm
type Name = String
type Arity = Int

-- | Build a conjunction of literals out of a list of literals
eqF :: [EqLiteral] -> EqFormula

-- | 'eq a b' builds the literal a = b
eq :: EqTerm -> EqTerm -> EqLiteral

-- | 'neq a b' builds the literal 'not (a = b)'
neq :: EqTerm -> EqTerm -> EqLiteral

-- | Returns a new variable
var :: Name -> EqTerm

-- | Returns a new function
fun :: Name -> Arity -> [EqTerm] -> EqTerm

-- | Returns true if the conjunction of literals given as an argument is
--   satisfiable in the first order theory of uninterpreted functions with
--   equality
satisfiableInEq :: EqFormula -> Bool
instance Eq Predicate
instance Ord Predicate
instance Show Predicate
instance Eq EqTerm
instance Ord EqTerm
instance Eq EqLiteral
instance Ord EqLiteral
instance Show EqLiteral
instance Eq EqFormula
instance Ord EqFormula
instance Show EqFormula
instance Show EqState
instance Show EqTerm