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