| Copyright | (c) Iago Abal 2013-2015 (c) David Castro 2013-2015 |
|---|---|
| License | BSD3 |
| Maintainer | Iago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com> |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Z3.Monad
Contents
- Z3 monad
- Types
- Parameters
- Symbols
- Sorts
- Constants and Applications
- Propositional Logic and Equality
- Arithmetic: Integers and Reals
- Bit-vectors
- Arrays
- Sets
- Numerals
- Sequences and regular expressions
- Quantifiers
- Accessors
- Modifiers
- Models
- Tactics
- String Conversion
- Parser interface
- Error Handling
- Miscellaneous
- Fixedpoint
- Floating-Point Arithmetic
- Z3-specific floating-point extensions
- Optimization
- Solvers
Description
A simple monadic interface to Z3 API.
Examples: https://bitbucket.org/iago/z3-haskell/src/tip/examples/Example/Monad
Synopsis
- class (Applicative m, Monad m, MonadIO m) => MonadZ3 m where
- getSolver :: m Solver
- getContext :: m Context
- data Z3 a
- module Z3.Opts
- data Logic
- evalZ3 :: Z3 a -> IO a
- evalZ3With :: Maybe Logic -> Opts -> Z3 a -> IO a
- data Z3Env
- newEnv :: Maybe Logic -> Opts -> IO Z3Env
- evalZ3WithEnv :: Z3 a -> Z3Env -> IO a
- data Symbol
- data AST
- data Sort
- data FuncDecl
- data App
- data Pattern
- data Constructor
- data Model
- data Context
- data FuncInterp
- data FuncEntry
- data Params
- data Solver
- data SortKind
- data ASTKind
- data Result
- mkParams :: MonadZ3 z3 => z3 Params
- paramsSetBool :: MonadZ3 z3 => Params -> Symbol -> Bool -> z3 ()
- paramsSetUInt :: MonadZ3 z3 => Params -> Symbol -> Word -> z3 ()
- paramsSetDouble :: MonadZ3 z3 => Params -> Symbol -> Double -> z3 ()
- paramsSetSymbol :: MonadZ3 z3 => Params -> Symbol -> Symbol -> z3 ()
- paramsToString :: MonadZ3 z3 => Params -> z3 String
- mkIntSymbol :: (MonadZ3 z3, Integral i) => i -> z3 Symbol
- mkStringSymbol :: MonadZ3 z3 => String -> z3 Symbol
- mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort
- mkBoolSort :: MonadZ3 z3 => z3 Sort
- mkIntSort :: MonadZ3 z3 => z3 Sort
- mkRealSort :: MonadZ3 z3 => z3 Sort
- mkBvSort :: MonadZ3 z3 => Int -> z3 Sort
- mkFiniteDomainSort :: MonadZ3 z3 => Symbol -> Word64 -> z3 Sort
- mkArraySort :: MonadZ3 z3 => Sort -> Sort -> z3 Sort
- mkTupleSort :: MonadZ3 z3 => Symbol -> [(Symbol, Sort)] -> z3 (Sort, FuncDecl, [FuncDecl])
- mkConstructor :: MonadZ3 z3 => Symbol -> Symbol -> [(Symbol, Maybe Sort, Int)] -> z3 Constructor
- mkDatatype :: MonadZ3 z3 => Symbol -> [Constructor] -> z3 Sort
- mkDatatypes :: MonadZ3 z3 => [Symbol] -> [[Constructor]] -> z3 [Sort]
- mkSetSort :: MonadZ3 z3 => Sort -> z3 Sort
- mkFuncDecl :: MonadZ3 z3 => Symbol -> [Sort] -> Sort -> z3 FuncDecl
- mkApp :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST
- mkConst :: MonadZ3 z3 => Symbol -> Sort -> z3 AST
- mkFreshConst :: MonadZ3 z3 => String -> Sort -> z3 AST
- mkFreshFuncDecl :: MonadZ3 z3 => String -> [Sort] -> Sort -> z3 FuncDecl
- mkRecFuncDecl :: MonadZ3 z3 => Symbol -> [Sort] -> Sort -> z3 FuncDecl
- addRecDef :: MonadZ3 z3 => FuncDecl -> [AST] -> AST -> z3 ()
- mkVar :: MonadZ3 z3 => Symbol -> Sort -> z3 AST
- mkBoolVar :: MonadZ3 z3 => Symbol -> z3 AST
- mkRealVar :: MonadZ3 z3 => Symbol -> z3 AST
- mkIntVar :: MonadZ3 z3 => Symbol -> z3 AST
- mkBvVar :: MonadZ3 z3 => Symbol -> Int -> z3 AST
- mkFreshVar :: MonadZ3 z3 => String -> Sort -> z3 AST
- mkFreshBoolVar :: MonadZ3 z3 => String -> z3 AST
- mkFreshRealVar :: MonadZ3 z3 => String -> z3 AST
- mkFreshIntVar :: MonadZ3 z3 => String -> z3 AST
- mkFreshBvVar :: MonadZ3 z3 => String -> Int -> z3 AST
- mkTrue :: MonadZ3 z3 => z3 AST
- mkFalse :: MonadZ3 z3 => z3 AST
- mkEq :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkNot :: MonadZ3 z3 => AST -> z3 AST
- mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
- mkIff :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkImplies :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkXor :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkAnd :: MonadZ3 z3 => [AST] -> z3 AST
- mkOr :: MonadZ3 z3 => [AST] -> z3 AST
- mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST
- mkDistinct1 :: MonadZ3 z3 => NonEmpty AST -> z3 AST
- mkBool :: MonadZ3 z3 => Bool -> z3 AST
- mkAdd :: MonadZ3 z3 => [AST] -> z3 AST
- mkMul :: MonadZ3 z3 => [AST] -> z3 AST
- mkSub :: MonadZ3 z3 => [AST] -> z3 AST
- mkSub1 :: MonadZ3 z3 => NonEmpty AST -> z3 AST
- mkUnaryMinus :: MonadZ3 z3 => AST -> z3 AST
- mkDiv :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkMod :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkRem :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkPower :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkLt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkLe :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkGt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkGe :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkInt2Real :: MonadZ3 z3 => AST -> z3 AST
- mkReal2Int :: MonadZ3 z3 => AST -> z3 AST
- mkIsInt :: MonadZ3 z3 => AST -> z3 AST
- mkBvnot :: MonadZ3 z3 => AST -> z3 AST
- mkBvredand :: MonadZ3 z3 => AST -> z3 AST
- mkBvredor :: MonadZ3 z3 => AST -> z3 AST
- mkBvand :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvor :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvxor :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvnand :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvnor :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvxnor :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvneg :: MonadZ3 z3 => AST -> z3 AST
- mkBvadd :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsub :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvmul :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvudiv :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsdiv :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvurem :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvult :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvslt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvule :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsle :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvuge :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvugt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsgt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkConcat :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkExtract :: MonadZ3 z3 => Int -> Int -> AST -> z3 AST
- mkSignExt :: MonadZ3 z3 => Int -> AST -> z3 AST
- mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 AST
- mkRepeat :: MonadZ3 z3 => Int -> AST -> z3 AST
- mkBvshl :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvlshr :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvashr :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkRotateLeft :: MonadZ3 z3 => Int -> AST -> z3 AST
- mkRotateRight :: MonadZ3 z3 => Int -> AST -> z3 AST
- mkExtRotateLeft :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkInt2bv :: MonadZ3 z3 => Int -> AST -> z3 AST
- mkBv2int :: MonadZ3 z3 => AST -> Bool -> z3 AST
- mkBvnegNoOverflow :: MonadZ3 z3 => AST -> z3 AST
- mkBvaddNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST
- mkBvaddNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsubNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsubNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvmulNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST
- mkBvmulNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkBvsdivNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkStore :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
- mkConstArray :: MonadZ3 z3 => Sort -> AST -> z3 AST
- mkMap :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST
- mkArrayDefault :: MonadZ3 z3 => AST -> z3 AST
- mkEmptySet :: MonadZ3 z3 => Sort -> z3 AST
- mkFullSet :: MonadZ3 z3 => Sort -> z3 AST
- mkSetAdd :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkSetDel :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkSetUnion :: MonadZ3 z3 => [AST] -> z3 AST
- mkSetIntersect :: MonadZ3 z3 => [AST] -> z3 AST
- mkSetDifference :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkSetComplement :: MonadZ3 z3 => AST -> z3 AST
- mkSetMember :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkSetSubset :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkNumeral :: MonadZ3 z3 => String -> Sort -> z3 AST
- mkInt :: MonadZ3 z3 => Int -> Sort -> z3 AST
- mkReal :: MonadZ3 z3 => Int -> Int -> z3 AST
- mkUnsignedInt :: MonadZ3 z3 => Word -> Sort -> z3 AST
- mkInt64 :: MonadZ3 z3 => Int64 -> Sort -> z3 AST
- mkUnsignedInt64 :: MonadZ3 z3 => Word64 -> Sort -> z3 AST
- mkIntegral :: (MonadZ3 z3, Integral a) => a -> Sort -> z3 AST
- mkRational :: MonadZ3 z3 => Rational -> z3 AST
- mkFixed :: (MonadZ3 z3, HasResolution a) => Fixed a -> z3 AST
- mkRealNum :: (MonadZ3 z3, Real r) => r -> z3 AST
- mkInteger :: MonadZ3 z3 => Integer -> z3 AST
- mkIntNum :: (MonadZ3 z3, Integral a) => a -> z3 AST
- mkBitvector :: MonadZ3 z3 => Int -> Integer -> z3 AST
- mkBvNum :: (MonadZ3 z3, Integral i) => Int -> i -> z3 AST
- mkSeqSort :: MonadZ3 z3 => Sort -> z3 Sort
- isSeqSort :: MonadZ3 z3 => Sort -> z3 Bool
- mkReSort :: MonadZ3 z3 => Sort -> z3 Sort
- isReSort :: MonadZ3 z3 => Sort -> z3 Bool
- mkStringSort :: MonadZ3 z3 => z3 Sort
- isStringSort :: MonadZ3 z3 => Sort -> z3 Bool
- mkString :: MonadZ3 z3 => String -> z3 AST
- isString :: MonadZ3 z3 => AST -> z3 Bool
- getString :: MonadZ3 z3 => AST -> z3 String
- mkSeqEmpty :: MonadZ3 z3 => Sort -> z3 AST
- mkSeqUnit :: MonadZ3 z3 => AST -> z3 AST
- mkSeqConcat :: MonadZ3 z3 => [AST] -> z3 AST
- mkSeqPrefix :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkSeqSuffix :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkSeqContains :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkStrLt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkStrLe :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkSeqExtract :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
- mkSeqReplace :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
- mkSeqAt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkSeqLength :: MonadZ3 z3 => AST -> z3 AST
- mkSeqIndex :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
- mkStrToInt :: MonadZ3 z3 => AST -> z3 AST
- mkIntToStr :: MonadZ3 z3 => AST -> z3 AST
- mkSeqToRe :: MonadZ3 z3 => AST -> z3 AST
- mkSeqInRe :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkRePlus :: MonadZ3 z3 => AST -> z3 AST
- mkReStar :: MonadZ3 z3 => AST -> z3 AST
- mkReOption :: MonadZ3 z3 => AST -> z3 AST
- mkReUnion :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST
- mkReConcat :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST
- mkReRange :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkReLoop :: (Integral int, MonadZ3 z3) => AST -> int -> int -> z3 AST
- mkReIntersect :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST
- mkReComplement :: MonadZ3 z3 => AST -> z3 AST
- mkReEmpty :: MonadZ3 z3 => Sort -> z3 AST
- mkReFull :: MonadZ3 z3 => Sort -> z3 AST
- mkPattern :: MonadZ3 z3 => [AST] -> z3 Pattern
- mkBound :: MonadZ3 z3 => Int -> Sort -> z3 AST
- mkForall :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST
- mkForallW :: MonadZ3 z3 => Int -> [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST
- mkExists :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST
- mkExistsW :: MonadZ3 z3 => Int -> [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST
- mkForallConst :: MonadZ3 z3 => [Pattern] -> [App] -> AST -> z3 AST
- mkForallWConst :: MonadZ3 z3 => Int -> [Pattern] -> [App] -> AST -> z3 AST
- mkExistsConst :: MonadZ3 z3 => [Pattern] -> [App] -> AST -> z3 AST
- mkExistsWConst :: MonadZ3 z3 => Int -> [Pattern] -> [App] -> AST -> z3 AST
- getSymbolString :: MonadZ3 z3 => Symbol -> z3 String
- getSortName :: MonadZ3 z3 => Sort -> z3 Symbol
- getSortId :: MonadZ3 z3 => Sort -> z3 Int
- sortToAst :: MonadZ3 z3 => Sort -> z3 AST
- isEqSort :: MonadZ3 z3 => Sort -> Sort -> z3 Bool
- getSortKind :: MonadZ3 z3 => Sort -> z3 SortKind
- getBvSortSize :: MonadZ3 z3 => Sort -> z3 Int
- getTupleSortMkDecl :: MonadZ3 z3 => Sort -> z3 FuncDecl
- getTupleSortNumFields :: MonadZ3 z3 => Sort -> z3 Int
- getTupleSortFieldDecl :: MonadZ3 z3 => Sort -> Int -> z3 FuncDecl
- getDatatypeSortConstructors :: MonadZ3 z3 => Sort -> z3 [FuncDecl]
- getDatatypeSortRecognizers :: MonadZ3 z3 => Sort -> z3 [FuncDecl]
- getDatatypeSortConstructorAccessors :: MonadZ3 z3 => Sort -> z3 [[FuncDecl]]
- mkAtMost :: MonadZ3 z3 => [AST] -> Int -> z3 AST
- mkAtLeast :: MonadZ3 z3 => [AST] -> Int -> z3 AST
- getDeclName :: MonadZ3 z3 => FuncDecl -> z3 Symbol
- getArity :: MonadZ3 z3 => FuncDecl -> z3 Int
- getDomain :: MonadZ3 z3 => FuncDecl -> Int -> z3 Sort
- getRange :: MonadZ3 z3 => FuncDecl -> z3 Sort
- appToAst :: MonadZ3 z3 => App -> z3 AST
- getAppDecl :: MonadZ3 z3 => App -> z3 FuncDecl
- getAppNumArgs :: MonadZ3 z3 => App -> z3 Int
- getAppArg :: MonadZ3 z3 => App -> Int -> z3 AST
- getAppArgs :: MonadZ3 z3 => App -> z3 [AST]
- getSort :: MonadZ3 z3 => AST -> z3 Sort
- getArraySortDomain :: MonadZ3 z3 => Sort -> z3 Sort
- getArraySortRange :: MonadZ3 z3 => Sort -> z3 Sort
- getBoolValue :: MonadZ3 z3 => AST -> z3 (Maybe Bool)
- getAstKind :: MonadZ3 z3 => AST -> z3 ASTKind
- isApp :: MonadZ3 z3 => AST -> z3 Bool
- toApp :: MonadZ3 z3 => AST -> z3 App
- getNumeralString :: MonadZ3 z3 => AST -> z3 String
- getNumerator :: MonadZ3 z3 => AST -> z3 AST
- getDenominator :: MonadZ3 z3 => AST -> z3 AST
- simplify :: MonadZ3 z3 => AST -> z3 AST
- simplifyEx :: MonadZ3 z3 => AST -> Params -> z3 AST
- getIndexValue :: MonadZ3 z3 => AST -> z3 Int
- isQuantifierForall :: MonadZ3 z3 => AST -> z3 Bool
- isQuantifierExists :: MonadZ3 z3 => AST -> z3 Bool
- getQuantifierWeight :: MonadZ3 z3 => AST -> z3 Int
- getQuantifierNumPatterns :: MonadZ3 z3 => AST -> z3 Int
- getQuantifierPatternAST :: MonadZ3 z3 => AST -> Int -> z3 AST
- getQuantifierPatterns :: MonadZ3 z3 => AST -> z3 [AST]
- getQuantifierNumNoPatterns :: MonadZ3 z3 => AST -> z3 Int
- getQuantifierNoPatternAST :: MonadZ3 z3 => AST -> Int -> z3 AST
- getQuantifierNoPatterns :: MonadZ3 z3 => AST -> z3 [AST]
- getQuantifierNumBound :: MonadZ3 z3 => AST -> z3 Int
- getQuantifierBoundName :: MonadZ3 z3 => AST -> Int -> z3 Symbol
- getQuantifierBoundSort :: MonadZ3 z3 => AST -> Int -> z3 Sort
- getQuantifierBoundVars :: MonadZ3 z3 => AST -> z3 [AST]
- getQuantifierBody :: MonadZ3 z3 => AST -> z3 AST
- getBool :: MonadZ3 z3 => AST -> z3 Bool
- getInt :: MonadZ3 z3 => AST -> z3 Integer
- getReal :: MonadZ3 z3 => AST -> z3 Rational
- substituteVars :: MonadZ3 z3 => AST -> [AST] -> z3 AST
- substitute :: MonadZ3 z3 => AST -> [(AST, AST)] -> z3 AST
- modelTranslate :: MonadZ3 z3 => Model -> Context -> z3 Model
- modelEval :: MonadZ3 z3 => Model -> AST -> Bool -> z3 (Maybe AST)
- evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel)
- getConstInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe AST)
- getFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncInterp)
- hasInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 Bool
- numConsts :: MonadZ3 z3 => Model -> z3 Word
- numFuncs :: MonadZ3 z3 => Model -> z3 Word
- getConstDecl :: MonadZ3 z3 => Model -> Word -> z3 FuncDecl
- getFuncDecl :: MonadZ3 z3 => Model -> Word -> z3 FuncDecl
- getConsts :: MonadZ3 z3 => Model -> z3 [FuncDecl]
- getFuncs :: MonadZ3 z3 => Model -> z3 [FuncDecl]
- isAsArray :: MonadZ3 z3 => AST -> z3 Bool
- isEqAST :: MonadZ3 z3 => AST -> AST -> z3 Bool
- addFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 FuncInterp
- addConstInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 ()
- getAsArrayFuncDecl :: MonadZ3 z3 => AST -> z3 FuncDecl
- funcInterpGetNumEntries :: MonadZ3 z3 => FuncInterp -> z3 Int
- funcInterpGetEntry :: MonadZ3 z3 => FuncInterp -> Int -> z3 FuncEntry
- funcInterpGetElse :: MonadZ3 z3 => FuncInterp -> z3 AST
- funcInterpGetArity :: MonadZ3 z3 => FuncInterp -> z3 Int
- funcEntryGetValue :: MonadZ3 z3 => FuncEntry -> z3 AST
- funcEntryGetNumArgs :: MonadZ3 z3 => FuncEntry -> z3 Int
- funcEntryGetArg :: MonadZ3 z3 => FuncEntry -> Int -> z3 AST
- modelToString :: MonadZ3 z3 => Model -> z3 String
- showModel :: MonadZ3 z3 => Model -> z3 String
- type EvalAst m a = Model -> AST -> m (Maybe a)
- eval :: MonadZ3 z3 => EvalAst z3 AST
- evalBool :: MonadZ3 z3 => EvalAst z3 Bool
- evalInt :: MonadZ3 z3 => EvalAst z3 Integer
- evalReal :: MonadZ3 z3 => EvalAst z3 Rational
- evalBv :: MonadZ3 z3 => Bool -> EvalAst z3 Integer
- evalT :: (MonadZ3 z3, Traversable t) => Model -> t AST -> z3 (Maybe (t AST))
- mapEval :: (MonadZ3 z3, Traversable t) => EvalAst z3 a -> Model -> t AST -> z3 (Maybe (t a))
- data FuncModel = FuncModel {
- interpMap :: [([AST], AST)]
- interpElse :: AST
- evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel)
- mkTactic :: MonadZ3 z3 => String -> z3 Tactic
- andThenTactic :: MonadZ3 z3 => Tactic -> Tactic -> z3 Tactic
- orElseTactic :: MonadZ3 z3 => Tactic -> Tactic -> z3 Tactic
- skipTactic :: MonadZ3 z3 => z3 Tactic
- tryForTactic :: MonadZ3 z3 => Tactic -> Int -> z3 Tactic
- tacticUsingParams :: MonadZ3 z3 => Tactic -> Params -> z3 Tactic
- repeatTactic :: MonadZ3 z3 => Tactic -> Int -> z3 Tactic
- mkQuantifierEliminationTactic :: MonadZ3 z3 => z3 Tactic
- mkAndInverterGraphTactic :: MonadZ3 z3 => z3 Tactic
- applyTactic :: MonadZ3 z3 => Tactic -> Goal -> z3 ApplyResult
- applyResultToString :: MonadZ3 z3 => ApplyResult -> z3 String
- getApplyResultNumSubgoals :: MonadZ3 z3 => ApplyResult -> z3 Int
- getApplyResultSubgoal :: MonadZ3 z3 => ApplyResult -> Int -> z3 Goal
- getApplyResultSubgoals :: MonadZ3 z3 => ApplyResult -> z3 [Goal]
- mkGoal :: MonadZ3 z3 => Bool -> Bool -> Bool -> z3 Goal
- goalAssert :: MonadZ3 z3 => Goal -> AST -> z3 ()
- getGoalSize :: MonadZ3 z3 => Goal -> z3 Int
- getGoalFormula :: MonadZ3 z3 => Goal -> Int -> z3 AST
- getGoalFormulas :: MonadZ3 z3 => Goal -> z3 [AST]
- goalToString :: MonadZ3 z3 => Goal -> z3 String
- convertModel :: MonadZ3 z3 => Goal -> Model -> z3 Model
- data ASTPrintMode
- setASTPrintMode :: MonadZ3 z3 => ASTPrintMode -> z3 ()
- astToString :: MonadZ3 z3 => AST -> z3 String
- patternToString :: MonadZ3 z3 => Pattern -> z3 String
- sortToString :: MonadZ3 z3 => Sort -> z3 String
- funcDeclToString :: MonadZ3 z3 => FuncDecl -> z3 String
- benchmarkToSMTLibString :: MonadZ3 z3 => String -> String -> String -> String -> [AST] -> AST -> z3 String
- parseSMTLib2String :: MonadZ3 z3 => String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> z3 [AST]
- parseSMTLib2File :: MonadZ3 z3 => String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> z3 [AST]
- evalSMTLib2String :: MonadZ3 z3 => String -> z3 String
- data Z3Error = Z3Error {
- errCode :: Z3ErrorCode
- errMsg :: String
- data Z3ErrorCode
- data Version = Version {}
- getVersion :: MonadZ3 z3 => z3 Version
- class MonadZ3 m => MonadFixedpoint m where
- getFixedpoint :: m Fixedpoint
- data Fixedpoint
- fixedpointAddRule :: MonadFixedpoint z3 => AST -> Symbol -> z3 ()
- fixedpointSetParams :: MonadFixedpoint z3 => Params -> z3 ()
- fixedpointRegisterRelation :: MonadFixedpoint z3 => FuncDecl -> z3 ()
- fixedpointQueryRelations :: MonadFixedpoint z3 => [FuncDecl] -> z3 Result
- fixedpointGetAnswer :: MonadFixedpoint z3 => z3 AST
- fixedpointGetAssertions :: MonadFixedpoint z3 => z3 [AST]
- mkFpaRoundingModeSort :: MonadZ3 z3 => z3 Sort
- mkFpaRoundNearestTiesToEven :: MonadZ3 z3 => z3 AST
- mkFpaRne :: MonadZ3 z3 => z3 AST
- mkFpaRoundNearestTiesToAway :: MonadZ3 z3 => z3 AST
- mkFpaRna :: MonadZ3 z3 => z3 AST
- mkFpaRoundTowardPositive :: MonadZ3 z3 => z3 AST
- mkFpaRtp :: MonadZ3 z3 => z3 AST
- mkFpaRoundTowardNegative :: MonadZ3 z3 => z3 AST
- mkFpaRtn :: MonadZ3 z3 => z3 AST
- mkFpaRoundTowardZero :: MonadZ3 z3 => z3 AST
- mkFpaRtz :: MonadZ3 z3 => z3 AST
- mkFpaSort :: (MonadZ3 z3, Integral int) => int -> int -> z3 Sort
- mkFpaSortHalf :: MonadZ3 z3 => z3 Sort
- mkFpaSort16 :: MonadZ3 z3 => z3 Sort
- mkFpaSortSingle :: MonadZ3 z3 => z3 Sort
- mkFpaSort32 :: MonadZ3 z3 => z3 Sort
- mkFpaSortDouble :: MonadZ3 z3 => z3 Sort
- mkFpaSort64 :: MonadZ3 z3 => z3 Sort
- mkFpaSortQuadruple :: MonadZ3 z3 => z3 Sort
- mkFpaSort128 :: MonadZ3 z3 => z3 Sort
- mkFpaNaN :: MonadZ3 z3 => Sort -> z3 AST
- mkFpaInf :: MonadZ3 z3 => Sort -> Bool -> z3 AST
- mkFpaZero :: MonadZ3 z3 => Sort -> Bool -> z3 AST
- mkFpaFp :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
- mkFpaNumeralFloat :: MonadZ3 z3 => Float -> Sort -> z3 AST
- mkFpaNumeralDouble :: MonadZ3 z3 => Double -> Sort -> z3 AST
- mkFpaNumeralInt :: (MonadZ3 z3, Integral int) => int -> Sort -> z3 AST
- mkFpaNumeralIntUInt :: (MonadZ3 z3, Integral int) => Bool -> int -> int -> Sort -> z3 AST
- mkFpaNumeralInt64UInt64 :: (MonadZ3 z3, Integral int) => Bool -> int -> int -> Sort -> z3 AST
- mkFpaAbs :: MonadZ3 z3 => AST -> z3 AST
- mkFpaNeg :: MonadZ3 z3 => AST -> z3 AST
- mkFpaAdd :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
- mkFpaSub :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
- mkFpaMul :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
- mkFpaDiv :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST
- mkFpaFma :: MonadZ3 z3 => AST -> AST -> AST -> AST -> z3 AST
- mkFpaSqrt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkFpaRem :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkFpaRoundToIntegral :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkFpaMin :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkFpaMax :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkFpaLeq :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkFpaLt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkFpaGeq :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkFpaGt :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkFpaEq :: MonadZ3 z3 => AST -> AST -> z3 AST
- mkFpaIsNormal :: MonadZ3 z3 => AST -> z3 AST
- mkFpaIsSubnormal :: MonadZ3 z3 => AST -> z3 AST
- mkFpaIsZero :: MonadZ3 z3 => AST -> z3 AST
- mkFpaIsInfinite :: MonadZ3 z3 => AST -> z3 AST
- mkFpaIsNaN :: MonadZ3 z3 => AST -> z3 AST
- mkFpaIsNegative :: MonadZ3 z3 => AST -> z3 AST
- mkFpaIsPositive :: MonadZ3 z3 => AST -> z3 AST
- mkFpaToFpBv :: MonadZ3 z3 => AST -> Sort -> z3 AST
- mkFpaToFpFloat :: MonadZ3 z3 => AST -> AST -> Sort -> z3 AST
- mkFpaToFpReal :: MonadZ3 z3 => AST -> AST -> Sort -> z3 AST
- mkFpaToFpSigned :: MonadZ3 z3 => AST -> AST -> Sort -> z3 AST
- mkFpaToFpUnsigned :: MonadZ3 z3 => AST -> AST -> Sort -> z3 AST
- mkFpaToUbv :: (MonadZ3 z3, Integral int) => AST -> AST -> int -> z3 AST
- mkFpaToSbv :: (MonadZ3 z3, Integral int) => AST -> AST -> int -> z3 AST
- mkFpaToReal :: MonadZ3 z3 => AST -> z3 AST
- fpaGetEbits :: (MonadZ3 z3, Integral int) => Sort -> z3 int
- fpaGetSbits :: (MonadZ3 z3, Integral int) => Sort -> z3 int
- fpaIsNumeralNaN :: MonadZ3 z3 => AST -> z3 Bool
- fpaIsNumeralInf :: MonadZ3 z3 => AST -> z3 Bool
- fpaIsNumeralZero :: MonadZ3 z3 => AST -> z3 Bool
- fpaIsNumeralNormal :: MonadZ3 z3 => AST -> z3 Bool
- fpaIsNumeralSubnormal :: MonadZ3 z3 => AST -> z3 Bool
- fpaIsNumeralPositive :: MonadZ3 z3 => AST -> z3 Bool
- fpaIsNumeralNegative :: MonadZ3 z3 => AST -> z3 Bool
- fpaGetNumeralSignBv :: MonadZ3 z3 => AST -> z3 AST
- fpaGetNumeralSignificandBv :: MonadZ3 z3 => AST -> z3 AST
- fpaGetNumeralSignificandString :: MonadZ3 z3 => AST -> z3 String
- fpaGetNumeralExponentString :: MonadZ3 z3 => AST -> Bool -> z3 String
- fpaGetNumeralExponentBv :: MonadZ3 z3 => AST -> Bool -> z3 AST
- mkFpaToIEEEBv :: MonadZ3 z3 => AST -> z3 AST
- mkFpaToFpIntReal :: MonadZ3 z3 => AST -> AST -> AST -> Sort -> z3 AST
- class MonadZ3 m => MonadOptimize m where
- getOptimize :: m Optimize
- data Optimize
- optimizeAssert :: MonadOptimize z3 => AST -> z3 ()
- optimizeAssertAndTrack :: MonadOptimize z3 => AST -> AST -> z3 ()
- optimizeAssertSoft :: MonadOptimize z3 => AST -> String -> Symbol -> z3 Int
- optimizeMaximize :: MonadOptimize z3 => AST -> z3 Int
- optimizeMinimize :: MonadOptimize z3 => AST -> z3 Int
- optimizePush :: MonadOptimize z3 => z3 ()
- optimizePop :: MonadOptimize z3 => z3 ()
- optimizeCheck :: MonadOptimize z3 => [AST] -> z3 Result
- optimizeGetReasonUnknown :: MonadOptimize z3 => z3 String
- optimizeGetModel :: MonadOptimize z3 => z3 Model
- optimizeGetUnsatCore :: MonadOptimize z3 => z3 [AST]
- optimizeSetParams :: MonadOptimize z3 => Params -> z3 ()
- optimizeGetLower :: MonadOptimize z3 => Int -> z3 AST
- optimizeGetUpper :: MonadOptimize z3 => Int -> z3 AST
- optimizeGetUpperAsVector :: MonadOptimize z3 => Int -> z3 [AST]
- optimizeGetLowerAsVector :: MonadOptimize z3 => Int -> z3 [AST]
- optimizeToString :: MonadOptimize z3 => z3 String
- optimizeFromString :: MonadOptimize z3 => String -> z3 ()
- optimizeFromFile :: MonadOptimize z3 => String -> z3 ()
- optimizeGetHelp :: MonadOptimize z3 => z3 String
- optimizeGetAssertions :: MonadOptimize z3 => z3 [AST]
- optimizeGetObjectives :: MonadOptimize z3 => z3 [AST]
- solverGetHelp :: MonadZ3 z3 => z3 String
- solverSetParams :: MonadZ3 z3 => Params -> z3 ()
- solverPush :: MonadZ3 z3 => z3 ()
- solverPop :: MonadZ3 z3 => Int -> z3 ()
- solverReset :: MonadZ3 z3 => z3 ()
- solverGetNumScopes :: MonadZ3 z3 => z3 Int
- solverAssertCnstr :: MonadZ3 z3 => AST -> z3 ()
- solverAssertAndTrack :: MonadZ3 z3 => AST -> AST -> z3 ()
- solverGetAssertions :: MonadZ3 z3 => z3 [AST]
- solverCheck :: MonadZ3 z3 => z3 Result
- solverCheckAssumptions :: MonadZ3 z3 => [AST] -> z3 Result
- solverGetModel :: MonadZ3 z3 => z3 Model
- solverGetProof :: MonadZ3 z3 => z3 AST
- solverGetUnsatCore :: MonadZ3 z3 => z3 [AST]
- solverGetReasonUnknown :: MonadZ3 z3 => z3 String
- solverToString :: MonadZ3 z3 => z3 String
- solverFromString :: MonadZ3 z3 => String -> z3 ()
- assert :: MonadZ3 z3 => AST -> z3 ()
- check :: MonadZ3 z3 => z3 Result
- checkAssumptions :: MonadZ3 z3 => [AST] -> z3 Result
- solverCheckAndGetModel :: MonadZ3 z3 => z3 (Result, Maybe Model)
- getModel :: MonadZ3 z3 => z3 (Result, Maybe Model)
- withModel :: (Applicative z3, MonadZ3 z3) => (Model -> z3 a) -> z3 (Result, Maybe a)
- getUnsatCore :: MonadZ3 z3 => z3 [AST]
- push :: MonadZ3 z3 => z3 ()
- pop :: MonadZ3 z3 => Int -> z3 ()
- local :: MonadZ3 z3 => z3 a -> z3 a
- reset :: MonadZ3 z3 => z3 ()
- getNumScopes :: MonadZ3 z3 => z3 Int
Z3 monad
class (Applicative m, Monad m, MonadIO m) => MonadZ3 m where Source #
module Z3.Opts
Solvers available in Z3.
These are described at http://smtlib.cs.uiowa.edu/logics.html
Constructors
| AUFLIA | Closed formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values. |
| AUFLIRA | Closed linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value. |
| AUFNIRA | Closed formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value. |
| LRA | Closed linear formulas in linear real arithmetic. |
| QF_ABV | Closed quantifier-free formulas over the theory of bitvectors and bitvector arrays. |
| QF_AUFBV | Closed quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols. |
| QF_AUFLIA | Closed quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols. |
| QF_AX | Closed quantifier-free formulas over the theory of arrays with extensionality. |
| QF_BV | Closed quantifier-free formulas over the theory of fixed-size bitvectors. |
| QF_IDL | Difference Logic over the integers. In essence, Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant. |
| QF_LIA | Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables. |
| QF_LRA | Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables. |
| QF_NIA | Quantifier-free integer arithmetic. |
| QF_NRA | Quantifier-free real arithmetic. |
| QF_RDL | Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant. |
| QF_UF | Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols. |
| QF_UFBV | Unquantified formulas over bitvectors with uninterpreted sort function and symbols. |
| QF_UFIDL | Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols. |
| QF_UFLIA | Unquantified linear integer arithmetic with uninterpreted sort and function symbols. |
| QF_UFLRA | Unquantified linear real arithmetic with uninterpreted sort and function symbols. |
| QF_UFNRA | Unquantified non-linear real arithmetic with uninterpreted sort and function symbols. |
| UFLRA | Linear real arithmetic with uninterpreted sort and function symbols. |
| UFNIA | Non-linear integer arithmetic with uninterpreted sort and function symbols. |
Z3 enviroments
evalZ3WithEnv :: Z3 a -> Z3Env -> IO a Source #
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).
Types
A Z3 symbol.
Used to name types, constants and functions.
Instances
| Storable Symbol Source # | |
| Show Symbol Source # | |
| Eq Symbol Source # | |
| Ord Symbol Source # | |
A Z3 AST node.
This is the data-structure used in Z3 to represent terms, formulas and types.
A kind of AST representing function symbols.
A kind of AST representing constant and function declarations.
A kind of AST representing pattern and multi-patterns to guide quantifier instantiation.
data Constructor Source #
A type contructor for a (recursive) datatype.
Instances
| Show Constructor Source # | |
Defined in Z3.Base Methods showsPrec :: Int -> Constructor -> ShowS # show :: Constructor -> String # showList :: [Constructor] -> ShowS # | |
| Eq Constructor Source # | |
Defined in Z3.Base | |
| Ord Constructor Source # | |
Defined in Z3.Base Methods compare :: Constructor -> Constructor -> Ordering # (<) :: Constructor -> Constructor -> Bool # (<=) :: Constructor -> Constructor -> Bool # (>) :: Constructor -> Constructor -> Bool # (>=) :: Constructor -> Constructor -> Bool # max :: Constructor -> Constructor -> Constructor # min :: Constructor -> Constructor -> Constructor # | |
A model for the constraints asserted into the logical context.
A Z3 logical context.
data FuncInterp Source #
An interpretation of a function in a model.
Instances
| Eq FuncInterp Source # | |
Defined in Z3.Base | |
Representation of the value of a Z3_func_interp at a particular point.
A Z3 parameter set.
Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.
A Z3 solver engine.
A(n) (incremental) solver, possibly specialized by a particular tactic or logic.
Different kinds of Z3 types.
Different kinds of Z3 AST nodes.
Satisfiability result
Result of a satisfiability check.
This corresponds to the z3_lbool type in the C API.
Parameters
mkParams :: MonadZ3 z3 => z3 Params Source #
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.
paramsSetBool :: MonadZ3 z3 => Params -> Symbol -> Bool -> z3 () Source #
Add a Boolean parameter k with value v to the parameter set p.
paramsSetUInt :: MonadZ3 z3 => Params -> Symbol -> Word -> z3 () Source #
Add a unsigned parameter k with value v to the parameter set p.
paramsSetDouble :: MonadZ3 z3 => Params -> Symbol -> Double -> z3 () Source #
Add a double parameter k with value v to the parameter set p.
paramsSetSymbol :: MonadZ3 z3 => Params -> Symbol -> Symbol -> z3 () Source #
Add a symbol parameter k with value v to the parameter set p.
paramsToString :: MonadZ3 z3 => Params -> z3 String Source #
Convert a parameter set into a string.
This function is mainly used for printing the contents of a parameter set.
Symbols
mkIntSymbol :: (MonadZ3 z3, Integral i) => i -> z3 Symbol Source #
Create a Z3 symbol using an integer.
Sorts
mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort Source #
Create a free (uninterpreted) type using the given name (symbol).
mkBoolSort :: MonadZ3 z3 => z3 Sort Source #
Create the boolean type.
mkRealSort :: MonadZ3 z3 => z3 Sort Source #
Create the real type.
mkBvSort :: MonadZ3 z3 => Int -> z3 Sort Source #
Create a bit-vector type of the given size.
This type can also be seen as a machine integer.
mkFiniteDomainSort :: MonadZ3 z3 => Symbol -> Word64 -> z3 Sort Source #
Create a finite-domain type.
Arguments
| :: 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. |
Create a tuple type
Arguments
| :: MonadZ3 z3 | |
| => Symbol | Name of the constructor |
| -> Symbol | Name of recognizer function |
| -> [(Symbol, Maybe Sort, Int)] | Name, sort option, and sortRefs |
| -> z3 Constructor |
Create a constructor
mkDatatype :: MonadZ3 z3 => Symbol -> [Constructor] -> z3 Sort Source #
Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.
mkDatatypes :: MonadZ3 z3 => [Symbol] -> [[Constructor]] -> z3 [Sort] Source #
Create mutually recursive datatypes, such as a tree and forest.
Returns the datatype sorts
Constants and Applications
mkApp :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST Source #
Create a constant or function application.
mkFreshFuncDecl :: MonadZ3 z3 => String -> [Sort] -> Sort -> z3 FuncDecl Source #
Declare a fresh constant or function.
mkRecFuncDecl :: MonadZ3 z3 => Symbol -> [Sort] -> Sort -> z3 FuncDecl Source #
A recursive Z3 function
addRecDef :: MonadZ3 z3 => FuncDecl -> [AST] -> AST -> z3 () Source #
Define the body of a recursive Z3 function
Helpers
mkVar :: MonadZ3 z3 => Symbol -> Sort -> z3 AST Source #
Declare and create a variable (aka constant).
An alias for mkConst.
mkBoolVar :: MonadZ3 z3 => Symbol -> z3 AST Source #
Declarate and create a variable of sort bool.
See mkVar.
mkRealVar :: MonadZ3 z3 => Symbol -> z3 AST Source #
Declarate and create a variable of sort real.
See mkVar.
mkIntVar :: MonadZ3 z3 => Symbol -> z3 AST Source #
Declarate and create a variable of sort int.
See mkVar.
Declarate and create a variable of sort bit-vector.
See mkVar.
mkFreshVar :: MonadZ3 z3 => String -> Sort -> z3 AST Source #
Declare and create a fresh variable (aka constant).
An alias for mkFreshConst.
mkFreshBoolVar :: MonadZ3 z3 => String -> z3 AST Source #
Declarate and create a fresh variable of sort bool.
See mkFreshVar.
mkFreshRealVar :: MonadZ3 z3 => String -> z3 AST Source #
Declarate and create a fresh variable of sort real.
See mkFreshVar.
mkFreshIntVar :: MonadZ3 z3 => String -> z3 AST Source #
Declarate and create a fresh variable of sort int.
See mkFreshVar.
Declarate and create a fresh variable of sort bit-vector.
See mkFreshVar.
Propositional Logic and Equality
mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST Source #
Create an AST node representing an if-then-else: ite(t1, t2, t3).
mkImplies :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Create an AST node representing t1 implies t2.
mkAnd :: MonadZ3 z3 => [AST] -> z3 AST Source #
Create an AST node representing args[0] and ... and args[num_args-1].
mkOr :: MonadZ3 z3 => [AST] -> z3 AST Source #
Create an AST node representing args[0] or ... or args[num_args-1].
mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST Source #
The distinct construct is used for declaring the arguments pairwise distinct.
Requires a non-empty list.
mkDistinct1 :: MonadZ3 z3 => NonEmpty AST -> z3 AST Source #
Same as mkDistinct but type-safe.
Helpers
Arithmetic: Integers and Reals
mkAdd :: MonadZ3 z3 => [AST] -> z3 AST Source #
Create an AST node representing args[0] + ... + args[num_args-1].
mkMul :: MonadZ3 z3 => [AST] -> z3 AST Source #
Create an AST node representing args[0] * ... * args[num_args-1].
mkSub :: MonadZ3 z3 => [AST] -> z3 AST Source #
Create an AST node representing args[0] - ... - args[num_args - 1].
Requires a non-empty list.
mkPower :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Create an AST node representing arg1 ^ arg2.
Reference: https://z3prover.github.io/api/html/group__capi.html#ga8414506c805caa171f0c1fe29f9f9612
Bit-vectors
mkBvredand :: MonadZ3 z3 => AST -> z3 AST Source #
Take conjunction of bits in vector, return vector of length 1.
mkBvredor :: MonadZ3 z3 => AST -> z3 AST Source #
Take disjunction of bits in vector, return vector of length 1.
mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Two's complement signed remainder (sign follows dividend).
mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Two's complement signed remainder (sign follows divisor).
mkBvsle :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Two's complement signed less than or equal to.
mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Two's complement signed greater than or equal to.
mkExtract :: MonadZ3 z3 => Int -> Int -> AST -> z3 AST Source #
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.
mkSignExt :: MonadZ3 z3 => Int -> AST -> z3 AST Source #
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.
mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 AST Source #
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.
mkExtRotateLeft :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Rotate bits of t1 to the left t2 times.
mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Rotate bits of t1 to the right t2 times.
mkInt2bv :: MonadZ3 z3 => Int -> AST -> z3 AST Source #
Create an n bit bit-vector from the integer argument t1.
mkBv2int :: MonadZ3 z3 => AST -> Bool -> z3 AST Source #
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.
mkBvnegNoOverflow :: MonadZ3 z3 => AST -> z3 AST Source #
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.
mkBvaddNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST Source #
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
mkBvaddNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
mkBvsubNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.
mkBvsubNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.
mkBvmulNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST Source #
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.
mkBvmulNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow.
mkBvsdivNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.
Arrays
mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Array read. The argument a is the array and i is the index of the array that gets read.
mkArrayDefault :: MonadZ3 z3 => AST -> z3 AST Source #
Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.
Sets
mkSetDifference :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Take the set difference between two sets.
mkSetSubset :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Check if the first set is a subset of the second set.
Numerals
mkInt :: MonadZ3 z3 => Int -> Sort -> z3 AST Source #
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.
mkUnsignedInt :: MonadZ3 z3 => Word -> Sort -> z3 AST Source #
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.
mkInt64 :: MonadZ3 z3 => Int64 -> Sort -> z3 AST Source #
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.
mkUnsignedInt64 :: MonadZ3 z3 => Word64 -> Sort -> z3 AST Source #
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.
Helpers
mkIntegral :: (MonadZ3 z3, Integral a) => a -> Sort -> z3 AST Source #
Create a numeral of an int, bit-vector, or finite-domain sort.
mkRational :: MonadZ3 z3 => Rational -> z3 AST Source #
Create a numeral of sort real from a Rational.
mkFixed :: (MonadZ3 z3, HasResolution a) => Fixed a -> z3 AST Source #
Create a numeral of sort real from a Fixed.
mkIntNum :: (MonadZ3 z3, Integral a) => a -> z3 AST Source #
Create a numeral of sort int from an Integral.
Create a numeral of sort Bit-vector from an Integer.
Create a numeral of sort Bit-vector from an Integral.
Sequences and regular expressions
mkSeqSort :: MonadZ3 z3 => Sort -> z3 Sort Source #
Create a sequence sort out of the sort for the elements.
mkReSort :: MonadZ3 z3 => Sort -> z3 Sort Source #
Create a regular expression sort out of a sequence sort.
mkStringSort :: MonadZ3 z3 => z3 Sort Source #
Create a sort for 8 bit strings. This function creates a sort for ASCII strings. Each character is 8 bits.
mkString :: MonadZ3 z3 => String -> z3 AST Source #
Create a string constant out of the string that is passed in.
mkSeqEmpty :: MonadZ3 z3 => Sort -> z3 AST Source #
Create an empty sequence of the sequence sort seq.
Check if prefix is a prefix of s.
Check if suffix is a suffix of s.
Check if container contains containee.
Check if s1 is equal or lexicographically strictly less than s2.
Check if s1 is lexicographically strictly less than s2.
Extract subsequence starting at offset of length.
Replace the first occurrence of src with dst in s.
Retrieve from s the unit sequence positioned at position index.
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.
mkSeqToRe :: MonadZ3 z3 => AST -> z3 AST Source #
Create a regular expression that accepts the sequence.
Check if seq is in the language generated by the regular expression re.
mkReUnion :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST Source #
Create the union of the regular languages.
mkReConcat :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST Source #
Create the concatenation of the regular languages.
Create the range regular expression over two sequences of length 1.
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.
mkReIntersect :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST Source #
Create the intersection of the regular languages.
mkReComplement :: MonadZ3 z3 => AST -> z3 AST Source #
Create the complement of the regular language.
Quantifiers
Accessors
getSortName :: MonadZ3 z3 => Sort -> z3 Symbol Source #
Return the sort name as a symbol.
Reference: https://z3prover.github.io/api/html/group__capi.html#gab66884f00730c61cf3a5e6814aa2ebd0
sortToAst :: MonadZ3 z3 => Sort -> z3 AST Source #
Convert a Z3_sort into Z3_ast. This is just type casting.
Reference: https://z3prover.github.io/api/html/group__capi.html#gac68cabaff75abfbf3d99f1f66d2e39a5
isEqSort :: MonadZ3 z3 => Sort -> Sort -> z3 Bool Source #
Compare sorts.
| Reference: https://z3prover.github.io/api/html/group__capi.html#gaf260f3b5bc786cd0552e1ed4f8232a4b
getSortKind :: MonadZ3 z3 => Sort -> z3 SortKind Source #
Return the sort kind.
Reference: http://z3prover.github.io/api/html/group__capi.html#gacd85d48842c7bfaa696596d16875681a
getDatatypeSortConstructors Source #
Get list of constructors for datatype.
getDatatypeSortRecognizers Source #
Get list of recognizers for datatype.
getDatatypeSortConstructorAccessors Source #
Get list of accessors for datatype.
mkAtMost :: MonadZ3 z3 => [AST] -> Int -> z3 AST Source #
At most k of the arguments ps may be true, i.e. encode p1 + p2
+ ... + pn <= k.
Reference: https://z3prover.github.io/api/html/group__capi.html#gaf2501779266a6dc2738a8928d1fc858c
mkAtLeast :: MonadZ3 z3 => [AST] -> Int -> z3 AST Source #
At least k of the arguments ps may be true, i.e. encode p1 +
p2 + ... + pn >= k.
Reference: https://z3prover.github.io/api/html/group__capi.html#gaaa996ab58cf979d5849178f1d2963efb
getDeclName :: MonadZ3 z3 => FuncDecl -> z3 Symbol Source #
Return the constant declaration name as a symbol.
getArity :: MonadZ3 z3 => FuncDecl -> z3 Int Source #
Returns the number of parameters of the given declaration
Returns the sort of the i-th parameter of the given function declaration
getAppDecl :: MonadZ3 z3 => App -> z3 FuncDecl Source #
Return the declaration of a constant or function application.
getAppNumArgs :: MonadZ3 z3 => App -> z3 Int Source #
Return the number of argument of an application. If t is an constant, then the number of arguments is 0.
getAppArg :: MonadZ3 z3 => App -> Int -> z3 AST Source #
Return the i-th argument of the given application.
getAppArgs :: MonadZ3 z3 => App -> z3 [AST] Source #
Return a list of all the arguments of the given application.
getBoolValue :: MonadZ3 z3 => AST -> z3 (Maybe Bool) Source #
Returns Just True, Just False, or Nothing for undefined.
getNumeralString :: MonadZ3 z3 => AST -> z3 String Source #
Return numeral value, as a string of a numeric constant term.
getNumerator :: MonadZ3 z3 => AST -> z3 AST Source #
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
Reference: https://z3prover.github.io/api/html/group__capi.html#ga2d37084eb47ea0ab19638a3407ce610b
getDenominator :: MonadZ3 z3 => AST -> z3 AST Source #
Return the denominator (as a numeral AST) of a numeral AST of sort Real.
Reference: https://z3prover.github.io/api/html/group__capi.html#ga07549939888e8fdfc8e0fde1776c31a7
simplifyEx :: MonadZ3 z3 => AST -> Params -> z3 AST Source #
Simplify the expression using the given parameters.
Helpers
Modifiers
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.
evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel) Source #
Get array as a list of argument/value pairs, if it is represented as a function (ie, using as-array).
getFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncInterp) Source #
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.
isAsArray :: MonadZ3 z3 => AST -> z3 Bool Source #
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.
addFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> AST -> z3 FuncInterp Source #
getAsArrayFuncDecl :: MonadZ3 z3 => AST -> z3 FuncDecl Source #
Return the function declaration f associated with a (_ as_array f) node.
funcInterpGetNumEntries :: MonadZ3 z3 => FuncInterp -> z3 Int Source #
Return the number of entries in the given function interpretation.
funcInterpGetEntry :: MonadZ3 z3 => FuncInterp -> Int -> z3 FuncEntry Source #
Return a "point" of the given function intepretation. It represents the value of f in a particular point.
funcInterpGetElse :: MonadZ3 z3 => FuncInterp -> z3 AST Source #
Return the 'else' value of the given function interpretation.
funcInterpGetArity :: MonadZ3 z3 => FuncInterp -> z3 Int Source #
Return the arity (number of arguments) of the given function interpretation.
funcEntryGetNumArgs :: MonadZ3 z3 => FuncEntry -> z3 Int Source #
Return the number of arguments in a Z3_func_entry object.
funcEntryGetArg :: MonadZ3 z3 => FuncEntry -> Int -> z3 AST Source #
Return an argument of a Z3_func_entry object.
Helpers
evalT :: (MonadZ3 z3, Traversable t) => Model -> t AST -> z3 (Maybe (t AST)) Source #
Evaluate a collection of AST nodes in the given model.
mapEval :: (MonadZ3 z3, Traversable t) => EvalAst z3 a -> Model -> t AST -> z3 (Maybe (t a)) Source #
Run a evaluation function on a Traversable data structure of ASTs
(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.
The interpretation of a function.
evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel) Source #
Get function as a list of argument/value pairs.
Tactics
skipTactic :: MonadZ3 z3 => z3 Tactic Source #
mkQuantifierEliminationTactic :: MonadZ3 z3 => z3 Tactic Source #
mkAndInverterGraphTactic :: MonadZ3 z3 => z3 Tactic Source #
applyTactic :: MonadZ3 z3 => Tactic -> Goal -> z3 ApplyResult Source #
applyResultToString :: MonadZ3 z3 => ApplyResult -> z3 String Source #
getApplyResultNumSubgoals :: MonadZ3 z3 => ApplyResult -> z3 Int Source #
getApplyResultSubgoal :: MonadZ3 z3 => ApplyResult -> Int -> z3 Goal Source #
getApplyResultSubgoals :: MonadZ3 z3 => ApplyResult -> z3 [Goal] Source #
String Conversion
data ASTPrintMode Source #
Pretty-printing mode for converting ASTs to strings. The mode can be one of the following:
- Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose format.
- Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format.
- Z3_PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant format.
- Z3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x compliant format.
setASTPrintMode :: MonadZ3 z3 => ASTPrintMode -> z3 () Source #
Set the mode for converting expressions to strings.
benchmarkToSMTLibString Source #
Arguments
| :: MonadZ3 z3 | |
| => String | name |
| -> String | logic |
| -> String | status |
| -> String | attributes |
| -> [AST] | assumptions1 |
| -> AST | formula |
| -> z3 String |
Convert the given benchmark into SMT-LIB formatted string.
The output format can be configured via setASTPrintMode.
Parser interface
Arguments
| :: MonadZ3 z3 | |
| => String | string to parse |
| -> [Symbol] | sort names |
| -> [Sort] | sorts |
| -> [Symbol] | declaration names |
| -> [FuncDecl] | declarations |
| -> z3 [AST] |
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.
Arguments
| :: MonadZ3 z3 | |
| => String | string to parse |
| -> [Symbol] | sort names |
| -> [Sort] | sorts |
| -> [Symbol] | declaration names |
| -> [FuncDecl] | declarations |
| -> z3 [AST] |
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.
Error Handling
Constructors
| Z3Error | |
Fields
| |
Instances
| Exception Z3Error Source # | |
Defined in Z3.Base Methods toException :: Z3Error -> SomeException # fromException :: SomeException -> Maybe Z3Error # displayException :: Z3Error -> String # | |
| Show Z3Error Source # | |
data Z3ErrorCode Source #
Z3 error codes.
Constructors
| SortError | |
| IOB | |
| InvalidArg | |
| ParserError | |
| NoParser | |
| InvalidPattern | |
| MemoutFail | |
| FileAccessError | |
| InternalFatal | |
| InvalidUsage | |
| DecRefError | |
| Z3Exception |
Instances
| Show Z3ErrorCode Source # | |
Defined in Z3.Base Methods showsPrec :: Int -> Z3ErrorCode -> ShowS # show :: Z3ErrorCode -> String # showList :: [Z3ErrorCode] -> ShowS # | |
Miscellaneous
getVersion :: MonadZ3 z3 => z3 Version Source #
Return Z3 version number information.
Fixedpoint
class MonadZ3 m => MonadFixedpoint m where Source #
Methods
getFixedpoint :: m Fixedpoint Source #
Instances
| MonadFixedpoint Z3 Source # | |
Defined in Z3.Monad Methods | |
data Fixedpoint Source #
Instances
| Eq Fixedpoint Source # | |
Defined in Z3.Base | |
fixedpointAddRule :: MonadFixedpoint z3 => AST -> Symbol -> z3 () Source #
fixedpointSetParams :: MonadFixedpoint z3 => Params -> z3 () Source #
fixedpointRegisterRelation :: MonadFixedpoint z3 => FuncDecl -> z3 () Source #
fixedpointQueryRelations :: MonadFixedpoint z3 => [FuncDecl] -> z3 Result Source #
fixedpointGetAnswer :: MonadFixedpoint z3 => z3 AST Source #
fixedpointGetAssertions :: MonadFixedpoint z3 => z3 [AST] Source #
Floating-Point Arithmetic
mkFpaRoundingModeSort :: MonadZ3 z3 => z3 Sort Source #
Create the RoundingMode sort.
mkFpaRoundNearestTiesToEven :: MonadZ3 z3 => z3 AST Source #
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
mkFpaRne :: MonadZ3 z3 => z3 AST Source #
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
mkFpaRoundNearestTiesToAway :: MonadZ3 z3 => z3 AST Source #
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
mkFpaRna :: MonadZ3 z3 => z3 AST Source #
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
mkFpaRoundTowardPositive :: MonadZ3 z3 => z3 AST Source #
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
mkFpaRtp :: MonadZ3 z3 => z3 AST Source #
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
mkFpaRoundTowardNegative :: MonadZ3 z3 => z3 AST Source #
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
mkFpaRtn :: MonadZ3 z3 => z3 AST Source #
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
mkFpaRoundTowardZero :: MonadZ3 z3 => z3 AST Source #
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
mkFpaRtz :: MonadZ3 z3 => z3 AST Source #
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
Arguments
| :: (MonadZ3 z3, Integral int) | |
| => int | Number of exponent bits |
| -> int | Number of significand bits |
| -> z3 Sort |
Create a FloatingPoint sort.
mkFpaSortHalf :: MonadZ3 z3 => z3 Sort Source #
Create the half-precision (16-bit) FloatingPoint sort.
mkFpaSort16 :: MonadZ3 z3 => z3 Sort Source #
Create the half-precision (16-bit) FloatingPoint sort.
mkFpaSortSingle :: MonadZ3 z3 => z3 Sort Source #
Create the single-precision (32-bit) FloatingPoint sort.
mkFpaSort32 :: MonadZ3 z3 => z3 Sort Source #
Create the single-precision (32-bit) FloatingPoint sort.
mkFpaSortDouble :: MonadZ3 z3 => z3 Sort Source #
Create the double-precision (64-bit) FloatingPoint sort.
mkFpaSort64 :: MonadZ3 z3 => z3 Sort Source #
Create the double-precision (64-bit) FloatingPoint sort.
mkFpaSortQuadruple :: MonadZ3 z3 => z3 Sort Source #
Create the quadruple-precision (128-bit) FloatingPoint sort.
mkFpaSort128 :: MonadZ3 z3 => z3 Sort Source #
Create the quadruple-precision (128-bit) FloatingPoint sort.
Arguments
| :: MonadZ3 z3 | |
| => Sort | Target sort |
| -> Bool | Indicates whether the result should be negative |
| -> z3 AST |
Create a floating-point infinity of sort s.
Arguments
| :: MonadZ3 z3 | |
| => Sort | Target sort |
| -> Bool | Indicates whether the result should be negative |
| -> z3 AST |
Create a floating-point zero of sort s.
Create an expression of FloatingPoint sort from three bit-vector expressions.
This is the operator named fp in the SMT FP theory definition.
Note that sgn is required to be a bit-vector of size 1.
Significand and exponent are required to be longer than 1 and 2
respectively. The FloatingPoint sort of the resulting expression
is automatically determined from the bit-vector sizes of the
arguments. The exponent is assumed to be in IEEE-754 biased
representation.
mkFpaNumeralFloat :: MonadZ3 z3 => Float -> Sort -> z3 AST Source #
Create a numeral of FloatingPoint sort from a float.
mkFpaNumeralDouble :: MonadZ3 z3 => Double -> Sort -> z3 AST Source #
Create a numeral of FloatingPoint sort from a double.
mkFpaNumeralInt :: (MonadZ3 z3, Integral int) => int -> Sort -> z3 AST Source #
Create a numeral of FloatingPoint sort from a signed integer.
Arguments
| :: (MonadZ3 z3, Integral int) | |
| => Bool | Sign bit (true == negative) |
| -> int | Significand |
| -> int | Exponent |
| -> Sort | Result sort |
| -> z3 AST |
Create a numeral of FLoatingPoint sort from a sign bit and two integers.
mkFpaNumeralInt64UInt64 Source #
Arguments
| :: (MonadZ3 z3, Integral int) | |
| => Bool | Sign bit (true == negative) |
| -> int | Significand |
| -> int | Exponent |
| -> Sort | Result sort |
| -> z3 AST |
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
Arguments
| :: MonadZ3 z3 | |
| => AST | Rounding Mode |
| -> AST | FloatingPoint sort term |
| -> AST | FloatingPoint sort term |
| -> z3 AST |
Floating-point addition.
Arguments
| :: MonadZ3 z3 | |
| => AST | Rounding Mode |
| -> AST | FloatingPoint sort term |
| -> AST | FloatingPoint sort term |
| -> z3 AST |
Floating-point subtraction.
Arguments
| :: MonadZ3 z3 | |
| => AST | Rounding Mode |
| -> AST | FloatingPoint sort term |
| -> AST | FloatingPoint sort term |
| -> z3 AST |
Floating-point multiplication.
Arguments
| :: MonadZ3 z3 | |
| => AST | Rounding Mode |
| -> AST | FloatingPoint sort term |
| -> AST | FloatingPoint sort term |
| -> z3 AST |
Floating-point division.
mkFpaFma :: MonadZ3 z3 => AST -> AST -> AST -> AST -> z3 AST Source #
Floating-point fused multiply-add.
The result is round((t1 * t2) + t3).
mkFpaRoundToIntegral :: MonadZ3 z3 => AST -> AST -> z3 AST Source #
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.
mkFpaIsNormal :: MonadZ3 z3 => AST -> z3 AST Source #
Predicate indicating whether t is a normal floating-point
number.
mkFpaIsSubnormal :: MonadZ3 z3 => AST -> z3 AST Source #
Predicate indicating whether t is a subnormal floating-point
number.
mkFpaIsZero :: MonadZ3 z3 => AST -> z3 AST Source #
Predicate indicating whether t is a floating-point number
with zero value, i.e., +zero or -zero.
mkFpaIsInfinite :: MonadZ3 z3 => AST -> z3 AST Source #
Predicate indicating whether t is a floating-point number
representing infinity, i.e., +oo or -oo.
mkFpaIsNegative :: MonadZ3 z3 => AST -> z3 AST Source #
Predicate indicating whether t is a negative floating-point
number.
mkFpaIsPositive :: MonadZ3 z3 => AST -> z3 AST Source #
Predicate indicating whether t is a positive floating-point
number.
mkFpaToFpBv :: MonadZ3 z3 => AST -> Sort -> z3 AST Source #
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
mkFpaToFpFloat :: MonadZ3 z3 => AST -> AST -> Sort -> z3 AST Source #
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
mkFpaToFpReal :: MonadZ3 z3 => AST -> AST -> Sort -> z3 AST Source #
Conversion of a term of real sort into a term of FloatingPoint sort.
mkFpaToFpSigned :: MonadZ3 z3 => AST -> AST -> Sort -> z3 AST Source #
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
mkFpaToFpUnsigned :: MonadZ3 z3 => AST -> AST -> Sort -> z3 AST Source #
Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
mkFpaToUbv :: (MonadZ3 z3, Integral int) => AST -> AST -> int -> z3 AST Source #
Conversion of a floating-point term into an unsigned bit-vector.
mkFpaToSbv :: (MonadZ3 z3, Integral int) => AST -> AST -> int -> z3 AST Source #
Conversion of a floating-point term into a signed bit-vector.
mkFpaToReal :: MonadZ3 z3 => AST -> z3 AST Source #
Conversion of a floating-point term into an real-numbered term.
Z3-specific floating-point extensions
fpaGetEbits :: (MonadZ3 z3, Integral int) => Sort -> z3 int Source #
Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.
fpaGetSbits :: (MonadZ3 z3, Integral int) => Sort -> z3 int Source #
Retrieves the number of bits reserved for the significand in a FloatingPoint sort.
fpaIsNumeralNaN :: MonadZ3 z3 => AST -> z3 Bool Source #
Checks whether a given floating-point numeral is a NaN.
fpaIsNumeralInf :: MonadZ3 z3 => AST -> z3 Bool Source #
Checks whether a given floating-point numeral is a +oo or -oo.
fpaIsNumeralZero :: MonadZ3 z3 => AST -> z3 Bool Source #
Checks whether a given floating-point numeral is a +zero or -zero.
fpaIsNumeralNormal :: MonadZ3 z3 => AST -> z3 Bool Source #
Checks whether a given floating-point numeral is normal.
fpaIsNumeralSubnormal :: MonadZ3 z3 => AST -> z3 Bool Source #
Checks whether a given floating-point numeral is subnormal.
fpaIsNumeralPositive :: MonadZ3 z3 => AST -> z3 Bool Source #
Checks whether a given floating-point numeral is positive.
fpaIsNumeralNegative :: MonadZ3 z3 => AST -> z3 Bool Source #
Checks whether a given floating-point numeral is negative.
fpaGetNumeralSignBv :: MonadZ3 z3 => AST -> z3 AST Source #
Retrieves the sign of a floating-point literal as a bit-vector expression.
fpaGetNumeralSignificandBv :: MonadZ3 z3 => AST -> z3 AST Source #
Retrieves the significand of a floating-point literal as a bit-vector expression.
fpaGetNumeralSignificandString :: MonadZ3 z3 => AST -> z3 String Source #
Return the significand value of a floating-point numeral as a string.
fpaGetNumeralExponentString :: MonadZ3 z3 => AST -> Bool -> z3 String Source #
Return the exponent value of a floating-point numeral as a string.
fpaGetNumeralExponentBv :: MonadZ3 z3 => AST -> Bool -> z3 AST Source #
Retrieves the exponent of a floating-point literal as a bit-vector expression.
mkFpaToIEEEBv :: MonadZ3 z3 => AST -> z3 AST Source #
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
mkFpaToFpIntReal :: MonadZ3 z3 => AST -> AST -> AST -> Sort -> z3 AST Source #
Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
Optimization
class MonadZ3 m => MonadOptimize m where Source #
Methods
getOptimize :: m Optimize Source #
Instances
optimizeAssert :: MonadOptimize z3 => AST -> z3 () Source #
optimizeAssertAndTrack :: MonadOptimize z3 => AST -> AST -> z3 () Source #
optimizeAssertSoft :: MonadOptimize z3 => AST -> String -> Symbol -> z3 Int Source #
optimizeMaximize :: MonadOptimize z3 => AST -> z3 Int Source #
optimizeMinimize :: MonadOptimize z3 => AST -> z3 Int Source #
optimizePush :: MonadOptimize z3 => z3 () Source #
optimizePop :: MonadOptimize z3 => z3 () Source #
optimizeCheck :: MonadOptimize z3 => [AST] -> z3 Result Source #
optimizeGetReasonUnknown :: MonadOptimize z3 => z3 String Source #
optimizeGetModel :: MonadOptimize z3 => z3 Model Source #
optimizeGetUnsatCore :: MonadOptimize z3 => z3 [AST] Source #
optimizeSetParams :: MonadOptimize z3 => Params -> z3 () Source #
optimizeGetLower :: MonadOptimize z3 => Int -> z3 AST Source #
optimizeGetUpper :: MonadOptimize z3 => Int -> z3 AST Source #
optimizeGetUpperAsVector :: MonadOptimize z3 => Int -> z3 [AST] Source #
optimizeGetLowerAsVector :: MonadOptimize z3 => Int -> z3 [AST] Source #
optimizeToString :: MonadOptimize z3 => z3 String Source #
optimizeFromString :: MonadOptimize z3 => String -> z3 () Source #
optimizeFromFile :: MonadOptimize z3 => String -> z3 () Source #
optimizeGetHelp :: MonadOptimize z3 => z3 String Source #
optimizeGetAssertions :: MonadOptimize z3 => z3 [AST] Source #
optimizeGetObjectives :: MonadOptimize z3 => z3 [AST] Source #
Solvers
solverGetHelp :: MonadZ3 z3 => z3 String Source #
Return a string describing all solver available parameters.
solverSetParams :: MonadZ3 z3 => Params -> z3 () Source #
Set the solver using the given parameters.
solverPush :: MonadZ3 z3 => z3 () Source #
Create a backtracking point.
solverReset :: MonadZ3 z3 => z3 () Source #
solverGetNumScopes :: MonadZ3 z3 => z3 Int Source #
Number of backtracking points.
solverAssertCnstr :: MonadZ3 z3 => AST -> z3 () Source #
Assert a constraing into the logical context.
solverAssertAndTrack :: MonadZ3 z3 => AST -> AST -> z3 () Source #
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.
solverGetAssertions :: MonadZ3 z3 => z3 [AST] Source #
Return the set of asserted formulas on the solver.
Reference: https://z3prover.github.io/api/html/group__capi.html#ga3b3d6d8c5bafd5be707cda2d144073db
solverCheck :: MonadZ3 z3 => z3 Result Source #
Check whether the assertions in a given solver are consistent or not.
Reference: https://z3prover.github.io/api/html/group__capi.html#ga3570e58a8c3d493da4109568b1eca2ce
solverCheckAssumptions :: MonadZ3 z3 => [AST] -> z3 Result Source #
Check whether the assertions in the given solver and optional assumptions are consistent or not.
Reference: https://z3prover.github.io/api/html/group__capi.html#ga65b2bd980519c0e873d328edcc5f9317
solverGetModel :: MonadZ3 z3 => z3 Model Source #
Retrieve the model for the last solverCheck or solverCheckAssumptions.
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.
Reference: https://z3prover.github.io/api/html/group__capi.html#ga6342b4260e9c92b11cb3eea3a145dff4
solverGetProof :: MonadZ3 z3 => z3 AST Source #
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).
solverGetUnsatCore :: MonadZ3 z3 => z3 [AST] Source #
Retrieve the unsat core for the last solverCheckAssumptions; the unsat core is a subset of the assumptions
solverGetReasonUnknown :: MonadZ3 z3 => z3 String Source #
Return a brief justification for an Unknown result for the commands solverCheck and solverCheckAssumptions.
solverToString :: MonadZ3 z3 => z3 String Source #
Convert the given solver into a string.
solverFromString :: MonadZ3 z3 => String -> z3 () Source #
Helpers
check :: MonadZ3 z3 => z3 Result Source #
Check whether the given logical context is consistent or not.
Alias for solverCheck
checkAssumptions :: MonadZ3 z3 => [AST] -> z3 Result Source #
Check whether the assertions in the given solver and optional assumptions are consistent or not.
Alias for solverCheckAssumptions
solverCheckAndGetModel :: MonadZ3 z3 => z3 (Result, Maybe Model) Source #
Call solverCheck and based on the result also call solverGetModel.
getModel :: MonadZ3 z3 => z3 (Result, Maybe Model) Source #
Check and get model.
Alias for solverCheckAndGetModel
withModel :: (Applicative z3, MonadZ3 z3) => (Model -> z3 a) -> z3 (Result, Maybe a) Source #
Check satisfiability and, if sat, compute a value from the given model.
E.g.
withModel $ \m ->
fromJust <$> evalInt m x
getUnsatCore :: MonadZ3 z3 => z3 [AST] Source #
Retrieve the unsat core for the last checkAssumptions; the unsat core is a subset of the assumptions.
Alias for solverGetUnsatCore
pop :: MonadZ3 z3 => Int -> z3 () Source #
Backtrack n backtracking points.
Contrary to solverPop this funtion checks whether n is within
the size of the solver scope stack.
reset :: MonadZ3 z3 => z3 () Source #
Backtrack all the way.
Alias for solverReset
getNumScopes :: MonadZ3 z3 => z3 Int Source #
Get number of backtracking points.