ToySolver.Arith.DifferenceLogic

• 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 b

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

Constructors

Diff :<= b infix 4

Instances

Show b => Show (SimpleAtom b)

Defined in ToySolver.Arith.DifferenceLogic

Methods

showsPrec :: Int -> SimpleAtom b -> ShowS

show :: SimpleAtom b -> String

showList :: [SimpleAtom b] -> ShowS

Eq b => Eq (SimpleAtom b)

Defined in ToySolver.Arith.DifferenceLogic

Methods

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

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

Ord b => Ord (SimpleAtom b)

Defined in ToySolver.Arith.DifferenceLogic

Methods

compare :: SimpleAtom b -> SimpleAtom b -> Ordering

(<) :: SimpleAtom b -> SimpleAtom b -> Bool

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

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

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

max :: SimpleAtom b -> SimpleAtom b -> SimpleAtom b

min :: SimpleAtom b -> SimpleAtom b -> SimpleAtom b

type Var = Int

data Diff

Difference of two variables

Constructors

Var :- Var infixl 6

Instances

Show Diff

Defined in ToySolver.Arith.DifferenceLogic

Methods

showsPrec :: Int -> Diff -> ShowS

show :: Diff -> String

showList :: [Diff] -> ShowS

Eq Diff

Defined in ToySolver.Arith.DifferenceLogic

Methods

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

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

Ord Diff

Defined in ToySolver.Arith.DifferenceLogic

Methods

compare :: Diff -> Diff -> Ordering

(<) :: Diff -> Diff -> Bool

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

(>) :: Diff -> Diff -> Bool

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

max :: Diff -> Diff -> Diff

min :: Diff -> Diff -> Diff

solve :: (Hashable label, Eq label, Real b) => [(label, SimpleAtom b)] -> Either (HashSet label) (IntMap b)

Takes labeled list of constraints, and returns eithera

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