module Z3.Lang.Monad (
Z3
, Z3State(..)
, evalZ3
, Args(..)
, stdArgs
, Logic(..)
, module Z3.Opts
, evalZ3With
, fresh
, deBruijnIx
, newQLayout
, getValue
, mkSort
, mkLiteral
, mkBoolBin
, mkBoolMulti
, mkQuant
, mkEq
, mkCmp
, mkCRingArith
, mkIntArith
, mkRealArith
, Base.Result
) where
import Z3.Lang.Exprs
import qualified Z3.Base as Base
import qualified Z3.Monad as MonadZ3
import Z3.Monad ( MonadZ3(..), Logic(..) )
import Z3.Opts
import Control.Applicative ( Applicative )
import Control.Monad.State
import qualified Data.Traversable as T
newtype Z3 a = Z3 (StateT Z3State IO a)
deriving (Functor, Applicative, Monad, MonadIO, MonadState Z3State)
instance MonadZ3 Z3 where
getSolver = Z3 $ gets solver
getContext = Z3 $ gets context
data Z3State
= Z3State { uniqVal :: !Uniq
, context :: Base.Context
, solver :: Maybe Base.Solver
, qLayout :: !Layout
}
evalZ3 :: Z3 a -> IO a
evalZ3 = evalZ3With stdArgs
evalZ3With :: Args -> Z3 a -> IO a
evalZ3With args (Z3 s) =
Base.withConfig $ \cfg -> do
setArgs cfg args
Base.withContext cfg $ \ctx ->
do mbSolver <- T.mapM (Base.mkSolverForLogic ctx) $ logic args
evalStateT s Z3State { uniqVal = 0
, context = ctx
, solver = mbSolver
, qLayout = 0
}
fresh :: Z3 Uniq
fresh = do
st <- get
let i = uniqVal st
put st { uniqVal = i + 1 }
return i
data Args
= Args {
logic :: Maybe Logic
, softTimeout :: Maybe Int
, options :: Opts
}
stdArgs :: Args
stdArgs
= Args {
logic = Nothing
, softTimeout = Nothing
, options = stdOpts +? opt "MODEL" True
+? opt "MODEL_COMPLETION" True
}
setArgs :: Base.Config -> Args -> IO ()
setArgs cfg args = do
Base.setParamValue cfg "SOFT_TIMEOUT" soft_timeout_val
setOpts cfg $ options args
where soft_timeout_val = show $ maybe 0 id $ softTimeout args
getQLayout :: Z3 Layout
getQLayout = gets qLayout
deBruijnIx :: Layout -> Z3 Int
deBruijnIx k = do lyt <- getQLayout; return $ lytk1
newQLayout :: (Expr a -> Z3 b) -> Z3 b
newQLayout f = do
lyt <- getQLayout
incQLayout
x <- f (Tag lyt)
decQLayout
return x
where incQLayout = modify (\st@Z3State{qLayout} -> st{ qLayout = qLayout+1 })
decQLayout = modify (\st@Z3State{qLayout} -> st{ qLayout = qLayout1 })
mkBoolBin :: BoolBinOp -> Base.AST -> Base.AST -> Z3 Base.AST
mkBoolBin Xor = MonadZ3.mkXor
mkBoolBin Implies = MonadZ3.mkImplies
mkBoolBin Iff = MonadZ3.mkIff
mkBoolMulti :: BoolMultiOp -> [Base.AST] -> Z3 Base.AST
mkBoolMulti And = MonadZ3.mkAnd
mkBoolMulti Or = MonadZ3.mkOr
mkQuant :: Quantifier
-> [Base.Pattern]
-> [Base.Symbol] -> [Base.Sort]
-> Base.AST -> Z3 Base.AST
mkQuant ForAll = MonadZ3.mkForall
mkQuant Exists = MonadZ3.mkExists
mkEq :: CmpOpE -> [Base.AST] -> Z3 Base.AST
mkEq Distinct = MonadZ3.mkDistinct
mkEq Eq = doMkEq
where doMkEq [e1,e2]
= MonadZ3.mkEq e1 e2
doMkEq es
| length es < 2 = error "Z3.Lang.Monad.mkEq:\
\ Invalid number of parameters."
| otherwise = join $ liftM (mkBoolMulti And) doEqs
where doEqs = mapM (uncurry $ MonadZ3.mkEq) pairs
pairs = init $ zip es $ tail $ cycle es
mkCmp :: CmpOpI -> Base.AST -> Base.AST -> Z3 Base.AST
mkCmp Le = MonadZ3.mkLe
mkCmp Lt = MonadZ3.mkLt
mkCmp Ge = MonadZ3.mkGe
mkCmp Gt = MonadZ3.mkGt
mkCRingArith :: CRingOp -> [Base.AST] -> Z3 Base.AST
mkCRingArith Add = MonadZ3.mkAdd
mkCRingArith Mul = MonadZ3.mkMul
mkCRingArith Sub = MonadZ3.mkSub
mkIntArith :: IntOp -> Base.AST -> Base.AST -> Z3 Base.AST
mkIntArith Quot = MonadZ3.mkDiv
mkIntArith Mod = MonadZ3.mkMod
mkIntArith Rem = MonadZ3.mkRem
mkRealArith :: RealOp -> Base.AST -> Base.AST -> Z3 Base.AST
mkRealArith Div = MonadZ3.mkDiv