ToySolver.SAT.Encoder.Integer

Documentation

newtype Expr

Constructors

Expr PBSum

Instances

Num Expr

Defined in ToySolver.SAT.Encoder.Integer

Methods

(+) :: Expr -> Expr -> Expr

(-) :: Expr -> Expr -> Expr

(*) :: Expr -> Expr -> Expr

negate :: Expr -> Expr

abs :: Expr -> Expr

signum :: Expr -> Expr

fromInteger :: Integer -> Expr

Read Expr

Defined in ToySolver.SAT.Encoder.Integer

Methods

readsPrec :: Int -> ReadS Expr

readList :: ReadS [Expr]

readPrec :: ReadPrec Expr

readListPrec :: ReadPrec [Expr]

Show Expr

Defined in ToySolver.SAT.Encoder.Integer

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

Eq Expr

Defined in ToySolver.SAT.Encoder.Integer

Methods

(==) :: Expr -> Expr -> Bool

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

AdditiveGroup Expr

Defined in ToySolver.SAT.Encoder.Integer

Methods

zeroV :: Expr

(^+^) :: Expr -> Expr -> Expr

negateV :: Expr -> Expr

(^-^) :: Expr -> Expr -> Expr

VectorSpace Expr

Defined in ToySolver.SAT.Encoder.Integer

Associated Types

type Scalar Expr

Methods

(*^) :: Scalar Expr -> Expr -> Expr

type Scalar Expr

Defined in ToySolver.SAT.Encoder.Integer

type Scalar Expr = Integer

newVar :: AddPBNL m enc => enc -> Integer -> Integer -> m Expr

linearize :: PrimMonad m => Encoder m -> Expr -> m (PBLinSum, Integer)

addConstraint :: AddPBNL m enc => enc -> OrdRel Expr -> m ()

addConstraintSoft :: AddPBNL m enc => enc -> Lit -> OrdRel Expr -> m ()

eval :: IModel m => m -> Expr -> Integer