toysolver-0.6.0: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc

Safe Haskell	None
Language	Haskell2010

ToySolver.SAT.PBO.Context

Documentation

class Context a where Source #

Minimal complete definition

getObjectiveFunction, isUnsat, getBestSolution, getLowerBound, setUnsat, addSolution, addLowerBound, logMessage

Methods

getObjectiveFunction :: a -> PBLinSum Source #

evalObjectiveFunction :: a -> Model -> Integer Source #

isUnsat :: a -> STM Bool Source #

getBestSolution :: a -> STM (Maybe (Model, Integer)) Source #

getLowerBound :: a -> STM Integer Source #

setUnsat :: a -> IO () Source #

addSolution :: a -> Model -> IO () Source #

addLowerBound :: a -> Integer -> IO () Source #

logMessage :: a -> String -> IO () Source #

Instances

Context SimpleContext Source #
Instance details Defined in ToySolver.SAT.PBO.Context Methods getObjectiveFunction :: SimpleContext -> PBLinSum Source # evalObjectiveFunction :: SimpleContext -> Model -> Integer Source # isUnsat :: SimpleContext -> STM Bool Source # getBestSolution :: SimpleContext -> STM (Maybe (Model, Integer)) Source # getLowerBound :: SimpleContext -> STM Integer Source # setUnsat :: SimpleContext -> IO () Source # addSolution :: SimpleContext -> Model -> IO () Source # addLowerBound :: SimpleContext -> Integer -> IO () Source # logMessage :: SimpleContext -> String -> IO () Source #
Context a => Context (Normalized a) Source #
Instance details Defined in ToySolver.SAT.PBO.Context Methods getObjectiveFunction :: Normalized a -> PBLinSum Source # evalObjectiveFunction :: Normalized a -> Model -> Integer Source # isUnsat :: Normalized a -> STM Bool Source # getBestSolution :: Normalized a -> STM (Maybe (Model, Integer)) Source # getLowerBound :: Normalized a -> STM Integer Source # setUnsat :: Normalized a -> IO () Source # addSolution :: Normalized a -> Model -> IO () Source # addLowerBound :: Normalized a -> Integer -> IO () Source # logMessage :: Normalized a -> String -> IO () Source #

getBestValue :: Context a => a -> STM (Maybe Integer) Source #

getBestModel :: Context a => a -> STM (Maybe Model) Source #

isOptimum :: Context a => a -> STM Bool Source #

isFinished :: Context a => a -> STM Bool Source #

getSearchUpperBound :: Context a => a -> STM Integer Source #

setFinished :: Context a => a -> IO () Source #

data SimpleContext Source #

Instances

Context SimpleContext Source #

Instance details

Defined in ToySolver.SAT.PBO.Context

Methods

getObjectiveFunction :: SimpleContext -> PBLinSum Source #

evalObjectiveFunction :: SimpleContext -> Model -> Integer Source #

isUnsat :: SimpleContext -> STM Bool Source #

getBestSolution :: SimpleContext -> STM (Maybe (Model, Integer)) Source #

getLowerBound :: SimpleContext -> STM Integer Source #

setUnsat :: SimpleContext -> IO () Source #

addSolution :: SimpleContext -> Model -> IO () Source #

addLowerBound :: SimpleContext -> Integer -> IO () Source #

logMessage :: SimpleContext -> String -> IO () Source #

newSimpleContext :: PBLinSum -> IO SimpleContext Source #

newSimpleContext2 :: PBLinSum -> (Model -> Integer) -> IO SimpleContext Source #

setOnUpdateBestSolution :: SimpleContext -> (Model -> Integer -> IO ()) -> IO () Source #

setOnUpdateLowerBound :: SimpleContext -> (Integer -> IO ()) -> IO () Source #

setLogger :: SimpleContext -> (String -> IO ()) -> IO () Source #

data Normalized a Source #

Instances

Context a => Context (Normalized a) Source #

Instance details

Defined in ToySolver.SAT.PBO.Context

Methods

getObjectiveFunction :: Normalized a -> PBLinSum Source #

evalObjectiveFunction :: Normalized a -> Model -> Integer Source #

isUnsat :: Normalized a -> STM Bool Source #

getBestSolution :: Normalized a -> STM (Maybe (Model, Integer)) Source #

getLowerBound :: Normalized a -> STM Integer Source #

setUnsat :: Normalized a -> IO () Source #

addSolution :: Normalized a -> Model -> IO () Source #

addLowerBound :: Normalized a -> Integer -> IO () Source #

logMessage :: Normalized a -> String -> IO () Source #

normalize :: Context a => a -> Normalized a Source #