{-# LANGUAGE GeneralizedNewtypeDeriving #-} -- | -- Module : Z3.Monad -- Copyright : (c) Iago Abal, 2013-2015 -- (c) David Castro, 2013-2015 -- License : BSD3 -- Maintainer: Iago Abal , -- David Castro -- -- A simple monadic interface to Z3 API. -- -- Examples: module Z3.Monad ( -- * Z3 monad MonadZ3(..) , Z3 , module Z3.Opts , Logic(..) , evalZ3 , evalZ3With -- ** Z3 enviroments , Z3Env , newEnv , evalZ3WithEnv -- * Types , Symbol , AST , Sort , FuncDecl , App , Pattern , Constructor , Model , Base.Context , FuncInterp , FuncEntry , Params , Solver , SortKind(..) , ASTKind(..) -- ** Satisfiability result , Result(..) -- * Parameters , mkParams , paramsSetBool , paramsSetUInt , paramsSetDouble , paramsSetSymbol , paramsToString -- * Symbols , mkIntSymbol , mkStringSymbol -- * Sorts , mkUninterpretedSort , mkBoolSort , mkIntSort , mkRealSort , mkBvSort , mkFiniteDomainSort , mkArraySort , mkTupleSort , mkConstructor , mkDatatype , mkDatatypes , mkSetSort -- * Constants and Applications , mkFuncDecl , mkApp , mkConst , mkFreshConst , mkFreshFuncDecl -- ** Helpers , mkVar , mkBoolVar , mkRealVar , mkIntVar , mkBvVar , mkFreshVar , mkFreshBoolVar , mkFreshRealVar , mkFreshIntVar , mkFreshBvVar -- * Propositional Logic and Equality , mkTrue , mkFalse , mkEq , mkNot , mkIte , mkIff , mkImplies , mkXor , mkAnd , mkOr , mkDistinct , mkDistinct1 -- ** Helpers , mkBool -- * Arithmetic: Integers and Reals , mkAdd , mkMul , mkSub , mkSub1 , mkUnaryMinus , mkDiv , mkMod , mkRem , mkLt , mkLe , mkGt , mkGe , mkInt2Real , mkReal2Int , mkIsInt -- * Bit-vectors , 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 -- * Arrays , mkSelect , mkStore , mkConstArray , mkMap , mkArrayDefault -- * Sets , mkEmptySet , mkFullSet , mkSetAdd , mkSetDel , mkSetUnion , mkSetIntersect , mkSetDifference , mkSetComplement , mkSetMember , mkSetSubset -- * Numerals , mkNumeral , mkInt , mkReal , mkUnsignedInt , mkInt64 , mkUnsignedInt64 -- ** Helpers , mkIntegral , mkRational , mkFixed , mkRealNum , mkInteger , mkIntNum , mkBitvector , mkBvNum -- * Sequences and regular expressions , mkSeqSort , isSeqSort , mkReSort , isReSort , mkStringSort , isStringSort , mkString , isString , getString , mkSeqEmpty , mkSeqUnit , mkSeqConcat , mkSeqPrefix , mkSeqSuffix , mkSeqContains , mkSeqExtract , mkSeqReplace , mkSeqAt , mkSeqLength , mkSeqIndex , mkStrToInt , mkIntToStr , mkSeqToRe , mkSeqInRe , mkRePlus , mkReStar , mkReOption , mkReUnion , mkReConcat , mkReRange , mkReLoop , mkReIntersect , mkReComplement , mkReEmpty , mkReFull -- * Quantifiers , mkPattern , mkBound , mkForall , mkExists , mkForallConst , mkExistsConst -- * Accessors , 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 -- ** Helpers , getBool , getInt , getReal , getBv -- * Modifiers , substituteVars , substitute -- * Models , modelEval , evalArray , getConstInterp , getFuncInterp , hasInterp , numConsts , numFuncs , getConstDecl , getFuncDecl , getConsts , getFuncs , isAsArray , isEqAST , addFuncInterp , addConstInterp , getAsArrayFuncDecl , funcInterpGetNumEntries , funcInterpGetEntry , funcInterpGetElse , funcInterpGetArity , funcEntryGetValue , funcEntryGetNumArgs , funcEntryGetArg , modelToString , showModel -- ** Helpers , EvalAst , eval , evalBool , evalInt , evalReal , evalBv , evalT , mapEval , FuncModel(..) , evalFunc -- * Tactics , mkTactic , andThenTactic , orElseTactic , skipTactic , tryForTactic , mkQuantifierEliminationTactic , mkAndInverterGraphTactic , applyTactic , getApplyResultNumSubgoals , getApplyResultSubgoal , getApplyResultSubgoals , mkGoal , goalAssert , getGoalSize , getGoalFormula , getGoalFormulas -- * String Conversion , ASTPrintMode(..) , setASTPrintMode , astToString , patternToString , sortToString , funcDeclToString , benchmarkToSMTLibString -- * Parser interface , parseSMTLib2String , parseSMTLib2File -- * Error Handling , Base.Z3Error(..) , Base.Z3ErrorCode(..) -- * Miscellaneous , Version(..) , getVersion -- * Fixedpoint , MonadFixedpoint(..) , Fixedpoint , fixedpointAddRule , fixedpointSetParams , fixedpointRegisterRelation , fixedpointQueryRelations , fixedpointGetAnswer , fixedpointGetAssertions -- * Optimization , MonadOptimize(..) , Optimize , optimizeAssert , optimizeAssertAndTrack , optimizeAssertSoft , optimizeMaximize , optimizeMinimize , optimizePush , optimizePop , optimizeCheck , optimizeGetReasonUnknown , optimizeGetModel , optimizeGetUnsatCore , optimizeSetParams , optimizeGetLower , optimizeGetUpper , optimizeGetUpperAsVector , optimizeGetLowerAsVector , optimizeToString , optimizeFromString , optimizeFromFile , optimizeGetHelp , optimizeGetAssertions , optimizeGetObjectives -- * Solvers , solverGetHelp , solverSetParams , solverPush , solverPop , solverReset , solverGetNumScopes , solverAssertCnstr , solverAssertAndTrack , solverCheck , solverCheckAssumptions , solverGetModel , solverGetProof , solverGetUnsatCore , solverGetReasonUnknown , solverToString -- ** Helpers , assert , check , checkAssumptions , solverCheckAndGetModel , getModel , withModel , getUnsatCore , push , pop , local , reset , getNumScopes ) where import Z3.Opts import Z3.Base ( Symbol , AST , Sort , FuncDecl , App , Pattern , Constructor , Model , FuncInterp , FuncEntry , FuncModel(..) , Result(..) , Logic(..) , ASTPrintMode(..) , Version(..) , Params , Solver , Fixedpoint , Optimize , SortKind(..) , ASTKind(..) , Tactic , ApplyResult , Goal ) import qualified Z3.Base as Base import Control.Applicative ( Applicative ) import Data.Fixed ( Fixed, HasResolution ) import Control.Monad.Fail import Control.Monad.IO.Class ( MonadIO, liftIO ) import Control.Monad.Trans.Reader ( ReaderT(..), runReaderT, asks ) import Control.Monad.Fix ( MonadFix ) import Data.Int ( Int64 ) import Data.List.NonEmpty (NonEmpty) import Data.Word ( Word, Word64 ) import Data.Traversable ( Traversable ) import qualified Data.Traversable as T --------------------------------------------------------------------- -- The Z3 monad-class class (Applicative m, Monad m, MonadIO m) => MonadZ3 m where getSolver :: m Base.Solver getContext :: m Base.Context instance MonadZ3 m => MonadZ3 (ReaderT r m) where getSolver = ReaderT $ const getSolver getContext = ReaderT $ const getContext ------------------------------------------------- -- Lifting -- TODO: Rename to liftFun0 for consistency liftScalar :: MonadZ3 z3 => (Base.Context -> IO b) -> z3 b liftScalar f = liftIO . f =<< getContext liftFun1 :: MonadZ3 z3 => (Base.Context -> a -> IO b) -> a -> z3 b liftFun1 f a = getContext >>= \ctx -> liftIO (f ctx a) liftFun2 :: MonadZ3 z3 => (Base.Context -> a -> b -> IO c) -> a -> b -> z3 c liftFun2 f a b = getContext >>= \ctx -> liftIO (f ctx a b) liftFun3 :: MonadZ3 z3 => (Base.Context -> a -> b -> c -> IO d) -> a -> b -> c -> z3 d liftFun3 f a b c = getContext >>= \ctx -> liftIO (f ctx a b c) liftFun4 :: MonadZ3 z3 => (Base.Context -> a -> b -> c -> d -> IO e) -> a -> b -> c -> d -> z3 e liftFun4 f a b c d = getContext >>= \ctx -> liftIO (f ctx a b c d) liftFun5 :: MonadZ3 z3 => (Base.Context -> a1 -> a2 -> a3 -> a4 -> a5 -> IO b) -> a1 -> a2 -> a3 -> a4 -> a5-> z3 b liftFun5 f x1 x2 x3 x4 x5 = getContext >>= \ctx -> liftIO (f ctx x1 x2 x3 x4 x5) liftFun6 :: MonadZ3 z3 => (Base.Context -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> IO b) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> z3 b liftFun6 f x1 x2 x3 x4 x5 x6 = getContext >>= \ctx -> liftIO (f ctx x1 x2 x3 x4 x5 x6) liftSolver0 :: MonadZ3 z3 => (Base.Context -> Base.Solver -> IO b) -> z3 b liftSolver0 f_s = do ctx <- getContext liftIO . f_s ctx =<< getSolver liftSolver1 :: MonadZ3 z3 => (Base.Context -> Base.Solver -> a -> IO b) -> a -> z3 b liftSolver1 f_s a = do ctx <- getContext liftIO . (\s -> f_s ctx s a) =<< getSolver liftSolver2 :: MonadZ3 z3 => (Base.Context -> Base.Solver -> a -> b -> IO c) -> a -> b -> z3 c liftSolver2 f a b = do ctx <- getContext slv <- getSolver liftIO $ f ctx slv a b liftFixedpoint0 :: MonadFixedpoint z3 => (Base.Context -> Base.Fixedpoint -> IO b) -> z3 b liftFixedpoint0 f_s = do ctx <- getContext liftIO . f_s ctx =<< getFixedpoint liftFixedpoint1 :: MonadFixedpoint z3 => (Base.Context -> Base.Fixedpoint -> a -> IO b) -> a -> z3 b liftFixedpoint1 f_s a = do ctx <- getContext liftIO . (\s -> f_s ctx s a) =<< getFixedpoint liftFixedpoint2 :: MonadFixedpoint z3 => (Base.Context -> Base.Fixedpoint -> a -> b -> IO c) -> a -> b -> z3 c liftFixedpoint2 f a b = do ctx <- getContext slv <- getFixedpoint liftIO $ f ctx slv a b liftOptimize0 :: MonadOptimize z3 => (Base.Context -> Base.Optimize -> IO b) -> z3 b liftOptimize0 f_s = do ctx <- getContext liftIO . f_s ctx =<< getOptimize liftOptimize1 :: MonadOptimize z3 => (Base.Context -> Base.Optimize -> a -> IO b) -> a -> z3 b liftOptimize1 f_s a = do ctx <- getContext liftIO . (\s -> f_s ctx s a) =<< getOptimize liftOptimize2 :: MonadOptimize z3 => (Base.Context -> Base.Optimize -> a -> b -> IO c) -> a -> b -> z3 c liftOptimize2 f a b = do ctx <- getContext slv <- getOptimize liftIO $ f ctx slv a b ------------------------------------------------- -- A simple Z3 monad. newtype Z3 a = Z3 { _unZ3 :: ReaderT Z3Env IO a } deriving (Functor, Applicative, Monad, MonadIO, MonadFix, MonadFail) -- | Z3 environment. data Z3Env = Z3Env { envSolver :: Base.Solver , envContext :: Base.Context , envFixedpoint :: Base.Fixedpoint , envOptimize :: Base.Optimize } instance MonadZ3 Z3 where getSolver = Z3 $ asks envSolver getContext = Z3 $ asks envContext instance MonadFixedpoint Z3 where getFixedpoint = Z3 $ asks envFixedpoint instance MonadOptimize Z3 where getOptimize = Z3 $ asks envOptimize -- | Eval a Z3 script. evalZ3With :: Maybe Logic -> Opts -> Z3 a -> IO a evalZ3With mbLogic opts (Z3 s) = do env <- newEnv mbLogic opts runReaderT s env -- | Eval a Z3 script with default configuration options. evalZ3 :: Z3 a -> IO a evalZ3 = evalZ3With Nothing stdOpts newEnvWith :: (Base.Config -> IO Base.Context) -> Maybe Logic -> Opts -> IO Z3Env newEnvWith mkContext mbLogic opts = Base.withConfig $ \cfg -> do setOpts cfg opts ctx <- mkContext cfg solver <- maybe (Base.mkSolver ctx) (Base.mkSolverForLogic ctx) mbLogic fixedpoint <- Base.mkFixedpoint ctx optimize <- Base.mkOptimize ctx return $ Z3Env solver ctx fixedpoint optimize -- | Create a new Z3 environment. newEnv :: Maybe Logic -> Opts -> IO Z3Env newEnv = newEnvWith Base.mkContext -- | Eval a Z3 script with a given environment. -- -- Environments may facilitate running many queries under the same -- logical context. -- -- Note that an environment may change after each query. -- If you want to preserve the same environment then use 'local', as in -- @evalZ3WithEnv /env/ (local /query/)@. evalZ3WithEnv :: Z3 a -> Z3Env -> IO a evalZ3WithEnv (Z3 s) = runReaderT s --------------------------------------------------------------------- -- * Parameters -- | Create a Z3 (empty) parameter set. -- -- Starting at Z3 4.0, parameter sets are used to configure many components -- such as: simplifiers, tactics, solvers, etc. mkParams :: MonadZ3 z3 => z3 Params mkParams = liftScalar Base.mkParams -- | Add a Boolean parameter /k/ with value /v/ to the parameter set /p/. paramsSetBool :: MonadZ3 z3 => Params -> Symbol -> Bool -> z3 () paramsSetBool = liftFun3 Base.paramsSetBool -- | Add a unsigned parameter /k/ with value /v/ to the parameter set /p/. paramsSetUInt :: MonadZ3 z3 => Params -> Symbol -> Word -> z3 () paramsSetUInt = liftFun3 Base.paramsSetUInt -- | Add a double parameter /k/ with value /v/ to the parameter set /p/. paramsSetDouble :: MonadZ3 z3 => Params -> Symbol -> Double -> z3 () paramsSetDouble = liftFun3 Base.paramsSetDouble -- | Add a symbol parameter /k/ with value /v/ to the parameter set /p/. paramsSetSymbol :: MonadZ3 z3 => Params -> Symbol -> Symbol -> z3 () paramsSetSymbol = liftFun3 Base.paramsSetSymbol -- | Convert a parameter set into a string. -- -- This function is mainly used for printing the contents of a parameter set. paramsToString :: MonadZ3 z3 => Params -> z3 String paramsToString = liftFun1 Base.paramsToString -- TODO: Z3_params_validate --------------------------------------------------------------------- -- Symbols -- | Create a Z3 symbol using an integer. mkIntSymbol :: (MonadZ3 z3, Integral i) => i -> z3 Symbol mkIntSymbol = liftFun1 Base.mkIntSymbol -- | Create a Z3 symbol using a string. -- -- Reference: mkStringSymbol :: MonadZ3 z3 => String -> z3 Symbol mkStringSymbol = liftFun1 Base.mkStringSymbol --------------------------------------------------------------------- -- Sorts -- | Create a free (uninterpreted) type using the given name (symbol). -- -- Reference: mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort mkUninterpretedSort = liftFun1 Base.mkUninterpretedSort -- | Create the /boolean/ type. -- -- Reference: mkBoolSort :: MonadZ3 z3 => z3 Sort mkBoolSort = liftScalar Base.mkBoolSort -- | Create the /integer/ type. -- -- Reference: mkIntSort :: MonadZ3 z3 => z3 Sort mkIntSort = liftScalar Base.mkIntSort -- | Create the /real/ type. -- -- Reference: mkRealSort :: MonadZ3 z3 => z3 Sort mkRealSort = liftScalar Base.mkRealSort -- | Create a bit-vector type of the given size. -- -- This type can also be seen as a machine integer. -- -- Reference: mkBvSort :: MonadZ3 z3 => Int -> z3 Sort mkBvSort = liftFun1 Base.mkBvSort -- | Create a finite-domain type. mkFiniteDomainSort :: MonadZ3 z3 => Symbol -> Word64 -> z3 Sort mkFiniteDomainSort = liftFun2 Base.mkFiniteDomainSort -- | Create an array type -- -- Reference: -- mkArraySort :: MonadZ3 z3 => Sort -> Sort -> z3 Sort mkArraySort = liftFun2 Base.mkArraySort -- | Create a tuple type -- -- Reference: mkTupleSort :: MonadZ3 z3 => Symbol -- ^ Name of the sort -> [(Symbol, Sort)] -- ^ Name and sort of each field -> z3 (Sort, FuncDecl, [FuncDecl]) -- ^ Resulting sort, and function -- declarations for the -- constructor and projections. mkTupleSort = liftFun2 Base.mkTupleSort -- | Create a constructor -- -- Reference: mkConstructor :: MonadZ3 z3 => Symbol -- ^ Name of the constructor -> Symbol -- ^ Name of recognizer function -> [(Symbol, Maybe Sort, Int)] -- ^ Name, sort option, and sortRefs -> z3 Constructor mkConstructor = liftFun3 Base.mkConstructor -- | Create datatype, such as lists, trees, records, enumerations or unions of -- records. The datatype may be recursive. Return the datatype sort. -- -- Reference mkDatatype :: MonadZ3 z3 => Symbol -> [Constructor] -> z3 Sort mkDatatype = liftFun2 Base.mkDatatype -- | Create mutually recursive datatypes, such as a tree and forest. -- -- Returns the datatype sorts mkDatatypes :: MonadZ3 z3 => [Symbol] -> [[Constructor]] -> z3 [Sort] mkDatatypes = liftFun2 Base.mkDatatypes -- | Create a set type -- -- Reference: -- mkSetSort :: MonadZ3 z3 => Sort -> z3 Sort mkSetSort = liftFun1 Base.mkSetSort --------------------------------------------------------------------- -- Constants and Applications -- | A Z3 function mkFuncDecl :: MonadZ3 z3 => Symbol -> [Sort] -> Sort -> z3 FuncDecl mkFuncDecl = liftFun3 Base.mkFuncDecl -- | Create a constant or function application. -- -- Reference: mkApp :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST mkApp = liftFun2 Base.mkApp -- | Declare and create a constant. -- -- Reference: mkConst :: MonadZ3 z3 => Symbol -> Sort -> z3 AST mkConst = liftFun2 Base.mkConst -- | Declare and create a constant. -- -- Reference: mkFreshConst :: MonadZ3 z3 => String -> Sort -> z3 AST mkFreshConst = liftFun2 Base.mkFreshConst -- | Declare a fresh constant or function. -- -- Reference: mkFreshFuncDecl :: MonadZ3 z3 => String -> [Sort] -> Sort -> z3 FuncDecl mkFreshFuncDecl = liftFun3 Base.mkFreshFuncDecl ------------------------------------------------- -- ** Helpers -- | Declare and create a variable (aka /constant/). -- -- An alias for 'mkConst'. mkVar :: MonadZ3 z3 => Symbol -> Sort -> z3 AST mkVar = liftFun2 Base.mkVar -- | Declarate and create a variable of sort /bool/. -- -- See 'mkVar'. mkBoolVar :: MonadZ3 z3 => Symbol -> z3 AST mkBoolVar = liftFun1 Base.mkBoolVar -- | Declarate and create a variable of sort /real/. -- -- See 'mkVar'. mkRealVar :: MonadZ3 z3 => Symbol -> z3 AST mkRealVar = liftFun1 Base.mkRealVar -- | Declarate and create a variable of sort /int/. -- -- See 'mkVar'. mkIntVar :: MonadZ3 z3 => Symbol -> z3 AST mkIntVar = liftFun1 Base.mkIntVar -- | Declarate and create a variable of sort /bit-vector/. -- -- See 'mkVar'. mkBvVar :: MonadZ3 z3 => Symbol -> Int -- ^ bit-width -> z3 AST mkBvVar = liftFun2 Base.mkBvVar -- | Declare and create a /fresh/ variable (aka /constant/). -- -- An alias for 'mkFreshConst'. mkFreshVar :: MonadZ3 z3 => String -> Sort -> z3 AST mkFreshVar = liftFun2 Base.mkFreshConst -- | Declarate and create a /fresh/ variable of sort /bool/. -- -- See 'mkFreshVar'. mkFreshBoolVar :: MonadZ3 z3 => String -> z3 AST mkFreshBoolVar = liftFun1 Base.mkFreshBoolVar -- | Declarate and create a /fresh/ variable of sort /real/. -- -- See 'mkFreshVar'. mkFreshRealVar :: MonadZ3 z3 => String -> z3 AST mkFreshRealVar = liftFun1 Base.mkFreshRealVar -- | Declarate and create a /fresh/ variable of sort /int/. -- -- See 'mkFreshVar'. mkFreshIntVar :: MonadZ3 z3 => String -> z3 AST mkFreshIntVar = liftFun1 Base.mkFreshIntVar -- | Declarate and create a /fresh/ variable of sort /bit-vector/. -- -- See 'mkFreshVar'. mkFreshBvVar :: MonadZ3 z3 => String -> Int -- ^ bit-width -> z3 AST mkFreshBvVar = liftFun2 Base.mkFreshBvVar --------------------------------------------------------------------- -- Propositional Logic and Equality -- | Create an AST node representing /true/. -- -- Reference: mkTrue :: MonadZ3 z3 => z3 AST mkTrue = liftScalar Base.mkTrue -- | Create an AST node representing /false/. -- -- Reference: mkFalse :: MonadZ3 z3 => z3 AST mkFalse = liftScalar Base.mkFalse -- | Create an AST node representing /l = r/. -- -- Reference: mkEq :: MonadZ3 z3 => AST -> AST -> z3 AST mkEq = liftFun2 Base.mkEq -- | The distinct construct is used for declaring the arguments pairwise -- distinct. -- -- Requires a non-empty list. -- -- Reference: mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST mkDistinct = liftFun1 Base.mkDistinct -- | Same as 'mkDistinct' but type-safe. mkDistinct1 :: MonadZ3 z3 => NonEmpty AST -> z3 AST mkDistinct1 = liftFun1 Base.mkDistinct1 -- | Create an AST node representing /not(a)/. -- -- Reference: mkNot :: MonadZ3 z3 => AST -> z3 AST mkNot = liftFun1 Base.mkNot -- | Create an AST node representing an if-then-else: /ite(t1, t2, t3)/. -- -- Reference: mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST mkIte = liftFun3 Base.mkIte -- | Create an AST node representing /t1 iff t2/. -- -- Reference: mkIff :: MonadZ3 z3 => AST -> AST -> z3 AST mkIff = liftFun2 Base.mkIff -- | Create an AST node representing /t1 implies t2/. -- -- Reference: mkImplies :: MonadZ3 z3 => AST -> AST -> z3 AST mkImplies = liftFun2 Base.mkImplies -- | Create an AST node representing /t1 xor t2/. -- -- Reference: mkXor :: MonadZ3 z3 => AST -> AST -> z3 AST mkXor = liftFun2 Base.mkXor -- | Create an AST node representing args[0] and ... and args[num_args-1]. -- -- Reference: mkAnd :: MonadZ3 z3 => [AST] -> z3 AST mkAnd = liftFun1 Base.mkAnd -- | Create an AST node representing args[0] or ... or args[num_args-1]. -- -- Reference: mkOr :: MonadZ3 z3 => [AST] -> z3 AST mkOr = liftFun1 Base.mkOr ------------------------------------------------- -- ** Helpers -- | Create an AST node representing the given boolean. mkBool :: MonadZ3 z3 => Bool -> z3 AST mkBool = liftFun1 Base.mkBool --------------------------------------------------------------------- -- Arithmetic: Integers and Reals -- | Create an AST node representing args[0] + ... + args[num_args-1]. -- -- Reference: mkAdd :: MonadZ3 z3 => [AST] -> z3 AST mkAdd = liftFun1 Base.mkAdd -- | Create an AST node representing args[0] * ... * args[num_args-1]. -- -- Reference: mkMul :: MonadZ3 z3 => [AST] -> z3 AST mkMul = liftFun1 Base.mkMul -- | Create an AST node representing args[0] - ... - args[num_args - 1]. -- -- Requires a non-empty list. -- -- Reference: mkSub :: MonadZ3 z3 => [AST] -> z3 AST mkSub = liftFun1 Base.mkSub -- | Same as 'mkSub' but type-safe. mkSub1 :: MonadZ3 z3 => NonEmpty AST -> z3 AST mkSub1 = liftFun1 Base.mkSub1 -- | Create an AST node representing -arg. -- -- Reference: mkUnaryMinus :: MonadZ3 z3 => AST -> z3 AST mkUnaryMinus = liftFun1 Base.mkUnaryMinus -- | Create an AST node representing arg1 div arg2. -- -- Reference: mkDiv :: MonadZ3 z3 => AST -> AST -> z3 AST mkDiv = liftFun2 Base.mkDiv -- | Create an AST node representing arg1 mod arg2. -- -- Reference: mkMod :: MonadZ3 z3 => AST -> AST -> z3 AST mkMod = liftFun2 Base.mkMod -- | Create an AST node representing arg1 rem arg2. -- -- Reference: mkRem :: MonadZ3 z3 => AST -> AST -> z3 AST mkRem = liftFun2 Base.mkRem -- | Create less than. -- -- Reference: mkLt :: MonadZ3 z3 => AST -> AST -> z3 AST mkLt = liftFun2 Base.mkLt -- | Create less than or equal to. -- -- Reference: mkLe :: MonadZ3 z3 => AST -> AST -> z3 AST mkLe = liftFun2 Base.mkLe -- | Create greater than. -- -- Reference: mkGt :: MonadZ3 z3 => AST -> AST -> z3 AST mkGt = liftFun2 Base.mkGt -- | Create greater than or equal to. -- -- Reference: mkGe :: MonadZ3 z3 => AST -> AST -> z3 AST mkGe = liftFun2 Base.mkGe -- | Coerce an integer to a real. -- -- Reference: mkInt2Real :: MonadZ3 z3 => AST -> z3 AST mkInt2Real = liftFun1 Base.mkInt2Real -- | Coerce a real to an integer. -- -- Reference: mkReal2Int :: MonadZ3 z3 => AST -> z3 AST mkReal2Int = liftFun1 Base.mkReal2Int -- | Check if a real number is an integer. -- -- Reference: mkIsInt :: MonadZ3 z3 => AST -> z3 AST mkIsInt = liftFun1 Base.mkIsInt --------------------------------------------------------------------- -- Bit-vectors -- | Bitwise negation. -- -- Reference: mkBvnot :: MonadZ3 z3 => AST -> z3 AST mkBvnot = liftFun1 Base.mkBvnot -- | Take conjunction of bits in vector, return vector of length 1. -- -- Reference: mkBvredand :: MonadZ3 z3 => AST -> z3 AST mkBvredand = liftFun1 Base.mkBvredand -- | Take disjunction of bits in vector, return vector of length 1. -- -- Reference: mkBvredor :: MonadZ3 z3 => AST -> z3 AST mkBvredor = liftFun1 Base.mkBvredor -- | Bitwise and. -- -- Reference: mkBvand :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvand = liftFun2 Base.mkBvand -- | Bitwise or. -- -- Reference: mkBvor :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvor = liftFun2 Base.mkBvor -- | Bitwise exclusive-or. -- -- Reference: mkBvxor :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvxor = liftFun2 Base.mkBvxor -- | Bitwise nand. -- -- Reference: mkBvnand :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvnand = liftFun2 Base.mkBvnand -- | Bitwise nor. -- -- Reference: mkBvnor :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvnor = liftFun2 Base.mkBvnor -- | Bitwise xnor. -- -- Reference: mkBvxnor :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvxnor = liftFun2 Base.mkBvxnor -- | Standard two's complement unary minus. -- -- Reference: AST -> z3 AST mkBvneg = liftFun1 Base.mkBvneg -- | Standard two's complement addition. -- -- Reference: mkBvadd :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvadd = liftFun2 Base.mkBvadd -- | Standard two's complement subtraction. -- -- Reference: mkBvsub :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvsub = liftFun2 Base.mkBvsub -- | Standard two's complement multiplication. -- -- Reference: mkBvmul :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvmul = liftFun2 Base.mkBvmul -- | Unsigned division. -- -- Reference: mkBvudiv :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvudiv = liftFun2 Base.mkBvudiv -- | Two's complement signed division. -- -- Reference: mkBvsdiv :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvsdiv = liftFun2 Base.mkBvsdiv -- | Unsigned remainder. -- -- Reference: mkBvurem :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvurem = liftFun2 Base.mkBvurem -- | Two's complement signed remainder (sign follows dividend). -- -- Reference: mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvsrem = liftFun2 Base.mkBvsrem -- | Two's complement signed remainder (sign follows divisor). -- -- Reference: mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvsmod = liftFun2 Base.mkBvsmod -- | Unsigned less than. -- -- Reference: mkBvult :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvult = liftFun2 Base.mkBvult -- | Two's complement signed less than. -- -- Reference: mkBvslt :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvslt = liftFun2 Base.mkBvslt -- | Unsigned less than or equal to. -- -- Reference: mkBvule :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvule = liftFun2 Base.mkBvule -- | Two's complement signed less than or equal to. -- -- Reference: mkBvsle :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvsle = liftFun2 Base.mkBvsle -- | Unsigned greater than or equal to. -- -- Reference: mkBvuge :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvuge = liftFun2 Base.mkBvuge -- | Two's complement signed greater than or equal to. -- -- Reference: mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvsge = liftFun2 Base.mkBvsge -- | Unsigned greater than. -- -- Reference: mkBvugt :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvugt = liftFun2 Base.mkBvugt -- | Two's complement signed greater than. -- -- Reference: mkBvsgt :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvsgt = liftFun2 Base.mkBvsgt -- | Concatenate the given bit-vectors. -- -- Reference: mkConcat :: MonadZ3 z3 => AST -> AST -> z3 AST mkConcat = liftFun2 Base.mkConcat -- | Extract the bits high down to low from a bitvector of size m to yield a new -- bitvector of size /n/, where /n = high - low + 1/. -- -- Reference: mkExtract :: MonadZ3 z3 => Int -> Int -> AST -> z3 AST mkExtract = liftFun3 Base.mkExtract -- | Sign-extend of the given bit-vector to the (signed) equivalent bitvector -- of size /m+i/, where /m/ is the size of the given bit-vector. -- -- Reference: mkSignExt :: MonadZ3 z3 => Int -> AST -> z3 AST mkSignExt = liftFun2 Base.mkSignExt -- | Extend the given bit-vector with zeros to the (unsigned) equivalent -- bitvector of size /m+i/, where /m/ is the size of the given bit-vector. -- -- Reference: mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 AST mkZeroExt = liftFun2 Base.mkZeroExt -- | Repeat the given bit-vector up length /i/. -- -- Reference: mkRepeat :: MonadZ3 z3 => Int -> AST -> z3 AST mkRepeat = liftFun2 Base.mkRepeat -- | Shift left. -- -- Reference: mkBvshl :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvshl = liftFun2 Base.mkBvshl -- | Logical shift right. -- -- Reference: mkBvlshr :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvlshr = liftFun2 Base.mkBvlshr -- | Arithmetic shift right. -- -- Reference: mkBvashr :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvashr = liftFun2 Base.mkBvashr -- | Rotate bits of /t1/ to the left /i/ times. -- -- Reference: mkRotateLeft :: MonadZ3 z3 => Int -> AST -> z3 AST mkRotateLeft = liftFun2 Base.mkRotateLeft -- | Rotate bits of /t1/ to the right /i/ times. -- -- Reference: mkRotateRight :: MonadZ3 z3 => Int -> AST -> z3 AST mkRotateRight = liftFun2 Base.mkRotateRight -- | Rotate bits of /t1/ to the left /t2/ times. -- -- Reference: mkExtRotateLeft :: MonadZ3 z3 => AST -> AST -> z3 AST mkExtRotateLeft = liftFun2 Base.mkExtRotateLeft -- | Rotate bits of /t1/ to the right /t2/ times. -- -- Reference: mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST mkExtRotateRight = liftFun2 Base.mkExtRotateRight -- | Create an /n/ bit bit-vector from the integer argument /t1/. -- -- Reference: mkInt2bv :: MonadZ3 z3 => Int -> AST -> z3 AST mkInt2bv = liftFun2 Base.mkInt2bv -- | Create an integer from the bit-vector argument /t1/. If /is_signed/ is false, -- then the bit-vector /t1/ is treated as unsigned. So the result is non-negative -- and in the range [0..2^/N/-1], where /N/ are the number of bits in /t1/. -- If /is_signed/ is true, /t1/ is treated as a signed bit-vector. -- -- Reference: mkBv2int :: MonadZ3 z3 => AST -> Bool -> z3 AST mkBv2int = liftFun2 Base.mkBv2int -- | Create a predicate that checks that the bit-wise addition of /t1/ and /t2/ -- does not overflow. -- -- Reference: mkBvaddNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST mkBvaddNoOverflow = liftFun3 Base.mkBvaddNoOverflow -- | Create a predicate that checks that the bit-wise signed addition of /t1/ -- and /t2/ does not underflow. -- -- Reference: mkBvaddNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvaddNoUnderflow = liftFun2 Base.mkBvaddNoUnderflow -- | Create a predicate that checks that the bit-wise signed subtraction of /t1/ -- and /t2/ does not overflow. -- -- Reference: mkBvsubNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvsubNoOverflow = liftFun2 Base.mkBvsubNoOverflow -- | Create a predicate that checks that the bit-wise subtraction of /t1/ and -- /t2/ does not underflow. -- -- Reference: mkBvsubNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvsubNoUnderflow = liftFun2 Base.mkBvsubNoUnderflow -- | Create a predicate that checks that the bit-wise signed division of /t1/ -- and /t2/ does not overflow. -- -- Reference: mkBvsdivNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvsdivNoOverflow = liftFun2 Base.mkBvsdivNoOverflow -- | Check that bit-wise negation does not overflow when /t1/ is interpreted as -- a signed bit-vector. -- -- Reference: mkBvnegNoOverflow :: MonadZ3 z3 => AST -> z3 AST mkBvnegNoOverflow = liftFun1 Base.mkBvnegNoOverflow -- | Create a predicate that checks that the bit-wise multiplication of /t1/ and -- /t2/ does not overflow. -- -- Reference: mkBvmulNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST mkBvmulNoOverflow = liftFun3 Base.mkBvmulNoOverflow -- | Create a predicate that checks that the bit-wise signed multiplication of -- /t1/ and /t2/ does not underflow. -- -- Reference: mkBvmulNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST mkBvmulNoUnderflow = liftFun2 Base.mkBvmulNoUnderflow --------------------------------------------------------------------- -- Arrays -- | Array read. The argument a is the array and i is the index of the array -- that gets read. -- -- Reference: mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST mkSelect = liftFun2 Base.mkSelect -- | Array update. -- -- Reference: mkStore :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST mkStore = liftFun3 Base.mkStore -- | Create the constant array. -- -- Reference: mkConstArray :: MonadZ3 z3 => Sort -> AST -> z3 AST mkConstArray = liftFun2 Base.mkConstArray -- | map f on the the argument arrays. -- -- Reference: mkMap :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST mkMap = liftFun2 Base.mkMap -- | Access the array default value. Produces the default range value, for -- arrays that can be represented as finite maps with a default range value. -- -- Reference: mkArrayDefault :: MonadZ3 z3 => AST -> z3 AST mkArrayDefault = liftFun1 Base.mkArrayDefault --------------------------------------------------------------------- -- Sets -- | Create the empty set. -- -- Reference: mkEmptySet :: MonadZ3 z3 => Sort -> z3 AST mkEmptySet = liftFun1 Base.mkEmptySet -- | Create the full set. -- -- Reference: mkFullSet :: MonadZ3 z3 => Sort -> z3 AST mkFullSet = liftFun1 Base.mkFullSet -- | Add an element to a set. -- -- Reference: mkSetAdd :: MonadZ3 z3 => AST -> AST -> z3 AST mkSetAdd = liftFun2 Base.mkSetAdd -- | Remove an element from a set. -- -- Reference: mkSetDel :: MonadZ3 z3 => AST -> AST -> z3 AST mkSetDel = liftFun2 Base.mkSetDel -- | Take the union of a list of sets. -- -- Reference: mkSetUnion :: MonadZ3 z3 => [AST] -> z3 AST mkSetUnion = liftFun1 Base.mkSetUnion -- | Take the intersection of a list of sets. -- -- Reference: mkSetIntersect :: MonadZ3 z3 => [AST] -> z3 AST mkSetIntersect = liftFun1 Base.mkSetIntersect -- | Take the set difference between two sets. -- -- Reference: mkSetDifference :: MonadZ3 z3 => AST -> AST -> z3 AST mkSetDifference = liftFun2 Base.mkSetDifference -- | Take the complement of a set. -- -- Reference: mkSetComplement :: MonadZ3 z3 => AST -> z3 AST mkSetComplement = liftFun1 Base.mkSetComplement -- | Check for set membership. -- -- Reference: mkSetMember :: MonadZ3 z3 => AST -> AST -> z3 AST mkSetMember = liftFun2 Base.mkSetMember -- | Check if the first set is a subset of the second set. -- -- Reference: mkSetSubset :: MonadZ3 z3 => AST -> AST -> z3 AST mkSetSubset = liftFun2 Base.mkSetSubset --------------------------------------------------------------------- -- * Numerals -- | Create a numeral of a given sort. -- -- Reference: mkNumeral :: MonadZ3 z3 => String -> Sort -> z3 AST mkNumeral = liftFun2 Base.mkNumeral -- | Create a numeral of sort /real/. mkReal :: MonadZ3 z3 => Int -> Int -> z3 AST mkReal = liftFun2 Base.mkReal -- | Create a numeral of an int, bit-vector, or finite-domain sort. -- -- This function can be use to create numerals that fit in a -- /machine integer/. -- It is slightly faster than 'mkNumeral' since it is not necessary -- to parse a string. mkInt :: MonadZ3 z3 => Int -> Sort -> z3 AST mkInt = liftFun2 Base.mkInt -- | Create a numeral of an int, bit-vector, or finite-domain sort. -- -- This function can be use to create numerals that fit in a -- /machine unsigned integer/. -- It is slightly faster than 'mkNumeral' since it is not necessary -- to parse a string. mkUnsignedInt :: MonadZ3 z3 => Word -> Sort -> z3 AST mkUnsignedInt = liftFun2 Base.mkUnsignedInt -- | Create a numeral of an int, bit-vector, or finite-domain sort. -- -- This function can be use to create numerals that fit in a -- /machine 64-bit integer/. -- It is slightly faster than 'mkNumeral' since it is not necessary -- to parse a string. mkInt64 :: MonadZ3 z3 => Int64 -> Sort -> z3 AST mkInt64 = liftFun2 Base.mkInt64 -- | Create a numeral of an int, bit-vector, or finite-domain sort. -- -- This function can be use to create numerals that fit in a -- /machine unsigned 64-bit integer/. -- It is slightly faster than 'mkNumeral' since it is not necessary -- to parse a string. mkUnsignedInt64 :: MonadZ3 z3 => Word64 -> Sort -> z3 AST mkUnsignedInt64 = liftFun2 Base.mkUnsignedInt64 ------------------------------------------------- -- ** Helpers -- | Create a numeral of an int, bit-vector, or finite-domain sort. mkIntegral :: (MonadZ3 z3, Integral a) => a -> Sort -> z3 AST mkIntegral = liftFun2 Base.mkIntegral -- | Create a numeral of sort /real/ from a 'Rational'. mkRational :: MonadZ3 z3 => Rational -> z3 AST mkRational = liftFun1 Base.mkRational -- | Create a numeral of sort /real/ from a 'Fixed'. mkFixed :: (MonadZ3 z3, HasResolution a) => Fixed a -> z3 AST mkFixed = liftFun1 Base.mkFixed -- | Create a numeral of sort /real/ from a 'Real'. mkRealNum :: (MonadZ3 z3, Real r) => r -> z3 AST mkRealNum = liftFun1 Base.mkRealNum -- | Create a numeral of sort /int/ from an 'Integer'. mkInteger :: MonadZ3 z3 => Integer -> z3 AST mkInteger = liftFun1 Base.mkInteger -- | Create a numeral of sort /int/ from an 'Integral'. mkIntNum :: (MonadZ3 z3, Integral a) => a -> z3 AST mkIntNum = liftFun1 Base.mkIntNum -- | Create a numeral of sort /Bit-vector/ from an 'Integer'. mkBitvector :: MonadZ3 z3 => Int -- ^ bit-width -> Integer -- ^ integer value -> z3 AST mkBitvector = liftFun2 Base.mkBitvector -- | Create a numeral of sort /Bit-vector/ from an 'Integral'. mkBvNum :: (MonadZ3 z3, Integral i) => Int -- ^ bit-width -> i -- ^ integer value -> z3 AST mkBvNum = liftFun2 Base.mkBvNum --------------------------------------------------------------------- -- Sequences and regular expressions -- | Create a sequence sort out of the sort for the elements. mkSeqSort :: MonadZ3 z3 => Sort -> z3 Sort mkSeqSort = liftFun1 Base.mkSeqSort -- | Check if s is a sequence sort. isSeqSort :: MonadZ3 z3 => Sort -> z3 Bool isSeqSort = liftFun1 Base.isSeqSort -- | Create a regular expression sort out of a sequence sort. mkReSort :: MonadZ3 z3 => Sort -> z3 Sort mkReSort = liftFun1 Base.mkReSort -- | Check if s is a regular expression sort. isReSort :: MonadZ3 z3 => Sort -> z3 Bool isReSort = liftFun1 Base.isReSort -- | Create a sort for 8 bit strings. This function creates a sort for ASCII -- strings. Each character is 8 bits. mkStringSort :: MonadZ3 z3 => z3 Sort mkStringSort = liftScalar Base.mkStringSort -- | Check if s is a string sort. isStringSort :: MonadZ3 z3 => Sort -> z3 Bool isStringSort = liftFun1 Base.isStringSort -- | Create a string constant out of the string that is passed in. mkString :: MonadZ3 z3 => String -> z3 AST mkString = liftFun1 Base.mkString -- | Determine if s is a string constant. isString :: MonadZ3 z3 => AST -> z3 Bool isString = liftFun1 Base.isString -- | Retrieve the string constant stored in s. getString :: MonadZ3 z3 => AST -> z3 String getString = liftFun1 Base.getString -- | Create an empty sequence of the sequence sort seq. mkSeqEmpty :: MonadZ3 z3 => Sort -> z3 AST mkSeqEmpty = liftFun1 Base.mkSeqEmpty -- | Create a unit sequence of a. mkSeqUnit :: MonadZ3 z3 => AST -> z3 AST mkSeqUnit = liftFun1 Base.mkSeqUnit -- | Concatenate sequences. mkSeqConcat :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST mkSeqConcat = liftFun2 Base.mkSeqConcat -- | Check if prefix is a prefix of s. mkSeqPrefix :: MonadZ3 z3 => AST -- ^ prefix -> AST -- ^ s -> z3 AST mkSeqPrefix = liftFun2 Base.mkSeqPrefix -- | Check if suffix is a suffix of s. mkSeqSuffix :: MonadZ3 z3 => AST -- ^ suffix -> AST -- ^ s -> z3 AST mkSeqSuffix = liftFun2 Base.mkSeqSuffix -- | Check if container contains containee. mkSeqContains :: MonadZ3 z3 => AST -- ^ container -> AST -- ^ containee -> z3 AST mkSeqContains = liftFun2 Base.mkSeqContains -- | Extract subsequence starting at offset of length. mkSeqExtract :: MonadZ3 z3 => AST -- ^ s -> AST -- ^ offset -> AST -- ^ length -> z3 AST mkSeqExtract = liftFun3 Base.mkSeqExtract -- | Replace the first occurrence of src with dst in s. mkSeqReplace :: MonadZ3 z3 => AST -- ^ s -> AST -- ^ src -> AST -- ^ dst -> z3 AST mkSeqReplace = liftFun3 Base.mkSeqReplace -- | Retrieve from s the unit sequence positioned at position index. mkSeqAt :: MonadZ3 z3 => AST -- ^ s -> AST -- ^ index -> z3 AST mkSeqAt = liftFun2 Base.mkSeqAt -- | Return the length of the sequence s. mkSeqLength :: MonadZ3 z3 => AST -> z3 AST mkSeqLength = liftFun1 Base.mkSeqLength -- | Return index of first occurrence of substr in s starting from offset -- offset. If s does not contain substr, then the value is -1, if offset is the -- length of s, then the value is -1 as well. The function is under-specified if -- offset is negative or larger than the length of s. mkSeqIndex :: MonadZ3 z3 => AST -- ^ s -> AST -- ^ substr -> AST -- ^ offset -> z3 AST mkSeqIndex = liftFun3 Base.mkSeqIndex -- | Convert string to integer. mkStrToInt :: MonadZ3 z3 => AST -> z3 AST mkStrToInt = liftFun1 Base.mkStrToInt -- | Integer to string conversion. mkIntToStr :: MonadZ3 z3 => AST -> z3 AST mkIntToStr = liftFun1 Base.mkIntToStr -- | Create a regular expression that accepts the sequence. mkSeqToRe :: MonadZ3 z3 => AST -> z3 AST mkSeqToRe = liftFun1 Base.mkSeqToRe -- | Check if seq is in the language generated by the regular expression re. mkSeqInRe :: MonadZ3 z3 => AST -- ^ seq -> AST -- ^ re -> z3 AST mkSeqInRe = liftFun2 Base.mkSeqInRe -- | Create the regular language re+. mkRePlus :: MonadZ3 z3 => AST -> z3 AST mkRePlus = liftFun1 Base.mkRePlus -- | Create the regular language re*. mkReStar :: MonadZ3 z3 => AST -> z3 AST mkReStar = liftFun1 Base.mkReStar -- | Create the regular language [re]. mkReOption :: MonadZ3 z3 => AST -> z3 AST mkReOption = liftFun1 Base.mkReOption -- | Create the union of the regular languages. mkReUnion :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST mkReUnion = liftFun2 Base.mkReUnion -- | Create the concatenation of the regular languages. mkReConcat :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST mkReConcat = liftFun2 Base.mkReConcat -- | Create the range regular expression over two sequences of length 1. mkReRange :: MonadZ3 z3 => AST -- ^ lo -> AST -- ^ hi -> z3 AST mkReRange = liftFun2 Base.mkReRange -- | Create a regular expression loop. The supplied regular expression r is -- repeated between lo and hi times. The lo should be below hi with one -- exception: when supplying the value hi as 0, the meaning is to repeat the -- argument r at least lo number of times, and with an unbounded upper bound. mkReLoop :: (Integral int, MonadZ3 z3) => AST -- ^ r -> int -- ^ lo -> int -- ^ hi -> z3 AST mkReLoop = liftFun3 Base.mkReLoop -- | Create the intersection of the regular languages. mkReIntersect :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST mkReIntersect = liftFun2 Base.mkReIntersect -- | Create the complement of the regular language. mkReComplement :: MonadZ3 z3 => AST -> z3 AST mkReComplement = liftFun1 Base.mkReComplement -- | Create an empty regular expression of sort re. mkReEmpty :: MonadZ3 z3 => Sort -> z3 AST mkReEmpty = liftFun1 Base.mkReEmpty -- | Create an universal regular expression of sort re. mkReFull :: MonadZ3 z3 => Sort -> z3 AST mkReFull = liftFun1 Base.mkReFull --------------------------------------------------------------------- -- Quantifiers mkPattern :: MonadZ3 z3 => [AST] -> z3 Pattern mkPattern = liftFun1 Base.mkPattern mkBound :: MonadZ3 z3 => Int -> Sort -> z3 AST mkBound = liftFun2 Base.mkBound mkForall :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST mkForall = liftFun4 Base.mkForall mkForallConst :: MonadZ3 z3 => [Pattern] -> [App] -> AST -> z3 AST mkForallConst = liftFun3 Base.mkForallConst mkExistsConst :: MonadZ3 z3 => [Pattern] -> [App] -> AST -> z3 AST mkExistsConst = liftFun3 Base.mkExistsConst mkExists :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST mkExists = liftFun4 Base.mkExists --------------------------------------------------------------------- -- Accessors -- | Return the symbol name. -- -- Reference: getSymbolString :: MonadZ3 z3 => Symbol -> z3 String getSymbolString = liftFun1 Base.getSymbolString -- | Return the sort kind. -- -- Reference: getSortKind :: MonadZ3 z3 => Sort -> z3 SortKind getSortKind = liftFun1 Base.getSortKind -- | Return the size of the given bit-vector sort. -- -- Reference: getBvSortSize :: MonadZ3 z3 => Sort -> z3 Int getBvSortSize = liftFun1 Base.getBvSortSize -- | Get list of constructors for datatype. getDatatypeSortConstructors :: MonadZ3 z3 => Sort -- ^ Datatype sort. -> z3 [FuncDecl] -- ^ Constructor declarations. getDatatypeSortConstructors = liftFun1 Base.getDatatypeSortConstructors -- | Get list of recognizers for datatype. getDatatypeSortRecognizers :: MonadZ3 z3 => Sort -- ^ Datatype sort. -> z3 [FuncDecl] -- ^ Constructor recognizers. getDatatypeSortRecognizers = liftFun1 Base.getDatatypeSortRecognizers -- | Get list of accessors for datatype. getDatatypeSortConstructorAccessors :: MonadZ3 z3 => Sort -- ^ Datatype sort. -> z3 [[FuncDecl]] -- ^ Constructor recognizers. getDatatypeSortConstructorAccessors = liftFun1 Base.getDatatypeSortConstructorAccessors -- | Return the constant declaration name as a symbol. -- -- Reference: getDeclName :: MonadZ3 z3 => FuncDecl -> z3 Symbol getDeclName = liftFun1 Base.getDeclName -- | Returns the number of parameters of the given declaration getArity :: MonadZ3 z3 => FuncDecl -> z3 Int getArity = liftFun1 Base.getArity -- | Returns the sort of the i-th parameter of the given function declaration getDomain :: MonadZ3 z3 => FuncDecl -- ^ A function declaration -> Int -- ^ i -> z3 Sort getDomain = liftFun2 Base.getDomain -- | Returns the range of the given declaration. getRange :: MonadZ3 z3 => FuncDecl -> z3 Sort getRange = liftFun1 Base.getRange -- | Convert an app into AST. This is just type casting. appToAst :: MonadZ3 z3 => App -> z3 AST appToAst = liftFun1 Base.appToAst -- | Return the declaration of a constant or function application. getAppDecl :: MonadZ3 z3 => App -> z3 FuncDecl getAppDecl = liftFun1 Base.getAppDecl -- | Return the number of argument of an application. If t is an constant, then the number of arguments is 0. getAppNumArgs :: MonadZ3 z3 => App -> z3 Int getAppNumArgs = liftFun1 Base.getAppNumArgs -- | Return the i-th argument of the given application. getAppArg :: MonadZ3 z3 => App -> Int -> z3 AST getAppArg = liftFun2 Base.getAppArg -- | Return a list of all the arguments of the given application. getAppArgs :: MonadZ3 z3 => App -> z3 [AST] getAppArgs = liftFun1 Base.getAppArgs -- | Return the sort of an AST node. getSort :: MonadZ3 z3 => AST -> z3 Sort getSort = liftFun1 Base.getSort getArraySortDomain :: MonadZ3 z3 => Sort -> z3 Sort getArraySortDomain = liftFun1 Base.getArraySortDomain getArraySortRange :: MonadZ3 z3 => Sort -> z3 Sort getArraySortRange = liftFun1 Base.getArraySortRange -- | Returns @Just True@, @Just False@, or @Nothing@ for /undefined/. -- -- Reference: getBoolValue :: MonadZ3 z3 => AST -> z3 (Maybe Bool) getBoolValue = liftFun1 Base.getBoolValue -- | Return the kind of the given AST. -- -- Reference: getAstKind :: MonadZ3 z3 => AST -> z3 ASTKind getAstKind = liftFun1 Base.getAstKind -- | Return True if an ast is APP_AST, False otherwise. isApp :: MonadZ3 z3 => AST -> z3 Bool isApp = liftFun1 Base.isApp -- | Cast AST into an App. toApp :: MonadZ3 z3 => AST -> z3 App toApp = liftFun1 Base.toApp -- | Return numeral value, as a string of a numeric constant term. getNumeralString :: MonadZ3 z3 => AST -> z3 String getNumeralString = liftFun1 Base.getNumeralString getIndexValue :: MonadZ3 z3 => AST -> z3 Int getIndexValue = liftFun1 Base.getIndexValue isQuantifierForall :: MonadZ3 z3 => AST -> z3 Bool isQuantifierForall = liftFun1 Base.isQuantifierForall isQuantifierExists :: MonadZ3 z3 => AST -> z3 Bool isQuantifierExists = liftFun1 Base.isQuantifierExists getQuantifierWeight :: MonadZ3 z3 => AST -> z3 Int getQuantifierWeight = liftFun1 Base.getQuantifierWeight getQuantifierNumPatterns :: MonadZ3 z3 => AST -> z3 Int getQuantifierNumPatterns = liftFun1 Base.getQuantifierNumPatterns getQuantifierPatternAST :: MonadZ3 z3 => AST -> Int -> z3 AST getQuantifierPatternAST = liftFun2 Base.getQuantifierPatternAST getQuantifierPatterns :: MonadZ3 z3 => AST -> z3 [AST] getQuantifierPatterns = liftFun1 Base.getQuantifierPatterns getQuantifierNumNoPatterns :: MonadZ3 z3 => AST -> z3 Int getQuantifierNumNoPatterns = liftFun1 Base.getQuantifierNumNoPatterns getQuantifierNoPatternAST :: MonadZ3 z3 => AST -> Int -> z3 AST getQuantifierNoPatternAST = liftFun2 Base.getQuantifierNoPatternAST getQuantifierNoPatterns :: MonadZ3 z3 => AST -> z3 [AST] getQuantifierNoPatterns = liftFun1 Base.getQuantifierNoPatterns getQuantifierNumBound :: MonadZ3 z3 => AST -> z3 Int getQuantifierNumBound = liftFun1 Base.getQuantifierNumBound getQuantifierBoundName :: MonadZ3 z3 => AST -> Int -> z3 Symbol getQuantifierBoundName = liftFun2 Base.getQuantifierBoundName getQuantifierBoundSort :: MonadZ3 z3 => AST -> Int -> z3 Sort getQuantifierBoundSort = liftFun2 Base.getQuantifierBoundSort getQuantifierBoundVars :: MonadZ3 z3 => AST -> z3 [AST] getQuantifierBoundVars = liftFun1 Base.getQuantifierBoundVars getQuantifierBody :: MonadZ3 z3 => AST -> z3 AST getQuantifierBody = liftFun1 Base.getQuantifierBody -- | Simplify the expression. -- -- Reference: simplify :: MonadZ3 z3 => AST -> z3 AST simplify = liftFun1 Base.simplify -- | Simplify the expression using the given parameters. -- -- Reference: simplifyEx :: MonadZ3 z3 => AST -> Params -> z3 AST simplifyEx = liftFun2 Base.simplifyEx ------------------------------------------------- -- ** Helpers -- | Read a 'Bool' value from an 'AST' getBool :: MonadZ3 z3 => AST -> z3 Bool getBool = liftFun1 Base.getBool -- | Return the integer value getInt :: MonadZ3 z3 => AST -> z3 Integer getInt = liftFun1 Base.getInt -- | Return rational value getReal :: MonadZ3 z3 => AST -> z3 Rational getReal = liftFun1 Base.getReal -- | Read the 'Integer' value from an 'AST' of sort /bit-vector/. -- -- See 'mkBv2int'. getBv :: MonadZ3 z3 => AST -> Bool -- ^ signed? -> z3 Integer getBv = liftFun2 Base.getBv --------------------------------------------------------------------- -- Modifiers substituteVars :: MonadZ3 z3 => AST -> [AST] -> z3 AST substituteVars = liftFun2 Base.substituteVars substitute :: MonadZ3 z3 => AST -> [(AST, AST)] -> z3 AST substitute = liftFun2 Base.substitute --------------------------------------------------------------------- -- Models -- | Evaluate an AST node in the given model. -- -- The evaluation may fail for the following reasons: -- -- * /t/ contains a quantifier. -- * the model /m/ is partial. -- * /t/ is type incorrect. modelEval :: MonadZ3 z3 => Model -> AST -> Bool -- ^ Model completion? -> z3 (Maybe AST) modelEval = liftFun3 Base.modelEval -- | Get array as a list of argument/value pairs, if it is -- represented as a function (ie, using as-array). evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel) evalArray = liftFun2 Base.evalArray getConstInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe AST) getConstInterp = liftFun2 Base.getConstInterp -- | Return the interpretation of the function f in the model m. -- Return NULL, if the model does not assign an interpretation for f. -- That should be interpreted as: the f does not matter. -- -- Reference: getFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncInterp) getFuncInterp = liftFun2 Base.getFuncInterp hasInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 Bool hasInterp = liftFun2 Base.hasInterp numConsts :: MonadZ3 z3 => Model -> z3 Word numConsts = liftFun1 Base.numConsts numFuncs :: MonadZ3 z3 => Model -> z3 Word numFuncs = liftFun1 Base.numFuncs getConstDecl :: MonadZ3 z3 => Model -> Word -> z3 FuncDecl getConstDecl = liftFun2 Base.getConstDecl getFuncDecl :: MonadZ3 z3 => Model -> Word -> z3 FuncDecl getFuncDecl = liftFun2 Base.getFuncDecl getConsts :: MonadZ3 z3 => Model -> z3 [FuncDecl] getConsts = liftFun1 Base.getConsts getFuncs :: MonadZ3 z3 => Model -> z3 [FuncDecl] getFuncs = liftFun1 Base.getFuncs -- | The (_ as-array f) AST node is a construct for assigning interpretations -- for arrays in Z3. It is the array such that forall indices i we have that -- (select (_ as-array f) i) is equal to (f i). This procedure returns Z3_TRUE -- if the a is an as-array AST node. -- -- Reference: isAsArray :: MonadZ3 z3 => AST -> z3 Bool isAsArray = liftFun1 Base.isAsArray isEqAST :: MonadZ3 z3 => AST -> AST -> z3 Bool isEqAST = liftFun2 Base.isEqAST addFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 FuncInterp addFuncInterp = liftFun3 Base.addFuncInterp addConstInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 () addConstInterp = liftFun3 Base.addConstInterp -- | Return the function declaration f associated with a (_ as_array f) node. -- -- Reference: getAsArrayFuncDecl :: MonadZ3 z3 => AST -> z3 FuncDecl getAsArrayFuncDecl = liftFun1 Base.getAsArrayFuncDecl -- | Return the number of entries in the given function interpretation. -- -- Reference: funcInterpGetNumEntries :: MonadZ3 z3 => FuncInterp -> z3 Int funcInterpGetNumEntries = liftFun1 Base.funcInterpGetNumEntries -- | Return a "point" of the given function intepretation. -- It represents the value of f in a particular point. -- -- Reference: funcInterpGetEntry :: MonadZ3 z3 => FuncInterp -> Int -> z3 FuncEntry funcInterpGetEntry = liftFun2 Base.funcInterpGetEntry -- | Return the 'else' value of the given function interpretation. -- -- Reference: funcInterpGetElse :: MonadZ3 z3 => FuncInterp -> z3 AST funcInterpGetElse = liftFun1 Base.funcInterpGetElse -- | Return the arity (number of arguments) of the given function -- interpretation. -- -- Reference: funcInterpGetArity :: MonadZ3 z3 => FuncInterp -> z3 Int funcInterpGetArity = liftFun1 Base.funcInterpGetArity -- | Return the value of this point. -- -- Reference: funcEntryGetValue :: MonadZ3 z3 => FuncEntry -> z3 AST funcEntryGetValue = liftFun1 Base.funcEntryGetValue -- | Return the number of arguments in a Z3_func_entry object. -- -- Reference: funcEntryGetNumArgs :: MonadZ3 z3 => FuncEntry -> z3 Int funcEntryGetNumArgs = liftFun1 Base.funcEntryGetNumArgs -- | Return an argument of a Z3_func_entry object. -- -- Reference: funcEntryGetArg :: MonadZ3 z3 => FuncEntry -> Int -> z3 AST funcEntryGetArg = liftFun2 Base.funcEntryGetArg -- | Convert the given model into a string. modelToString :: MonadZ3 z3 => Model -> z3 String modelToString = liftFun1 Base.modelToString -- | Alias for 'modelToString'. showModel :: MonadZ3 z3 => Model -> z3 String showModel = modelToString ------------------------------------------------- -- ** Helpers -- | Type of an evaluation function for 'AST'. -- -- Evaluation may fail (i.e. return 'Nothing') for a few -- reasons, see 'modelEval'. type EvalAst m a = Model -> AST -> m (Maybe a) -- | An alias for 'modelEval' with model completion enabled. eval :: MonadZ3 z3 => EvalAst z3 AST eval = liftFun2 Base.eval -- | Evaluate an AST node of sort /bool/ in the given model. -- -- See 'modelEval' and 'getBool'. evalBool :: MonadZ3 z3 => EvalAst z3 Bool evalBool = liftFun2 Base.evalBool -- | Evaluate an AST node of sort /int/ in the given model. -- -- See 'modelEval' and 'getInt'. evalInt :: MonadZ3 z3 => EvalAst z3 Integer evalInt = liftFun2 Base.evalInt -- | Evaluate an AST node of sort /real/ in the given model. -- -- See 'modelEval' and 'getReal'. evalReal :: MonadZ3 z3 => EvalAst z3 Rational evalReal = liftFun2 Base.evalReal -- | Evaluate an AST node of sort /bit-vector/ in the given model. -- -- The flag /signed/ decides whether the bit-vector value is -- interpreted as a signed or unsigned integer. -- -- See 'modelEval' and 'getBv'. evalBv :: MonadZ3 z3 => Bool -- ^ signed? -> EvalAst z3 Integer evalBv = liftFun3 Base.evalBv -- | Evaluate a collection of AST nodes in the given model. evalT :: (MonadZ3 z3,Traversable t) => Model -> t AST -> z3 (Maybe (t AST)) evalT = liftFun2 Base.evalT -- | Run a evaluation function on a 'Traversable' data structure of 'AST's -- (e.g. @[AST]@, @Vector AST@, @Maybe AST@, etc). -- -- This a generic version of 'evalT' which can be used in combination with -- other helpers. For instance, @mapEval evalInt@ can be used to obtain -- the 'Integer' interpretation of a list of 'AST' of sort /int/. mapEval :: (MonadZ3 z3, Traversable t) => EvalAst z3 a -> Model -> t AST -> z3 (Maybe (t a)) mapEval f m = fmap T.sequence . T.mapM (f m) -- | Get function as a list of argument/value pairs. evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel) evalFunc = liftFun2 Base.evalFunc --------------------------------------------------------------------- -- Tactics mkTactic :: MonadZ3 z3 => String -> z3 Tactic mkTactic = liftFun1 Base.mkTactic andThenTactic :: MonadZ3 z3 => Tactic -> Tactic -> z3 Tactic andThenTactic = liftFun2 Base.andThenTactic orElseTactic :: MonadZ3 z3 => Tactic -> Tactic -> z3 Tactic orElseTactic = liftFun2 Base.andThenTactic skipTactic :: MonadZ3 z3 => z3 Tactic skipTactic = liftScalar Base.skipTactic tryForTactic :: MonadZ3 z3 => Tactic -> Int -> z3 Tactic tryForTactic = liftFun2 Base.tryForTactic mkQuantifierEliminationTactic :: MonadZ3 z3 => z3 Tactic mkQuantifierEliminationTactic = liftScalar Base.mkQuantifierEliminationTactic mkAndInverterGraphTactic :: MonadZ3 z3 => z3 Tactic mkAndInverterGraphTactic = liftScalar Base.mkAndInverterGraphTactic applyTactic :: MonadZ3 z3 => Tactic -> Goal -> z3 ApplyResult applyTactic = liftFun2 Base.applyTactic getApplyResultNumSubgoals :: MonadZ3 z3 => ApplyResult -> z3 Int getApplyResultNumSubgoals = liftFun1 Base.getApplyResultNumSubgoals getApplyResultSubgoal :: MonadZ3 z3 => ApplyResult -> Int -> z3 Goal getApplyResultSubgoal = liftFun2 Base.getApplyResultSubgoal getApplyResultSubgoals :: MonadZ3 z3 => ApplyResult -> z3 [Goal] getApplyResultSubgoals = liftFun1 Base.getApplyResultSubgoals mkGoal :: MonadZ3 z3 => Bool -> Bool -> Bool -> z3 Goal mkGoal = liftFun3 Base.mkGoal goalAssert :: MonadZ3 z3 => Goal -> AST -> z3 () goalAssert = liftFun2 Base.goalAssert getGoalSize :: MonadZ3 z3 => Goal -> z3 Int getGoalSize = liftFun1 Base.getGoalSize getGoalFormula :: MonadZ3 z3 => Goal -> Int -> z3 AST getGoalFormula = liftFun2 Base.getGoalFormula getGoalFormulas :: MonadZ3 z3 => Goal -> z3 [AST] getGoalFormulas = liftFun1 Base.getGoalFormulas --------------------------------------------------------------------- -- String Conversion -- | Set the mode for converting expressions to strings. setASTPrintMode :: MonadZ3 z3 => ASTPrintMode -> z3 () setASTPrintMode = liftFun1 Base.setASTPrintMode -- | Convert an AST to a string. astToString :: MonadZ3 z3 => AST -> z3 String astToString = liftFun1 Base.astToString -- | Convert a pattern to a string. patternToString :: MonadZ3 z3 => Pattern -> z3 String patternToString = liftFun1 Base.patternToString -- | Convert a sort to a string. sortToString :: MonadZ3 z3 => Sort -> z3 String sortToString = liftFun1 Base.sortToString -- | Convert a FuncDecl to a string. funcDeclToString :: MonadZ3 z3 => FuncDecl -> z3 String funcDeclToString = liftFun1 Base.funcDeclToString -- | Convert the given benchmark into SMT-LIB formatted string. -- -- The output format can be configured via 'setASTPrintMode'. benchmarkToSMTLibString :: MonadZ3 z3 => String -- ^ name -> String -- ^ logic -> String -- ^ status -> String -- ^ attributes -> [AST] -- ^ assumptions1 -> AST -- ^ formula -> z3 String benchmarkToSMTLibString = liftFun6 Base.benchmarkToSMTLibString --------------------------------------------------------------------- -- Parser interface -- | Parse SMT expressions from a string -- -- The sort and declaration arguments allow parsing in a context in which variables and functions have already been declared. They are almost never used. parseSMTLib2String :: MonadZ3 z3 => String -- ^ string to parse -> [Symbol] -- ^ sort names -> [Sort] -- ^ sorts -> [Symbol] -- ^ declaration names -> [FuncDecl] -- ^ declarations -> z3 AST parseSMTLib2String = liftFun5 Base.parseSMTLib2String -- | Parse SMT expressions from a file -- -- The sort and declaration arguments allow parsing in a context in which variables and functions have already been declared. They are almost never used. parseSMTLib2File :: MonadZ3 z3 => String -- ^ string to parse -> [Symbol] -- ^ sort names -> [Sort] -- ^ sorts -> [Symbol] -- ^ declaration names -> [FuncDecl] -- ^ declarations -> z3 AST parseSMTLib2File = liftFun5 Base.parseSMTLib2File --------------------------------------------------------------------- -- Miscellaneous -- | Return Z3 version number information. getVersion :: MonadZ3 z3 => z3 Version getVersion = liftIO Base.getVersion --------------------------------------------------------------------- -- Fixedpoint class MonadZ3 m => MonadFixedpoint m where getFixedpoint :: m Base.Fixedpoint fixedpointAddRule :: MonadFixedpoint z3 => AST -> Symbol -> z3 () fixedpointAddRule = liftFixedpoint2 Base.fixedpointAddRule fixedpointSetParams :: MonadFixedpoint z3 => Params -> z3 () fixedpointSetParams = liftFixedpoint1 Base.fixedpointSetParams fixedpointRegisterRelation :: MonadFixedpoint z3 => FuncDecl -> z3 () fixedpointRegisterRelation = liftFixedpoint1 Base.fixedpointRegisterRelation fixedpointQueryRelations :: MonadFixedpoint z3 => [FuncDecl] -> z3 Result fixedpointQueryRelations = liftFixedpoint1 Base.fixedpointQueryRelations fixedpointGetAnswer :: MonadFixedpoint z3 => z3 AST fixedpointGetAnswer = liftFixedpoint0 Base.fixedpointGetAnswer fixedpointGetAssertions :: MonadFixedpoint z3 => z3 [AST] fixedpointGetAssertions = liftFixedpoint0 Base.fixedpointGetAssertions --------------------------------------------------------------------- -- Optimization class MonadZ3 m => MonadOptimize m where getOptimize :: m Base.Optimize optimizeAssert :: MonadOptimize z3 => AST -> z3 () optimizeAssert = liftOptimize1 Base.optimizeAssert optimizeAssertAndTrack :: MonadOptimize z3 => AST -> AST -> z3 () optimizeAssertAndTrack = liftOptimize2 Base.optimizeAssertAndTrack optimizeAssertSoft :: MonadOptimize z3 => AST -> String -> Symbol -> z3 () optimizeAssertSoft = undefined optimizeMaximize :: MonadOptimize z3 => AST -> z3 Int optimizeMaximize = liftOptimize1 Base.optimizeMaximize optimizeMinimize :: MonadOptimize z3 => AST -> z3 Int optimizeMinimize = liftOptimize1 Base.optimizeMinimize optimizePush :: MonadOptimize z3 => z3 () optimizePush = liftOptimize0 Base.optimizePush optimizePop :: MonadOptimize z3 => z3 () optimizePop = liftOptimize0 Base.optimizePop optimizeCheck :: MonadOptimize z3 => [AST] -> z3 Result optimizeCheck = liftOptimize1 Base.optimizeCheck optimizeGetReasonUnknown :: MonadOptimize z3 => z3 String optimizeGetReasonUnknown = liftOptimize0 Base.optimizeGetReasonUnknown optimizeGetModel :: MonadOptimize z3 => z3 Model optimizeGetModel = liftOptimize0 Base.optimizeGetModel optimizeGetUnsatCore :: MonadOptimize z3 => z3 [AST] optimizeGetUnsatCore = liftOptimize0 Base.optimizeGetUnsatCore optimizeSetParams :: MonadOptimize z3 => Params -> z3 () optimizeSetParams = liftOptimize1 Base.optimizeSetParams optimizeGetLower :: MonadOptimize z3 => Int -> z3 AST optimizeGetLower = liftOptimize1 Base.optimizeGetLower optimizeGetUpper :: MonadOptimize z3 => Int -> z3 AST optimizeGetUpper = liftOptimize1 Base.optimizeGetLower optimizeGetUpperAsVector :: MonadOptimize z3 => Int -> z3 [AST] optimizeGetUpperAsVector = liftOptimize1 Base.optimizeGetUpperAsVector optimizeGetLowerAsVector :: MonadOptimize z3 => Int -> z3 [AST] optimizeGetLowerAsVector = liftOptimize1 Base.optimizeGetLowerAsVector optimizeToString :: MonadOptimize z3 => z3 String optimizeToString = liftOptimize0 Base.optimizeToString optimizeFromString :: MonadOptimize z3 => String -> z3 () optimizeFromString = liftOptimize1 Base.optimizeFromString optimizeFromFile :: MonadOptimize z3 => String -> z3 () optimizeFromFile = liftOptimize1 Base.optimizeFromFile optimizeGetHelp :: MonadOptimize z3 => z3 String optimizeGetHelp = liftOptimize0 Base.optimizeGetHelp optimizeGetAssertions :: MonadOptimize z3 => z3 [AST] optimizeGetAssertions = liftOptimize0 Base.optimizeGetAssertions optimizeGetObjectives :: MonadOptimize z3 => z3 [AST] optimizeGetObjectives = liftOptimize0 Base.optimizeGetObjectives --------------------------------------------------------------------- -- * Solvers -- mkSolver :: Context -> IO Solver -- mkSolver = liftFun0 z3_mk_solver -- mkSimpleSolver :: Context -> IO Solver -- mkSimpleSolver = liftFun0 z3_mk_simple_solver -- mkSolverForLogic :: Context -> Logic -> IO Solver -- mkSolverForLogic c logic = withContextError c $ \cPtr -> -- do sym <- mkStringSymbol c (show logic) -- c2h c =<< z3_mk_solver_for_logic cPtr (unSymbol sym) -- | Return a string describing all solver available parameters. solverGetHelp :: MonadZ3 z3 => z3 String solverGetHelp = liftSolver0 Base.solverGetHelp -- | Set the solver using the given parameters. solverSetParams :: MonadZ3 z3 => Params -> z3 () solverSetParams = liftSolver1 Base.solverSetParams -- | Create a backtracking point. solverPush :: MonadZ3 z3 => z3 () solverPush = liftSolver0 Base.solverPush -- | Backtrack /n/ backtracking points. solverPop :: MonadZ3 z3 => Int -> z3 () solverPop = liftSolver1 Base.solverPop solverReset :: MonadZ3 z3 => z3 () solverReset = liftSolver0 Base.solverReset -- | Number of backtracking points. solverGetNumScopes :: MonadZ3 z3 => z3 Int solverGetNumScopes = liftSolver0 Base.solverGetNumScopes -- | Assert a constraing into the logical context. -- -- Reference: solverAssertCnstr :: MonadZ3 z3 => AST -> z3 () solverAssertCnstr = liftSolver1 Base.solverAssertCnstr -- | Assert a constraint a into the solver, and track it -- (in the unsat) core using the Boolean constant /p/. -- -- This API is an alternative to Z3_solver_check_assumptions -- for extracting unsat cores. Both APIs can be used in the same -- solver. The unsat core will contain a combination of the Boolean -- variables provided using Z3_solver_assert_and_track and the -- Boolean literals provided using Z3_solver_check_assumptions. solverAssertAndTrack :: MonadZ3 z3 => AST -> AST -> z3 () solverAssertAndTrack = liftSolver2 Base.solverAssertAndTrack -- | Check whether the assertions in a given solver are consistent or not. solverCheck :: MonadZ3 z3 => z3 Result solverCheck = liftSolver0 Base.solverCheck -- | Check whether the assertions in the given solver and optional assumptions are consistent or not. solverCheckAssumptions :: MonadZ3 z3 => [AST] -> z3 Result solverCheckAssumptions = liftSolver1 Base.solverCheckAssumptions -- | Retrieve the model for the last 'solverCheck'. -- -- The error handler is invoked if a model is not available because -- the commands above were not invoked for the given solver, -- or if the result was 'Unsat'. solverGetModel :: MonadZ3 z3 => z3 Model solverGetModel = liftSolver0 Base.solverGetModel -- -- | Retrieve the proof for the last 'solverCheck' or 'solverCheckAssumptions'. -- -- The error handler is invoked if a proof is not available because -- the commands above were not invoked for the given solver, -- or if the result was different from 'Unsat' (so 'Sat' does not have a proof). solverGetProof :: MonadZ3 z3 => z3 AST solverGetProof = liftSolver0 Base.solverGetProof -- | Retrieve the unsat core for the last 'solverCheckAssumptions'; the unsat core is a subset of the assumptions solverGetUnsatCore :: MonadZ3 z3 => z3 [AST] solverGetUnsatCore = liftSolver0 Base.solverGetUnsatCore -- | Return a brief justification for an 'Unknown' result for the commands 'solverCheck' and 'solverCheckAssumptions'. solverGetReasonUnknown :: MonadZ3 z3 => z3 String solverGetReasonUnknown = liftSolver0 Base.solverGetReasonUnknown -- | Convert the given solver into a string. solverToString :: MonadZ3 z3 => z3 String solverToString = liftSolver0 Base.solverToString ------------------------------------------------- -- ** Helpers -- | Create a backtracking point. -- -- For @push; m; pop 1@ see 'local'. push :: MonadZ3 z3 => z3 () push = solverPush -- | Backtrack /n/ backtracking points. -- -- Contrary to 'solverPop' this funtion checks whether /n/ is within -- the size of the solver scope stack. pop :: MonadZ3 z3 => Int -> z3 () pop n = do scopes <- solverGetNumScopes if n <= scopes then solverPop n else error "Z3.Monad.safePop: too many scopes to backtrack" -- | Run a query and restore the initial logical context. -- -- This is a shorthand for 'push', run the query, and 'pop'. local :: MonadZ3 z3 => z3 a -> z3 a local q = do push r <- q pop 1 return r -- | Backtrack all the way. reset :: MonadZ3 z3 => z3 () reset = solverReset -- | Get number of backtracking points. getNumScopes :: MonadZ3 z3 => z3 Int getNumScopes = liftSolver0 Base.solverGetNumScopes assert :: MonadZ3 z3 => AST -> z3 () assert = solverAssertCnstr -- | Check whether the given logical context is consistent or not. check :: MonadZ3 z3 => z3 Result check = solverCheck -- | Check whether the assertions in the given solver and optional assumptions are consistent or not. checkAssumptions :: MonadZ3 z3 => [AST] -> z3 Result checkAssumptions = solverCheckAssumptions solverCheckAndGetModel :: MonadZ3 z3 => z3 (Result, Maybe Model) solverCheckAndGetModel = liftSolver0 Base.solverCheckAndGetModel -- | Get model. -- -- Reference : getModel :: MonadZ3 z3 => z3 (Result, Maybe Model) getModel = solverCheckAndGetModel -- | Check satisfiability and, if /sat/, compute a value from the given model. -- -- E.g. -- @ -- withModel $ \\m -> -- fromJust \<$\> evalInt m x -- @ withModel :: (Applicative z3, MonadZ3 z3) => (Base.Model -> z3 a) -> z3 (Result, Maybe a) withModel f = do (r,mb_m) <- getModel mb_e <- T.traverse f mb_m return (r, mb_e) -- | Retrieve the unsat core for the last 'checkAssumptions'; the unsat core is a subset of the assumptions. getUnsatCore :: MonadZ3 z3 => z3 [AST] getUnsatCore = solverGetUnsatCore