diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright M Farkas-Dyck © 2018 + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of M Farkas-Dyck nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,1 @@ +# ez3 diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/Z3/Tagged.hs b/Z3/Tagged.hs new file mode 100644 --- /dev/null +++ b/Z3/Tagged.hs @@ -0,0 +1,2155 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE MonadComprehensions #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE UnicodeSyntax #-} + +module Z3.Tagged + ( -- * Z3 monad + Z3 + , module Z3.Opts + , Logic(..) + , evalZ3 + , evalZ3With + -- ** Z3 enviroments + , Z3Env + , newEnv + , newItpEnv + , 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 + , 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 + -- ** Helpers + , mkBool + + -- * Arithmetic: Integers and Reals + , mkAdd + , mkMul + , mkSub + , 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 + + -- * 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 + + -- * Models + , modelEval + , evalArray + , getConstInterp + , getFuncInterp + , hasInterp + , numConsts + , numFuncs + , getConstDecl + , getFuncDecl + , getConsts + , getFuncs + , isAsArray + , 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 + , getParserError + + -- * Error Handling + , Base.Z3Error(..) + , Base.Z3ErrorCode(..) + + -- * Miscellaneous + , Version(..) + , getVersion + + -- * Fixedpoint + , Fixedpoint + , fixedpointPush + , fixedpointPop + , fixedpointAddRule + , fixedpointSetParams + , fixedpointRegisterRelation + , fixedpointQueryRelations + , fixedpointGetAnswer + , fixedpointGetAssertions + + -- * Interpolation + , Base.InterpolationProblem(..) + , mkInterpolant + , Base.mkInterpolationContext + , getInterpolant + , computeInterpolant + , readInterpolationProblem + , checkInterpolant + , interpolationProfile + , writeInterpolationProblem + + -- * Solvers + , solverGetHelp + , solverSetParams + , solverPush + , solverPop + , solverReset + , solverGetNumScopes + , solverAssertCnstr + , solverAssertAndTrack + , solverCheck + , solverCheckAssumptions + , solverGetModel + , solverGetUnsatCore + , solverGetReasonUnknown + , solverToString + -- ** Helpers + , assert + , check + , checkAssumptions + , solverCheckAndGetModel + , getModel + , withModel + , getUnsatCore + , push + , pop + , local + , reset + , getNumScopes + ) + where + +import Z3.Opts +import Z3.Base + ( FuncModel(..) + , Result(..) + , Logic(..) + , ASTPrintMode(..) + , Version(..) + , SortKind(..) + , ASTKind(..) + ) + +import qualified Z3.Base as Base + +import Control.Applicative ( Applicative ) +import Control.Monad.Fix ( MonadFix ) +import Control.Monad.ST +import Control.Monad.ST.Unsafe +import Control.Monad.Trans.Class ( lift ) +import Control.Monad.Trans.Reader ( ReaderT (..) ) +import Data.Coerce ( Coercible, coerce ) +import Data.Fixed ( Fixed, HasResolution ) +import Data.Int ( Int64 ) +import Data.Traversable ( Traversable ) +import qualified Data.Traversable as T +import Data.Word ( Word, Word64 ) +import Foreign.Storable + +liftF0 :: (Coercible a' a) + => (Base.Context -> IO a') -> Z3 s a +liftF0 f = Z3 . ReaderT $ \ (Z3Env {..}) -> unsafeIOToST $ coerce f context + +liftF1 :: (Coercible a' a, Coercible b' b) + => (Base.Context -> a' -> IO b') -> a -> Z3 s b +liftF1 f a = Z3 . ReaderT $ \ (Z3Env {..}) -> unsafeIOToST $ coerce f context a + +liftF2 :: (Coercible a' a, Coercible b' b, Coercible c' c) + => (Base.Context -> a' -> b' -> IO c') -> a -> b -> Z3 s c +liftF2 f a b = Z3 . ReaderT $ \ (Z3Env {..}) -> unsafeIOToST $ coerce f context a b + +liftF3 :: (Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d) + => (Base.Context -> a' -> b' -> c' -> IO d') -> a -> b -> c -> Z3 s d +liftF3 f a b c = Z3 . ReaderT $ \ (Z3Env {..}) -> unsafeIOToST $ coerce f context a b c + +liftF4 :: (Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d, Coercible e' e) + => (Base.Context -> a' -> b' -> c' -> d' -> IO e') -> a -> b -> c -> d -> Z3 s e +liftF4 f a b c d = Z3 . ReaderT $ \ (Z3Env {..}) -> unsafeIOToST $ coerce f context a b c d + +liftF5 :: (Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d, Coercible e' e, Coercible f' f) + => (Base.Context -> a' -> b' -> c' -> d' -> e' -> IO f') -> a -> b -> c -> d -> e -> Z3 s f +liftF5 f a b c d e = Z3 . ReaderT $ \ (Z3Env {..}) -> unsafeIOToST $ coerce f context a b c d e + +liftF6 :: (Coercible a' a, Coercible b' b, Coercible c' c, Coercible d' d, Coercible e' e, Coercible f' f, Coercible g' g) + => (Base.Context -> a' -> b' -> c' -> d' -> e' -> f' -> IO g') -> a -> b -> c -> d -> e -> f -> Z3 s g +liftF6 φ a b c d e f = Z3 . ReaderT $ \ (Z3Env {..}) -> unsafeIOToST $ coerce φ context a b c d e f + +liftSolver0 :: (Coercible a' a) + => (Base.Context -> Base.Solver -> IO a') -> Z3 s a +liftSolver0 f = Z3 . ReaderT $ \ (Z3Env {..}) -> unsafeIOToST $ coerce f context solver + +liftSolver1 :: (Coercible a' a, Coercible b' b) + => (Base.Context -> Base.Solver -> a' -> IO b') -> a -> Z3 s b +liftSolver1 f a = Z3 . ReaderT $ \ (Z3Env {..}) -> unsafeIOToST $ coerce f context solver a + +liftSolver2 :: (Coercible a' a, Coercible b' b, Coercible c' c) + => (Base.Context -> Base.Solver -> a' -> b' -> IO c') -> a -> b -> Z3 s c +liftSolver2 f a b = Z3 . ReaderT $ \ (Z3Env {..}) -> unsafeIOToST $ coerce f context solver a b + +liftFixedpoint0 :: (Coercible a' a) + => (Base.Context -> Base.Fixedpoint -> IO a') -> Z3 s a +liftFixedpoint0 f = Z3 . ReaderT $ \ (Z3Env {..}) -> unsafeIOToST $ coerce f context fixedpoint + +liftFixedpoint1 :: (Coercible a' a, Coercible b' b) + => (Base.Context -> Base.Fixedpoint -> a' -> IO b') -> a -> Z3 s b +liftFixedpoint1 f a = Z3 . ReaderT $ \ (Z3Env {..}) -> unsafeIOToST $ coerce f context fixedpoint a + +liftFixedpoint2 :: (Coercible a' a, Coercible b' b, Coercible c' c) + => (Base.Context -> Base.Fixedpoint -> a' -> b' -> IO c') -> a -> b -> Z3 s c +liftFixedpoint2 f a b = Z3 . ReaderT $ \ (Z3Env {..}) -> unsafeIOToST $ coerce f context fixedpoint a b + +------------------------------------------------- +-- A simple Z3 monad. + +newtype Z3 s a = Z3 { _unZ3 :: ReaderT (Z3Env s) (ST s) a } + deriving (Functor, Applicative, Monad, MonadFix) + +-- | Z3 environment. +data Z3Env s = Z3Env { solver :: Solver s, context :: Context s, fixedpoint :: Fixedpoint s } + +-- | Eval a Z3 script. +evalZ3With :: Maybe Logic -> Opts -> Z3 s a -> ST s a +evalZ3With mbLogic opts (Z3 (ReaderT a)) = a =<< newEnv mbLogic opts + +-- | Eval a Z3 script with default configuration options. +evalZ3 :: Z3 s a -> ST s a +evalZ3 = evalZ3With Nothing stdOpts + + +newEnvWith :: (Base.Config -> IO Base.Context) -> Maybe Logic -> Opts -> ST s (Z3Env s) +newEnvWith mkContext mbLogic opts = + unsafeIOToST . Base.withConfig $ \cfg -> do + setOpts cfg opts + ctx <- mkContext cfg + [coerce Z3Env solver ctx fixedpoint + | solver <- maybe (Base.mkSolver ctx) (Base.mkSolverForLogic ctx) mbLogic + , fixedpoint <- Base.mkFixedpoint ctx] + +-- | Create a new Z3 environment. +newEnv :: Maybe Logic -> Opts -> ST s (Z3Env s) +newEnv = newEnvWith Base.mkContext + +newItpEnv :: Maybe Logic -> Opts -> ST s (Z3Env s) +newItpEnv = newEnvWith Base.mkInterpolationContext + +-- | 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 s a + -> Z3Env s + -> ST s 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 :: Z3 s (Params s) +mkParams = liftF0 Base.mkParams + +-- | Add a Boolean parameter /k/ with value /v/ to the parameter set /p/. +paramsSetBool :: Params s -> Symbol s -> Bool -> Z3 s () +paramsSetBool = liftF3 Base.paramsSetBool + +-- | Add a unsigned parameter /k/ with value /v/ to the parameter set /p/. +paramsSetUInt :: Params s -> Symbol s -> Word -> Z3 s () +paramsSetUInt = liftF3 Base.paramsSetUInt + +-- | Add a double parameter /k/ with value /v/ to the parameter set /p/. +paramsSetDouble :: Params s -> Symbol s -> Double -> Z3 s () +paramsSetDouble = liftF3 Base.paramsSetDouble + +-- | Add a symbol parameter /k/ with value /v/ to the parameter set /p/. +paramsSetSymbol :: Params s -> Symbol s -> Symbol s -> Z3 s () +paramsSetSymbol = liftF3 Base.paramsSetSymbol + +-- | Convert a parameter set into a string. +-- +-- This function is mainly used for printing the contents of a parameter set. +paramsToString :: Params s -> Z3 s String +paramsToString = liftF1 Base.paramsToString + +-- TODO: Z3_params_validate + +--------------------------------------------------------------------- +-- Symbols + +-- | Create a Z3 symbol using an integer. +mkIntSymbol :: ∀ i s . Integral i => i -> Z3 s (Symbol s) +mkIntSymbol = liftF1 (Base.mkIntSymbol @i) + +-- | Create a Z3 symbol using a string. +-- +-- Reference: +mkStringSymbol :: String -> Z3 s (Symbol s) +mkStringSymbol = liftF1 Base.mkStringSymbol + +--------------------------------------------------------------------- +-- Sorts + +-- | Create a free (uninterpreted) type using the given name (symbol). +-- +-- Reference: +mkUninterpretedSort :: Symbol s -> Z3 s (Sort s) +mkUninterpretedSort = liftF1 Base.mkUninterpretedSort + +-- | Create the /boolean/ type. +-- +-- Reference: +mkBoolSort :: Z3 s (Sort s) +mkBoolSort = liftF0 Base.mkBoolSort + +-- | Create the /integer/ type. +-- +-- Reference: +mkIntSort :: Z3 s (Sort s) +mkIntSort = liftF0 Base.mkIntSort + +-- | Create the /real/ type. +-- +-- Reference: +mkRealSort :: Z3 s (Sort s) +mkRealSort = liftF0 Base.mkRealSort + +-- | Create a bit-vector type of the given size. +-- +-- This type can also be seen as a machine integer. +-- +-- Reference: +mkBvSort :: ∀ i s . Integral i => i -> Z3 s (Sort s) +mkBvSort = liftF1 (Base.mkBvSort @i) + +-- | Create an array type +-- +-- Reference: +-- +mkArraySort :: Sort s -> Sort s -> Z3 s (Sort s) +mkArraySort = liftF2 Base.mkArraySort + +-- | Create a tuple type +-- +-- Reference: +mkTupleSort :: Symbol s -- ^ Name of the sort + -> [(Symbol s, Sort s)] -- ^ Name and sort of each field + -> Z3 s (Sort s, FuncDecl s, [FuncDecl s]) -- ^ Resulting sort, and function + -- declarations for the + -- constructor and projections. +mkTupleSort = liftF2 Base.mkTupleSort + +-- | Create a contructor +-- +-- Reference: +mkConstructor :: Symbol s -- ^ Name of the sonstructor + -> Symbol s -- ^ Name of recognizer function + -> [(Symbol s, Maybe (Sort s), Int)] -- ^ Name, sort option, and sortRefs + -> Z3 s (Constructor s) +mkConstructor = liftF3 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 :: Symbol s + -> [Constructor s] + -> Z3 s (Sort s) +mkDatatype = liftF2 Base.mkDatatype + +-- | Create mutually recursive datatypes, such as a tree and forest. +-- +-- Returns the datatype sorts +mkDatatypes :: [Symbol s] + -> [[Constructor s]] + -> Z3 s [Sort s] +mkDatatypes = liftF2 Base.mkDatatypes + +-- | Create a set type +-- +-- Reference: +-- +mkSetSort :: Sort s -> Z3 s (Sort s) +mkSetSort = liftF1 Base.mkSetSort + +--------------------------------------------------------------------- +-- Constants and Applications + +-- | A Z3 function +mkFuncDecl :: Symbol s -> [Sort s] -> Sort s -> Z3 s (FuncDecl s) +mkFuncDecl = liftF3 Base.mkFuncDecl + +-- | Create a constant or function application. +-- +-- Reference: +mkApp :: FuncDecl s -> [AST s] -> Z3 s (AST s) +mkApp = liftF2 Base.mkApp + +-- | Declare and create a constant. +-- +-- Reference: +mkConst :: Symbol s -> Sort s -> Z3 s (AST s) +mkConst = liftF2 Base.mkConst + +-- | Declare and create a constant. +-- +-- Reference: +mkFreshConst :: String -> Sort s -> Z3 s (AST s) +mkFreshConst = liftF2 Base.mkFreshConst + +-- | Declare a fresh constant or function. +-- +-- Reference: +mkFreshFuncDecl :: String -> [Sort s] -> Sort s -> Z3 s (FuncDecl s) +mkFreshFuncDecl = liftF3 Base.mkFreshFuncDecl + +------------------------------------------------- +-- ** Helpers + +-- | Declare and create a variable (aka /constant/). +-- +-- An alias for 'mkConst'. +mkVar :: Symbol s -> Sort s -> Z3 s (AST s) +mkVar = liftF2 Base.mkVar + +-- | Declarate and create a variable of sort /bool/. +-- +-- See 'mkVar'. +mkBoolVar :: Symbol s -> Z3 s (AST s) +mkBoolVar = liftF1 Base.mkBoolVar + +-- | Declarate and create a variable of sort /real/. +-- +-- See 'mkVar'. +mkRealVar :: Symbol s -> Z3 s (AST s) +mkRealVar = liftF1 Base.mkRealVar + +-- | Declarate and create a variable of sort /int/. +-- +-- See 'mkVar'. +mkIntVar :: Symbol s -> Z3 s (AST s) +mkIntVar = liftF1 Base.mkIntVar + +-- | Declarate and create a variable of sort /bit-vector/. +-- +-- See 'mkVar'. +mkBvVar :: Symbol s + -> Int -- ^ bit-width + -> Z3 s (AST s) +mkBvVar = liftF2 Base.mkBvVar + +-- | Declare and create a /fresh/ variable (aka /constant/). +-- +-- An alias for 'mkFreshConst'. +mkFreshVar :: String -> Sort s -> Z3 s (AST s) +mkFreshVar = liftF2 Base.mkFreshConst + +-- | Declarate and create a /fresh/ variable of sort /bool/. +-- +-- See 'mkFreshVar'. +mkFreshBoolVar :: String -> Z3 s (AST s) +mkFreshBoolVar = liftF1 Base.mkFreshBoolVar + +-- | Declarate and create a /fresh/ variable of sort /real/. +-- +-- See 'mkFreshVar'. +mkFreshRealVar :: String -> Z3 s (AST s) +mkFreshRealVar = liftF1 Base.mkFreshRealVar + +-- | Declarate and create a /fresh/ variable of sort /int/. +-- +-- See 'mkFreshVar'. +mkFreshIntVar :: String -> Z3 s (AST s) +mkFreshIntVar = liftF1 Base.mkFreshIntVar + +-- | Declarate and create a /fresh/ variable of sort /bit-vector/. +-- +-- See 'mkFreshVar'. +mkFreshBvVar :: String + -> Int -- ^ bit-width + -> Z3 s (AST s) +mkFreshBvVar = liftF2 Base.mkFreshBvVar + +--------------------------------------------------------------------- +-- Propositional Logic and Equality + +-- | Create an (AST s) node representing /true/. +-- +-- Reference: +mkTrue :: Z3 s (AST s) +mkTrue = liftF0 Base.mkTrue + +-- | Create an (AST s) node representing /false/. +-- +-- Reference: +mkFalse :: Z3 s (AST s) +mkFalse = liftF0 Base.mkFalse + +-- | Create an (AST s) node representing /l = r/. +-- +-- Reference: +mkEq :: AST s -> AST s -> Z3 s (AST s) +mkEq = liftF2 Base.mkEq + +-- | The distinct construct is used for declaring the arguments pairwise +-- distinct. +-- +-- Reference: +mkDistinct :: [AST s] -> Z3 s (AST s) +mkDistinct = liftF1 Base.mkDistinct + +-- | Create an (AST s) node representing /not(a)/. +-- +-- Reference: +mkNot :: AST s -> Z3 s (AST s) +mkNot = liftF1 Base.mkNot + +-- | Create an (AST s) node representing an if-then-else: /ite(t1, t2, t3)/. +-- +-- Reference: +mkIte :: AST s -> AST s -> AST s -> Z3 s (AST s) +mkIte = liftF3 Base.mkIte + +-- | Create an (AST s) node representing /t1 iff t2/. +-- +-- Reference: +mkIff :: AST s -> AST s -> Z3 s (AST s) +mkIff = liftF2 Base.mkIff + +-- | Create an (AST s) node representing /t1 implies t2/. +-- +-- Reference: +mkImplies :: AST s -> AST s -> Z3 s (AST s) +mkImplies = liftF2 Base.mkImplies + +-- | Create an (AST s) node representing /t1 xor t2/. +-- +-- Reference: +mkXor :: AST s -> AST s -> Z3 s (AST s) +mkXor = liftF2 Base.mkXor + +-- | Create an (AST s) node representing args[0] and ... and args[num_args-1]. +-- +-- Reference: +mkAnd :: [AST s] -> Z3 s (AST s) +mkAnd = liftF1 Base.mkAnd + +-- | Create an (AST s) node representing args[0] or ... or args[num_args-1]. +-- +-- Reference: +mkOr :: [AST s] -> Z3 s (AST s) +mkOr = liftF1 Base.mkOr + +------------------------------------------------- +-- ** Helpers + +-- | Create an (AST s) node representing the given boolean. +mkBool :: Bool -> Z3 s (AST s) +mkBool = liftF1 Base.mkBool + +--------------------------------------------------------------------- +-- Arithmetic: Integers and Reals + +-- | Create an (AST s) node representing args[0] + ... + args[num_args-1]. +-- +-- Reference: +mkAdd :: [AST s] -> Z3 s (AST s) +mkAdd = liftF1 Base.mkAdd + +-- | Create an (AST s) node representing args[0] * ... * args[num_args-1]. +-- +-- Reference: +mkMul :: [AST s] -> Z3 s (AST s) +mkMul = liftF1 Base.mkMul + +-- | Create an (AST s) node representing args[0] - ... - args[num_args - 1]. +-- +-- Reference: +mkSub :: [AST s] -> Z3 s (AST s) +mkSub = liftF1 Base.mkSub + +-- | Create an (AST s) node representing -arg. +-- +-- Reference: +mkUnaryMinus :: AST s -> Z3 s (AST s) +mkUnaryMinus = liftF1 Base.mkUnaryMinus + +-- | Create an (AST s) node representing arg1 div arg2. +-- +-- Reference: +mkDiv :: AST s -> AST s -> Z3 s (AST s) +mkDiv = liftF2 Base.mkDiv + +-- | Create an (AST s) node representing arg1 mod arg2. +-- +-- Reference: +mkMod :: AST s -> AST s -> Z3 s (AST s) +mkMod = liftF2 Base.mkMod + +-- | Create an (AST s) node representing arg1 rem arg2. +-- +-- Reference: +mkRem :: AST s -> AST s -> Z3 s (AST s) +mkRem = liftF2 Base.mkRem + +-- | Create less than. +-- +-- Reference: +mkLt :: AST s -> AST s -> Z3 s (AST s) +mkLt = liftF2 Base.mkLt + +-- | Create less than or equal to. +-- +-- Reference: +mkLe :: AST s -> AST s -> Z3 s (AST s) +mkLe = liftF2 Base.mkLe + +-- | Create greater than. +-- +-- Reference: +mkGt :: AST s -> AST s -> Z3 s (AST s) +mkGt = liftF2 Base.mkGt + +-- | Create greater than or equal to. +-- +-- Reference: +mkGe :: AST s -> AST s -> Z3 s (AST s) +mkGe = liftF2 Base.mkGe + +-- | Coerce an integer to a real. +-- +-- Reference: +mkInt2Real :: AST s -> Z3 s (AST s) +mkInt2Real = liftF1 Base.mkInt2Real + +-- | Coerce a real to an integer. +-- +-- Reference: +mkReal2Int :: AST s -> Z3 s (AST s) +mkReal2Int = liftF1 Base.mkReal2Int + +-- | Check if a real number is an integer. +-- +-- Reference: +mkIsInt :: AST s -> Z3 s (AST s) +mkIsInt = liftF1 Base.mkIsInt + +--------------------------------------------------------------------- +-- Bit-vectors + +-- | Bitwise negation. +-- +-- Reference: +mkBvnot :: AST s -> Z3 s (AST s) +mkBvnot = liftF1 Base.mkBvnot + +-- | Take conjunction of bits in vector, return vector of length 1. +-- +-- Reference: +mkBvredand :: AST s -> Z3 s (AST s) +mkBvredand = liftF1 Base.mkBvredand + +-- | Take disjunction of bits in vector, return vector of length 1. +-- +-- Reference: +mkBvredor :: AST s -> Z3 s (AST s) +mkBvredor = liftF1 Base.mkBvredor + +-- | Bitwise and. +-- +-- Reference: +mkBvand :: AST s -> AST s -> Z3 s (AST s) +mkBvand = liftF2 Base.mkBvand + +-- | Bitwise or. +-- +-- Reference: +mkBvor :: AST s -> AST s -> Z3 s (AST s) +mkBvor = liftF2 Base.mkBvor + +-- | Bitwise exclusive-or. +-- +-- Reference: +mkBvxor :: AST s -> AST s -> Z3 s (AST s) +mkBvxor = liftF2 Base.mkBvxor + +-- | Bitwise nand. +-- +-- Reference: +mkBvnand :: AST s -> AST s -> Z3 s (AST s) +mkBvnand = liftF2 Base.mkBvnand + +-- | Bitwise nor. +-- +-- Reference: +mkBvnor :: AST s -> AST s -> Z3 s (AST s) +mkBvnor = liftF2 Base.mkBvnor + +-- | Bitwise xnor. +-- +-- Reference: +mkBvxnor :: AST s -> AST s -> Z3 s (AST s) +mkBvxnor = liftF2 Base.mkBvxnor + +-- | Standard two's complement unary minus. +-- +-- Reference: Z3 s (AST s) +mkBvneg = liftF1 Base.mkBvneg + +-- | Standard two's complement addition. +-- +-- Reference: +mkBvadd :: AST s -> AST s -> Z3 s (AST s) +mkBvadd = liftF2 Base.mkBvadd + +-- | Standard two's complement subtraction. +-- +-- Reference: +mkBvsub :: AST s -> AST s -> Z3 s (AST s) +mkBvsub = liftF2 Base.mkBvsub + +-- | Standard two's complement multiplication. +-- +-- Reference: +mkBvmul :: AST s -> AST s -> Z3 s (AST s) +mkBvmul = liftF2 Base.mkBvmul + +-- | Unsigned division. +-- +-- Reference: +mkBvudiv :: AST s -> AST s -> Z3 s (AST s) +mkBvudiv = liftF2 Base.mkBvudiv + +-- | Two's complement signed division. +-- +-- Reference: +mkBvsdiv :: AST s -> AST s -> Z3 s (AST s) +mkBvsdiv = liftF2 Base.mkBvsdiv + +-- | Unsigned remainder. +-- +-- Reference: +mkBvurem :: AST s -> AST s -> Z3 s (AST s) +mkBvurem = liftF2 Base.mkBvurem + +-- | Two's complement signed remainder (sign follows dividend). +-- +-- Reference: +mkBvsrem :: AST s -> AST s -> Z3 s (AST s) +mkBvsrem = liftF2 Base.mkBvsrem + +-- | Two's complement signed remainder (sign follows divisor). +-- +-- Reference: +mkBvsmod :: AST s -> AST s -> Z3 s (AST s) +mkBvsmod = liftF2 Base.mkBvsmod + +-- | Unsigned less than. +-- +-- Reference: +mkBvult :: AST s -> AST s -> Z3 s (AST s) +mkBvult = liftF2 Base.mkBvult + +-- | Two's complement signed less than. +-- +-- Reference: +mkBvslt :: AST s -> AST s -> Z3 s (AST s) +mkBvslt = liftF2 Base.mkBvslt + +-- | Unsigned less than or equal to. +-- +-- Reference: +mkBvule :: AST s -> AST s -> Z3 s (AST s) +mkBvule = liftF2 Base.mkBvule + +-- | Two's complement signed less than or equal to. +-- +-- Reference: +mkBvsle :: AST s -> AST s -> Z3 s (AST s) +mkBvsle = liftF2 Base.mkBvsle + +-- | Unsigned greater than or equal to. +-- +-- Reference: +mkBvuge :: AST s -> AST s -> Z3 s (AST s) +mkBvuge = liftF2 Base.mkBvuge + +-- | Two's complement signed greater than or equal to. +-- +-- Reference: +mkBvsge :: AST s -> AST s -> Z3 s (AST s) +mkBvsge = liftF2 Base.mkBvsge + +-- | Unsigned greater than. +-- +-- Reference: +mkBvugt :: AST s -> AST s -> Z3 s (AST s) +mkBvugt = liftF2 Base.mkBvugt + +-- | Two's complement signed greater than. +-- +-- Reference: +mkBvsgt :: AST s -> AST s -> Z3 s (AST s) +mkBvsgt = liftF2 Base.mkBvsgt + +-- | Concatenate the given bit-vectors. +-- +-- Reference: +mkConcat :: AST s -> AST s -> Z3 s (AST s) +mkConcat = liftF2 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 :: Int -> Int -> AST s -> Z3 s (AST s) +mkExtract = liftF3 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 :: Int -> AST s -> Z3 s (AST s) +mkSignExt = liftF2 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 :: Int -> AST s -> Z3 s (AST s) +mkZeroExt = liftF2 Base.mkZeroExt + +-- | Repeat the given bit-vector up length /i/. +-- +-- Reference: +mkRepeat :: Int -> AST s -> Z3 s (AST s) +mkRepeat = liftF2 Base.mkRepeat + +-- | Shift left. +-- +-- Reference: +mkBvshl :: AST s -> AST s -> Z3 s (AST s) +mkBvshl = liftF2 Base.mkBvshl + +-- | Logical shift right. +-- +-- Reference: +mkBvlshr :: AST s -> AST s -> Z3 s (AST s) +mkBvlshr = liftF2 Base.mkBvlshr + +-- | Arithmetic shift right. +-- +-- Reference: +mkBvashr :: AST s -> AST s -> Z3 s (AST s) +mkBvashr = liftF2 Base.mkBvashr + +-- | Rotate bits of /t1/ to the left /i/ times. +-- +-- Reference: +mkRotateLeft :: Int -> AST s -> Z3 s (AST s) +mkRotateLeft = liftF2 Base.mkRotateLeft + +-- | Rotate bits of /t1/ to the right /i/ times. +-- +-- Reference: +mkRotateRight :: Int -> AST s -> Z3 s (AST s) +mkRotateRight = liftF2 Base.mkRotateRight + +-- | Rotate bits of /t1/ to the left /t2/ times. +-- +-- Reference: +mkExtRotateLeft :: AST s -> AST s -> Z3 s (AST s) +mkExtRotateLeft = liftF2 Base.mkExtRotateLeft + +-- | Rotate bits of /t1/ to the right /t2/ times. +-- +-- Reference: +mkExtRotateRight :: AST s -> AST s -> Z3 s (AST s) +mkExtRotateRight = liftF2 Base.mkExtRotateRight + +-- | Create an /n/ bit bit-vector from the integer argument /t1/. +-- +-- Reference: +mkInt2bv :: Int -> AST s -> Z3 s (AST s) +mkInt2bv = liftF2 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 :: AST s -> Bool -> Z3 s (AST s) +mkBv2int = liftF2 Base.mkBv2int + +-- | Create a predicate that checks that the bit-wise addition of /t1/ and /t2/ +-- does not overflow. +-- +-- Reference: +mkBvaddNoOverflow :: AST s -> AST s -> Bool -> Z3 s (AST s) +mkBvaddNoOverflow = liftF3 Base.mkBvaddNoOverflow + +-- | Create a predicate that checks that the bit-wise signed addition of /t1/ +-- and /t2/ does not underflow. +-- +-- Reference: +mkBvaddNoUnderflow :: AST s -> AST s -> Z3 s (AST s) +mkBvaddNoUnderflow = liftF2 Base.mkBvaddNoUnderflow + +-- | Create a predicate that checks that the bit-wise signed subtraction of /t1/ +-- and /t2/ does not overflow. +-- +-- Reference: +mkBvsubNoOverflow :: AST s -> AST s -> Z3 s (AST s) +mkBvsubNoOverflow = liftF2 Base.mkBvsubNoOverflow + +-- | Create a predicate that checks that the bit-wise subtraction of /t1/ and +-- /t2/ does not underflow. +-- +-- Reference: +mkBvsubNoUnderflow :: AST s -> AST s -> Z3 s (AST s) +mkBvsubNoUnderflow = liftF2 Base.mkBvsubNoUnderflow + +-- | Create a predicate that checks that the bit-wise signed division of /t1/ +-- and /t2/ does not overflow. +-- +-- Reference: +mkBvsdivNoOverflow :: AST s -> AST s -> Z3 s (AST s) +mkBvsdivNoOverflow = liftF2 Base.mkBvsdivNoOverflow + +-- | Check that bit-wise negation does not overflow when /t1/ is interpreted as +-- a signed bit-vector. +-- +-- Reference: +mkBvnegNoOverflow :: AST s -> Z3 s (AST s) +mkBvnegNoOverflow = liftF1 Base.mkBvnegNoOverflow + +-- | Create a predicate that checks that the bit-wise multiplication of /t1/ and +-- /t2/ does not overflow. +-- +-- Reference: +mkBvmulNoOverflow :: AST s -> AST s -> Bool -> Z3 s (AST s) +mkBvmulNoOverflow = liftF3 Base.mkBvmulNoOverflow + +-- | Create a predicate that checks that the bit-wise signed multiplication of +-- /t1/ and /t2/ does not underflow. +-- +-- Reference: +mkBvmulNoUnderflow :: AST s -> AST s -> Z3 s (AST s) +mkBvmulNoUnderflow = liftF2 Base.mkBvmulNoUnderflow + +--------------------------------------------------------------------- +-- Arrays + +-- | Array read. The argument a is the array and i is the index of the array +-- that gets read. +-- +-- Reference: +mkSelect :: AST s -> AST s -> Z3 s (AST s) +mkSelect = liftF2 Base.mkSelect + +-- | Array update.   +-- +-- Reference: +mkStore :: AST s -> AST s -> AST s -> Z3 s (AST s) +mkStore = liftF3 Base.mkStore + +-- | Create the constant array. +-- +-- Reference: +mkConstArray :: Sort s -> AST s -> Z3 s (AST s) +mkConstArray = liftF2 Base.mkConstArray + +-- | map f on the the argument arrays. +-- +-- Reference: +mkMap :: FuncDecl s -> [AST s] -> Z3 s (AST s) +mkMap = liftF2 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 :: AST s -> Z3 s (AST s) +mkArrayDefault = liftF1 Base.mkArrayDefault + +--------------------------------------------------------------------- +-- Sets + +-- | Create the empty set. +-- +-- Reference: +mkEmptySet :: Sort s -> Z3 s (AST s) +mkEmptySet = liftF1 Base.mkEmptySet + +-- | Create the full set. +-- +-- Reference: +mkFullSet :: Sort s -> Z3 s (AST s) +mkFullSet = liftF1 Base.mkFullSet + +-- | Add an element to a set. +-- +-- Reference: +mkSetAdd :: AST s -> AST s -> Z3 s (AST s) +mkSetAdd = liftF2 Base.mkSetAdd + +-- | Remove an element from a set. +-- +-- Reference: +mkSetDel :: AST s -> AST s -> Z3 s (AST s) +mkSetDel = liftF2 Base.mkSetDel + +-- | Take the union of a list of sets. +-- +-- Reference: +mkSetUnion :: [AST s] -> Z3 s (AST s) +mkSetUnion = liftF1 Base.mkSetUnion + +-- | Take the intersection of a list of sets. +-- +-- Reference: +mkSetIntersect :: [AST s] -> Z3 s (AST s) +mkSetIntersect = liftF1 Base.mkSetIntersect + +-- | Take the set difference between two sets. +-- +-- Reference: +mkSetDifference :: AST s -> AST s -> Z3 s (AST s) +mkSetDifference = liftF2 Base.mkSetDifference + +-- | Take the complement of a set. +-- +-- Reference: +mkSetComplement :: AST s -> Z3 s (AST s) +mkSetComplement = liftF1 Base.mkSetComplement + +-- | Check for set membership. +-- +-- Reference: +mkSetMember :: AST s -> AST s -> Z3 s (AST s) +mkSetMember = liftF2 Base.mkSetMember + +-- | Check if the first set is a subset of the second set. +-- +-- Reference: +mkSetSubset :: AST s -> AST s -> Z3 s (AST s) +mkSetSubset = liftF2 Base.mkSetSubset + +--------------------------------------------------------------------- +-- * Numerals + +-- | Create a numeral of a given sort. +-- +-- Reference: +mkNumeral :: String -> Sort s -> Z3 s (AST s) +mkNumeral = liftF2 Base.mkNumeral + +-- | Create a numeral of sort /real/. +mkReal :: Int -> Int -> Z3 s (AST s) +mkReal = liftF2 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 :: Int -> Sort s -> Z3 s (AST s) +mkInt = liftF2 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 :: Word -> Sort s -> Z3 s (AST s) +mkUnsignedInt = liftF2 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 :: Int64 -> Sort s -> Z3 s (AST s) +mkInt64 = liftF2 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 :: Word64 -> Sort s -> Z3 s (AST s) +mkUnsignedInt64 = liftF2 Base.mkUnsignedInt64 + +------------------------------------------------- +-- ** Helpers + +-- | Create a numeral of an int, bit-vector, or finite-domain sort. +mkIntegral :: ∀ a s . (Integral a) => a -> Sort s -> Z3 s (AST s) +mkIntegral = liftF2 (Base.mkIntegral @a) + +-- | Create a numeral of sort /real/ from a 'Rational'. +mkRational :: Rational -> Z3 s (AST s) +mkRational = liftF1 Base.mkRational + +-- | Create a numeral of sort /real/ from a 'Fixed'. +mkFixed :: ∀ a s . (HasResolution a) => Fixed a -> Z3 s (AST s) +mkFixed = liftF1 (Base.mkFixed @a) + +-- | Create a numeral of sort /real/ from a 'Real'. +mkRealNum :: ∀ r s . (Real r) => r -> Z3 s (AST s) +mkRealNum = liftF1 (Base.mkRealNum @r) + +-- | Create a numeral of sort /int/ from an 'Integer'. +mkInteger :: Integer -> Z3 s (AST s) +mkInteger = liftF1 Base.mkInteger + +-- | Create a numeral of sort /int/ from an 'Integral'. +mkIntNum :: ∀ a s . (Integral a) => a -> Z3 s (AST s) +mkIntNum = liftF1 (Base.mkIntNum @a) + +-- | Create a numeral of sort /Bit-vector/ from an 'Integer'. +mkBitvector :: Int -- ^ bit-width + -> Integer -- ^ integer value + -> Z3 s (AST s) +mkBitvector = liftF2 Base.mkBitvector + +-- | Create a numeral of sort /Bit-vector/ from an 'Integral'. +mkBvNum :: ∀ i s . + (Integral i) => Int -- ^ bit-width + -> i -- ^ integer value + -> Z3 s (AST s) +mkBvNum = liftF2 (Base.mkBvNum @i) + +--------------------------------------------------------------------- +-- Quantifiers + +mkPattern :: [AST s] -> Z3 s (Pattern s) +mkPattern = liftF1 Base.mkPattern + +mkBound :: Int -> Sort s -> Z3 s (AST s) +mkBound = liftF2 Base.mkBound + +mkForall :: [Pattern s] -> [Symbol s] -> [Sort s] -> AST s -> Z3 s (AST s) +mkForall = liftF4 Base.mkForall + +mkForallConst :: [Pattern s] -> [App s] -> AST s -> Z3 s (AST s) +mkForallConst = liftF3 Base.mkForallConst + +mkExistsConst :: [Pattern s] -> [App s] -> AST s -> Z3 s (AST s) +mkExistsConst = liftF3 Base.mkExistsConst + +mkExists :: [Pattern s] -> [Symbol s] -> [Sort s] -> AST s -> Z3 s (AST s) +mkExists = liftF4 Base.mkExists + +--------------------------------------------------------------------- +-- Accessors + +-- | Return the symbol name. +-- +-- Reference: +getSymbolString :: Symbol s -> Z3 s String +getSymbolString = liftF1 Base.getSymbolString + +-- | Return the sort kind. +-- +-- Reference: +getSortKind :: Sort s -> Z3 s SortKind +getSortKind = liftF1 Base.getSortKind + +-- | Return the size of the given bit-vector sort. +-- +-- Reference: +getBvSortSize :: Sort s -> Z3 s Int +getBvSortSize = liftF1 Base.getBvSortSize + +-- | Get list of constructors for datatype. +getDatatypeSortConstructors :: Sort s -- ^ Datatype sort. + -> Z3 s [FuncDecl s] -- ^ (Constructor s) declarations. +getDatatypeSortConstructors = liftF1 Base.getDatatypeSortConstructors + +-- | Get list of recognizers for datatype. +getDatatypeSortRecognizers :: Sort s -- ^ Datatype sort. + -> Z3 s [FuncDecl s] -- ^ (Constructor s) recognizers. +getDatatypeSortRecognizers = liftF1 Base.getDatatypeSortRecognizers + +-- | Get list of accessors for datatype. +getDatatypeSortConstructorAccessors :: Sort s -- ^ Datatype sort. + -> Z3 s [[FuncDecl s]] -- ^ (Constructor s) recognizers. +getDatatypeSortConstructorAccessors = liftF1 Base.getDatatypeSortConstructorAccessors + +-- | Return the constant declaration name as a symbol. +-- +-- Reference: +getDeclName :: FuncDecl s -> Z3 s (Symbol s) +getDeclName = liftF1 Base.getDeclName + +-- | Returns the number of parameters of the given declaration +getArity :: FuncDecl s -> Z3 s Int +getArity = liftF1 Base.getArity + +-- | Returns the sort of the i-th parameter of the given function declaration +getDomain :: FuncDecl s -- ^ A function declaration + -> Int -- ^ i + -> Z3 s (Sort s) +getDomain = liftF2 Base.getDomain + +-- | Returns the range of the given declaration. +getRange :: FuncDecl s -> Z3 s (Sort s) +getRange = liftF1 Base.getRange + +-- | Convert an app into (AST s). This is just type casting. +appToAst :: App s -> Z3 s (AST s) +appToAst = liftF1 Base.appToAst + +-- | Return the declaration of a constant or function application. +getAppDecl :: App s -> Z3 s (FuncDecl s) +getAppDecl = liftF1 Base.getAppDecl + +-- | Return the number of argument of an application. If t is an constant, then the number of arguments is 0. +getAppNumArgs :: App s -> Z3 s Int +getAppNumArgs = liftF1 Base.getAppNumArgs + +-- | Return the i-th argument of the given application. +getAppArg :: App s -> Int -> Z3 s (AST s) +getAppArg = liftF2 Base.getAppArg + +-- | Return a list of all the arguments of the given application. +getAppArgs :: App s -> Z3 s [AST s] +getAppArgs = liftF1 Base.getAppArgs + +-- | Return the sort of an (AST s) node. +getSort :: AST s -> Z3 s (Sort s) +getSort = liftF1 Base.getSort + +getArraySortDomain :: Sort s -> Z3 s (Sort s) +getArraySortDomain = liftF1 Base.getArraySortDomain + +getArraySortRange :: Sort s -> Z3 s (Sort s) +getArraySortRange = liftF1 Base.getArraySortRange + +-- | Returns @Just True@, @Just False@, or @Nothing@ for /undefined/. +-- +-- Reference: +getBoolValue :: AST s -> Z3 s (Maybe Bool) +getBoolValue = liftF1 Base.getBoolValue + +-- | Return the kind of the given (AST s). +-- +-- Reference: +getAstKind :: AST s -> Z3 s ASTKind +getAstKind = liftF1 Base.getAstKind + +-- | Return True if an ast is APP_AST, False otherwise. +isApp :: AST s -> Z3 s Bool +isApp = liftF1 Base.isApp + +-- | Cast (AST s) into an (App s). +toApp :: AST s -> Z3 s (App s) +toApp = liftF1 Base.toApp + +-- | Return numeral value, as a string of a numeric constant term. +getNumeralString :: AST s -> Z3 s String +getNumeralString = liftF1 Base.getNumeralString + +getIndexValue :: AST s -> Z3 s Int +getIndexValue = liftF1 Base.getIndexValue + +isQuantifierForall :: AST s -> Z3 s Bool +isQuantifierForall = liftF1 Base.isQuantifierForall + +isQuantifierExists :: AST s -> Z3 s Bool +isQuantifierExists = liftF1 Base.isQuantifierExists + +getQuantifierWeight :: AST s -> Z3 s Int +getQuantifierWeight = liftF1 Base.getQuantifierWeight + +getQuantifierNumPatterns :: AST s -> Z3 s Int +getQuantifierNumPatterns = liftF1 Base.getQuantifierNumPatterns + +getQuantifierPatternAST :: AST s -> Int -> Z3 s (AST s) +getQuantifierPatternAST = liftF2 Base.getQuantifierPatternAST + +getQuantifierPatterns :: AST s -> Z3 s [AST s] +getQuantifierPatterns = liftF1 Base.getQuantifierPatterns + +getQuantifierNumNoPatterns :: AST s -> Z3 s Int +getQuantifierNumNoPatterns = liftF1 Base.getQuantifierNumNoPatterns + +getQuantifierNoPatternAST :: AST s -> Int -> Z3 s (AST s) +getQuantifierNoPatternAST = liftF2 Base.getQuantifierNoPatternAST + +getQuantifierNoPatterns :: AST s -> Z3 s [AST s] +getQuantifierNoPatterns = liftF1 Base.getQuantifierNoPatterns + +getQuantifierNumBound :: AST s -> Z3 s Int +getQuantifierNumBound = liftF1 Base.getQuantifierNumBound + +getQuantifierBoundName :: AST s -> Int -> Z3 s (Symbol s) +getQuantifierBoundName = liftF2 Base.getQuantifierBoundName + +getQuantifierBoundSort :: AST s -> Int -> Z3 s (Sort s) +getQuantifierBoundSort = liftF2 Base.getQuantifierBoundSort + +getQuantifierBoundVars :: AST s -> Z3 s [AST s] +getQuantifierBoundVars = liftF1 Base.getQuantifierBoundVars + +getQuantifierBody :: AST s -> Z3 s (AST s) +getQuantifierBody = liftF1 Base.getQuantifierBody + +-- | Simplify the expression. +-- +-- Reference: +simplify :: AST s -> Z3 s (AST s) +simplify = liftF1 Base.simplify + +-- | Simplify the expression using the given parameters. +-- +-- Reference: +simplifyEx :: AST s -> Params s -> Z3 s (AST s) +simplifyEx = liftF2 Base.simplifyEx + +------------------------------------------------- +-- ** Helpers + +-- | Read a 'Bool' value from an '(AST s)' +getBool :: AST s -> Z3 s Bool +getBool = liftF1 Base.getBool + +-- | Return the integer value +getInt :: AST s -> Z3 s Integer +getInt = liftF1 Base.getInt + +-- | Return rational value +getReal :: AST s -> Z3 s Rational +getReal = liftF1 Base.getReal + +-- | Read the 'Integer' value from an '(AST s)' of sort /bit-vector/. +-- +-- See 'mkBv2int'. +getBv :: AST s + -> Bool -- ^ signed? + -> Z3 s Integer +getBv = liftF2 Base.getBv + + +--------------------------------------------------------------------- +-- Modifiers + +substituteVars :: AST s -> [AST s] -> Z3 s (AST s) +substituteVars = liftF2 Base.substituteVars + +--------------------------------------------------------------------- +-- Models + +-- | Evaluate an (AST s) 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 :: Model s -> AST s + -> Bool -- ^ (Model s) completion? + -> Z3 s (Maybe (AST s)) +modelEval = liftF3 Base.modelEval + +-- | Get array as a list of argument/value pairs, if it is +-- represented as a function (ie, using as-array). +evalArray :: Model s -> AST s -> Z3 s (Maybe FuncModel) +evalArray = liftF2 Base.evalArray + +getConstInterp :: Model s -> FuncDecl s -> Z3 s (Maybe (AST s)) +getConstInterp = liftF2 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 :: Model s -> FuncDecl s -> Z3 s (Maybe (FuncInterp s)) +getFuncInterp = liftF2 Base.getFuncInterp + +hasInterp :: Model s -> FuncDecl s -> Z3 s Bool +hasInterp = liftF2 Base.hasInterp + +numConsts :: Model s -> Z3 s Word +numConsts = liftF1 Base.numConsts + +numFuncs :: Model s -> Z3 s Word +numFuncs = liftF1 Base.numFuncs + +getConstDecl :: Model s -> Word -> Z3 s (FuncDecl s) +getConstDecl = liftF2 Base.getConstDecl + +getFuncDecl :: Model s -> Word -> Z3 s (FuncDecl s) +getFuncDecl = liftF2 Base.getFuncDecl + +getConsts :: Model s -> Z3 s [FuncDecl s] +getConsts = liftF1 Base.getConsts + +getFuncs :: Model s -> Z3 s [FuncDecl s] +getFuncs = liftF1 Base.getFuncs + +-- | The (_ as-array f) (AST s) 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 s) node. +-- +-- Reference: +isAsArray :: AST s -> Z3 s Bool +isAsArray = liftF1 Base.isAsArray + +addFuncInterp :: Model s -> FuncDecl s -> AST s -> Z3 s (FuncInterp s) +addFuncInterp = liftF3 Base.addFuncInterp + +addConstInterp :: Model s -> FuncDecl s -> AST s -> Z3 s () +addConstInterp = liftF3 Base.addConstInterp + + +-- | Return the function declaration f associated with a (_ as_array f) node. +-- +-- Reference: +getAsArrayFuncDecl :: AST s -> Z3 s (FuncDecl s) +getAsArrayFuncDecl = liftF1 Base.getAsArrayFuncDecl + +-- | Return the number of entries in the given function interpretation. +-- +-- Reference: +funcInterpGetNumEntries :: FuncInterp s -> Z3 s Int +funcInterpGetNumEntries = liftF1 Base.funcInterpGetNumEntries + +-- | Return a "point" of the given function intepretation. +-- It represents the value of f in a particular point. +-- +-- Reference: +funcInterpGetEntry :: FuncInterp s -> Int -> Z3 s (FuncEntry s) +funcInterpGetEntry = liftF2 Base.funcInterpGetEntry + +-- | Return the 'else' value of the given function interpretation. +-- +-- Reference: +funcInterpGetElse :: FuncInterp s -> Z3 s (AST s) +funcInterpGetElse = liftF1 Base.funcInterpGetElse + +-- | Return the arity (number of arguments) of the given function +-- interpretation. +-- +-- Reference: +funcInterpGetArity :: FuncInterp s -> Z3 s Int +funcInterpGetArity = liftF1 Base.funcInterpGetArity + +-- | Return the value of this point. +-- +-- Reference: +funcEntryGetValue :: FuncEntry s -> Z3 s (AST s) +funcEntryGetValue = liftF1 Base.funcEntryGetValue + +-- | Return the number of arguments in a Z3_func_entry object. +-- +-- Reference: +funcEntryGetNumArgs :: FuncEntry s -> Z3 s Int +funcEntryGetNumArgs = liftF1 Base.funcEntryGetNumArgs + +-- | Return an argument of a Z3_func_entry object. +-- +-- Reference: +funcEntryGetArg :: FuncEntry s -> Int -> Z3 s (AST s) +funcEntryGetArg = liftF2 Base.funcEntryGetArg + +-- | Convert the given model into a string. +modelToString :: Model s -> Z3 s String +modelToString = liftF1 Base.modelToString + +-- | Alias for 'modelToString'. +showModel :: Model s -> Z3 s String +showModel = modelToString + +------------------------------------------------- +-- ** Helpers + +-- | Type of an evaluation function for '(AST s)'. +-- +-- Evaluation may fail (i.e. return 'Nothing') for a few +-- reasons, see 'modelEval'. +type EvalAst m s a = Model s -> AST s -> m s (Maybe a) + +-- | An alias for 'modelEval' with model completion enabled. +eval :: EvalAst Z3 s (AST s) +eval = liftF2 Base.eval + +-- | Evaluate an (AST s) node of sort /bool/ in the given model. +-- +-- See 'modelEval' and 'getBool'. +evalBool :: EvalAst Z3 s Bool +evalBool = liftF2 Base.evalBool + +-- | Evaluate an (AST s) node of sort /int/ in the given model. +-- +-- See 'modelEval' and 'getInt'. +evalInt :: EvalAst Z3 s Integer +evalInt = liftF2 Base.evalInt + +-- | Evaluate an (AST s) node of sort /real/ in the given model. +-- +-- See 'modelEval' and 'getReal'. +evalReal :: EvalAst Z3 s Rational +evalReal = liftF2 Base.evalReal + +-- | Evaluate an (AST s) 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 :: Bool -- ^ signed? + -> EvalAst Z3 s Integer +evalBv = liftF3 Base.evalBv + +-- | Evaluate a collection of (AST s) nodes in the given model. +evalT :: ∀ t s . (Traversable t) => Model s -> t (AST s) -> Z3 s (Maybe (t (AST s))) +evalT model asts = (fmap . fmap . fmap) coerce . Z3 . ReaderT $ \ (Z3Env {..}) -> unsafeIOToST $ Base.evalT (coerce context) (coerce model) (coerce <$> asts) + +-- | Run a evaluation function on a 'Traversable' data structure of '(AST s)'s +-- (e.g. @[(AST s)]@, @Vector (AST s)@, @Maybe (AST s)@, 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 s)' of sort /int/. +mapEval :: (Traversable t) => EvalAst Z3 s a + -> Model s + -> t (AST s) + -> Z3 s (Maybe (t a)) +mapEval f m = fmap T.sequence . T.mapM (f m) + +-- | Get function as a list of argument/value pairs. +evalFunc :: Model s -> FuncDecl s -> Z3 s (Maybe FuncModel) +evalFunc = liftF2 Base.evalFunc + +--------------------------------------------------------------------- +-- Tactics + +mkTactic :: String -> Z3 s( Tactic s) +mkTactic = liftF1 Base.mkTactic + +andThenTactic ::Tactic s ->Tactic s -> Z3 s( Tactic s) +andThenTactic = liftF2 Base.andThenTactic + +orElseTactic ::Tactic s ->Tactic s -> Z3 s( Tactic s) +orElseTactic = liftF2 Base.andThenTactic + +skipTactic :: Z3 s( Tactic s) +skipTactic = liftF0 Base.skipTactic + +tryForTactic ::Tactic s -> Int -> Z3 s( Tactic s) +tryForTactic = liftF2 Base.tryForTactic + +mkQuantifierEliminationTactic :: Z3 s( Tactic s) +mkQuantifierEliminationTactic = liftF0 Base.mkQuantifierEliminationTactic + +mkAndInverterGraphTactic :: Z3 s( Tactic s) +mkAndInverterGraphTactic = liftF0 Base.mkAndInverterGraphTactic + +applyTactic ::Tactic s ->Goal s -> Z3 s( ApplyResult s) +applyTactic = liftF2 Base.applyTactic + +getApplyResultNumSubgoals ::ApplyResult s -> Z3 s Int +getApplyResultNumSubgoals = liftF1 Base.getApplyResultNumSubgoals + +getApplyResultSubgoal ::ApplyResult s -> Int -> Z3 s (Goal s) +getApplyResultSubgoal = liftF2 Base.getApplyResultSubgoal + +getApplyResultSubgoals ::ApplyResult s -> Z3 s [Goal s] +getApplyResultSubgoals = liftF1 Base.getApplyResultSubgoals + +mkGoal :: Bool -> Bool -> Bool -> Z3 s( Goal s) +mkGoal = liftF3 Base.mkGoal + +goalAssert ::Goal s -> AST s -> Z3 s () +goalAssert = liftF2 Base.goalAssert + +getGoalSize ::Goal s -> Z3 s Int +getGoalSize = liftF1 Base.getGoalSize + +getGoalFormula ::Goal s -> Int -> Z3 s (AST s) +getGoalFormula = liftF2 Base.getGoalFormula + +getGoalFormulas ::Goal s -> Z3 s [AST s] +getGoalFormulas = liftF1 Base.getGoalFormulas + +--------------------------------------------------------------------- +-- String Conversion + +-- | Set the mode for converting expressions to strings. +setASTPrintMode :: ASTPrintMode -> Z3 s () +setASTPrintMode = liftF1 Base.setASTPrintMode + +-- | Convert an (AST s) to a string. +astToString :: AST s -> Z3 s String +astToString = liftF1 Base.astToString + +-- | Convert a pattern to a string. +patternToString :: Pattern s -> Z3 s String +patternToString = liftF1 Base.patternToString + +-- | Convert a sort to a string. +sortToString :: Sort s -> Z3 s String +sortToString = liftF1 Base.sortToString + +-- | Convert a (FuncDecl s) to a string. +funcDeclToString :: FuncDecl s -> Z3 s String +funcDeclToString = liftF1 Base.funcDeclToString + +-- | Convert the given benchmark into SMT-LIB formatted string. +-- +-- The output format can be configured via 'setASTPrintMode'. +benchmarkToSMTLibString :: + String -- ^ name + -> String -- ^ logic + -> String -- ^ status + -> String -- ^ attributes + -> [AST s] -- ^ assumptions1 + -> AST s -- ^ formula + -> Z3 s String +benchmarkToSMTLibString = liftF6 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 :: + String -- ^ string to parse + -> [Symbol s] -- ^ sort names + -> [Sort s] -- ^ sorts + -> [Symbol s] -- ^ declaration names + -> [FuncDecl s] -- ^ declarations + -> Z3 s (AST s) +parseSMTLib2String = liftF5 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 :: + String -- ^ string to parse + -> [Symbol s] -- ^ sort names + -> [Sort s] -- ^ sorts + -> [Symbol s] -- ^ declaration names + -> [FuncDecl s] -- ^ declarations + -> Z3 s (AST s) +parseSMTLib2File = liftF5 Base.parseSMTLib2File + +getParserError :: Z3 s String +getParserError = liftF0 Base.getParserError + +--------------------------------------------------------------------- +-- Miscellaneous + +-- | Return Z3 version number information. +getVersion :: Z3 s Version +getVersion = Z3 . lift . unsafeIOToST $ Base.getVersion + +--------------------------------------------------------------------- +-- Fixedpoint + +fixedpointPush :: Z3 s () +fixedpointPush = liftFixedpoint0 Base.fixedpointPush + +fixedpointPop :: Z3 s () +fixedpointPop = liftFixedpoint0 Base.fixedpointPush + +fixedpointAddRule :: AST s -> Symbol s -> Z3 s () +fixedpointAddRule = liftFixedpoint2 Base.fixedpointAddRule + +fixedpointSetParams :: Params s -> Z3 s () +fixedpointSetParams = liftFixedpoint1 Base.fixedpointSetParams + +fixedpointRegisterRelation :: FuncDecl s -> Z3 s () +fixedpointRegisterRelation = liftFixedpoint1 Base.fixedpointRegisterRelation + +fixedpointQueryRelations :: [FuncDecl s] -> Z3 s Result +fixedpointQueryRelations = liftFixedpoint1 Base.fixedpointQueryRelations + +fixedpointGetAnswer :: Z3 s (AST s) +fixedpointGetAnswer = liftFixedpoint0 Base.fixedpointGetAnswer + +fixedpointGetAssertions :: Z3 s [AST s] +fixedpointGetAssertions = liftFixedpoint0 Base.fixedpointGetAssertions + +--------------------------------------------------------------------- +-- * Interpolation + +mkInterpolant :: AST s -> Z3 s (AST s) +mkInterpolant = liftF1 Base.mkInterpolant + +getInterpolant :: AST s -> AST s -> Params s -> Z3 s [AST s] +getInterpolant = liftF3 Base.getInterpolant + +computeInterpolant :: AST s -> Params s + -> Z3 s (Maybe (Either (Model s) [AST s])) +computeInterpolant = liftF2 Base.computeInterpolant + +readInterpolationProblem :: FilePath -> Z3 s (Either String Base.InterpolationProblem) +readInterpolationProblem = liftF1 Base.readInterpolationProblem + +checkInterpolant :: Base.InterpolationProblem -> [AST s] -> Z3 s (Result, Maybe String) +checkInterpolant = liftF2 Base.checkInterpolant + +interpolationProfile :: Z3 s String +interpolationProfile = liftF0 Base.interpolationProfile + +writeInterpolationProblem :: FilePath -> Base.InterpolationProblem -> Z3 s () +writeInterpolationProblem = liftF2 Base.writeInterpolationProblem + +--------------------------------------------------------------------- +-- * Solvers + +-- mkSolver :: Context s -> ST s (Solver s) +-- mkSolver = liftF0 z3_mk_solver + +-- mkSimpleSolver :: Context s -> ST s (Solver s) +-- mkSimpleSolver = liftF0 z3_mk_simple_solver + +-- mkSolverForLogic :: Context s -> Logic -> ST s (Solver s) +-- 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 :: Z3 s String +solverGetHelp = liftSolver0 Base.solverGetHelp + +-- | Set the solver using the given parameters. +solverSetParams :: Params s -> Z3 s () +solverSetParams = liftSolver1 Base.solverSetParams + +-- | Create a backtracking point. +solverPush :: Z3 s () +solverPush = liftSolver0 Base.solverPush + +-- | Backtrack /n/ backtracking points. +solverPop :: Int -> Z3 s () +solverPop = liftSolver1 Base.solverPop + +solverReset :: Z3 s () +solverReset = liftSolver0 Base.solverReset + +-- | Number of backtracking points. +solverGetNumScopes :: Z3 s Int +solverGetNumScopes = liftSolver0 Base.solverGetNumScopes + +-- | Assert a constraing into the logical context. +-- +-- Reference: +solverAssertCnstr :: AST s -> Z3 s () +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 :: AST s -> AST s -> Z3 s () +solverAssertAndTrack = liftSolver2 Base.solverAssertAndTrack + +-- | Check whether the assertions in a given solver are consistent or not. +solverCheck :: Z3 s Result +solverCheck = liftSolver0 Base.solverCheck + +-- | Check whether the assertions in the given solver and optional assumptions are consistent or not. +solverCheckAssumptions :: [AST s] -> Z3 s 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 :: Z3 s (Model s) +solverGetModel = liftSolver0 Base.solverGetModel + +-- | Retrieve the unsat core for the last 'solverCheckAssumptions'; the unsat core is a subset of the assumptions +solverGetUnsatCore :: Z3 s [AST s] +solverGetUnsatCore = liftSolver0 Base.solverGetUnsatCore + +-- | Return a brief justification for an 'Unknown' result for the commands 'solverCheck' and 'solverCheckAssumptions'. +solverGetReasonUnknown :: Z3 s String +solverGetReasonUnknown = liftSolver0 Base.solverGetReasonUnknown + +-- | Convert the given solver into a string. +solverToString :: Z3 s String +solverToString = liftSolver0 Base.solverToString + +------------------------------------------------- +-- ** Helpers + +-- | Create a backtracking point. +-- +-- For @push; m; pop 1@ see 'local'. +push :: Z3 s () +push = solverPush + +-- | Backtrack /n/ backtracking points. +-- +-- Contrary to 'solverPop' this funtion checks whether /n/ is within +-- the size of the solver scope stack. +pop :: Int -> Z3 s () +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 :: Z3 s a -> Z3 s a +local q = do + push + r <- q + pop 1 + return r + +-- | Backtrack all the way. +reset :: Z3 s () +reset = solverReset + +-- | Get number of backtracking points. +getNumScopes :: Z3 s Int +getNumScopes = liftSolver0 Base.solverGetNumScopes + +assert :: AST s -> Z3 s () +assert = solverAssertCnstr + +-- | Check whether the given logical context is consistent or not. +check :: Z3 s Result +check = solverCheck + +-- | Check whether the assertions in the given solver and optional assumptions are consistent or not. +checkAssumptions :: [AST s] -> Z3 s Result +checkAssumptions = solverCheckAssumptions + +solverCheckAndGetModel :: Z3 s (Result, Maybe (Model s)) +solverCheckAndGetModel = liftSolver0 Base.solverCheckAndGetModel + +-- | Get model. +-- +-- Reference : +getModel :: Z3 s (Result, Maybe (Model s)) +getModel = solverCheckAndGetModel + +-- | Check satisfiability and, if /sat/, compute a value from the given model. +-- +-- E.g. +-- @ +-- withModel $ \\m -> +-- fromJust \<$\> evalInt m x +-- @ +withModel :: (Model s -> Z3 s a) -> Z3 s (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 :: Z3 s [AST s] +getUnsatCore = solverGetUnsatCore + +newtype Config s = Config { _unConfig :: Base.Config } deriving (Eq) +newtype Context s = Context { _unContext :: Base.Context } deriving (Eq) +newtype Symbol s = Symbol { _unSymbol :: Base.Symbol } deriving (Eq, Ord, Show, Storable) +newtype AST s = AST { _unAST :: Base.AST } deriving (Eq, Ord, Show) +newtype Sort s = Sort { _unSort :: Base.Sort } deriving (Eq, Ord, Show) +newtype FuncDecl s = FuncDecl { _unFuncDecl :: Base.FuncDecl } deriving (Eq, Ord, Show) +newtype App s = App { _unApp :: Base.App } deriving (Eq, Ord, Show) +newtype Pattern s = Pattern { _unPattern :: Base.Pattern } deriving (Eq, Ord, Show) +newtype Constructor s = Constructor { _unConstructor :: Base.Constructor } deriving (Eq, Ord, Show) +newtype Model s = Model { _unModel :: Base.Model } deriving (Eq) +newtype FuncInterp s = FuncInterp { _unFuncInterp :: Base.FuncInterp } deriving (Eq) +newtype FuncEntry s = FuncEntry { _unFuncEntry :: Base.FuncEntry } deriving (Eq) +newtype Tactic s = Tactic { _unTactic :: Base.Tactic } deriving (Eq) +newtype Goal s = Goal { _unGoal :: Base.Goal } deriving (Eq) +newtype ApplyResult s = ApplyResult { _unApplyResult :: Base.ApplyResult } deriving (Eq) +newtype Params s = Params { _unParams :: Base.Params } deriving (Eq) +newtype Solver s = Solver { _unSolver :: Base.Solver } deriving (Eq) +newtype Fixedpoint s = Fixedpoint { _unFixedpoint :: Base.Fixedpoint } deriving (Eq) diff --git a/ez3.cabal b/ez3.cabal new file mode 100644 --- /dev/null +++ b/ez3.cabal @@ -0,0 +1,42 @@ +name: ez3 +version: 0.1.0.0 +synopsis: Z3 bonds with pure interface +description: Z3 bonds with universally-quantified pure interface, like `ST` +license: BSD3 +license-file: LICENSE +author: M Farkas-Dyck +maintainer: strake888@gmail.com +copyright: 2018 M Farkas-Dyck +-- category: +build-type: Simple +extra-source-files: README.md +cabal-version: >=1.10 + +library + hs-source-dirs: . + exposed-modules: Z3.Tagged + build-depends: base >= 4.7 && < 5 + , transformers + , z3 + default-language: Haskell2010 + default-extensions: UnicodeSyntax + , LambdaCase + , EmptyCase + , InstanceSigs + , PartialTypeSignatures + , PolyKinds + , ConstraintKinds + , FlexibleContexts + , FlexibleInstances + , StandaloneDeriving + , GeneralizedNewtypeDeriving + , DeriveFunctor + , DeriveFoldable + , DeriveTraversable + , OverloadedStrings + ghc-options: -Wall -Wcompat -Wredundant-constraints -Wno-name-shadowing + -Wincomplete-record-updates -Wincomplete-uni-patterns + +source-repository head + type: git + location: https://github.com/strake/ez3.hs