ToySolver.Arith.DifferenceLogic

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

Documentation

data SimpleAtom v b

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

Constructors

(Diff v) :<= b infix 4

Instances

(Eq b, Eq v) => Eq (SimpleAtom v b)

Methods

(==) :: SimpleAtom v b -> SimpleAtom v b -> Bool

(/=) :: SimpleAtom v b -> SimpleAtom v b -> Bool

(Ord b, Ord v) => Ord (SimpleAtom v b)

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)

Methods

showsPrec :: Int -> SimpleAtom v b -> ShowS

show :: SimpleAtom v b -> String

showList :: [SimpleAtom v b] -> ShowS

data Diff v

Difference of two variables

Constructors

v :- v infixl 6

Instances

Eq v => Eq (Diff v)

Methods

(==) :: Diff v -> Diff v -> Bool

(/=) :: Diff v -> Diff v -> Bool

Ord v => Ord (Diff v)

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)

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)

Takes labeled list of constraints, and returns either

• unsatisfiable set of constraints as a set of labels, or
• satisfying assignment.