DifferenceLogic 0.1.0.1 → 0.1.0.2

raw patch · 2 files changed

+87/−6 lines, 2 filesdep +FirstOrderTheory

Dependencies added: FirstOrderTheory

Files

• DifferenceLogic.cabal +2/−2
• src/DifferenceLogic/Solver.hs +85/−4

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                DifferenceLogic-version:             0.1.0.1+version:             0.1.0.2 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:@@ -25,5 +25,5 @@ library   exposed-modules:     DifferenceLogic.Solver   -- other-modules:       -  build-depends:       base ==4.6.*, containers ==0.5.*, HUnit ==1.2.*, fgl+  build-depends:       base ==4.6.*, containers ==0.5.*, HUnit ==1.2.*, fgl, FirstOrderTheory   hs-source-dirs:      src

@@ -1,8 +1,10 @@ module DifferenceLogic.Solver(+  ZFormula, ZLiteral,+  integerDifferenceLogic,   zF,   zLit,   eq, gt, lt, geq, leq,-  consistentOverZ) where+  decideSatisfiability) where  import Data.Graph.Inductive.Graph import Data.Graph.Inductive.PatriciaTree@@ -11,13 +13,41 @@ import Data.Maybe import Data.Set as S --- This solver solves conjuctions of literals+import FirstOrderTheory.Syntax+import FirstOrderTheory.Theory as T+import FirstOrderTheory.Utils as U++-- | FirstOrderTheory implementation for integer difference logic+data IntegerDifferenceLogic = IDF++integerDifferenceLogic = IDF++instance FirstOrderTheory IntegerDifferenceLogic where+  theoryName t = "IntegerDifferenceLogic"+  sorts t = S.singleton $ U.sort "Integer"+  predicates t = S.fromList [eqPred, leqPred, geqPred, ltPred, gtPred]+  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)++minusFunc = functionDecl "-" 2 [U.sort "Integer", U.sort "Integer"] (U.sort "Integer")++eqPred = predicateDecl "=" 2 [U.sort "Integer", U.sort "Integer"]+leqPred = predicateDecl "<=" 2 [U.sort "Integer", U.sort "Integer"]+geqPred = predicateDecl ">=" 2 [U.sort "Integer", U.sort "Integer"]+ltPred = predicateDecl "<" 2 [U.sort "Integer", U.sort "Integer"]+gtPred = predicateDecl ">" 2 [U.sort "Integer", U.sort "Integer"]++-- |A conjunction of literals in integer difference logic data ZFormula = ZFormula (Set ZLiteral)                 deriving (Eq, Ord, Show) +-- | Make a conjuction of literals in integer difference logic zF :: [ZLiteral] -> ZFormula zF litList = ZFormula $ S.fromList litList +-- |Literal of the form 'a - b <predicate> <integer constant> data ZLiteral = ZLiteral {   left :: String,   right :: String,@@ -25,8 +55,52 @@   const :: Int   } deriving (Eq, Ord, Show) +-- |'zLit a b <pred> c' returns the literal 'a - b <pred> c' zLit = ZLiteral +toZLiteral :: Literal -> ZLiteral+toZLiteral l = case isNeg l of+  True -> negateZLit $ toZLit predL+  False -> toZLit predL+  where+    predL = getAtom l++toZLit :: Atom -> ZLiteral+toZLit a = case predicateName a of+  "=" -> ZLiteral leftVar rightVar Eq constVal+  ">" -> ZLiteral leftVar rightVar Gt constVal+  "<" -> ZLiteral leftVar rightVar Lt constVal+  "<=" -> ZLiteral leftVar rightVar Leq constVal+  ">=" -> ZLiteral leftVar rightVar Geq constVal+  other -> error $ "Predicate " ++ other ++ " is not supported"+  where+    args = extractArgs a+    leftVar = varName $ args !! 0+    rightVar = varName $ args !! 1+    constVal = intVal $ args !! 2++extractArgs :: Atom -> [Term]+extractArgs a = case length pArgs /= 2 of+  True -> error $ "Too many arguments to " ++ show a+  False -> vars ++ [const]+  where+    pArgs = atomArgs a+    vars = extractVars pArgs+    const = head $ tail pArgs++extractVars :: [Term] -> [Term]+extractVars (x:y:[]) = case isFunctionWithName "-" x of+  True -> funcArgs x+  False -> error $ show x ++ " is not a valid function in integer difference logic"++negateZLit :: ZLiteral -> ZLiteral+negateZLit (ZLiteral l r Lt c) = ZLiteral l r Geq c+negateZLit (ZLiteral l r Gt c) = ZLiteral l r Leq c+negateZLit (ZLiteral l r Geq c) = ZLiteral l r Lt c+negateZLit (ZLiteral l r Leq c) = ZLiteral l r Gt c+negateZLit eqLit@(ZLiteral l r Eq c) =+  error $ "Error: Cannot negate " ++ show eqLit ++ ", this solver does not currently support disequality"+ normalizeLiteral :: ZLiteral -> [ZLiteral] normalizeLiteral (ZLiteral l r Eq c) = [zLit l r leq c, zLit r l leq (-c)] normalizeLiteral (ZLiteral l r Lt c) = [zLit l r leq (c - 1)]@@ -52,14 +126,21 @@   | Geq     deriving (Eq, Ord, Show) +-- |Predicate '=' eq = Eq+-- |Predicate '<' lt = Lt+-- |Predicate '>' gt = Gt+-- |Predicate '<=' leq = Leq+-- |Predicate '>=' geq = Geq -consistentOverZ :: ZFormula -> Bool-consistentOverZ formula = not $ containsNegCycle formulaGraph+-- Solver for conjunctions of literals++decideSatisfiability :: ZFormula -> Bool+decideSatisfiability formula = not $ containsNegCycle formulaGraph   where     normedForm = normalizeFormula formula     nodeList = buildNodeList normedForm