toysolver-0.5.0: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
ToySolver.SAT.Encoder.Integer
newtype Expr Source #
Constructors
Instances
Methods
(+) :: Expr -> Expr -> Expr #
(-) :: Expr -> Expr -> Expr #
(*) :: Expr -> Expr -> Expr #
negate :: Expr -> Expr #
abs :: Expr -> Expr #
signum :: Expr -> Expr #
fromInteger :: Integer -> Expr #
Associated Types
type Scalar Expr :: * #
(*^) :: Scalar Expr -> Expr -> Expr #
zeroV :: Expr #
(^+^) :: Expr -> Expr -> Expr #
negateV :: Expr -> Expr #
(^-^) :: Expr -> Expr -> Expr #
newVar :: AddPBNL m enc => enc -> Integer -> Integer -> m Expr Source #
linearize :: PrimMonad m => Encoder m -> Expr -> m (PBLinSum, Integer) Source #
addConstraint :: AddPBNL m enc => enc -> OrdRel Expr -> m () Source #
addConstraintSoft :: AddPBNL m enc => enc -> Lit -> OrdRel Expr -> m () Source #
eval :: IModel m => m -> Expr -> Integer Source #