toysolver-0.9.0: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Copyright(c) Masahiro Sakai 2016
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010
Extensions
  • ScopedTypeVariables
  • FlexibleContexts
  • ExplicitForAll

ToySolver.BitVector.Solver

Description

 
Synopsis

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 #