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

Copyright	(c) Masahiro Sakai 2016
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

ToySolver.BitVector.Solver

Contents

BitVector solver

Description

Synopsis

data Solver
newSolver :: IO Solver
newVar :: Solver -> Int -> IO Expr
newVar' :: Solver -> Int -> IO Var
assertAtom :: Solver -> Atom -> Maybe Int -> IO ()
check :: Solver -> IO Bool
getModel :: Solver -> IO Model
explain :: Solver -> IO IntSet
pushBacktrackPoint :: Solver -> IO ()
popBacktrackPoint :: Solver -> IO ()

BitVector solver

data Solver Source #

newSolver :: IO Solver Source #

newVar :: Solver -> Int -> IO Expr Source #

newVar' :: Solver -> Int -> IO Var Source #

assertAtom :: Solver -> Atom -> Maybe Int -> IO () Source #

check :: Solver -> IO Bool Source #

getModel :: Solver -> IO Model Source #

explain :: Solver -> IO IntSet Source #

pushBacktrackPoint :: Solver -> IO () Source #

popBacktrackPoint :: Solver -> IO () Source #