{-# OPTIONS_GHC -Wall #-}
module ToySolver.Arith.DifferenceLogic
( SimpleAtom (..)
, Diff (..)
, solve
) where
import Data.Hashable
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HashMap
import Data.HashSet (HashSet)
import qualified Data.HashSet as HashSet
import Data.Monoid
import ToySolver.Graph.ShortestPath (bellmanFord, lastInEdge, bellmanFordDetectNegativeCycle, monoid')
infixl 6 :-
infix 4 :<=
data Diff v = v :- v
deriving (Eq, Ord, Show)
data SimpleAtom v b = Diff v :<= b
deriving (Eq, Ord, Show)
solve
:: (Hashable label, Eq label, Hashable v, Eq v, Real b)
=> [(label, SimpleAtom v b)]
-> Either (HashSet label) (HashMap v b)
solve xs =
case bellmanFordDetectNegativeCycle (monoid' (\(_,_,_,l) -> Endo (l:))) g d of
Just f -> Left $ HashSet.fromList $ appEndo f []
Nothing -> Right $ fmap (\(c,_) -> - c) d
where
vs = HashSet.toList $ HashSet.fromList [v | (_,(a :- b :<= _)) <- xs, v <- [a,b]]
g = HashMap.fromList [(a,[(b,k,l)]) | (l,(a :- b :<= k)) <- xs]
d = bellmanFord lastInEdge g vs
_test_sat :: Either (HashSet Int) (HashMap Char Int)
_test_sat = solve xs
where
xs :: [(Int, SimpleAtom Char Int)]
xs = [(1, ('a' :- 'b' :<= 2)), (2, ('b' :- 'c' :<= 3)), (3, ('c' :- 'a' :<= -3))]
_test_unsat :: Either (HashSet Int) (HashMap Char Int)
_test_unsat = solve xs
where
xs :: [(Int, SimpleAtom Char Int)]
xs = [(1, ('a' :- 'b' :<= 2)), (2, ('b' :- 'c' :<= 3)), (3, ('c' :- 'a' :<= -7))]