{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
{-# language CPP #-}
{-# language GeneralizedNewtypeDeriving #-}
{-# language NoMonomorphismRestriction #-}
{-# language FlexibleContexts #-}
module Boolector (
Boolector
, MonadBoolector(..)
, evalBoolector
, runBoolector
, BoolectorState
, newBoolectorState
, Option(..)
, setOpt
, getOpt
, SatSolver(..)
, setSatSolver
, Node
, sat
, limitedSat
, simplify
, Status(..)
, assert
, assume
, failed
, fixateAssumptions
, resetAssumptions
, push
, pop
, var
, const
, constd
, consth
, bool
, true
, false
, zero
, one
, ones
, unsignedInt
, signedInt
, array
, fun
, uf
, param
, forall
, exists
, implies
, iff
, cond
, eq
, ne
, not
, neg
, redor
, redxor
, redand
, slice
, uext
, sext
, concat
, repeat
, xor
, xnor
, and
, nand
, or
, nor
, sll
, srl
, sra
, rol
, ror
, add
, inc
, sub
, dec
, mul
, udiv
, sdiv
, urem
, srem
, smod
, uaddo
, saddo
, usubo
, ssubo
, umulo
, smulo
, sdivo
, ult
, slt
, ulte
, slte
, ugt
, sgt
, ugte
, sgte
, read
, write
, apply
, getSort
, funGetDomainSort
, funGetCodomainSort
, funGetArity
, getSymbol
, setSymbol
, getWidth
, getIndexWidth
, isConst
, isVar
, isArray
, isArrayVar
, isParam
, isBoundParam
, isUf
, isFun
, bvAssignment
, unsignedBvAssignment
, signedBvAssignment
, boolAssignment
, Sort
, SortTy, sortTy
, boolSort
, bitvecSort
, funSort
, arraySort
, isEqualSort
, isArraySort
, isBitvecSort
, isFunSort
, funSortCheck
, dump
, dumpNode
, dumpToString
, dumpNodeToString
, DumpFormat(..)
) where
import Boolector.Foreign (Option(..), Status(..))
import qualified Boolector.Foreign as B
import Data.Char (isDigit)
import Data.Maybe (listToMaybe)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.Word
import Control.Applicative ((<$>))
import Control.Monad.State.Strict
import Control.Exception hiding (assert)
import Control.Concurrent
import Prelude hiding (read, not, and, or, const, concat, repeat)
import qualified Prelude as Prelude
class MonadIO m => MonadBoolector m where
getBoolectorState :: m BoolectorState
putBoolectorState :: BoolectorState -> m ()
instance MonadBoolector Boolector where
getBoolectorState = get
putBoolectorState = put
data BoolectorState = BoolectorState { unBoolectorState :: B.Btor
, unBoolectorCache :: BoolectorCache }
newtype Boolector a = Boolector { unBoolector :: StateT BoolectorState IO a }
deriving (Functor, Applicative, Monad, MonadState BoolectorState, MonadIO)
evalBoolector :: BoolectorState -> Boolector a -> IO a
evalBoolector bState act = evalStateT (unBoolector act) bState
runBoolector :: BoolectorState -> Boolector a -> IO (a, BoolectorState)
runBoolector bState act = runStateT (unBoolector act) bState
newBoolectorState :: Maybe Int -> IO BoolectorState
newBoolectorState Nothing = do
b <- B.new
B.setOpt b OPT_MODEL_GEN 2
B.setOpt b OPT_AUTO_CLEANUP 1
B.setOpt b OPT_INCREMENTAL 1
return $ BoolectorState b emptyBoolectorCache
newBoolectorState (Just time) = do
term <- newMVar 0
btorState@(BoolectorState b _) <- newBoolectorState Nothing
B.setTerm b $ \_ -> do
readMVar term
void $ forkIO $ do threadDelay $ time * 1000
putMVar term 1
return btorState
setOpt :: MonadBoolector m => Option -> Word32 -> m ()
setOpt o w = liftBoolector2 B.setOpt o (fromIntegral w)
getOpt :: MonadBoolector m => Option -> m Word32
getOpt o = fromIntegral `liftM` liftBoolector1 B.getOpt o
data SatSolver = Lingeling
| PicoSAT
| MiniSAT
deriving Show
setSatSolver :: MonadBoolector m => SatSolver -> m ()
setSatSolver solver = liftBoolector1 B.setSatSolver (show solver)
assert :: MonadBoolector m => Node -> m ()
assert = liftBoolector1 B.assert . _node
assume :: MonadBoolector m => Node -> m ()
assume = liftBoolector1 B.assume . _node
failed :: MonadBoolector m => Node -> m Bool
failed = liftBoolector1 B.failed . _node
fixateAssumptions :: MonadBoolector m => m ()
fixateAssumptions = liftBoolector0 B.fixateAssumptions
resetAssumptions :: MonadBoolector m => m ()
resetAssumptions = liftBoolector0 B.resetAssumptions
sat :: MonadBoolector m => m Status
sat = liftBoolector0 B.sat
push :: MonadBoolector m => Word32 -> m ()
push w = liftBoolector1 B.push (fromIntegral w)
pop :: MonadBoolector m => Word32 -> m ()
pop w = liftBoolector1 B.pop (fromIntegral w)
limitedSat :: MonadBoolector m
=> Int
-> Int
-> m Status
limitedSat = liftBoolector2 B.limitedSat
simplify :: MonadBoolector m => m Status
simplify = liftBoolector0 B.sat
data Node = Node { _node :: B.Node
, _showNode :: String } deriving (Eq, Ord)
instance Show Node where
show = _showNode
bool :: MonadBoolector m => Bool -> m Node
bool True = true
bool False = false
true :: MonadBoolector m => m Node
true = mkNode "true" $ liftBoolector0 B.true
false :: MonadBoolector m => m Node
false = mkNode "false" $ liftBoolector0 B.false
const :: MonadBoolector m => String -> m Node
const str = mkNode ("0b" ++ str) $ liftBoolector1 B.const str
constd :: MonadBoolector m => Sort -> String -> m Node
constd srt str = mkNode str $ liftBoolector2 B.constd (_sort srt) str
consth :: MonadBoolector m => Sort -> String -> m Node
consth srt str = mkNode ("0x" ++ str) $ liftBoolector2 B.consth (_sort srt) str
zero :: MonadBoolector m => Sort -> m Node
zero = mkNode "zero" . liftBoolector1 B.zero . _sort
ones :: MonadBoolector m => Sort -> m Node
ones srt = mkNode onesStr $ liftBoolector1 B.one $ _sort srt
where onesStr = "0b" ++ replicate nr '1'
nr = case sortTy srt of
BoolSort -> 1
BitVecSort wNr -> fromIntegral wNr
_ -> error "invalid sort"
one :: MonadBoolector m => Sort -> m Node
one = mkNode "1" . liftBoolector1 B.one . _sort
unsignedInt :: MonadBoolector m => Integer -> Sort -> m Node
unsignedInt i srt = constd srt (show i)
signedInt :: MonadBoolector m => Integer -> Sort -> m Node
signedInt i srt = constd srt (show i)
var :: MonadBoolector m => Sort -> String -> m Node
var srt str = mkNamedNode "var" B.var srt str
not :: MonadBoolector m => Node -> m Node
not n1 = mkNode ["not", show n1] $ liftBoolector1 B.not (_node n1)
neg :: MonadBoolector m => Node -> m Node
neg n1 = mkNode ["neg", show n1] $ liftBoolector1 B.neg (_node n1)
redor :: MonadBoolector m => Node -> m Node
redor n1 = mkNode ["redor", show n1] $ liftBoolector1 B.redor (_node n1)
redxor :: MonadBoolector m => Node -> m Node
redxor n1 = mkNode ["redxor", show n1] $ liftBoolector1 B.redxor (_node n1)
redand :: MonadBoolector m => Node -> m Node
redand n = mkNode ["redand", show n] $ liftBoolector1 B.redand (_node n)
slice :: MonadBoolector m
=> Node
-> Word32
-> Word32
-> m Node
slice n u l = mkNode ["slice", show n, show u, show l] $
liftBoolector3 B.slice (_node n) (fromIntegral u) (fromIntegral l)
uext :: MonadBoolector m => Node -> Word32 -> m Node
uext n w = mkNode ["uext", show n, show w] $
liftBoolector2 B.uext (_node n) (fromIntegral w)
sext :: MonadBoolector m => Node -> Word32 -> m Node
sext n w = mkNode ["sext", show n, show w] $
liftBoolector2 B.sext (_node n) (fromIntegral w)
concat :: MonadBoolector m => Node -> Node -> m Node
concat n1 n2 = mkNode ["concat", show n1, show n2] $
liftBoolector2 B.concat (_node n1) (_node n2)
repeat :: MonadBoolector m => Node -> Word32 -> m Node
repeat n w = mkNode ["repeat", show n, show w] $
liftBoolector2 B.repeat (_node n) (fromIntegral w)
implies :: MonadBoolector m => Node -> Node -> m Node
implies n1 n2 = mkNode ["implies", show n1, show n2] $
liftBoolector2 B.implies (_node n1) (_node n2)
iff :: MonadBoolector m => Node -> Node -> m Node
iff n1 n2 = mkNode ["iff", show n1, show n2] $
liftBoolector2 B.iff (_node n1) (_node n2)
eq :: MonadBoolector m => Node -> Node -> m Node
eq n1 n2 = mkNode ["eq", show n1, show n2] $
liftBoolector2 B.eq (_node n1) (_node n2)
ne :: MonadBoolector m => Node -> Node -> m Node
ne n1 n2 = mkNode ["ne", show n1, show n2] $
liftBoolector2 B.ne (_node n1) (_node n2)
cond :: MonadBoolector m
=> Node
-> Node
-> Node
-> m Node
cond n1 n2 n3 = mkNode ["cond", show n1, show n2, show n3] $
liftBoolector3 B.cond (_node n1) (_node n2) (_node n3)
xor :: MonadBoolector m => Node -> Node -> m Node
xor n1 n2 = mkNode ["xor", show n1, show n2] $ liftBoolector2 B.xor (_node n1) (_node n2)
xnor :: MonadBoolector m => Node -> Node -> m Node
xnor n1 n2 = mkNode ["xnor", show n1, show n2] $ liftBoolector2 B.xnor (_node n1) (_node n2)
and :: MonadBoolector m => Node -> Node -> m Node
and n1 n2 = mkNode ["and", show n1, show n2] $ liftBoolector2 B.and (_node n1) (_node n2)
nand :: MonadBoolector m => Node -> Node -> m Node
nand n1 n2 = mkNode ["nand", show n1, show n2] $ liftBoolector2 B.nand (_node n1) (_node n2)
or :: MonadBoolector m => Node -> Node -> m Node
or n1 n2 = mkNode ["or", show n1, show n2] $ liftBoolector2 B.or (_node n1) (_node n2)
nor :: MonadBoolector m => Node -> Node -> m Node
nor n1 n2 = mkNode ["nor", show n1, show n2] $ liftBoolector2 B.nor (_node n1) (_node n2)
sll :: MonadBoolector m
=> Node
-> Node
-> m Node
sll n1 n2 = mkNode ["sll", show n1, show n2] $ liftBoolector2 B.sll (_node n1) (_node n2)
srl :: MonadBoolector m
=> Node
-> Node
-> m Node
srl n1 n2 = mkNode ["srl", show n1, show n2] $ liftBoolector2 B.srl (_node n1) (_node n2)
sra :: MonadBoolector m
=> Node
-> Node
-> m Node
sra n1 n2 = mkNode ["sra", show n1, show n2] $ liftBoolector2 B.sra (_node n1) (_node n2)
rol :: MonadBoolector m
=> Node
-> Node
-> m Node
rol n1 n2 = mkNode ["rol", show n1, show n2] $ liftBoolector2 B.rol (_node n1) (_node n2)
ror :: MonadBoolector m
=> Node
-> Node
-> m Node
ror n1 n2 = mkNode ["ror", show n1, show n2] $ liftBoolector2 B.ror (_node n1) (_node n2)
add :: MonadBoolector m => Node -> Node -> m Node
add n1 n2 = mkNode ["add", show n1, show n2] $ liftBoolector2 B.add (_node n1) (_node n2)
inc :: Node -> Boolector Node
inc n = mkNode ["inc", show n] $ liftBoolector1 B.inc (_node n)
sub :: MonadBoolector m => Node -> Node -> m Node
sub n1 n2 = mkNode ["sub", show n1, show n2] $ liftBoolector2 B.sub (_node n1) (_node n2)
dec :: MonadBoolector m => Node -> m Node
dec n = mkNode ["dec", show n] $ liftBoolector1 B.dec (_node n)
mul :: MonadBoolector m => Node -> Node -> m Node
mul n1 n2 = mkNode ["mul", show n1, show n2] $ liftBoolector2 B.mul (_node n1) (_node n2)
udiv :: MonadBoolector m => Node -> Node -> m Node
udiv n1 n2 = mkNode ["udiv", show n1, show n2] $ liftBoolector2 B.udiv (_node n1) (_node n2)
sdiv :: MonadBoolector m => Node -> Node -> m Node
sdiv n1 n2 = mkNode ["sdiv", show n1, show n2] $ liftBoolector2 B.sdiv (_node n1) (_node n2)
urem :: MonadBoolector m => Node -> Node -> m Node
urem n1 n2 = mkNode ["urem", show n1, show n2] $ liftBoolector2 B.urem (_node n1) (_node n2)
srem :: MonadBoolector m => Node -> Node -> m Node
srem n1 n2 = mkNode ["srem", show n1, show n2] $ liftBoolector2 B.srem (_node n1) (_node n2)
smod :: MonadBoolector m => Node -> Node -> m Node
smod n1 n2 = mkNode ["smod", show n1, show n2] $ liftBoolector2 B.smod (_node n1) (_node n2)
usubo :: MonadBoolector m => Node -> Node -> m Node
usubo n1 n2 = mkNode ["usubo", show n1, show n2] $ liftBoolector2 B.usubo (_node n1) (_node n2)
ssubo :: MonadBoolector m => Node -> Node -> m Node
ssubo n1 n2 = mkNode ["ssubo", show n1, show n2] $ liftBoolector2 B.ssubo (_node n1) (_node n2)
uaddo :: MonadBoolector m => Node -> Node -> m Node
uaddo n1 n2 = mkNode ["uaddo", show n1, show n2] $ liftBoolector2 B.uaddo (_node n1) (_node n2)
saddo :: MonadBoolector m => Node -> Node -> m Node
saddo n1 n2 = mkNode ["saddo", show n1, show n2] $ liftBoolector2 B.saddo (_node n1) (_node n2)
umulo :: MonadBoolector m => Node -> Node -> m Node
umulo n1 n2 = mkNode ["umulo", show n1, show n2] $ liftBoolector2 B.umulo (_node n1) (_node n2)
smulo :: MonadBoolector m => Node -> Node -> m Node
smulo n1 n2 = mkNode ["smulo", show n1, show n2] $ liftBoolector2 B.smulo (_node n1) (_node n2)
sdivo :: MonadBoolector m => Node -> Node -> m Node
sdivo n1 n2 = mkNode ["sdivo", show n1, show n2] $ liftBoolector2 B.sdivo (_node n1) (_node n2)
ult :: MonadBoolector m => Node -> Node -> m Node
ult n1 n2 = mkNode ["ult", show n1, show n2] $ liftBoolector2 B.ult (_node n1) (_node n2)
slt :: MonadBoolector m => Node -> Node -> m Node
slt n1 n2 = mkNode ["slt", show n1, show n2] $ liftBoolector2 B.slt (_node n1) (_node n2)
ulte :: MonadBoolector m => Node -> Node -> m Node
ulte n1 n2 = mkNode ["ulte", show n1, show n2] $ liftBoolector2 B.ulte (_node n1) (_node n2)
slte :: MonadBoolector m => Node -> Node -> m Node
slte n1 n2 = mkNode ["slte", show n1, show n2] $ liftBoolector2 B.slte (_node n1) (_node n2)
ugt :: MonadBoolector m => Node -> Node -> m Node
ugt n1 n2 = mkNode ["ugt", show n1, show n2] $ liftBoolector2 B.ugt (_node n1) (_node n2)
sgt :: MonadBoolector m => Node -> Node -> m Node
sgt n1 n2 = mkNode ["sgt", show n1, show n2] $ liftBoolector2 B.sgt (_node n1) (_node n2)
ugte :: MonadBoolector m => Node -> Node -> m Node
ugte n1 n2 = mkNode ["ugte", show n1, show n2] $ liftBoolector2 B.ugte (_node n1) (_node n2)
sgte :: MonadBoolector m => Node -> Node -> m Node
sgte n1 n2 = mkNode ["sgte", show n1, show n2] $ liftBoolector2 B.sgte (_node n1) (_node n2)
array :: MonadBoolector m => Sort -> String -> m Node
array srt str = mkNamedNode "array" B.array srt str
read :: MonadBoolector m
=> Node
-> Node
-> m Node
read n1 n2 = mkNode ["read", show n1, show n2] $ liftBoolector2 B.read (_node n1) (_node n2)
write :: MonadBoolector m
=> Node
-> Node
-> Node
-> m Node
write n1 n2 n3 = mkNode ["write", show n1, show n2, show n3] $ liftBoolector3 B.write (_node n1) (_node n2) (_node n3)
uf :: MonadBoolector m => Sort -> String -> m Node
uf srt str = mkNamedNode "uf" B.uf srt str
param :: MonadBoolector m => Sort -> String -> m Node
param srt str = mkNode ["param", show srt, str] $ liftBoolector2 B.param (_sort srt) str
fun :: MonadBoolector m
=> [Node]
-> Node
-> m Node
fun n1 n2 = mkNode ["fun", show n1, show n2] $ liftBoolector2 B.fun (map _node n1) (_node n2)
apply :: MonadBoolector m
=> [Node]
-> Node
-> m Node
apply n1 n2 = mkNode ["apply", show n1, show n2] $ liftBoolector2 B.apply (map _node n1) (_node n2)
forall :: MonadBoolector m
=> [Node]
-> Node
-> m Node
forall n1 n2 = mkNode ["forall", show n1, show n2] $ liftBoolector2 B.forall (map _node n1) (_node n2)
exists :: MonadBoolector m
=> [Node]
-> Node
-> m Node
exists n1 n2 = mkNode ["exists", show n1, show n2] $ liftBoolector2 B.exists (map _node n1) (_node n2)
getSort :: MonadBoolector m => Node -> m Sort
getSort n = liftBoolector1 B.getSort (_node n) >>= lookupSort
funGetDomainSort :: MonadBoolector m => Node -> m Sort
funGetDomainSort n = liftBoolector1 B.funGetDomainSort (_node n) >>= lookupSort
funGetCodomainSort :: MonadBoolector m => Node -> m Sort
funGetCodomainSort n = liftBoolector1 B.funGetCodomainSort (_node n) >>= lookupSort
funGetArity :: MonadBoolector m => Node -> m Word
funGetArity n = fromIntegral `liftM` liftBoolector1 B.getFunArity (_node n)
getSymbol :: MonadBoolector m => Node -> m (Maybe String)
getSymbol = liftBoolector1 B.getSymbol . _node
setSymbol :: MonadBoolector m => Node -> String -> m ()
setSymbol n str = liftBoolector2 B.setSymbol (_node n) str
getWidth :: MonadBoolector m => Node -> m Word32
getWidth n = fromIntegral `liftM` liftBoolector1 B.getWidth (_node n)
getIndexWidth :: MonadBoolector m => Node -> m Word32
getIndexWidth n = fromIntegral `liftM` liftBoolector1 B.getIndexWidth (_node n)
isConst :: MonadBoolector m => Node -> m Bool
isConst = liftBoolector1 B.isConst . _node
isVar :: MonadBoolector m => Node -> m Bool
isVar = liftBoolector1 B.isVar . _node
isArray :: MonadBoolector m => Node -> m Bool
isArray = liftBoolector1 B.isArray . _node
isArrayVar :: MonadBoolector m => Node -> m Bool
isArrayVar = liftBoolector1 B.isArrayVar . _node
isParam :: MonadBoolector m => Node -> m Bool
isParam = liftBoolector1 B.isParam . _node
isBoundParam :: MonadBoolector m => Node -> m Bool
isBoundParam = liftBoolector1 B.isBoundParam . _node
isUf :: MonadBoolector m => Node -> m Bool
isUf = liftBoolector1 B.isUf . _node
isFun :: MonadBoolector m => Node -> m Bool
isFun = liftBoolector1 B.isFun . _node
bvAssignment :: MonadBoolector m => Node -> m String
bvAssignment = liftBoolector1 B.bvAssignment . _node
unsignedBvAssignment :: MonadBoolector m => Node -> m Integer
unsignedBvAssignment node = do
str <- bvAssignment node
when (Prelude.not $ all isDigit str) $ error $ "getModelVal: not numeric: " ++ str
liftIO $ evaluate $ foldl (\ n c -> 2 * n + Prelude.read [c]) 0 str
signedBvAssignment :: MonadBoolector m => Node -> m Integer
signedBvAssignment node = do
val <- unsignedBvAssignment node
w <- getWidth node
let max_signed_w = 2 ^ pred w
return $ if val >= max_signed_w
then val - (2*max_signed_w)
else val
boolAssignment :: MonadBoolector m => Node -> m Bool
boolAssignment node = do
str <- bvAssignment node
liftIO $ evaluate $ case str of
"0" -> False
"1" -> True
_ -> error $ "boolAssignment: not boolean: " ++ str
data SortTy = BoolSort
| BitVecSort Word
| FunSort [SortTy] SortTy
| ArraySort SortTy SortTy
deriving (Eq, Ord, Show)
data Sort = Sort { sortTy :: SortTy
, _sort :: B.Sort
} deriving (Eq, Ord)
instance Show Sort where
show = show . sortTy
boolSort :: Boolector Sort
boolSort = do
sc <- getSortCache
case scBool sc of
Just srt -> return srt
_ -> do srt <- Sort BoolSort <$> liftBoolector0 B.boolSort
setSortCache $ sc { scBool = Just srt }
return srt
bitvecSort :: MonadBoolector m => Word -> m Sort
bitvecSort wnr = do
sc <- getSortCache
let bvMap = scBitVec sc
case IntMap.lookup nr bvMap of
Just srt -> return srt
_ -> do srt <- Sort (BitVecSort nr) <$> liftBoolector1 B.bitvecSort nr
setSortCache $ sc { scBitVec = IntMap.insert nr srt bvMap }
return srt
where nr = fromIntegral wnr
funSort :: MonadBoolector m => [Sort] -> Sort -> m Sort
funSort args ret = do
sc <- getSortCache
let funMap = scFun sc
case Map.lookup (ret, args) funMap of
Just srt -> return srt
_ -> do srt <- Sort (FunSort (map sortTy args) (sortTy ret))
<$> liftBoolector2 B.funSort (map _sort args) (_sort ret)
setSortCache $ sc { scFun = Map.insert (ret, args) srt funMap }
return srt
arraySort :: MonadBoolector m => Sort -> Sort -> m Sort
arraySort dom rng = do
sc <- getSortCache
let arrMap = scArray sc
case Map.lookup (dom, rng) arrMap of
Just srt -> return srt
_ -> do srt <- Sort (ArraySort (sortTy dom) (sortTy rng))
<$> liftBoolector2 B.arraySort (_sort dom) (_sort rng)
setSortCache $ sc { scArray = Map.insert (dom, rng) srt arrMap }
return srt
isEqualSort :: MonadBoolector m => Node -> Node -> m Bool
isEqualSort n1 n2 = liftBoolector2 B.isEqualSort (_node n1) (_node n2)
isArraySort :: Sort -> Bool
isArraySort srt = case sortTy srt of
BitVecSort _ -> True
_ -> False
isBitvecSort :: Sort -> Bool
isBitvecSort srt = case sortTy srt of
ArraySort _ _ -> True
_ -> False
isFunSort :: Sort -> Bool
isFunSort srt = case sortTy srt of
FunSort _ _ -> True
_ -> False
funSortCheck :: MonadBoolector m => [Node] -> Node -> m (Maybe Int)
funSortCheck n1 n2 = liftBoolector2 B.funSortCheck (map _node n1) (_node n2)
data DumpFormat = DumpBtor | DumpSMT2
deriving (Eq, Show)
dumpNode :: MonadBoolector m => DumpFormat -> FilePath -> Node -> m ()
dumpNode fmt path node = do
btor <- unBoolectorState `liftM` getBoolectorState
liftIO $ B.withDumpFile path $ \file -> dumper btor file (_node node)
where dumper = case fmt of
DumpBtor -> B.dumpBtorNode
_ -> B.dumpSmt2Node
dump :: MonadBoolector m => DumpFormat -> FilePath -> m ()
dump fmt path = do
btor <- unBoolectorState `liftM` getBoolectorState
liftIO $ B.withDumpFile path (dumper btor)
where dumper = case fmt of
DumpBtor -> B.dumpBtor
_ -> B.dumpSmt2
dumpNodeToString :: MonadBoolector m => DumpFormat -> Node -> m String
dumpNodeToString fmt node = do
btor <- unBoolectorState `liftM` getBoolectorState
liftIO $ B.withTempDumpFile (\file -> dumper btor file (_node node))
where dumper = case fmt of
DumpBtor -> B.dumpBtorNode
_ -> B.dumpSmt2Node
dumpToString :: MonadBoolector m => DumpFormat -> m String
dumpToString fmt = do
btor <- unBoolectorState `liftM` getBoolectorState
liftIO $ B.withTempDumpFile (dumper btor)
where dumper = case fmt of
DumpBtor -> B.dumpBtor
_ -> B.dumpSmt2
liftBoolector0 :: MonadBoolector m => (B.Btor -> IO a) -> m a
liftBoolector0 f = do
s <- getBoolectorState
liftIO $ f (unBoolectorState s)
liftBoolector1 :: MonadBoolector m => (B.Btor -> a -> IO b) -> a -> m b
liftBoolector1 f x1 = do
s <- getBoolectorState
liftIO $ f (unBoolectorState s) x1
liftBoolector2 :: MonadBoolector m => (B.Btor -> a -> b -> IO c) -> a -> b -> m c
liftBoolector2 f x1 x2 = do
s <- getBoolectorState
liftIO $ f (unBoolectorState s) x1 x2
liftBoolector3 :: MonadBoolector m => (B.Btor -> a -> b -> c -> IO d) -> a -> b -> c -> m d
liftBoolector3 f x1 x2 x3 = do
s <- getBoolectorState
liftIO $ f (unBoolectorState s) x1 x2 x3
data BoolectorCache = BoolectorCache {
sortCache :: SortCache
, varCache :: VarCache
}
emptyBoolectorCache :: BoolectorCache
emptyBoolectorCache = BoolectorCache emptySortCache Map.empty
data SortCache = SortCache {
scBool :: Maybe Sort
, scBitVec :: IntMap Sort
, scFun :: Map (Sort, [Sort]) Sort
, scArray :: Map (Sort, Sort) Sort
}
emptySortCache :: SortCache
emptySortCache = SortCache Nothing IntMap.empty Map.empty Map.empty
getSortCache :: MonadBoolector m => m SortCache
getSortCache = (sortCache . unBoolectorCache) `liftM` getBoolectorState
setSortCache :: MonadBoolector m => SortCache -> m ()
setSortCache sc = do
s0 <- getBoolectorState
putBoolectorState $ s0 { unBoolectorCache = (unBoolectorCache s0) { sortCache = sc } }
type VarCache = Map (String, Sort) Node
getVarCache :: MonadBoolector m => m VarCache
getVarCache = (varCache . unBoolectorCache) `liftM` getBoolectorState
setVarCache :: MonadBoolector m => VarCache -> m ()
setVarCache vc = do
s0 <- getBoolectorState
putBoolectorState $ s0 { unBoolectorCache = (unBoolectorCache s0) { varCache = vc } }
class Show s => MkNode s where
mkNode :: MonadBoolector m => s -> m B.Node -> m Node
instance MkNode String where
mkNode str act = do
node <- act
return $ Node node str
instance MkNode [String] where
mkNode str act = do
node <- act
return $ Node node $ "(" ++ unwords str ++ ")"
mkNamedNode :: MonadBoolector m
=> String
-> (B.Btor -> B.Sort -> String -> IO B.Node)
-> Sort
-> String
-> m Node
mkNamedNode kind ctor sort name = do
vc <- getVarCache
case Map.lookup (name, sort) vc of
Just srt -> return srt
_ -> do node <- mkNode [kind, name, "::", show sort] $
liftBoolector2 ctor (_sort sort) name
setVarCache $ Map.insert (name, sort) node vc
return node
lookupSort :: MonadBoolector m => B.Sort -> m Sort
lookupSort bSort = do
sc <- getSortCache
case () of
_ | Just srt <- lookupBoolSort sc -> return srt
_ | Just srt <- lookupBitVecSort sc -> return srt
_ | Just srt <- lookupFunSort sc -> return srt
_ | Just srt <- lookupArraySort sc -> return srt
_ -> fail "BUG: should really have the sort in the cache"
where lookupBoolSort sc = case scBool sc of
Just srt | _sort srt == bSort -> Just srt
_ -> Nothing
lookupBitVecSort sc = listToMaybe $ IntMap.elems $
IntMap.filter (\s -> _sort s == bSort) $ scBitVec sc
lookupFunSort sc = listToMaybe $ Map.elems $
Map.filter (\s -> _sort s == bSort) $ scFun sc
lookupArraySort sc = listToMaybe $ Map.elems $
Map.filter (\s -> _sort s == bSort) $ scArray sc