{-# 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
, xor
, xnor
, and
, nand
, or
, nor
, sll
, srl
, sra
, rol
, ror
, add
, uaddo
, saddo
, inc
, sub
, usubo
, ssubo
, dec
, mul
, umulo
, smulo
, udiv
, sdiv
, sdivo
, urem
, srem
, smod
, ult
, slt
, ulte
, slte
, ugt
, sgt
, ugte
, sgte
, read
, write
, apply
, getSort
, funGetDomainSort
, funGetCodomainSort
, funGetArity
, getSymbol
, getWidth
, getIndexWidth
, isConst
, isVar
, isArray
, isArrayVar
, isParam
, isBoundParam
, isUf
, isFun
, bvAssignment
, unsignedBvAssignment
, signedBvAssignment
, boolAssignment
, Sort
, boolSort
, bitvecSort
, funSort
, arraySort
, isEqualSort
, isArraySort
, isBitvecSort
, isFunSort
, funSortCheck
, dumpBtorNode
, dumpSmt2Node
, dumpBtor
, dumpSmt2
) where
import Boolector.Foreign (Option(..), Status(..), Node, Sort)
import qualified Boolector.Foreign as B
import Data.Char (isDigit)
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.Monad.State.Strict
import Control.Exception hiding (assert)
import Control.Concurrent
import Prelude hiding (read, not, and, or, const, concat)
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 -> Word -> m ()
setOpt o w = liftBoolector2 B.setOpt o (fromIntegral w)
getOpt :: MonadBoolector m => Option -> m Word
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
assume :: MonadBoolector m => Node -> m ()
assume = liftBoolector1 B.assume
failed :: MonadBoolector m => Node -> m Bool
failed = liftBoolector1 B.failed
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 => Word -> m ()
push w = liftBoolector1 B.push (fromIntegral w)
pop :: MonadBoolector m => Word -> 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
bool :: MonadBoolector m => Bool -> m Node
bool True = true
bool False = false
true :: MonadBoolector m => m Node
true = liftBoolector0 B.true
false :: MonadBoolector m => m Node
false = liftBoolector0 B.false
const :: MonadBoolector m => String -> m Node
const = liftBoolector1 B.const
constd :: MonadBoolector m => Sort -> String -> m Node
constd = liftBoolector2 B.constd
consth :: MonadBoolector m => Sort -> String -> m Node
consth = liftBoolector2 B.consth
zero :: MonadBoolector m => Sort -> m Node
zero = liftBoolector1 B.zero
ones :: MonadBoolector m => Sort -> m Node
ones = liftBoolector1 B.ones
one :: MonadBoolector m => Sort -> m Node
one = liftBoolector1 B.one
unsignedInt :: MonadBoolector m => Integer -> Sort -> m Node
unsignedInt i sort = liftBoolector2 B.unsignedInt (fromIntegral i) sort
signedInt :: MonadBoolector m => Integer -> Sort -> m Node
signedInt i sort = liftBoolector2 B.int (fromIntegral i) sort
var :: MonadBoolector m => Sort -> String -> m Node
var = createNamedNode B.var
not :: MonadBoolector m => Node -> m Node
not = liftBoolector1 B.not
neg :: MonadBoolector m => Node -> m Node
neg = liftBoolector1 B.neg
redor :: MonadBoolector m => Node -> m Node
redor = liftBoolector1 B.redor
redxor :: MonadBoolector m => Node -> m Node
redxor = liftBoolector1 B.redxor
redand :: MonadBoolector m => Node -> m Node
redand = liftBoolector1 B.redand
slice :: MonadBoolector m
=> Node
-> Word
-> Word
-> m Node
slice n u l = (liftBoolector3 B.slice) n (fromIntegral u) (fromIntegral l)
uext :: MonadBoolector m => Node -> Word -> m Node
uext n w = (liftBoolector2 B.uext) n $ fromIntegral w
sext :: MonadBoolector m => Node -> Word -> m Node
sext n w = liftBoolector2 B.sext n (fromIntegral w)
concat :: MonadBoolector m => Node -> Node -> m Node
concat = liftBoolector2 B.concat
implies :: MonadBoolector m => Node -> Node -> m Node
implies = liftBoolector2 B.implies
iff :: MonadBoolector m => Node -> Node -> m Node
iff = liftBoolector2 B.iff
eq :: MonadBoolector m => Node -> Node -> m Node
eq = liftBoolector2 B.eq
ne :: MonadBoolector m => Node -> Node -> m Node
ne = liftBoolector2 B.ne
cond :: MonadBoolector m
=> Node
-> Node
-> Node
-> m Node
cond = liftBoolector3 B.cond
xor :: MonadBoolector m => Node -> Node -> m Node
xor = liftBoolector2 B.xor
xnor :: MonadBoolector m => Node -> Node -> m Node
xnor = liftBoolector2 B.xnor
and :: MonadBoolector m => Node -> Node -> m Node
and = liftBoolector2 B.and
nand :: MonadBoolector m => Node -> Node -> m Node
nand = liftBoolector2 B.nand
or :: MonadBoolector m => Node -> Node -> m Node
or = liftBoolector2 B.or
nor :: MonadBoolector m => Node -> Node -> m Node
nor = liftBoolector2 B.nor
sll :: MonadBoolector m
=> Node
-> Node
-> m Node
sll = liftBoolector2 B.sll
srl :: MonadBoolector m
=> Node
-> Node
-> m Node
srl = liftBoolector2 B.srl
sra :: MonadBoolector m
=> Node
-> Node
-> m Node
sra = liftBoolector2 B.sra
rol :: MonadBoolector m
=> Node
-> Node
-> m Node
rol = liftBoolector2 B.rol
ror :: MonadBoolector m
=> Node
-> Node
-> m Node
ror = liftBoolector2 B.ror
add :: MonadBoolector m => Node -> Node -> m Node
add = liftBoolector2 B.add
uaddo :: MonadBoolector m => Node -> Node -> m Node
uaddo = liftBoolector2 B.uaddo
saddo :: MonadBoolector m => Node -> Node -> m Node
saddo = liftBoolector2 B.saddo
inc :: Node -> Boolector Node
inc = liftBoolector1 B.inc
sub :: MonadBoolector m => Node -> Node -> m Node
sub = liftBoolector2 B.sub
usubo :: MonadBoolector m => Node -> Node -> m Node
usubo = liftBoolector2 B.usubo
ssubo :: MonadBoolector m => Node -> Node -> m Node
ssubo = liftBoolector2 B.ssubo
dec :: MonadBoolector m => Node -> m Node
dec = liftBoolector1 B.dec
mul :: MonadBoolector m => Node -> Node -> m Node
mul = liftBoolector2 B.mul
umulo :: MonadBoolector m => Node -> Node -> m Node
umulo = liftBoolector2 B.umulo
smulo :: MonadBoolector m => Node -> Node -> m Node
smulo = liftBoolector2 B.smulo
udiv :: MonadBoolector m => Node -> Node -> m Node
udiv = liftBoolector2 B.udiv
sdiv :: MonadBoolector m => Node -> Node -> m Node
sdiv = liftBoolector2 B.sdiv
sdivo :: MonadBoolector m => Node -> Node -> m Node
sdivo = liftBoolector2 B.sdivo
urem :: MonadBoolector m => Node -> Node -> m Node
urem = liftBoolector2 B.urem
srem :: MonadBoolector m => Node -> Node -> m Node
srem = liftBoolector2 B.srem
smod :: MonadBoolector m => Node -> Node -> m Node
smod = liftBoolector2 B.smod
ult :: MonadBoolector m => Node -> Node -> m Node
ult = liftBoolector2 B.ult
slt :: MonadBoolector m => Node -> Node -> m Node
slt = liftBoolector2 B.slt
ulte :: MonadBoolector m => Node -> Node -> m Node
ulte = liftBoolector2 B.ulte
slte :: MonadBoolector m => Node -> Node -> m Node
slte = liftBoolector2 B.slte
ugt :: MonadBoolector m => Node -> Node -> m Node
ugt = liftBoolector2 B.ugt
sgt :: MonadBoolector m => Node -> Node -> m Node
sgt = liftBoolector2 B.sgt
ugte :: MonadBoolector m => Node -> Node -> m Node
ugte = liftBoolector2 B.ugte
sgte :: MonadBoolector m => Node -> Node -> m Node
sgte = liftBoolector2 B.sgte
array :: MonadBoolector m => Sort -> String -> m Node
array = createNamedNode B.array
read :: MonadBoolector m
=> Node
-> Node
-> m Node
read = liftBoolector2 B.read
write :: MonadBoolector m
=> Node
-> Node
-> Node
-> m Node
write = liftBoolector3 B.write
uf :: MonadBoolector m => Sort -> String -> m Node
uf = createNamedNode B.uf
param :: MonadBoolector m => Sort -> String -> m Node
param = liftBoolector2 B.param
fun :: MonadBoolector m
=> [Node]
-> Node
-> m Node
fun = liftBoolector2 B.fun
apply :: MonadBoolector m
=> [Node]
-> Node
-> m Node
apply = liftBoolector2 B.apply
forall :: MonadBoolector m
=> [Node]
-> Node
-> m Node
forall = liftBoolector2 B.forall
exists :: MonadBoolector m
=> [Node]
-> Node
-> m Node
exists = liftBoolector2 B.exists
getSort :: MonadBoolector m => Node -> m Sort
getSort = liftBoolector1 B.getSort
funGetDomainSort :: MonadBoolector m => Node -> m Sort
funGetDomainSort = liftBoolector1 B.funGetDomainSort
funGetCodomainSort :: MonadBoolector m => Node -> m Sort
funGetCodomainSort = liftBoolector1 B.funGetCodomainSort
funGetArity :: MonadBoolector m => Node -> m Word
funGetArity n = fromIntegral `liftM` liftBoolector1 B.getFunArity n
getSymbol :: MonadBoolector m => Node -> m String
getSymbol = liftBoolector1 B.getSymbol
getWidth :: MonadBoolector m => Node -> m Word
getWidth n = fromIntegral `liftM` liftBoolector1 B.getWidth n
getIndexWidth :: MonadBoolector m => Node -> m Word
getIndexWidth n = fromIntegral `liftM` liftBoolector1 B.getIndexWidth n
isConst :: MonadBoolector m => Node -> m Bool
isConst = liftBoolector1 B.isConst
isVar :: MonadBoolector m => Node -> m Bool
isVar = liftBoolector1 B.isVar
isArray :: MonadBoolector m => Node -> m Bool
isArray = liftBoolector1 B.isArray
isArrayVar :: MonadBoolector m => Node -> m Bool
isArrayVar = liftBoolector1 B.isArrayVar
isParam :: MonadBoolector m => Node -> m Bool
isParam = liftBoolector1 B.isParam
isBoundParam :: MonadBoolector m => Node -> m Bool
isBoundParam = liftBoolector1 B.isBoundParam
isUf :: MonadBoolector m => Node -> m Bool
isUf = liftBoolector1 B.isUf
isFun :: MonadBoolector m => Node -> m Bool
isFun = liftBoolector1 B.isFun
bvAssignment :: MonadBoolector m => Node -> m String
bvAssignment = liftBoolector1 B.bvAssignment
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
boolSort :: Boolector Sort
boolSort = do
sc <- getSortCache
case scBool sc of
Just srt -> return srt
_ -> do srt <- 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 <- 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 <- liftBoolector2 B.funSort args 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 <- liftBoolector2 B.arraySort dom rng
setSortCache $ sc { scArray = Map.insert (dom, rng) srt arrMap }
return srt
isEqualSort :: MonadBoolector m => Node -> Node -> m Bool
isEqualSort = liftBoolector2 B.isEqualSort
isArraySort :: MonadBoolector m => Sort -> m Bool
isArraySort = liftBoolector1 B.isArraySort
isBitvecSort :: MonadBoolector m => Sort -> m Bool
isBitvecSort = liftBoolector1 B.isBitvecSort
isFunSort :: MonadBoolector m => Sort -> m Bool
isFunSort = liftBoolector1 B.isFunSort
funSortCheck :: MonadBoolector m => [Node] -> Node -> m (Maybe Int)
funSortCheck = liftBoolector2 B.funSortCheck
dumpBtorNode :: MonadBoolector m => FilePath -> Node -> m ()
dumpBtorNode path node = do
file <- liftIO $ B.fopen path "w"
liftBoolector2 B.dumpBtorNode file node
dumpSmt2Node :: MonadBoolector m => FilePath -> Node -> m ()
dumpSmt2Node path node = do
file <- liftIO $ B.fopen path "w"
liftBoolector2 B.dumpSmt2Node file node
dumpBtor :: MonadBoolector m => FilePath -> m ()
dumpBtor path = do
file <- liftIO $ B.fopen path "w"
liftBoolector1 B.dumpBtor file
dumpSmt2 :: MonadBoolector m => FilePath -> m ()
dumpSmt2 path = do
file <- liftIO $ B.fopen path "w"
liftBoolector1 B.dumpSmt2 file
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 } }
createNamedNode :: MonadBoolector m
=> (B.Btor -> Sort -> String -> IO Node)
-> Sort -> String -> m Node
createNamedNode ctor sort name = do
vc <- getVarCache
case Map.lookup (name, sort) vc of
Just srt -> return srt
_ -> do node <- liftBoolector2 ctor sort name
setVarCache $ Map.insert (name, sort) node vc
return node