Copyright	(c) Masahiro Sakai 2012
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	None
Language	Haskell2010
Extensions	MonoLocalBinds TypeFamilies KindSignatures ExplicitNamespaces

ToySolver.SAT.Encoder.Integer

Description

Synopsis

newtype Expr = Expr PBSum
newVar :: AddPBNL m enc => enc -> Integer -> Integer -> m Expr
newVarPBLinSum :: AddPBNL m enc => enc -> Integer -> m PBLinSum
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

Documentation

newtype Expr Source #

Constructors

Expr PBSum

Instances

Instances details

Num Expr Source #

Instance details

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 Source #

Instance details

Defined in ToySolver.SAT.Encoder.Integer

Methods

readsPrec :: Int -> ReadS Expr #

readList :: ReadS [Expr] #

readPrec :: ReadPrec Expr #

readListPrec :: ReadPrec [Expr] #

Show Expr Source #

Instance details

Defined in ToySolver.SAT.Encoder.Integer

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

Eq Expr Source #

Instance details

Defined in ToySolver.SAT.Encoder.Integer

Methods

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

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

AdditiveGroup Expr Source #

Instance details

Defined in ToySolver.SAT.Encoder.Integer

Methods

zeroV :: Expr #

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

negateV :: Expr -> Expr #

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

VectorSpace Expr Source #

Instance details

Defined in ToySolver.SAT.Encoder.Integer

Associated Types

type Scalar Expr
Instance details Defined in ToySolver.SAT.Encoder.Integer type Scalar Expr = Integer

Methods

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

type Scalar Expr Source #

Instance details

Defined in ToySolver.SAT.Encoder.Integer

type Scalar Expr = Integer

newVar Source #

Arguments

:: AddPBNL m enc
=> enc
-> Integer	lower bound
-> Integer	upper bound
-> m Expr

newVarPBLinSum Source #

Arguments

:: AddPBNL m enc
=> enc
-> Integer	upper bound
-> m PBLinSum

Lower-level version of newVar

It takes only upper bound. Lower bound is always 0.
Return type is PBLinSum. It is inconvenient for performing operations, but it is sometimes useful to be guaranteed to be in a linear form.

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 #