EqualitySolver.Solver

Documentation

data EqFormula

Instances

Eq EqFormula

Ord EqFormula

Show EqFormula

data EqLiteral

Instances

Eq EqLiteral

Ord EqLiteral

Show EqLiteral

data EqTerm

Instances

Eq EqTerm

Ord EqTerm

Show EqTerm

type Name = String

type Arity = Int

eqF :: [EqLiteral] -> EqFormula

Build a conjunction of literals out of a list of literals

eq :: EqTerm -> EqTerm -> EqLiteral

'eq a b' builds the literal a = b

neq :: EqTerm -> EqTerm -> EqLiteral

'neq a b' builds the literal 'not (a = b)'

var :: Name -> EqTerm

Returns a new variable

fun :: Name -> Arity -> [EqTerm] -> EqTerm

Returns a new function

satisfiableInEq :: EqFormula -> Bool

Returns true if the conjunction of literals given as an argument is satisfiable in the first order theory of uninterpreted functions with equality