ToySolver.Arith.DifferenceLogic

Description

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

data SimpleAtom b = Diff :<= b
type Var = Int
data Diff = Var :- Var
solve :: (Hashable label, Eq label, Real b) => [(label, SimpleAtom b)] -> Either (HashSet label) (IntMap b)

Documentation

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

Constructors

Diff :<= b infix 4

Instances details

Show b => Show (SimpleAtom b) Source #
Instance details Defined in ToySolver.Arith.DifferenceLogic Methods showsPrec :: Int -> SimpleAtom b -> ShowS # show :: SimpleAtom b -> String # showList :: [SimpleAtom b] -> ShowS #
Eq b => Eq (SimpleAtom b) Source #
Instance details Defined in ToySolver.Arith.DifferenceLogic Methods (==) :: SimpleAtom b -> SimpleAtom b -> Bool # (/=) :: SimpleAtom b -> SimpleAtom b -> Bool #
Ord b => Ord (SimpleAtom b) Source #
Instance details 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 #

Difference of two variables

Constructors

Var :- Var infixl 6

Instances details

Show Diff Source #
Instance details Defined in ToySolver.Arith.DifferenceLogic Methods showsPrec :: Int -> Diff -> ShowS # show :: Diff -> String # showList :: [Diff] -> ShowS #
Eq Diff Source #
Instance details Defined in ToySolver.Arith.DifferenceLogic Methods (==) :: Diff -> Diff -> Bool # (/=) :: Diff -> Diff -> Bool #
Ord Diff Source #
Instance details 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) Source #

Takes labeled list of constraints, and returns eithera