DifferenceLogic (empty) → 0.1.0.1

raw patch · 4 files changed

+201/−0 lines, 4 filesdep +HUnitdep +basedep +containerssetup-changed

Dependencies added: HUnit, base, containers, fgl

Files

• DifferenceLogic.cabal +29/−0
• LICENSE +30/−0
• Setup.hs +2/−0
• src/DifferenceLogic/Solver.hs +140/−0

@@ -0,0 +1,29 @@+-- Initial DifferenceLogic.cabal generated by cabal init.  For further +-- documentation, see http://haskell.org/cabal/users-guide/++name:                DifferenceLogic+version:             0.1.0.1+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:+		     >+		     <+		     >=+		     <=+		     =+		     It does not currently support disequality+license:             BSD3+license-file:        LICENSE+author:              Dillon Huff+maintainer:          dillonhuff@gmail.com+homepage:	     https://github.com/dillonhuff/DifferenceLogic+-- copyright:           +category:            Math+build-type:          Simple+cabal-version:       >=1.8++library+  exposed-modules:     DifferenceLogic.Solver+  -- other-modules:       +  build-depends:       base ==4.6.*, containers ==0.5.*, HUnit ==1.2.*, fgl+  hs-source-dirs:      src

@@ -0,0 +1,30 @@+Copyright (c) 2014, Dillon Huff++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE CONTRIBUTORS ``AS IS'' AND ANY EXPRESS+OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,140 @@+module DifferenceLogic.Solver(+  zF,+  zLit,+  eq, gt, lt, geq, leq,+  consistentOverZ) where++import Data.Graph.Inductive.Graph+import Data.Graph.Inductive.PatriciaTree+import Data.List as L+import Data.Map as M+import Data.Maybe+import Data.Set as S++-- This solver solves conjuctions of literals+data ZFormula = ZFormula (Set ZLiteral)+                deriving (Eq, Ord, Show)++zF :: [ZLiteral] -> ZFormula+zF litList = ZFormula $ S.fromList litList++data ZLiteral = ZLiteral {+  left :: String,+  right :: String,+  predicate :: Predicate,+  const :: Int+  } deriving (Eq, Ord, Show)++zLit = ZLiteral++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)]+normalizeLiteral (ZLiteral l r Gt c) = [zLit r l leq (-(c - 1))]+normalizeLiteral (ZLiteral l r Geq c) = [zLit r l leq (-c)]+normalizeLiteral l = [l]++literalNames :: ZLiteral -> [String]+literalNames (ZLiteral l r _ _) = [l, r]++buildLiteralEdge :: Map String Node -> ZLiteral -> LEdge Int+buildLiteralEdge namesToNodes (ZLiteral l r Leq c) = (lNode, rNode, c)+  where+    lNode = fromJust $ M.lookup l namesToNodes+    rNode = fromJust $ M.lookup r namesToNodes+buildLiteralEdge _ l = error $ "Trying to build literal from " ++ show l++data Predicate+  = Eq+  | Lt+  | Gt+  | Leq+  | Geq+    deriving (Eq, Ord, Show)++eq = Eq+lt = Lt+gt = Gt+leq = Leq+geq = Geq++consistentOverZ :: ZFormula -> Bool+consistentOverZ formula = not $ containsNegCycle formulaGraph+  where+    normedForm = normalizeFormula formula+    nodeList = buildNodeList normedForm+    litNameNodeMap = M.fromList $ L.map (\(n, s) -> (s, n)) nodeList+    edgeList = buildEdgeList normedForm litNameNodeMap+    formulaGraph = mkGraph nodeList edgeList :: Gr String Int++buildNodeList :: ZFormula -> [(Node, String)]+buildNodeList (ZFormula lits) = L.zip [1..(length litNames)] litNames+  where+    litNames = L.nub $ L.concat $ L.map literalNames $ S.toList lits++buildEdgeList :: ZFormula -> Map String Node -> [LEdge Int]+buildEdgeList (ZFormula lits) namesToNodes = edgeList+  where+    edgeList = S.toList $ S.map (buildLiteralEdge namesToNodes) lits++normalizeFormula :: ZFormula -> ZFormula+normalizeFormula (ZFormula lits) = ZFormula $ S.fromList normedLits+  where+    normedLits = L.concat $ L.map normalizeLiteral $ S.toList lits++containsNegCycle :: Gr String Int -> Bool+containsNegCycle formulaGraph = case isEmpty formulaGraph of+  True -> False+  False -> negCycleFrom headNode graphNodes graphEdges+  where+    graphNodes = nodes formulaGraph+    graphEdges = labEdges formulaGraph+    headNode = head graphNodes++negCycleFrom :: Node -> [Node] -> [LEdge Int] -> Bool+negCycleFrom source nodes edges = checkNegCycle edges weights+  where+    initialWeights = M.fromList $ L.zip nodes $ L.map (initWeight source) nodes+    weights = computeWeights nodes edges M.empty initialWeights 0++initWeight :: Node -> Node -> Int+initWeight source node = case source == node of+  True -> 0+  False -> maxBound :: Int++computeWeights :: [Node] ->+                  [LEdge Int] ->+                  Map Node Node ->+                  Map Node Int ->+                  Int ->+                  Map Node Int+computeWeights nodes edges predecessors weights i = case i == L.length nodes of+  True -> weights+  False -> computeWeights nodes edges newPredecessors newWeights (i + 1)+  where+    (newWeights, newPredecessors) = updateWeightsAndPreds edges weights predecessors++updateWeightsAndPreds :: [LEdge Int] ->+                         Map Node Int ->+                         Map Node Node ->+                         (Map Node Int, Map Node Node)+updateWeightsAndPreds edges weights preds = L.foldl updateEdge (weights, preds) edges++updateEdge :: (Map Node Int, Map Node Node) -> LEdge Int -> (Map Node Int, Map Node Node)+updateEdge (weights, preds) (u, v, w) = case wu + w < wv of+  True -> (M.insert v (wu + w) weights, M.insert v u preds)+  False -> (weights, preds)+  where+    wu = fromJust $ M.lookup u weights+    wv = fromJust $ M.lookup v weights++checkNegCycle :: [LEdge Int] -> Map Node Int -> Bool+checkNegCycle edges weights = L.or negCycleChecks+  where+    negCycleChecks = L.map (checkEdgeForNegCycle weights) edges++checkEdgeForNegCycle :: Map Node Int -> LEdge Int -> Bool+checkEdgeForNegCycle weights (u, v, w) = wu + w < wv+  where+    wu = fromJust $ M.lookup u weights+    wv = fromJust $ M.lookup v weights