EqualitySolver 0.1.0.0 → 0.1.0.1

raw patch · 2 files changed

+10/−1 lines, 2 files

Files

• EqualitySolver.cabal +1/−1
• src/EqualitySolver/Solver.hs +9/−0

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                EqualitySolver-version:             0.1.0.0+version:             0.1.0.1 synopsis:            A theory solver for conjunctions of literals in the theory of uninterpreted functions with equality -- description:          license:             BSD3

@@ -11,6 +11,9 @@ import Data.Maybe import Data.Set as S +-- |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 satisfiableInEq formula = fst $ runDecideEq $ decideEq formula @@ -18,6 +21,7 @@ data EqFormula = EqFormula (Set EqLiteral)                  deriving (Eq, Ord, Show) +-- |Build a conjunction of literals out of a list of literals eqF = EqFormula . S.fromList  allTerms :: EqFormula -> [EqTerm]@@ -36,7 +40,10 @@   = EqLiteral Predicate EqTerm EqTerm     deriving (Eq, Ord, Show) +-- |'eq a b' builds the literal a = b eq = EqLiteral Eq++-- |'neq a b' builds the literal 'not (a = b)' neq = EqLiteral Neq  isEq (EqLiteral Eq _ _) = True@@ -62,7 +69,9 @@ showEqTerm (Function name arity args) = name ++ "(" ++ intercalate "," (L.map show args) ++ ")" showEqTerm (Variable name) = name +-- |Returns a new variable var = Variable+-- |Returns a new function fun = Function  subTerms :: EqTerm -> [EqTerm]