module Z3.Monad
(
MonadZ3(..)
, Z3
, module Z3.Opts
, Logic(..)
, evalZ3
, evalZ3With
, Z3Env
, newEnv
, evalZ3WithEnv
, Symbol
, AST
, Sort
, FuncDecl
, App
, Pattern
, Constructor
, Model
, Base.Context
, FuncInterp
, FuncEntry
, Params
, Solver
, SortKind(..)
, ASTKind(..)
, Result(..)
, mkParams
, paramsSetBool
, paramsSetUInt
, paramsSetDouble
, paramsSetSymbol
, paramsToString
, mkIntSymbol
, mkStringSymbol
, mkUninterpretedSort
, mkBoolSort
, mkIntSort
, mkRealSort
, mkBvSort
, mkFiniteDomainSort
, mkArraySort
, mkTupleSort
, mkConstructor
, mkDatatype
, mkDatatypes
, mkSetSort
, mkFuncDecl
, mkApp
, mkConst
, mkFreshConst
, mkFreshFuncDecl
, mkVar
, mkBoolVar
, mkRealVar
, mkIntVar
, mkBvVar
, mkFreshVar
, mkFreshBoolVar
, mkFreshRealVar
, mkFreshIntVar
, mkFreshBvVar
, mkTrue
, mkFalse
, mkEq
, mkNot
, mkIte
, mkIff
, mkImplies
, mkXor
, mkAnd
, mkOr
, mkDistinct
, mkDistinct1
, mkBool
, mkAdd
, mkMul
, mkSub
, mkSub1
, mkUnaryMinus
, mkDiv
, mkMod
, mkRem
, mkLt
, mkLe
, mkGt
, mkGe
, mkInt2Real
, mkReal2Int
, mkIsInt
, mkBvnot
, mkBvredand
, mkBvredor
, mkBvand
, mkBvor
, mkBvxor
, mkBvnand
, mkBvnor
, mkBvxnor
, mkBvneg
, mkBvadd
, mkBvsub
, mkBvmul
, mkBvudiv
, mkBvsdiv
, mkBvurem
, mkBvsrem
, mkBvsmod
, mkBvult
, mkBvslt
, mkBvule
, mkBvsle
, mkBvuge
, mkBvsge
, mkBvugt
, mkBvsgt
, mkConcat
, mkExtract
, mkSignExt
, mkZeroExt
, mkRepeat
, mkBvshl
, mkBvlshr
, mkBvashr
, mkRotateLeft
, mkRotateRight
, mkExtRotateLeft
, mkExtRotateRight
, mkInt2bv
, mkBv2int
, mkBvnegNoOverflow
, mkBvaddNoOverflow
, mkBvaddNoUnderflow
, mkBvsubNoOverflow
, mkBvsubNoUnderflow
, mkBvmulNoOverflow
, mkBvmulNoUnderflow
, mkBvsdivNoOverflow
, mkSelect
, mkStore
, mkConstArray
, mkMap
, mkArrayDefault
, mkEmptySet
, mkFullSet
, mkSetAdd
, mkSetDel
, mkSetUnion
, mkSetIntersect
, mkSetDifference
, mkSetComplement
, mkSetMember
, mkSetSubset
, mkNumeral
, mkInt
, mkReal
, mkUnsignedInt
, mkInt64
, mkUnsignedInt64
, mkIntegral
, mkRational
, mkFixed
, mkRealNum
, mkInteger
, mkIntNum
, mkBitvector
, mkBvNum
, mkSeqSort
, isSeqSort
, mkReSort
, isReSort
, mkStringSort
, isStringSort
, mkString
, isString
, getString
, mkSeqEmpty
, mkSeqUnit
, mkSeqConcat
, mkSeqPrefix
, mkSeqSuffix
, mkSeqContains
, mkSeqExtract
, mkSeqReplace
, mkSeqAt
, mkSeqLength
, mkSeqIndex
, mkStrToInt
, mkIntToStr
, mkSeqToRe
, mkSeqInRe
, mkRePlus
, mkReStar
, mkReOption
, mkReUnion
, mkReConcat
, mkReRange
, mkReLoop
, mkReIntersect
, mkReComplement
, mkReEmpty
, mkReFull
, mkPattern
, mkBound
, mkForall
, mkExists
, mkForallConst
, mkExistsConst
, getSymbolString
, getSortKind
, getBvSortSize
, getDatatypeSortConstructors
, getDatatypeSortRecognizers
, getDatatypeSortConstructorAccessors
, getDeclName
, getArity
, getDomain
, getRange
, appToAst
, getAppDecl
, getAppNumArgs
, getAppArg
, getAppArgs
, getSort
, getArraySortDomain
, getArraySortRange
, getBoolValue
, getAstKind
, isApp
, toApp
, getNumeralString
, simplify
, simplifyEx
, getIndexValue
, isQuantifierForall
, isQuantifierExists
, getQuantifierWeight
, getQuantifierNumPatterns
, getQuantifierPatternAST
, getQuantifierPatterns
, getQuantifierNumNoPatterns
, getQuantifierNoPatternAST
, getQuantifierNoPatterns
, getQuantifierNumBound
, getQuantifierBoundName
, getQuantifierBoundSort
, getQuantifierBoundVars
, getQuantifierBody
, getBool
, getInt
, getReal
, getBv
, substituteVars
, substitute
, modelEval
, evalArray
, getConstInterp
, getFuncInterp
, hasInterp
, numConsts
, numFuncs
, getConstDecl
, getFuncDecl
, getConsts
, getFuncs
, isAsArray
, isEqAST
, addFuncInterp
, addConstInterp
, getAsArrayFuncDecl
, funcInterpGetNumEntries
, funcInterpGetEntry
, funcInterpGetElse
, funcInterpGetArity
, funcEntryGetValue
, funcEntryGetNumArgs
, funcEntryGetArg
, modelToString
, showModel
, EvalAst
, eval
, evalBool
, evalInt
, evalReal
, evalBv
, evalT
, mapEval
, FuncModel(..)
, evalFunc
, mkTactic
, andThenTactic
, orElseTactic
, skipTactic
, tryForTactic
, mkQuantifierEliminationTactic
, mkAndInverterGraphTactic
, applyTactic
, getApplyResultNumSubgoals
, getApplyResultSubgoal
, getApplyResultSubgoals
, mkGoal
, goalAssert
, getGoalSize
, getGoalFormula
, getGoalFormulas
, ASTPrintMode(..)
, setASTPrintMode
, astToString
, patternToString
, sortToString
, funcDeclToString
, benchmarkToSMTLibString
, parseSMTLib2String
, parseSMTLib2File
, Base.Z3Error(..)
, Base.Z3ErrorCode(..)
, Version(..)
, getVersion
, MonadFixedpoint(..)
, Fixedpoint
, fixedpointAddRule
, fixedpointSetParams
, fixedpointRegisterRelation
, fixedpointQueryRelations
, fixedpointGetAnswer
, fixedpointGetAssertions
, MonadOptimize(..)
, Optimize
, optimizeAssert
, optimizeAssertAndTrack
, optimizeAssertSoft
, optimizeMaximize
, optimizeMinimize
, optimizePush
, optimizePop
, optimizeCheck
, optimizeGetReasonUnknown
, optimizeGetModel
, optimizeGetUnsatCore
, optimizeSetParams
, optimizeGetLower
, optimizeGetUpper
, optimizeGetUpperAsVector
, optimizeGetLowerAsVector
, optimizeToString
, optimizeFromString
, optimizeFromFile
, optimizeGetHelp
, optimizeGetAssertions
, optimizeGetObjectives
, solverGetHelp
, solverSetParams
, solverPush
, solverPop
, solverReset
, solverGetNumScopes
, solverAssertCnstr
, solverAssertAndTrack
, solverCheck
, solverCheckAssumptions
, solverGetModel
, solverGetProof
, solverGetUnsatCore
, solverGetReasonUnknown
, solverToString
, assert
, check
, checkAssumptions
, solverCheckAndGetModel
, getModel
, withModel
, getUnsatCore
, push
, pop
, local
, reset
, getNumScopes
)
where
import Z3.Opts
import Z3.Base
( Symbol
, AST
, Sort
, FuncDecl
, App
, Pattern
, Constructor
, Model
, FuncInterp
, FuncEntry
, FuncModel(..)
, Result(..)
, Logic(..)
, ASTPrintMode(..)
, Version(..)
, Params
, Solver
, Fixedpoint
, Optimize
, SortKind(..)
, ASTKind(..)
, Tactic
, ApplyResult
, Goal
)
import qualified Z3.Base as Base
import Control.Applicative ( Applicative )
import Data.Fixed ( Fixed, HasResolution )
import Control.Monad.Fail
import Control.Monad.IO.Class ( MonadIO, liftIO )
import Control.Monad.Trans.Reader ( ReaderT(..), runReaderT, asks )
import Control.Monad.Fix ( MonadFix )
import Data.Int ( Int64 )
import Data.List.NonEmpty (NonEmpty)
import Data.Word ( Word, Word64 )
import Data.Traversable ( Traversable )
import qualified Data.Traversable as T
class (Applicative m, Monad m, MonadIO m) => MonadZ3 m where
getSolver :: m Base.Solver
getContext :: m Base.Context
instance MonadZ3 m => MonadZ3 (ReaderT r m) where
getSolver = ReaderT $ const getSolver
getContext = ReaderT $ const getContext
liftScalar :: MonadZ3 z3 => (Base.Context -> IO b) -> z3 b
liftScalar f = liftIO . f =<< getContext
liftFun1 :: MonadZ3 z3 => (Base.Context -> a -> IO b) -> a -> z3 b
liftFun1 f a = getContext >>= \ctx -> liftIO (f ctx a)
liftFun2 :: MonadZ3 z3 => (Base.Context -> a -> b -> IO c) -> a -> b -> z3 c
liftFun2 f a b = getContext >>= \ctx -> liftIO (f ctx a b)
liftFun3 :: MonadZ3 z3 => (Base.Context -> a -> b -> c -> IO d)
-> a -> b -> c -> z3 d
liftFun3 f a b c = getContext >>= \ctx -> liftIO (f ctx a b c)
liftFun4 :: MonadZ3 z3 => (Base.Context -> a -> b -> c -> d -> IO e)
-> a -> b -> c -> d -> z3 e
liftFun4 f a b c d = getContext >>= \ctx -> liftIO (f ctx a b c d)
liftFun5 :: MonadZ3 z3 =>
(Base.Context -> a1 -> a2 -> a3 -> a4 -> a5 -> IO b)
-> a1 -> a2 -> a3 -> a4 -> a5-> z3 b
liftFun5 f x1 x2 x3 x4 x5 =
getContext >>= \ctx -> liftIO (f ctx x1 x2 x3 x4 x5)
liftFun6 :: MonadZ3 z3 =>
(Base.Context -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> IO b)
-> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> z3 b
liftFun6 f x1 x2 x3 x4 x5 x6 =
getContext >>= \ctx -> liftIO (f ctx x1 x2 x3 x4 x5 x6)
liftSolver0 :: MonadZ3 z3 =>
(Base.Context -> Base.Solver -> IO b)
-> z3 b
liftSolver0 f_s =
do ctx <- getContext
liftIO . f_s ctx =<< getSolver
liftSolver1 :: MonadZ3 z3 =>
(Base.Context -> Base.Solver -> a -> IO b)
-> a -> z3 b
liftSolver1 f_s a =
do ctx <- getContext
liftIO . (\s -> f_s ctx s a) =<< getSolver
liftSolver2 :: MonadZ3 z3 => (Base.Context -> Base.Solver -> a -> b -> IO c)
-> a -> b -> z3 c
liftSolver2 f a b = do
ctx <- getContext
slv <- getSolver
liftIO $ f ctx slv a b
liftFixedpoint0 :: MonadFixedpoint z3 =>
(Base.Context -> Base.Fixedpoint -> IO b)
-> z3 b
liftFixedpoint0 f_s =
do ctx <- getContext
liftIO . f_s ctx =<< getFixedpoint
liftFixedpoint1 :: MonadFixedpoint z3 =>
(Base.Context -> Base.Fixedpoint -> a -> IO b)
-> a -> z3 b
liftFixedpoint1 f_s a =
do ctx <- getContext
liftIO . (\s -> f_s ctx s a) =<< getFixedpoint
liftFixedpoint2 :: MonadFixedpoint z3 => (Base.Context -> Base.Fixedpoint -> a -> b -> IO c)
-> a -> b -> z3 c
liftFixedpoint2 f a b = do
ctx <- getContext
slv <- getFixedpoint
liftIO $ f ctx slv a b
liftOptimize0 :: MonadOptimize z3 =>
(Base.Context -> Base.Optimize -> IO b)
-> z3 b
liftOptimize0 f_s =
do ctx <- getContext
liftIO . f_s ctx =<< getOptimize
liftOptimize1 :: MonadOptimize z3 =>
(Base.Context -> Base.Optimize -> a -> IO b)
-> a -> z3 b
liftOptimize1 f_s a =
do ctx <- getContext
liftIO . (\s -> f_s ctx s a) =<< getOptimize
liftOptimize2 :: MonadOptimize z3 => (Base.Context -> Base.Optimize -> a -> b -> IO c)
-> a -> b -> z3 c
liftOptimize2 f a b = do
ctx <- getContext
slv <- getOptimize
liftIO $ f ctx slv a b
newtype Z3 a = Z3 { _unZ3 :: ReaderT Z3Env IO a }
deriving (Functor, Applicative, Monad, MonadIO, MonadFix, MonadFail)
data Z3Env
= Z3Env {
envSolver :: Base.Solver
, envContext :: Base.Context
, envFixedpoint :: Base.Fixedpoint
, envOptimize :: Base.Optimize
}
instance MonadZ3 Z3 where
getSolver = Z3 $ asks envSolver
getContext = Z3 $ asks envContext
instance MonadFixedpoint Z3 where
getFixedpoint = Z3 $ asks envFixedpoint
instance MonadOptimize Z3 where
getOptimize = Z3 $ asks envOptimize
evalZ3With :: Maybe Logic -> Opts -> Z3 a -> IO a
evalZ3With mbLogic opts (Z3 s) = do
env <- newEnv mbLogic opts
runReaderT s env
evalZ3 :: Z3 a -> IO a
evalZ3 = evalZ3With Nothing stdOpts
newEnvWith :: (Base.Config -> IO Base.Context) -> Maybe Logic -> Opts -> IO Z3Env
newEnvWith mkContext mbLogic opts =
Base.withConfig $ \cfg -> do
setOpts cfg opts
ctx <- mkContext cfg
solver <- maybe (Base.mkSolver ctx) (Base.mkSolverForLogic ctx) mbLogic
fixedpoint <- Base.mkFixedpoint ctx
optimize <- Base.mkOptimize ctx
return $ Z3Env solver ctx fixedpoint optimize
newEnv :: Maybe Logic -> Opts -> IO Z3Env
newEnv = newEnvWith Base.mkContext
evalZ3WithEnv :: Z3 a
-> Z3Env
-> IO a
evalZ3WithEnv (Z3 s) = runReaderT s
mkParams :: MonadZ3 z3 => z3 Params
mkParams = liftScalar Base.mkParams
paramsSetBool :: MonadZ3 z3 => Params -> Symbol -> Bool -> z3 ()
paramsSetBool = liftFun3 Base.paramsSetBool
paramsSetUInt :: MonadZ3 z3 => Params -> Symbol -> Word -> z3 ()
paramsSetUInt = liftFun3 Base.paramsSetUInt
paramsSetDouble :: MonadZ3 z3 => Params -> Symbol -> Double -> z3 ()
paramsSetDouble = liftFun3 Base.paramsSetDouble
paramsSetSymbol :: MonadZ3 z3 => Params -> Symbol -> Symbol -> z3 ()
paramsSetSymbol = liftFun3 Base.paramsSetSymbol
paramsToString :: MonadZ3 z3 => Params -> z3 String
paramsToString = liftFun1 Base.paramsToString
mkIntSymbol :: (MonadZ3 z3, Integral i) => i -> z3 Symbol
mkIntSymbol = liftFun1 Base.mkIntSymbol
mkStringSymbol :: MonadZ3 z3 => String -> z3 Symbol
mkStringSymbol = liftFun1 Base.mkStringSymbol
mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort
mkUninterpretedSort = liftFun1 Base.mkUninterpretedSort
mkBoolSort :: MonadZ3 z3 => z3 Sort
mkBoolSort = liftScalar Base.mkBoolSort
mkIntSort :: MonadZ3 z3 => z3 Sort
mkIntSort = liftScalar Base.mkIntSort
mkRealSort :: MonadZ3 z3 => z3 Sort
mkRealSort = liftScalar Base.mkRealSort
mkBvSort :: MonadZ3 z3 => Int -> z3 Sort
mkBvSort = liftFun1 Base.mkBvSort
mkFiniteDomainSort :: MonadZ3 z3 => Symbol -> Word64 -> z3 Sort
mkFiniteDomainSort = liftFun2 Base.mkFiniteDomainSort
mkArraySort :: MonadZ3 z3 => Sort -> Sort -> z3 Sort
mkArraySort = liftFun2 Base.mkArraySort
mkTupleSort :: MonadZ3 z3
=> Symbol
-> [(Symbol, Sort)]
-> z3 (Sort, FuncDecl, [FuncDecl])
mkTupleSort = liftFun2 Base.mkTupleSort
mkConstructor :: MonadZ3 z3
=> Symbol
-> Symbol
-> [(Symbol, Maybe Sort, Int)]
-> z3 Constructor
mkConstructor = liftFun3 Base.mkConstructor
mkDatatype :: MonadZ3 z3
=> Symbol
-> [Constructor]
-> z3 Sort
mkDatatype = liftFun2 Base.mkDatatype
mkDatatypes :: MonadZ3 z3
=> [Symbol]
-> [[Constructor]]
-> z3 [Sort]
mkDatatypes = liftFun2 Base.mkDatatypes
mkSetSort :: MonadZ3 z3 => Sort -> z3 Sort
mkSetSort = liftFun1 Base.mkSetSort
mkFuncDecl :: MonadZ3 z3 => Symbol -> [Sort] -> Sort -> z3 FuncDecl
mkFuncDecl = liftFun3 Base.mkFuncDecl
mkApp :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST
mkApp = liftFun2 Base.mkApp
mkConst :: MonadZ3 z3 => Symbol -> Sort -> z3 AST
mkConst = liftFun2 Base.mkConst
mkFreshConst :: MonadZ3 z3 => String -> Sort -> z3 AST
mkFreshConst = liftFun2 Base.mkFreshConst
mkFreshFuncDecl :: MonadZ3 z3 => String -> [Sort] -> Sort -> z3 FuncDecl
mkFreshFuncDecl = liftFun3 Base.mkFreshFuncDecl
mkVar :: MonadZ3 z3 => Symbol -> Sort -> z3 AST
mkVar = liftFun2 Base.mkVar
mkBoolVar :: MonadZ3 z3 => Symbol -> z3 AST
mkBoolVar = liftFun1 Base.mkBoolVar
mkRealVar :: MonadZ3 z3 => Symbol -> z3 AST
mkRealVar = liftFun1 Base.mkRealVar
mkIntVar :: MonadZ3 z3 => Symbol -> z3 AST
mkIntVar = liftFun1 Base.mkIntVar
mkBvVar :: MonadZ3 z3 => Symbol
-> Int
-> z3 AST
mkBvVar = liftFun2 Base.mkBvVar
mkFreshVar :: MonadZ3 z3 => String -> Sort -> z3 AST
mkFreshVar = liftFun2 Base.mkFreshConst
mkFreshBoolVar :: MonadZ3 z3 => String -> z3 AST
mkFreshBoolVar = liftFun1 Base.mkFreshBoolVar
mkFreshRealVar :: MonadZ3 z3 => String -> z3 AST
mkFreshRealVar = liftFun1 Base.mkFreshRealVar
mkFreshIntVar :: MonadZ3 z3 => String -> z3 AST
mkFreshIntVar = liftFun1 Base.mkFreshIntVar
mkFreshBvVar :: MonadZ3 z3 => String
-> Int
-> z3 AST
mkFreshBvVar = liftFun2 Base.mkFreshBvVar
mkTrue :: MonadZ3 z3 => z3 AST
mkTrue = liftScalar Base.mkTrue
mkFalse :: MonadZ3 z3 => z3 AST
mkFalse = liftScalar Base.mkFalse
mkEq :: MonadZ3 z3 => AST -> AST -> z3 AST
mkEq = liftFun2 Base.mkEq
mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST
mkDistinct = liftFun1 Base.mkDistinct
mkDistinct1 :: MonadZ3 z3 => NonEmpty AST -> z3 AST
mkDistinct1 = liftFun1 Base.mkDistinct1
mkNot :: MonadZ3 z3 => AST -> z3 AST
mkNot = liftFun1 Base.mkNot
mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
mkIte = liftFun3 Base.mkIte
mkIff :: MonadZ3 z3 => AST -> AST -> z3 AST
mkIff = liftFun2 Base.mkIff
mkImplies :: MonadZ3 z3 => AST -> AST -> z3 AST
mkImplies = liftFun2 Base.mkImplies
mkXor :: MonadZ3 z3 => AST -> AST -> z3 AST
mkXor = liftFun2 Base.mkXor
mkAnd :: MonadZ3 z3 => [AST] -> z3 AST
mkAnd = liftFun1 Base.mkAnd
mkOr :: MonadZ3 z3 => [AST] -> z3 AST
mkOr = liftFun1 Base.mkOr
mkBool :: MonadZ3 z3 => Bool -> z3 AST
mkBool = liftFun1 Base.mkBool
mkAdd :: MonadZ3 z3 => [AST] -> z3 AST
mkAdd = liftFun1 Base.mkAdd
mkMul :: MonadZ3 z3 => [AST] -> z3 AST
mkMul = liftFun1 Base.mkMul
mkSub :: MonadZ3 z3 => [AST] -> z3 AST
mkSub = liftFun1 Base.mkSub
mkSub1 :: MonadZ3 z3 => NonEmpty AST -> z3 AST
mkSub1 = liftFun1 Base.mkSub1
mkUnaryMinus :: MonadZ3 z3 => AST -> z3 AST
mkUnaryMinus = liftFun1 Base.mkUnaryMinus
mkDiv :: MonadZ3 z3 => AST -> AST -> z3 AST
mkDiv = liftFun2 Base.mkDiv
mkMod :: MonadZ3 z3 => AST -> AST -> z3 AST
mkMod = liftFun2 Base.mkMod
mkRem :: MonadZ3 z3 => AST -> AST -> z3 AST
mkRem = liftFun2 Base.mkRem
mkLt :: MonadZ3 z3 => AST -> AST -> z3 AST
mkLt = liftFun2 Base.mkLt
mkLe :: MonadZ3 z3 => AST -> AST -> z3 AST
mkLe = liftFun2 Base.mkLe
mkGt :: MonadZ3 z3 => AST -> AST -> z3 AST
mkGt = liftFun2 Base.mkGt
mkGe :: MonadZ3 z3 => AST -> AST -> z3 AST
mkGe = liftFun2 Base.mkGe
mkInt2Real :: MonadZ3 z3 => AST -> z3 AST
mkInt2Real = liftFun1 Base.mkInt2Real
mkReal2Int :: MonadZ3 z3 => AST -> z3 AST
mkReal2Int = liftFun1 Base.mkReal2Int
mkIsInt :: MonadZ3 z3 => AST -> z3 AST
mkIsInt = liftFun1 Base.mkIsInt
mkBvnot :: MonadZ3 z3 => AST -> z3 AST
mkBvnot = liftFun1 Base.mkBvnot
mkBvredand :: MonadZ3 z3 => AST -> z3 AST
mkBvredand = liftFun1 Base.mkBvredand
mkBvredor :: MonadZ3 z3 => AST -> z3 AST
mkBvredor = liftFun1 Base.mkBvredor
mkBvand :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvand = liftFun2 Base.mkBvand
mkBvor :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvor = liftFun2 Base.mkBvor
mkBvxor :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvxor = liftFun2 Base.mkBvxor
mkBvnand :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvnand = liftFun2 Base.mkBvnand
mkBvnor :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvnor = liftFun2 Base.mkBvnor
mkBvxnor :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvxnor = liftFun2 Base.mkBvxnor
mkBvneg :: MonadZ3 z3 => AST -> z3 AST
mkBvneg = liftFun1 Base.mkBvneg
mkBvadd :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvadd = liftFun2 Base.mkBvadd
mkBvsub :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsub = liftFun2 Base.mkBvsub
mkBvmul :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvmul = liftFun2 Base.mkBvmul
mkBvudiv :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvudiv = liftFun2 Base.mkBvudiv
mkBvsdiv :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsdiv = liftFun2 Base.mkBvsdiv
mkBvurem :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvurem = liftFun2 Base.mkBvurem
mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsrem = liftFun2 Base.mkBvsrem
mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsmod = liftFun2 Base.mkBvsmod
mkBvult :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvult = liftFun2 Base.mkBvult
mkBvslt :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvslt = liftFun2 Base.mkBvslt
mkBvule :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvule = liftFun2 Base.mkBvule
mkBvsle :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsle = liftFun2 Base.mkBvsle
mkBvuge :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvuge = liftFun2 Base.mkBvuge
mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsge = liftFun2 Base.mkBvsge
mkBvugt :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvugt = liftFun2 Base.mkBvugt
mkBvsgt :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsgt = liftFun2 Base.mkBvsgt
mkConcat :: MonadZ3 z3 => AST -> AST -> z3 AST
mkConcat = liftFun2 Base.mkConcat
mkExtract :: MonadZ3 z3 => Int -> Int -> AST -> z3 AST
mkExtract = liftFun3 Base.mkExtract
mkSignExt :: MonadZ3 z3 => Int -> AST -> z3 AST
mkSignExt = liftFun2 Base.mkSignExt
mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 AST
mkZeroExt = liftFun2 Base.mkZeroExt
mkRepeat :: MonadZ3 z3 => Int -> AST -> z3 AST
mkRepeat = liftFun2 Base.mkRepeat
mkBvshl :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvshl = liftFun2 Base.mkBvshl
mkBvlshr :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvlshr = liftFun2 Base.mkBvlshr
mkBvashr :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvashr = liftFun2 Base.mkBvashr
mkRotateLeft :: MonadZ3 z3 => Int -> AST -> z3 AST
mkRotateLeft = liftFun2 Base.mkRotateLeft
mkRotateRight :: MonadZ3 z3 => Int -> AST -> z3 AST
mkRotateRight = liftFun2 Base.mkRotateRight
mkExtRotateLeft :: MonadZ3 z3 => AST -> AST -> z3 AST
mkExtRotateLeft = liftFun2 Base.mkExtRotateLeft
mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST
mkExtRotateRight = liftFun2 Base.mkExtRotateRight
mkInt2bv :: MonadZ3 z3 => Int -> AST -> z3 AST
mkInt2bv = liftFun2 Base.mkInt2bv
mkBv2int :: MonadZ3 z3 => AST -> Bool -> z3 AST
mkBv2int = liftFun2 Base.mkBv2int
mkBvaddNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST
mkBvaddNoOverflow = liftFun3 Base.mkBvaddNoOverflow
mkBvaddNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvaddNoUnderflow = liftFun2 Base.mkBvaddNoUnderflow
mkBvsubNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsubNoOverflow = liftFun2 Base.mkBvsubNoOverflow
mkBvsubNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsubNoUnderflow = liftFun2 Base.mkBvsubNoUnderflow
mkBvsdivNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvsdivNoOverflow = liftFun2 Base.mkBvsdivNoOverflow
mkBvnegNoOverflow :: MonadZ3 z3 => AST -> z3 AST
mkBvnegNoOverflow = liftFun1 Base.mkBvnegNoOverflow
mkBvmulNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST
mkBvmulNoOverflow = liftFun3 Base.mkBvmulNoOverflow
mkBvmulNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
mkBvmulNoUnderflow = liftFun2 Base.mkBvmulNoUnderflow
mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST
mkSelect = liftFun2 Base.mkSelect
mkStore :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
mkStore = liftFun3 Base.mkStore
mkConstArray :: MonadZ3 z3 => Sort -> AST -> z3 AST
mkConstArray = liftFun2 Base.mkConstArray
mkMap :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST
mkMap = liftFun2 Base.mkMap
mkArrayDefault :: MonadZ3 z3 => AST -> z3 AST
mkArrayDefault = liftFun1 Base.mkArrayDefault
mkEmptySet :: MonadZ3 z3 => Sort -> z3 AST
mkEmptySet = liftFun1 Base.mkEmptySet
mkFullSet :: MonadZ3 z3 => Sort -> z3 AST
mkFullSet = liftFun1 Base.mkFullSet
mkSetAdd :: MonadZ3 z3 => AST -> AST -> z3 AST
mkSetAdd = liftFun2 Base.mkSetAdd
mkSetDel :: MonadZ3 z3 => AST -> AST -> z3 AST
mkSetDel = liftFun2 Base.mkSetDel
mkSetUnion :: MonadZ3 z3 => [AST] -> z3 AST
mkSetUnion = liftFun1 Base.mkSetUnion
mkSetIntersect :: MonadZ3 z3 => [AST] -> z3 AST
mkSetIntersect = liftFun1 Base.mkSetIntersect
mkSetDifference :: MonadZ3 z3 => AST -> AST -> z3 AST
mkSetDifference = liftFun2 Base.mkSetDifference
mkSetComplement :: MonadZ3 z3 => AST -> z3 AST
mkSetComplement = liftFun1 Base.mkSetComplement
mkSetMember :: MonadZ3 z3 => AST -> AST -> z3 AST
mkSetMember = liftFun2 Base.mkSetMember
mkSetSubset :: MonadZ3 z3 => AST -> AST -> z3 AST
mkSetSubset = liftFun2 Base.mkSetSubset
mkNumeral :: MonadZ3 z3 => String -> Sort -> z3 AST
mkNumeral = liftFun2 Base.mkNumeral
mkReal :: MonadZ3 z3 => Int -> Int -> z3 AST
mkReal = liftFun2 Base.mkReal
mkInt :: MonadZ3 z3 => Int -> Sort -> z3 AST
mkInt = liftFun2 Base.mkInt
mkUnsignedInt :: MonadZ3 z3 => Word -> Sort -> z3 AST
mkUnsignedInt = liftFun2 Base.mkUnsignedInt
mkInt64 :: MonadZ3 z3 => Int64 -> Sort -> z3 AST
mkInt64 = liftFun2 Base.mkInt64
mkUnsignedInt64 :: MonadZ3 z3 => Word64 -> Sort -> z3 AST
mkUnsignedInt64 = liftFun2 Base.mkUnsignedInt64
mkIntegral :: (MonadZ3 z3, Integral a) => a -> Sort -> z3 AST
mkIntegral = liftFun2 Base.mkIntegral
mkRational :: MonadZ3 z3 => Rational -> z3 AST
mkRational = liftFun1 Base.mkRational
mkFixed :: (MonadZ3 z3, HasResolution a) => Fixed a -> z3 AST
mkFixed = liftFun1 Base.mkFixed
mkRealNum :: (MonadZ3 z3, Real r) => r -> z3 AST
mkRealNum = liftFun1 Base.mkRealNum
mkInteger :: MonadZ3 z3 => Integer -> z3 AST
mkInteger = liftFun1 Base.mkInteger
mkIntNum :: (MonadZ3 z3, Integral a) => a -> z3 AST
mkIntNum = liftFun1 Base.mkIntNum
mkBitvector :: MonadZ3 z3 => Int
-> Integer
-> z3 AST
mkBitvector = liftFun2 Base.mkBitvector
mkBvNum :: (MonadZ3 z3, Integral i) => Int
-> i
-> z3 AST
mkBvNum = liftFun2 Base.mkBvNum
mkSeqSort :: MonadZ3 z3 => Sort -> z3 Sort
mkSeqSort = liftFun1 Base.mkSeqSort
isSeqSort :: MonadZ3 z3 => Sort -> z3 Bool
isSeqSort = liftFun1 Base.isSeqSort
mkReSort :: MonadZ3 z3 => Sort -> z3 Sort
mkReSort = liftFun1 Base.mkReSort
isReSort :: MonadZ3 z3 => Sort -> z3 Bool
isReSort = liftFun1 Base.isReSort
mkStringSort :: MonadZ3 z3 => z3 Sort
mkStringSort = liftScalar Base.mkStringSort
isStringSort :: MonadZ3 z3 => Sort -> z3 Bool
isStringSort = liftFun1 Base.isStringSort
mkString :: MonadZ3 z3 => String -> z3 AST
mkString = liftFun1 Base.mkString
isString :: MonadZ3 z3 => AST -> z3 Bool
isString = liftFun1 Base.isString
getString :: MonadZ3 z3 => AST -> z3 String
getString = liftFun1 Base.getString
mkSeqEmpty :: MonadZ3 z3 => Sort -> z3 AST
mkSeqEmpty = liftFun1 Base.mkSeqEmpty
mkSeqUnit :: MonadZ3 z3 => AST -> z3 AST
mkSeqUnit = liftFun1 Base.mkSeqUnit
mkSeqConcat :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST
mkSeqConcat = liftFun2 Base.mkSeqConcat
mkSeqPrefix :: MonadZ3 z3
=> AST
-> AST
-> z3 AST
mkSeqPrefix = liftFun2 Base.mkSeqPrefix
mkSeqSuffix :: MonadZ3 z3
=> AST
-> AST
-> z3 AST
mkSeqSuffix = liftFun2 Base.mkSeqSuffix
mkSeqContains :: MonadZ3 z3
=> AST
-> AST
-> z3 AST
mkSeqContains = liftFun2 Base.mkSeqContains
mkSeqExtract :: MonadZ3 z3
=> AST
-> AST
-> AST
-> z3 AST
mkSeqExtract = liftFun3 Base.mkSeqExtract
mkSeqReplace :: MonadZ3 z3
=> AST
-> AST
-> AST
-> z3 AST
mkSeqReplace = liftFun3 Base.mkSeqReplace
mkSeqAt :: MonadZ3 z3
=> AST
-> AST
-> z3 AST
mkSeqAt = liftFun2 Base.mkSeqAt
mkSeqLength :: MonadZ3 z3 => AST -> z3 AST
mkSeqLength = liftFun1 Base.mkSeqLength
mkSeqIndex :: MonadZ3 z3
=> AST
-> AST
-> AST
-> z3 AST
mkSeqIndex = liftFun3 Base.mkSeqIndex
mkStrToInt :: MonadZ3 z3 => AST -> z3 AST
mkStrToInt = liftFun1 Base.mkStrToInt
mkIntToStr :: MonadZ3 z3 => AST -> z3 AST
mkIntToStr = liftFun1 Base.mkIntToStr
mkSeqToRe :: MonadZ3 z3 => AST -> z3 AST
mkSeqToRe = liftFun1 Base.mkSeqToRe
mkSeqInRe :: MonadZ3 z3
=> AST
-> AST
-> z3 AST
mkSeqInRe = liftFun2 Base.mkSeqInRe
mkRePlus :: MonadZ3 z3 => AST -> z3 AST
mkRePlus = liftFun1 Base.mkRePlus
mkReStar :: MonadZ3 z3 => AST -> z3 AST
mkReStar = liftFun1 Base.mkReStar
mkReOption :: MonadZ3 z3 => AST -> z3 AST
mkReOption = liftFun1 Base.mkReOption
mkReUnion :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST
mkReUnion = liftFun2 Base.mkReUnion
mkReConcat :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST
mkReConcat = liftFun2 Base.mkReConcat
mkReRange :: MonadZ3 z3
=> AST
-> AST
-> z3 AST
mkReRange = liftFun2 Base.mkReRange
mkReLoop :: (Integral int, MonadZ3 z3)
=> AST
-> int
-> int
-> z3 AST
mkReLoop = liftFun3 Base.mkReLoop
mkReIntersect :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST
mkReIntersect = liftFun2 Base.mkReIntersect
mkReComplement :: MonadZ3 z3 => AST -> z3 AST
mkReComplement = liftFun1 Base.mkReComplement
mkReEmpty :: MonadZ3 z3 => Sort -> z3 AST
mkReEmpty = liftFun1 Base.mkReEmpty
mkReFull :: MonadZ3 z3 => Sort -> z3 AST
mkReFull = liftFun1 Base.mkReFull
mkPattern :: MonadZ3 z3 => [AST] -> z3 Pattern
mkPattern = liftFun1 Base.mkPattern
mkBound :: MonadZ3 z3 => Int -> Sort -> z3 AST
mkBound = liftFun2 Base.mkBound
mkForall :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST
mkForall = liftFun4 Base.mkForall
mkForallConst :: MonadZ3 z3 => [Pattern] -> [App] -> AST -> z3 AST
mkForallConst = liftFun3 Base.mkForallConst
mkExistsConst :: MonadZ3 z3 => [Pattern] -> [App] -> AST -> z3 AST
mkExistsConst = liftFun3 Base.mkExistsConst
mkExists :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST
mkExists = liftFun4 Base.mkExists
getSymbolString :: MonadZ3 z3 => Symbol -> z3 String
getSymbolString = liftFun1 Base.getSymbolString
getSortKind :: MonadZ3 z3 => Sort -> z3 SortKind
getSortKind = liftFun1 Base.getSortKind
getBvSortSize :: MonadZ3 z3 => Sort -> z3 Int
getBvSortSize = liftFun1 Base.getBvSortSize
getDatatypeSortConstructors :: MonadZ3 z3
=> Sort
-> z3 [FuncDecl]
getDatatypeSortConstructors = liftFun1 Base.getDatatypeSortConstructors
getDatatypeSortRecognizers :: MonadZ3 z3
=> Sort
-> z3 [FuncDecl]
getDatatypeSortRecognizers = liftFun1 Base.getDatatypeSortRecognizers
getDatatypeSortConstructorAccessors :: MonadZ3 z3
=> Sort
-> z3 [[FuncDecl]]
getDatatypeSortConstructorAccessors = liftFun1 Base.getDatatypeSortConstructorAccessors
getDeclName :: MonadZ3 z3 => FuncDecl -> z3 Symbol
getDeclName = liftFun1 Base.getDeclName
getArity :: MonadZ3 z3 => FuncDecl -> z3 Int
getArity = liftFun1 Base.getArity
getDomain :: MonadZ3 z3
=> FuncDecl
-> Int
-> z3 Sort
getDomain = liftFun2 Base.getDomain
getRange :: MonadZ3 z3 => FuncDecl -> z3 Sort
getRange = liftFun1 Base.getRange
appToAst :: MonadZ3 z3 => App -> z3 AST
appToAst = liftFun1 Base.appToAst
getAppDecl :: MonadZ3 z3 => App -> z3 FuncDecl
getAppDecl = liftFun1 Base.getAppDecl
getAppNumArgs :: MonadZ3 z3 => App -> z3 Int
getAppNumArgs = liftFun1 Base.getAppNumArgs
getAppArg :: MonadZ3 z3 => App -> Int -> z3 AST
getAppArg = liftFun2 Base.getAppArg
getAppArgs :: MonadZ3 z3 => App -> z3 [AST]
getAppArgs = liftFun1 Base.getAppArgs
getSort :: MonadZ3 z3 => AST -> z3 Sort
getSort = liftFun1 Base.getSort
getArraySortDomain :: MonadZ3 z3 => Sort -> z3 Sort
getArraySortDomain = liftFun1 Base.getArraySortDomain
getArraySortRange :: MonadZ3 z3 => Sort -> z3 Sort
getArraySortRange = liftFun1 Base.getArraySortRange
getBoolValue :: MonadZ3 z3 => AST -> z3 (Maybe Bool)
getBoolValue = liftFun1 Base.getBoolValue
getAstKind :: MonadZ3 z3 => AST -> z3 ASTKind
getAstKind = liftFun1 Base.getAstKind
isApp :: MonadZ3 z3 => AST -> z3 Bool
isApp = liftFun1 Base.isApp
toApp :: MonadZ3 z3 => AST -> z3 App
toApp = liftFun1 Base.toApp
getNumeralString :: MonadZ3 z3 => AST -> z3 String
getNumeralString = liftFun1 Base.getNumeralString
getIndexValue :: MonadZ3 z3 => AST -> z3 Int
getIndexValue = liftFun1 Base.getIndexValue
isQuantifierForall :: MonadZ3 z3 => AST -> z3 Bool
isQuantifierForall = liftFun1 Base.isQuantifierForall
isQuantifierExists :: MonadZ3 z3 => AST -> z3 Bool
isQuantifierExists = liftFun1 Base.isQuantifierExists
getQuantifierWeight :: MonadZ3 z3 => AST -> z3 Int
getQuantifierWeight = liftFun1 Base.getQuantifierWeight
getQuantifierNumPatterns :: MonadZ3 z3 => AST -> z3 Int
getQuantifierNumPatterns = liftFun1 Base.getQuantifierNumPatterns
getQuantifierPatternAST :: MonadZ3 z3 => AST -> Int -> z3 AST
getQuantifierPatternAST = liftFun2 Base.getQuantifierPatternAST
getQuantifierPatterns :: MonadZ3 z3 => AST -> z3 [AST]
getQuantifierPatterns = liftFun1 Base.getQuantifierPatterns
getQuantifierNumNoPatterns :: MonadZ3 z3 => AST -> z3 Int
getQuantifierNumNoPatterns = liftFun1 Base.getQuantifierNumNoPatterns
getQuantifierNoPatternAST :: MonadZ3 z3 => AST -> Int -> z3 AST
getQuantifierNoPatternAST = liftFun2 Base.getQuantifierNoPatternAST
getQuantifierNoPatterns :: MonadZ3 z3 => AST -> z3 [AST]
getQuantifierNoPatterns = liftFun1 Base.getQuantifierNoPatterns
getQuantifierNumBound :: MonadZ3 z3 => AST -> z3 Int
getQuantifierNumBound = liftFun1 Base.getQuantifierNumBound
getQuantifierBoundName :: MonadZ3 z3 => AST -> Int -> z3 Symbol
getQuantifierBoundName = liftFun2 Base.getQuantifierBoundName
getQuantifierBoundSort :: MonadZ3 z3 => AST -> Int -> z3 Sort
getQuantifierBoundSort = liftFun2 Base.getQuantifierBoundSort
getQuantifierBoundVars :: MonadZ3 z3 => AST -> z3 [AST]
getQuantifierBoundVars = liftFun1 Base.getQuantifierBoundVars
getQuantifierBody :: MonadZ3 z3 => AST -> z3 AST
getQuantifierBody = liftFun1 Base.getQuantifierBody
simplify :: MonadZ3 z3 => AST -> z3 AST
simplify = liftFun1 Base.simplify
simplifyEx :: MonadZ3 z3 => AST -> Params -> z3 AST
simplifyEx = liftFun2 Base.simplifyEx
getBool :: MonadZ3 z3 => AST -> z3 Bool
getBool = liftFun1 Base.getBool
getInt :: MonadZ3 z3 => AST -> z3 Integer
getInt = liftFun1 Base.getInt
getReal :: MonadZ3 z3 => AST -> z3 Rational
getReal = liftFun1 Base.getReal
getBv :: MonadZ3 z3 => AST
-> Bool
-> z3 Integer
getBv = liftFun2 Base.getBv
substituteVars :: MonadZ3 z3 => AST -> [AST] -> z3 AST
substituteVars = liftFun2 Base.substituteVars
substitute :: MonadZ3 z3 => AST -> [(AST, AST)] -> z3 AST
substitute = liftFun2 Base.substitute
modelEval :: MonadZ3 z3 => Model -> AST
-> Bool
-> z3 (Maybe AST)
modelEval = liftFun3 Base.modelEval
evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel)
evalArray = liftFun2 Base.evalArray
getConstInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe AST)
getConstInterp = liftFun2 Base.getConstInterp
getFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncInterp)
getFuncInterp = liftFun2 Base.getFuncInterp
hasInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 Bool
hasInterp = liftFun2 Base.hasInterp
numConsts :: MonadZ3 z3 => Model -> z3 Word
numConsts = liftFun1 Base.numConsts
numFuncs :: MonadZ3 z3 => Model -> z3 Word
numFuncs = liftFun1 Base.numFuncs
getConstDecl :: MonadZ3 z3 => Model -> Word -> z3 FuncDecl
getConstDecl = liftFun2 Base.getConstDecl
getFuncDecl :: MonadZ3 z3 => Model -> Word -> z3 FuncDecl
getFuncDecl = liftFun2 Base.getFuncDecl
getConsts :: MonadZ3 z3 => Model -> z3 [FuncDecl]
getConsts = liftFun1 Base.getConsts
getFuncs :: MonadZ3 z3 => Model -> z3 [FuncDecl]
getFuncs = liftFun1 Base.getFuncs
isAsArray :: MonadZ3 z3 => AST -> z3 Bool
isAsArray = liftFun1 Base.isAsArray
isEqAST :: MonadZ3 z3 => AST -> AST -> z3 Bool
isEqAST = liftFun2 Base.isEqAST
addFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 FuncInterp
addFuncInterp = liftFun3 Base.addFuncInterp
addConstInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 ()
addConstInterp = liftFun3 Base.addConstInterp
getAsArrayFuncDecl :: MonadZ3 z3 => AST -> z3 FuncDecl
getAsArrayFuncDecl = liftFun1 Base.getAsArrayFuncDecl
funcInterpGetNumEntries :: MonadZ3 z3 => FuncInterp -> z3 Int
funcInterpGetNumEntries = liftFun1 Base.funcInterpGetNumEntries
funcInterpGetEntry :: MonadZ3 z3 => FuncInterp -> Int -> z3 FuncEntry
funcInterpGetEntry = liftFun2 Base.funcInterpGetEntry
funcInterpGetElse :: MonadZ3 z3 => FuncInterp -> z3 AST
funcInterpGetElse = liftFun1 Base.funcInterpGetElse
funcInterpGetArity :: MonadZ3 z3 => FuncInterp -> z3 Int
funcInterpGetArity = liftFun1 Base.funcInterpGetArity
funcEntryGetValue :: MonadZ3 z3 => FuncEntry -> z3 AST
funcEntryGetValue = liftFun1 Base.funcEntryGetValue
funcEntryGetNumArgs :: MonadZ3 z3 => FuncEntry -> z3 Int
funcEntryGetNumArgs = liftFun1 Base.funcEntryGetNumArgs
funcEntryGetArg :: MonadZ3 z3 => FuncEntry -> Int -> z3 AST
funcEntryGetArg = liftFun2 Base.funcEntryGetArg
modelToString :: MonadZ3 z3 => Model -> z3 String
modelToString = liftFun1 Base.modelToString
showModel :: MonadZ3 z3 => Model -> z3 String
showModel = modelToString
type EvalAst m a = Model -> AST -> m (Maybe a)
eval :: MonadZ3 z3 => EvalAst z3 AST
eval = liftFun2 Base.eval
evalBool :: MonadZ3 z3 => EvalAst z3 Bool
evalBool = liftFun2 Base.evalBool
evalInt :: MonadZ3 z3 => EvalAst z3 Integer
evalInt = liftFun2 Base.evalInt
evalReal :: MonadZ3 z3 => EvalAst z3 Rational
evalReal = liftFun2 Base.evalReal
evalBv :: MonadZ3 z3 => Bool
-> EvalAst z3 Integer
evalBv = liftFun3 Base.evalBv
evalT :: (MonadZ3 z3,Traversable t) => Model -> t AST -> z3 (Maybe (t AST))
evalT = liftFun2 Base.evalT
mapEval :: (MonadZ3 z3, Traversable t) => EvalAst z3 a
-> Model
-> t AST
-> z3 (Maybe (t a))
mapEval f m = fmap T.sequence . T.mapM (f m)
evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel)
evalFunc = liftFun2 Base.evalFunc
mkTactic :: MonadZ3 z3 => String -> z3 Tactic
mkTactic = liftFun1 Base.mkTactic
andThenTactic :: MonadZ3 z3 => Tactic -> Tactic -> z3 Tactic
andThenTactic = liftFun2 Base.andThenTactic
orElseTactic :: MonadZ3 z3 => Tactic -> Tactic -> z3 Tactic
orElseTactic = liftFun2 Base.andThenTactic
skipTactic :: MonadZ3 z3 => z3 Tactic
skipTactic = liftScalar Base.skipTactic
tryForTactic :: MonadZ3 z3 => Tactic -> Int -> z3 Tactic
tryForTactic = liftFun2 Base.tryForTactic
mkQuantifierEliminationTactic :: MonadZ3 z3 => z3 Tactic
mkQuantifierEliminationTactic = liftScalar Base.mkQuantifierEliminationTactic
mkAndInverterGraphTactic :: MonadZ3 z3 => z3 Tactic
mkAndInverterGraphTactic = liftScalar Base.mkAndInverterGraphTactic
applyTactic :: MonadZ3 z3 => Tactic -> Goal -> z3 ApplyResult
applyTactic = liftFun2 Base.applyTactic
getApplyResultNumSubgoals :: MonadZ3 z3 => ApplyResult -> z3 Int
getApplyResultNumSubgoals = liftFun1 Base.getApplyResultNumSubgoals
getApplyResultSubgoal :: MonadZ3 z3 => ApplyResult -> Int -> z3 Goal
getApplyResultSubgoal = liftFun2 Base.getApplyResultSubgoal
getApplyResultSubgoals :: MonadZ3 z3 => ApplyResult -> z3 [Goal]
getApplyResultSubgoals = liftFun1 Base.getApplyResultSubgoals
mkGoal :: MonadZ3 z3 => Bool -> Bool -> Bool -> z3 Goal
mkGoal = liftFun3 Base.mkGoal
goalAssert :: MonadZ3 z3 => Goal -> AST -> z3 ()
goalAssert = liftFun2 Base.goalAssert
getGoalSize :: MonadZ3 z3 => Goal -> z3 Int
getGoalSize = liftFun1 Base.getGoalSize
getGoalFormula :: MonadZ3 z3 => Goal -> Int -> z3 AST
getGoalFormula = liftFun2 Base.getGoalFormula
getGoalFormulas :: MonadZ3 z3 => Goal -> z3 [AST]
getGoalFormulas = liftFun1 Base.getGoalFormulas
setASTPrintMode :: MonadZ3 z3 => ASTPrintMode -> z3 ()
setASTPrintMode = liftFun1 Base.setASTPrintMode
astToString :: MonadZ3 z3 => AST -> z3 String
astToString = liftFun1 Base.astToString
patternToString :: MonadZ3 z3 => Pattern -> z3 String
patternToString = liftFun1 Base.patternToString
sortToString :: MonadZ3 z3 => Sort -> z3 String
sortToString = liftFun1 Base.sortToString
funcDeclToString :: MonadZ3 z3 => FuncDecl -> z3 String
funcDeclToString = liftFun1 Base.funcDeclToString
benchmarkToSMTLibString :: MonadZ3 z3 =>
String
-> String
-> String
-> String
-> [AST]
-> AST
-> z3 String
benchmarkToSMTLibString = liftFun6 Base.benchmarkToSMTLibString
parseSMTLib2String :: MonadZ3 z3 =>
String
-> [Symbol]
-> [Sort]
-> [Symbol]
-> [FuncDecl]
-> z3 AST
parseSMTLib2String = liftFun5 Base.parseSMTLib2String
parseSMTLib2File :: MonadZ3 z3 =>
String
-> [Symbol]
-> [Sort]
-> [Symbol]
-> [FuncDecl]
-> z3 AST
parseSMTLib2File = liftFun5 Base.parseSMTLib2File
getVersion :: MonadZ3 z3 => z3 Version
getVersion = liftIO Base.getVersion
class MonadZ3 m => MonadFixedpoint m where
getFixedpoint :: m Base.Fixedpoint
fixedpointAddRule :: MonadFixedpoint z3 => AST -> Symbol -> z3 ()
fixedpointAddRule = liftFixedpoint2 Base.fixedpointAddRule
fixedpointSetParams :: MonadFixedpoint z3 => Params -> z3 ()
fixedpointSetParams = liftFixedpoint1 Base.fixedpointSetParams
fixedpointRegisterRelation :: MonadFixedpoint z3 => FuncDecl -> z3 ()
fixedpointRegisterRelation = liftFixedpoint1 Base.fixedpointRegisterRelation
fixedpointQueryRelations :: MonadFixedpoint z3 => [FuncDecl] -> z3 Result
fixedpointQueryRelations = liftFixedpoint1 Base.fixedpointQueryRelations
fixedpointGetAnswer :: MonadFixedpoint z3 => z3 AST
fixedpointGetAnswer = liftFixedpoint0 Base.fixedpointGetAnswer
fixedpointGetAssertions :: MonadFixedpoint z3 => z3 [AST]
fixedpointGetAssertions = liftFixedpoint0 Base.fixedpointGetAssertions
class MonadZ3 m => MonadOptimize m where
getOptimize :: m Base.Optimize
optimizeAssert :: MonadOptimize z3 => AST -> z3 ()
optimizeAssert = liftOptimize1 Base.optimizeAssert
optimizeAssertAndTrack :: MonadOptimize z3 => AST -> AST -> z3 ()
optimizeAssertAndTrack = liftOptimize2 Base.optimizeAssertAndTrack
optimizeAssertSoft :: MonadOptimize z3 => AST -> String -> Symbol -> z3 ()
optimizeAssertSoft = undefined
optimizeMaximize :: MonadOptimize z3 => AST -> z3 Int
optimizeMaximize = liftOptimize1 Base.optimizeMaximize
optimizeMinimize :: MonadOptimize z3 => AST -> z3 Int
optimizeMinimize = liftOptimize1 Base.optimizeMinimize
optimizePush :: MonadOptimize z3 => z3 ()
optimizePush = liftOptimize0 Base.optimizePush
optimizePop :: MonadOptimize z3 => z3 ()
optimizePop = liftOptimize0 Base.optimizePop
optimizeCheck :: MonadOptimize z3 => [AST] -> z3 Result
optimizeCheck = liftOptimize1 Base.optimizeCheck
optimizeGetReasonUnknown :: MonadOptimize z3 => z3 String
optimizeGetReasonUnknown = liftOptimize0 Base.optimizeGetReasonUnknown
optimizeGetModel :: MonadOptimize z3 => z3 Model
optimizeGetModel = liftOptimize0 Base.optimizeGetModel
optimizeGetUnsatCore :: MonadOptimize z3 => z3 [AST]
optimizeGetUnsatCore = liftOptimize0 Base.optimizeGetUnsatCore
optimizeSetParams :: MonadOptimize z3 => Params -> z3 ()
optimizeSetParams = liftOptimize1 Base.optimizeSetParams
optimizeGetLower :: MonadOptimize z3 => Int -> z3 AST
optimizeGetLower = liftOptimize1 Base.optimizeGetLower
optimizeGetUpper :: MonadOptimize z3 => Int -> z3 AST
optimizeGetUpper = liftOptimize1 Base.optimizeGetLower
optimizeGetUpperAsVector :: MonadOptimize z3 => Int -> z3 [AST]
optimizeGetUpperAsVector = liftOptimize1 Base.optimizeGetUpperAsVector
optimizeGetLowerAsVector :: MonadOptimize z3 => Int -> z3 [AST]
optimizeGetLowerAsVector = liftOptimize1 Base.optimizeGetLowerAsVector
optimizeToString :: MonadOptimize z3 => z3 String
optimizeToString = liftOptimize0 Base.optimizeToString
optimizeFromString :: MonadOptimize z3 => String -> z3 ()
optimizeFromString = liftOptimize1 Base.optimizeFromString
optimizeFromFile :: MonadOptimize z3 => String -> z3 ()
optimizeFromFile = liftOptimize1 Base.optimizeFromFile
optimizeGetHelp :: MonadOptimize z3 => z3 String
optimizeGetHelp = liftOptimize0 Base.optimizeGetHelp
optimizeGetAssertions :: MonadOptimize z3 => z3 [AST]
optimizeGetAssertions = liftOptimize0 Base.optimizeGetAssertions
optimizeGetObjectives :: MonadOptimize z3 => z3 [AST]
optimizeGetObjectives = liftOptimize0 Base.optimizeGetObjectives
solverGetHelp :: MonadZ3 z3 => z3 String
solverGetHelp = liftSolver0 Base.solverGetHelp
solverSetParams :: MonadZ3 z3 => Params -> z3 ()
solverSetParams = liftSolver1 Base.solverSetParams
solverPush :: MonadZ3 z3 => z3 ()
solverPush = liftSolver0 Base.solverPush
solverPop :: MonadZ3 z3 => Int -> z3 ()
solverPop = liftSolver1 Base.solverPop
solverReset :: MonadZ3 z3 => z3 ()
solverReset = liftSolver0 Base.solverReset
solverGetNumScopes :: MonadZ3 z3 => z3 Int
solverGetNumScopes = liftSolver0 Base.solverGetNumScopes
solverAssertCnstr :: MonadZ3 z3 => AST -> z3 ()
solverAssertCnstr = liftSolver1 Base.solverAssertCnstr
solverAssertAndTrack :: MonadZ3 z3 => AST -> AST -> z3 ()
solverAssertAndTrack = liftSolver2 Base.solverAssertAndTrack
solverCheck :: MonadZ3 z3 => z3 Result
solverCheck = liftSolver0 Base.solverCheck
solverCheckAssumptions :: MonadZ3 z3 => [AST] -> z3 Result
solverCheckAssumptions = liftSolver1 Base.solverCheckAssumptions
solverGetModel :: MonadZ3 z3 => z3 Model
solverGetModel = liftSolver0 Base.solverGetModel
solverGetProof :: MonadZ3 z3 => z3 AST
solverGetProof = liftSolver0 Base.solverGetProof
solverGetUnsatCore :: MonadZ3 z3 => z3 [AST]
solverGetUnsatCore = liftSolver0 Base.solverGetUnsatCore
solverGetReasonUnknown :: MonadZ3 z3 => z3 String
solverGetReasonUnknown = liftSolver0 Base.solverGetReasonUnknown
solverToString :: MonadZ3 z3 => z3 String
solverToString = liftSolver0 Base.solverToString
push :: MonadZ3 z3 => z3 ()
push = solverPush
pop :: MonadZ3 z3 => Int -> z3 ()
pop n = do
scopes <- solverGetNumScopes
if n <= scopes
then solverPop n
else error "Z3.Monad.safePop: too many scopes to backtrack"
local :: MonadZ3 z3 => z3 a -> z3 a
local q = do
push
r <- q
pop 1
return r
reset :: MonadZ3 z3 => z3 ()
reset = solverReset
getNumScopes :: MonadZ3 z3 => z3 Int
getNumScopes = liftSolver0 Base.solverGetNumScopes
assert :: MonadZ3 z3 => AST -> z3 ()
assert = solverAssertCnstr
check :: MonadZ3 z3 => z3 Result
check = solverCheck
checkAssumptions :: MonadZ3 z3 => [AST] -> z3 Result
checkAssumptions = solverCheckAssumptions
solverCheckAndGetModel :: MonadZ3 z3 => z3 (Result, Maybe Model)
solverCheckAndGetModel = liftSolver0 Base.solverCheckAndGetModel
getModel :: MonadZ3 z3 => z3 (Result, Maybe Model)
getModel = solverCheckAndGetModel
withModel :: (Applicative z3, MonadZ3 z3) =>
(Base.Model -> z3 a) -> z3 (Result, Maybe a)
withModel f = do
(r,mb_m) <- getModel
mb_e <- T.traverse f mb_m
return (r, mb_e)
getUnsatCore :: MonadZ3 z3 => z3 [AST]
getUnsatCore = solverGetUnsatCore