DifferenceLogic 0.1.0.2 → 0.1.0.4

raw patch · 2 files changed

+4/−3 lines, 2 files

Files

• DifferenceLogic.cabal +1/−1
• src/DifferenceLogic/Solver.hs +3/−2

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                DifferenceLogic-version:             0.1.0.2+version:             0.1.0.4 synopsis:            A theory solver for conjunctions of literals in difference logic description:         This package contains a theory solver for conjunctions of literals 		     in difference logic. The logic supports predicates:

@@ -1,6 +1,7 @@ module DifferenceLogic.Solver(-  ZFormula, ZLiteral,+  IntegerDifferenceLogic,   integerDifferenceLogic,+  ZFormula, ZLiteral,   zF,   zLit,   eq, gt, lt, geq, leq,@@ -29,7 +30,7 @@   functions t = S.singleton minusFunc   decideSat t lits = case decideSatisfiability $ zF $ S.toList $ S.map toZLiteral lits of     True -> (True, S.empty)-    False -> (False, lits)+    False -> (False, S.map negateLit lits)  minusFunc = functionDecl "-" 2 [U.sort "Integer", U.sort "Integer"] (U.sort "Integer")