{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
{-# language CPP #-}
{-# language GeneralizedNewtypeDeriving #-}
{-# language NoMonomorphismRestriction #-}
{-# language FlexibleContexts #-}
module Boolector (
Boolector
, MonadBoolector(..)
, evalBoolector
, runBoolector
, BoolectorState
, newBoolectorState
, createDefaultSorts
, 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
, boolConst
, signedBvConst
, unsignedBvConst
, Sort
, SortTy, sortTy
, boolSort
, bitvecSort
, funSort
, arraySort
, isEqualSort
, isArraySort
, isBoolSort
, isBitvecSort
, isFunSort
, funSortCheck
, dump
, dumpNode
, dumpToString
, dumpNodeToString
, DumpFormat(..)
) where
import Boolector.Foreign (Option(..), Status(..))
import qualified Boolector.Foreign as B
import qualified Control.Monad.Fail as Fail
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 Data.Time.Clock
import Data.Time.Clock.TAI
import Data.Time.Clock.System
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, Fail.MonadFail)
evalBoolector :: BoolectorState -> Boolector a -> IO a
evalBoolector bState act = evalStateT (unBoolector $ createDefaultSorts >> act) bState
runBoolector :: BoolectorState -> Boolector a -> IO (a, BoolectorState)
runBoolector bState act = runStateT (unBoolector $ createDefaultSorts >> act) bState
newBoolectorState :: Maybe Integer -> 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
btorState@(BoolectorState b _) <- newBoolectorState Nothing
t0 <- systemToTAITime `liftM` getSystemTime
B.setTerm b $ \_ -> do
t1 <- systemToTAITime `liftM` getSystemTime
let shouldTerminate = diffAbsoluteTime t1 t0 > secondsToDiffTime time
return $ if shouldTerminate then 1 else 0
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.ones $ _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 = do
void $ bitvecSort (fromIntegral $ u - l + 1)
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 = do
nw <- getWidth n
void $ bitvecSort (fromIntegral $ nw + w)
mkNode ["uext", show n, show w] $
liftBoolector2 B.uext (_node n) (fromIntegral w)
sext :: MonadBoolector m => Node -> Word32 -> m Node
sext n w = do
nw <- getWidth n
void $ bitvecSort (fromIntegral $ nw + w)
mkNode ["sext", show n, show w] $
liftBoolector2 B.sext (_node n) (fromIntegral w)
concat :: MonadBoolector m => Node -> Node -> m Node
concat n1 n2 = do
nw1 <- getWidth n1
nw2 <- getWidth n2
void $ bitvecSort (fromIntegral $ nw1 + nw2)
mkNode ["concat", show n1, show n2] $
liftBoolector2 B.concat (_node n1) (_node n2)
repeat :: MonadBoolector m => Node -> Word32 -> m Node
repeat n w = do
nw <- getWidth n
void $ bitvecSort (fromIntegral $ nw * 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
getBits :: MonadBoolector m => Node -> m String
getBits = liftBoolector1 B.getBits . _node
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
boolConst :: MonadBoolector m => Node -> m (Maybe Bool)
boolConst node = do
cnst <- isConst node
if cnst
then do str <- getBits node
Just `liftM` bitsToBool str
else return Nothing
unsignedBvConst :: MonadBoolector m => Node -> m (Maybe Integer)
unsignedBvConst node = do
cnst <- isConst node
if cnst
then do str <- getBits node
Just `liftM` bitsToUnsignedInteger str
else return Nothing
signedBvConst :: MonadBoolector m => Node -> m (Maybe Integer)
signedBvConst node = do
cnst <- isConst node
if cnst
then do str <- getBits node
val <- bitsToUnsignedInteger str
w <- getWidth node
let max_signed_w = 2 ^ pred w
return . Just $ if val >= max_signed_w
then val - (2*max_signed_w)
else val
else return Nothing
bitsToUnsignedInteger :: MonadBoolector m => String -> m Integer
bitsToUnsignedInteger str = do
when (Prelude.not $ all isDigit str) $ error $ "getModelVal: not numeric: " ++ str
liftIO $ evaluate $ foldl (\ n c -> 2 * n + Prelude.read [c]) 0 str
bitsToBool :: MonadBoolector m => String -> m Bool
bitsToBool str = liftIO $ evaluate $ case str of
"0" -> False
"1" -> True
_ -> error $ "bitsToBool: not boolean: " ++ str
bvAssignment :: MonadBoolector m => Node -> m String
bvAssignment = liftBoolector1 B.bvAssignment . _node
unsignedBvAssignment :: MonadBoolector m => Node -> m Integer
unsignedBvAssignment node = do
str <- bvAssignment node
bitsToUnsignedInteger 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
bitsToBool 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
createDefaultSorts :: Boolector ()
createDefaultSorts = do
void $ boolSort
void $ bitvecSort 1
void $ bitvecSort 2
void $ bitvecSort 4
void $ bitvecSort 8
void $ bitvecSort 16
void $ bitvecSort 32
void $ bitvecSort 64
void $ bitvecSort 128
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
ArraySort _ _ -> True
_ -> False
isBoolSort :: Sort -> Bool
isBoolSort srt = case sortTy srt of
BoolSort -> True
_ -> False
isBitvecSort :: Sort -> Bool
isBitvecSort srt = case sortTy srt of
BitVecSort _ -> 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