ToySolver.Arith.DifferenceLogic

Description

Reference:

Albert Oliveras and Enric Rodriguez-Carbonell. “General overview of a T-Solver for Difference Logic”. https://www.cs.upc.edu/~oliveras/TDV/dl.pdf

Synopsis

Documentation

a :- b :<= k represents a - b ≤ k

Constructors

(Diff v) :<= b infix 4

Instances

(Eq b, Eq v) => Eq (SimpleAtom v b) Source #
Methods (==) :: SimpleAtom v b -> SimpleAtom v b -> Bool # (/=) :: SimpleAtom v b -> SimpleAtom v b -> Bool #
(Ord b, Ord v) => Ord (SimpleAtom v b) Source #
Methods compare :: SimpleAtom v b -> SimpleAtom v b -> Ordering # (<) :: SimpleAtom v b -> SimpleAtom v b -> Bool # (<=) :: SimpleAtom v b -> SimpleAtom v b -> Bool # (>) :: SimpleAtom v b -> SimpleAtom v b -> Bool # (>=) :: SimpleAtom v b -> SimpleAtom v b -> Bool # max :: SimpleAtom v b -> SimpleAtom v b -> SimpleAtom v b # min :: SimpleAtom v b -> SimpleAtom v b -> SimpleAtom v b #
(Show b, Show v) => Show (SimpleAtom v b) Source #
Methods showsPrec :: Int -> SimpleAtom v b -> ShowS # show :: SimpleAtom v b -> String # showList :: [SimpleAtom v b] -> ShowS #

Difference of two variables

Constructors

v :- v infixl 6

Instances

Eq v => Eq (Diff v) Source #
Methods (==) :: Diff v -> Diff v -> Bool # (/=) :: Diff v -> Diff v -> Bool #
Ord v => Ord (Diff v) Source #
Methods compare :: Diff v -> Diff v -> Ordering # (<) :: Diff v -> Diff v -> Bool # (<=) :: Diff v -> Diff v -> Bool # (>) :: Diff v -> Diff v -> Bool # (>=) :: Diff v -> Diff v -> Bool # max :: Diff v -> Diff v -> Diff v # min :: Diff v -> Diff v -> Diff v #
Show v => Show (Diff v) Source #
Methods showsPrec :: Int -> Diff v -> ShowS # show :: Diff v -> String # showList :: [Diff v] -> ShowS #

solve :: (Hashable label, Eq label, Hashable v, Eq v, Real b) => [(label, SimpleAtom v b)] -> Either (HashSet label) (HashMap v b) Source #

Takes labeled list of constraints, and returns either