| Copyright | (c) Iago Abal 2012-2015 (c) David Castro 2012-2015 |
|---|---|
| License | BSD3 |
| Maintainer | Iago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com> |
| Safe Haskell | None |
| Language | Haskell2010 |
Z3.Base
Contents
- Types
- Create configuration
- Create context
- 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
- Optimization
- Solvers
Description
Low-level bindings to Z3 API.
There is (mostly) a one-to-one correspondence with Z3 C API, thus see http://z3prover.github.io/api/html/group__capi.html for further details.
- data Config
- data Context
- data Symbol
- data AST
- data Sort
- data FuncDecl
- data App
- data Pattern
- data Constructor
- data Model
- data FuncInterp
- data FuncEntry
- data Params
- data Solver
- data SortKind
- data ASTKind
- data Tactic
- data ApplyResult
- data Goal
- data Result
- mkConfig :: IO Config
- delConfig :: Config -> IO ()
- setParamValue :: Config -> String -> String -> IO ()
- withConfig :: (Config -> IO a) -> IO a
- mkContext :: Config -> IO Context
- withContext :: Context -> (Ptr Z3_context -> IO r) -> IO r
- mkParams :: Context -> IO Params
- paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO ()
- paramsSetUInt :: Context -> Params -> Symbol -> Word -> IO ()
- paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO ()
- paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO ()
- paramsToString :: Context -> Params -> IO String
- mkIntSymbol :: Integral int => Context -> int -> IO Symbol
- mkStringSymbol :: Context -> String -> IO Symbol
- mkUninterpretedSort :: Context -> Symbol -> IO Sort
- mkBoolSort :: Context -> IO Sort
- mkIntSort :: Context -> IO Sort
- mkRealSort :: Context -> IO Sort
- mkBvSort :: Integral int => Context -> int -> IO Sort
- mkFiniteDomainSort :: Context -> Symbol -> Word64 -> IO Sort
- mkArraySort :: Context -> Sort -> Sort -> IO Sort
- mkTupleSort :: Context -> Symbol -> [(Symbol, Sort)] -> IO (Sort, FuncDecl, [FuncDecl])
- mkConstructor :: Context -> Symbol -> Symbol -> [(Symbol, Maybe Sort, Int)] -> IO Constructor
- mkDatatype :: Context -> Symbol -> [Constructor] -> IO Sort
- mkDatatypes :: Context -> [Symbol] -> [[Constructor]] -> IO [Sort]
- mkSetSort :: Context -> Sort -> IO Sort
- mkFuncDecl :: Context -> Symbol -> [Sort] -> Sort -> IO FuncDecl
- mkApp :: Context -> FuncDecl -> [AST] -> IO AST
- mkConst :: Context -> Symbol -> Sort -> IO AST
- mkFreshFuncDecl :: Context -> String -> [Sort] -> Sort -> IO FuncDecl
- mkFreshConst :: Context -> String -> Sort -> IO AST
- mkVar :: Context -> Symbol -> Sort -> IO AST
- mkBoolVar :: Context -> Symbol -> IO AST
- mkRealVar :: Context -> Symbol -> IO AST
- mkIntVar :: Context -> Symbol -> IO AST
- mkBvVar :: Context -> Symbol -> Int -> IO AST
- mkFreshVar :: Context -> String -> Sort -> IO AST
- mkFreshBoolVar :: Context -> String -> IO AST
- mkFreshRealVar :: Context -> String -> IO AST
- mkFreshIntVar :: Context -> String -> IO AST
- mkFreshBvVar :: Context -> String -> Int -> IO AST
- mkTrue :: Context -> IO AST
- mkFalse :: Context -> IO AST
- mkEq :: Context -> AST -> AST -> IO AST
- mkNot :: Context -> AST -> IO AST
- mkIte :: Context -> AST -> AST -> AST -> IO AST
- mkIff :: Context -> AST -> AST -> IO AST
- mkImplies :: Context -> AST -> AST -> IO AST
- mkXor :: Context -> AST -> AST -> IO AST
- mkAnd :: Context -> [AST] -> IO AST
- mkOr :: Context -> [AST] -> IO AST
- mkDistinct :: Context -> [AST] -> IO AST
- mkDistinct1 :: Context -> NonEmpty AST -> IO AST
- mkBool :: Context -> Bool -> IO AST
- mkAdd :: Context -> [AST] -> IO AST
- mkMul :: Context -> [AST] -> IO AST
- mkSub :: Context -> [AST] -> IO AST
- mkSub1 :: Context -> NonEmpty AST -> IO AST
- mkUnaryMinus :: Context -> AST -> IO AST
- mkDiv :: Context -> AST -> AST -> IO AST
- mkMod :: Context -> AST -> AST -> IO AST
- mkRem :: Context -> AST -> AST -> IO AST
- mkLt :: Context -> AST -> AST -> IO AST
- mkLe :: Context -> AST -> AST -> IO AST
- mkGt :: Context -> AST -> AST -> IO AST
- mkGe :: Context -> AST -> AST -> IO AST
- mkInt2Real :: Context -> AST -> IO AST
- mkReal2Int :: Context -> AST -> IO AST
- mkIsInt :: Context -> AST -> IO AST
- mkBvnot :: Context -> AST -> IO AST
- mkBvredand :: Context -> AST -> IO AST
- mkBvredor :: Context -> AST -> IO AST
- mkBvand :: Context -> AST -> AST -> IO AST
- mkBvor :: Context -> AST -> AST -> IO AST
- mkBvxor :: Context -> AST -> AST -> IO AST
- mkBvnand :: Context -> AST -> AST -> IO AST
- mkBvnor :: Context -> AST -> AST -> IO AST
- mkBvxnor :: Context -> AST -> AST -> IO AST
- mkBvneg :: Context -> AST -> IO AST
- mkBvadd :: Context -> AST -> AST -> IO AST
- mkBvsub :: Context -> AST -> AST -> IO AST
- mkBvmul :: Context -> AST -> AST -> IO AST
- mkBvudiv :: Context -> AST -> AST -> IO AST
- mkBvsdiv :: Context -> AST -> AST -> IO AST
- mkBvurem :: Context -> AST -> AST -> IO AST
- mkBvsrem :: Context -> AST -> AST -> IO AST
- mkBvsmod :: Context -> AST -> AST -> IO AST
- mkBvult :: Context -> AST -> AST -> IO AST
- mkBvslt :: Context -> AST -> AST -> IO AST
- mkBvule :: Context -> AST -> AST -> IO AST
- mkBvsle :: Context -> AST -> AST -> IO AST
- mkBvuge :: Context -> AST -> AST -> IO AST
- mkBvsge :: Context -> AST -> AST -> IO AST
- mkBvugt :: Context -> AST -> AST -> IO AST
- mkBvsgt :: Context -> AST -> AST -> IO AST
- mkConcat :: Context -> AST -> AST -> IO AST
- mkExtract :: Context -> Int -> Int -> AST -> IO AST
- mkSignExt :: Context -> Int -> AST -> IO AST
- mkZeroExt :: Context -> Int -> AST -> IO AST
- mkRepeat :: Context -> Int -> AST -> IO AST
- mkBvshl :: Context -> AST -> AST -> IO AST
- mkBvlshr :: Context -> AST -> AST -> IO AST
- mkBvashr :: Context -> AST -> AST -> IO AST
- mkRotateLeft :: Context -> Int -> AST -> IO AST
- mkRotateRight :: Context -> Int -> AST -> IO AST
- mkExtRotateLeft :: Context -> AST -> AST -> IO AST
- mkExtRotateRight :: Context -> AST -> AST -> IO AST
- mkInt2bv :: Context -> Int -> AST -> IO AST
- mkBv2int :: Context -> AST -> Bool -> IO AST
- mkBvnegNoOverflow :: Context -> AST -> IO AST
- mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
- mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST
- mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST
- mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST
- mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST
- mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST
- mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST
- mkSelect :: Context -> AST -> AST -> IO AST
- mkStore :: Context -> AST -> AST -> AST -> IO AST
- mkConstArray :: Context -> Sort -> AST -> IO AST
- mkMap :: Context -> FuncDecl -> [AST] -> IO AST
- mkArrayDefault :: Context -> AST -> IO AST
- mkEmptySet :: Context -> Sort -> IO AST
- mkFullSet :: Context -> Sort -> IO AST
- mkSetAdd :: Context -> AST -> AST -> IO AST
- mkSetDel :: Context -> AST -> AST -> IO AST
- mkSetUnion :: Context -> [AST] -> IO AST
- mkSetIntersect :: Context -> [AST] -> IO AST
- mkSetDifference :: Context -> AST -> AST -> IO AST
- mkSetComplement :: Context -> AST -> IO AST
- mkSetMember :: Context -> AST -> AST -> IO AST
- mkSetSubset :: Context -> AST -> AST -> IO AST
- mkNumeral :: Context -> String -> Sort -> IO AST
- mkReal :: Context -> Int -> Int -> IO AST
- mkInt :: Context -> Int -> Sort -> IO AST
- mkUnsignedInt :: Context -> Word -> Sort -> IO AST
- mkInt64 :: Context -> Int64 -> Sort -> IO AST
- mkUnsignedInt64 :: Context -> Word64 -> Sort -> IO AST
- mkIntegral :: Integral a => Context -> a -> Sort -> IO AST
- mkRational :: Context -> Rational -> IO AST
- mkFixed :: HasResolution a => Context -> Fixed a -> IO AST
- mkRealNum :: Real r => Context -> r -> IO AST
- mkInteger :: Context -> Integer -> IO AST
- mkIntNum :: Integral a => Context -> a -> IO AST
- mkBitvector :: Context -> Int -> Integer -> IO AST
- mkBvNum :: Integral i => Context -> Int -> i -> IO AST
- mkSeqSort :: Context -> Sort -> IO Sort
- isSeqSort :: Context -> Sort -> IO Bool
- mkReSort :: Context -> Sort -> IO Sort
- isReSort :: Context -> Sort -> IO Bool
- mkStringSort :: Context -> IO Sort
- isStringSort :: Context -> Sort -> IO Bool
- mkString :: Context -> String -> IO AST
- isString :: Context -> AST -> IO Bool
- getString :: Context -> AST -> IO String
- mkSeqEmpty :: Context -> Sort -> IO AST
- mkSeqUnit :: Context -> AST -> IO AST
- mkSeqConcat :: Integral int => Context -> int -> [AST] -> IO AST
- mkSeqPrefix :: Context -> AST -> AST -> IO AST
- mkSeqSuffix :: Context -> AST -> AST -> IO AST
- mkSeqContains :: Context -> AST -> AST -> IO AST
- mkSeqExtract :: Context -> AST -> AST -> AST -> IO AST
- mkSeqReplace :: Context -> AST -> AST -> AST -> IO AST
- mkSeqAt :: Context -> AST -> AST -> IO AST
- mkSeqLength :: Context -> AST -> IO AST
- mkSeqIndex :: Context -> AST -> AST -> AST -> IO AST
- mkStrToInt :: Context -> AST -> IO AST
- mkIntToStr :: Context -> AST -> IO AST
- mkSeqToRe :: Context -> AST -> IO AST
- mkSeqInRe :: Context -> AST -> AST -> IO AST
- mkRePlus :: Context -> AST -> IO AST
- mkReStar :: Context -> AST -> IO AST
- mkReOption :: Context -> AST -> IO AST
- mkReUnion :: Integral int => Context -> int -> [AST] -> IO AST
- mkReConcat :: Integral int => Context -> int -> [AST] -> IO AST
- mkReRange :: Context -> AST -> AST -> IO AST
- mkReLoop :: Integral int => Context -> AST -> int -> int -> IO AST
- mkReIntersect :: Integral int => Context -> int -> [AST] -> IO AST
- mkReComplement :: Context -> AST -> IO AST
- mkReEmpty :: Context -> Sort -> IO AST
- mkReFull :: Context -> Sort -> IO AST
- mkPattern :: Context -> [AST] -> IO Pattern
- mkBound :: Context -> Int -> Sort -> IO AST
- mkForall :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
- mkExists :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST
- mkForallConst :: Context -> [Pattern] -> [App] -> AST -> IO AST
- mkExistsConst :: Context -> [Pattern] -> [App] -> AST -> IO AST
- getSymbolString :: Context -> Symbol -> IO String
- getSortKind :: Context -> Sort -> IO SortKind
- getBvSortSize :: Context -> Sort -> IO Int
- getDatatypeSortConstructors :: Context -> Sort -> IO [FuncDecl]
- getDatatypeSortRecognizers :: Context -> Sort -> IO [FuncDecl]
- getDatatypeSortConstructorAccessors :: Context -> Sort -> IO [[FuncDecl]]
- getDeclName :: Context -> FuncDecl -> IO Symbol
- getArity :: Context -> FuncDecl -> IO Int
- getDomain :: Context -> FuncDecl -> Int -> IO Sort
- getRange :: Context -> FuncDecl -> IO Sort
- appToAst :: Context -> App -> IO AST
- getAppDecl :: Context -> App -> IO FuncDecl
- getAppNumArgs :: Context -> App -> IO Int
- getAppArg :: Context -> App -> Int -> IO AST
- getAppArgs :: Context -> App -> IO [AST]
- getSort :: Context -> AST -> IO Sort
- getArraySortDomain :: Context -> Sort -> IO Sort
- getArraySortRange :: Context -> Sort -> IO Sort
- getBoolValue :: Context -> AST -> IO (Maybe Bool)
- getAstKind :: Context -> AST -> IO ASTKind
- isApp :: Context -> AST -> IO Bool
- toApp :: Context -> AST -> IO App
- getNumeralString :: Context -> AST -> IO String
- simplify :: Context -> AST -> IO AST
- simplifyEx :: Context -> AST -> Params -> IO AST
- getIndexValue :: Context -> AST -> IO Int
- isQuantifierForall :: Context -> AST -> IO Bool
- isQuantifierExists :: Context -> AST -> IO Bool
- getQuantifierWeight :: Context -> AST -> IO Int
- getQuantifierNumPatterns :: Context -> AST -> IO Int
- getQuantifierPatternAST :: Context -> AST -> Int -> IO AST
- getQuantifierPatterns :: Context -> AST -> IO [AST]
- getQuantifierNumNoPatterns :: Context -> AST -> IO Int
- getQuantifierNoPatternAST :: Context -> AST -> Int -> IO AST
- getQuantifierNoPatterns :: Context -> AST -> IO [AST]
- getQuantifierNumBound :: Context -> AST -> IO Int
- getQuantifierBoundName :: Context -> AST -> Int -> IO Symbol
- getQuantifierBoundSort :: Context -> AST -> Int -> IO Sort
- getQuantifierBoundVars :: Context -> AST -> IO [AST]
- getQuantifierBody :: Context -> AST -> IO AST
- getBool :: Context -> AST -> IO Bool
- getInt :: Context -> AST -> IO Integer
- getReal :: Context -> AST -> IO Rational
- getBv :: Context -> AST -> Bool -> IO Integer
- substituteVars :: Context -> AST -> [AST] -> IO AST
- substitute :: Context -> AST -> [(AST, AST)] -> IO AST
- modelEval :: Context -> Model -> AST -> Bool -> IO (Maybe AST)
- evalArray :: Context -> Model -> AST -> IO (Maybe FuncModel)
- getConstInterp :: Context -> Model -> FuncDecl -> IO (Maybe AST)
- getFuncInterp :: Context -> Model -> FuncDecl -> IO (Maybe FuncInterp)
- hasInterp :: Context -> Model -> FuncDecl -> IO Bool
- numConsts :: Context -> Model -> IO Word
- numFuncs :: Context -> Model -> IO Word
- getConstDecl :: Context -> Model -> Word -> IO FuncDecl
- getFuncDecl :: Context -> Model -> Word -> IO FuncDecl
- getConsts :: Context -> Model -> IO [FuncDecl]
- getFuncs :: Context -> Model -> IO [FuncDecl]
- isAsArray :: Context -> AST -> IO Bool
- isEqAST :: Context -> AST -> AST -> IO Bool
- addFuncInterp :: Context -> Model -> FuncDecl -> AST -> IO FuncInterp
- addConstInterp :: Context -> Model -> FuncDecl -> AST -> IO ()
- getAsArrayFuncDecl :: Context -> AST -> IO FuncDecl
- funcInterpGetNumEntries :: Context -> FuncInterp -> IO Int
- funcInterpGetEntry :: Context -> FuncInterp -> Int -> IO FuncEntry
- funcInterpGetElse :: Context -> FuncInterp -> IO AST
- funcInterpGetArity :: Context -> FuncInterp -> IO Int
- funcEntryGetValue :: Context -> FuncEntry -> IO AST
- funcEntryGetNumArgs :: Context -> FuncEntry -> IO Int
- funcEntryGetArg :: Context -> FuncEntry -> Int -> IO AST
- modelToString :: Context -> Model -> IO String
- showModel :: Context -> Model -> IO String
- type EvalAst a = Model -> AST -> IO (Maybe a)
- eval :: Context -> EvalAst AST
- evalBool :: Context -> EvalAst Bool
- evalInt :: Context -> EvalAst Integer
- evalReal :: Context -> EvalAst Rational
- evalBv :: Context -> Bool -> EvalAst Integer
- mapEval :: Traversable t => EvalAst a -> Model -> t AST -> IO (Maybe (t a))
- evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST))
- data FuncModel = FuncModel {
- interpMap :: [([AST], AST)]
- interpElse :: AST
- evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe FuncModel)
- mkTactic :: Context -> String -> IO Tactic
- andThenTactic :: Context -> Tactic -> Tactic -> IO Tactic
- orElseTactic :: Context -> Tactic -> Tactic -> IO Tactic
- skipTactic :: Context -> IO Tactic
- tryForTactic :: Context -> Tactic -> Int -> IO Tactic
- mkQuantifierEliminationTactic :: Context -> IO Tactic
- mkAndInverterGraphTactic :: Context -> IO Tactic
- applyTactic :: Context -> Tactic -> Goal -> IO ApplyResult
- getApplyResultNumSubgoals :: Context -> ApplyResult -> IO Int
- getApplyResultSubgoal :: Context -> ApplyResult -> Int -> IO Goal
- getApplyResultSubgoals :: Context -> ApplyResult -> IO [Goal]
- mkGoal :: Context -> Bool -> Bool -> Bool -> IO Goal
- goalAssert :: Context -> Goal -> AST -> IO ()
- getGoalSize :: Context -> Goal -> IO Int
- getGoalFormula :: Context -> Goal -> Int -> IO AST
- getGoalFormulas :: Context -> Goal -> IO [AST]
- data ASTPrintMode
- setASTPrintMode :: Context -> ASTPrintMode -> IO ()
- astToString :: Context -> AST -> IO String
- patternToString :: Context -> Pattern -> IO String
- sortToString :: Context -> Sort -> IO String
- funcDeclToString :: Context -> FuncDecl -> IO String
- benchmarkToSMTLibString :: Context -> String -> String -> String -> String -> [AST] -> AST -> IO String
- parseSMTLib2String :: Context -> String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> IO AST
- parseSMTLib2File :: Context -> String -> [Symbol] -> [Sort] -> [Symbol] -> [FuncDecl] -> IO AST
- data Z3Error = Z3Error {
- errCode :: Z3ErrorCode
- errMsg :: String
- data Z3ErrorCode
- data Version = Version {
- z3Major :: !Int
- z3Minor :: !Int
- z3Build :: !Int
- z3Revision :: !Int
- getVersion :: IO Version
- newtype Fixedpoint = Fixedpoint {
- unFixedpoint :: ForeignPtr Z3_fixedpoint
- mkFixedpoint :: Context -> IO Fixedpoint
- fixedpointAddRule :: Context -> Fixedpoint -> AST -> Symbol -> IO ()
- fixedpointSetParams :: Context -> Fixedpoint -> Params -> IO ()
- fixedpointRegisterRelation :: Context -> Fixedpoint -> FuncDecl -> IO ()
- fixedpointQueryRelations :: Context -> Fixedpoint -> [FuncDecl] -> IO Result
- fixedpointGetAnswer :: Context -> Fixedpoint -> IO AST
- fixedpointGetAssertions :: Context -> Fixedpoint -> IO [AST]
- newtype Optimize = Optimize {
- unOptimize :: ForeignPtr Z3_optimize
- mkOptimize :: Context -> IO Optimize
- optimizeAssert :: Context -> Optimize -> AST -> IO ()
- optimizeAssertAndTrack :: Context -> Optimize -> AST -> AST -> IO ()
- optimizeAssertSoft :: Context -> Optimize -> AST -> String -> Symbol -> IO Int
- optimizeMaximize :: Context -> Optimize -> AST -> IO Int
- optimizeMinimize :: Context -> Optimize -> AST -> IO Int
- optimizePush :: Context -> Optimize -> IO ()
- optimizePop :: Context -> Optimize -> IO ()
- optimizeCheck :: Context -> Optimize -> [AST] -> IO Result
- optimizeGetReasonUnknown :: Context -> Optimize -> IO String
- optimizeGetModel :: Context -> Optimize -> IO Model
- optimizeGetUnsatCore :: Context -> Optimize -> IO [AST]
- optimizeSetParams :: Context -> Optimize -> Params -> IO ()
- optimizeGetLower :: Context -> Optimize -> Int -> IO AST
- optimizeGetUpper :: Context -> Optimize -> Int -> IO AST
- optimizeGetUpperAsVector :: Context -> Optimize -> Int -> IO [AST]
- optimizeGetLowerAsVector :: Context -> Optimize -> Int -> IO [AST]
- optimizeToString :: Context -> Optimize -> IO String
- optimizeFromString :: Context -> Optimize -> String -> IO ()
- optimizeFromFile :: Context -> Optimize -> String -> IO ()
- optimizeGetHelp :: Context -> Optimize -> IO String
- optimizeGetAssertions :: Context -> Optimize -> IO [AST]
- optimizeGetObjectives :: Context -> Optimize -> IO [AST]
- data Logic
- mkSolver :: Context -> IO Solver
- mkSimpleSolver :: Context -> IO Solver
- mkSolverForLogic :: Context -> Logic -> IO Solver
- solverGetHelp :: Context -> Solver -> IO String
- solverSetParams :: Context -> Solver -> Params -> IO ()
- solverPush :: Context -> Solver -> IO ()
- solverPop :: Context -> Solver -> Int -> IO ()
- solverReset :: Context -> Solver -> IO ()
- solverGetNumScopes :: Context -> Solver -> IO Int
- solverAssertCnstr :: Context -> Solver -> AST -> IO ()
- solverAssertAndTrack :: Context -> Solver -> AST -> AST -> IO ()
- solverCheck :: Context -> Solver -> IO Result
- solverCheckAssumptions :: Context -> Solver -> [AST] -> IO Result
- solverGetModel :: Context -> Solver -> IO Model
- solverGetProof :: Context -> Solver -> IO AST
- solverGetUnsatCore :: Context -> Solver -> IO [AST]
- solverGetReasonUnknown :: Context -> Solver -> IO String
- solverToString :: Context -> Solver -> IO String
- solverCheckAndGetModel :: Context -> Solver -> IO (Result, Maybe Model)
Types
A Z3 symbol.
Used to name types, constants and functions.
A Z3 AST node.
This is the data-structure used in Z3 to represent terms, formulas and types.
A kind of AST representing 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
| Eq Constructor Source # | |
| Ord Constructor Source # | |
| Show Constructor Source # | |
A model for the constraints asserted into the logical context.
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.
Create configuration
mkConfig :: IO Config Source #
Create a configuration.
See withConfig.
delConfig :: Config -> IO () Source #
Delete a configuration.
See withConfig.
setParamValue :: Config -> String -> String -> IO () Source #
Set a configuration parameter.
Helpers
withConfig :: (Config -> IO a) -> IO a Source #
Run a computation using a temporally created configuration.
Note that the configuration object can be thrown away once
it has been used to create the Z3 Context.
Create context
mkContext :: Config -> IO Context Source #
Create a context using the given configuration.
Z3_del_context is called by Haskell's garbage collector before
freeing the Context object.
withContext :: Context -> (Ptr Z3_context -> IO r) -> IO r Source #
Parameters
mkParams :: Context -> IO 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 :: Context -> Params -> Symbol -> Bool -> IO () Source #
Add a Boolean parameter k with value v to the parameter set p.
paramsSetUInt :: Context -> Params -> Symbol -> Word -> IO () Source #
Add a unsigned parameter k with value v to the parameter set p.
paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO () Source #
Add a double parameter k with value v to the parameter set p.
paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO () Source #
Add a symbol parameter k with value v to the parameter set p.
paramsToString :: Context -> Params -> IO String Source #
Convert a parameter set into a string.
This function is mainly used for printing the contents of a parameter set.
Symbols
mkIntSymbol :: Integral int => Context -> int -> IO Symbol Source #
Create a Z3 symbol using an integer.
mkIntSymbol c i requires 0 <= i < 2^30
mkStringSymbol :: Context -> String -> IO Symbol Source #
Create a Z3 symbol using a String.
Sorts
mkUninterpretedSort :: Context -> Symbol -> IO Sort Source #
Create a free (uninterpreted) type using the given name (symbol).
Two free types are considered the same iff the have the same name.
mkBoolSort :: Context -> IO Sort Source #
Create the boolean type.
This type is used to create propositional variables and predicates.
mkIntSort :: Context -> IO Sort Source #
Create the integer type.
This is the type of arbitrary precision integers.
A machine integer can be represented using bit-vectors, see mkBvSort.
mkRealSort :: Context -> IO Sort Source #
Create the real type.
This type is not a floating point number. Z3 does not have support for floating point numbers yet.
mkBvSort :: Integral int => Context -> int -> IO Sort Source #
Create a bit-vector type of the given size.
This type can also be seen as a machine integer.
mkBvSort c sz requires sz >= 0
mkArraySort :: Context -> Sort -> Sort -> IO Sort Source #
Create an array type
We usually represent the array type as: [domain -> range]. Arrays are usually used to model the heap/memory in software verification.
Arguments
| :: Context | Context |
| -> Symbol | Name of the sort |
| -> [(Symbol, Sort)] | Name and sort of each field |
| -> IO (Sort, FuncDecl, [FuncDecl]) | Resulting sort, and function declarations for the constructor and projections. |
Create a tuple type
A tuple with n fields has a constructor and n projections. This function will also declare the constructor and projection functions.
Arguments
| :: Context | Context |
| -> Symbol | Name of the constructor |
| -> Symbol | Name of recognizer function |
| -> [(Symbol, Maybe Sort, Int)] | Name, sort option, and sortRefs |
| -> IO Constructor |
Create a contructor
mkDatatype :: Context -> Symbol -> [Constructor] -> IO Sort Source #
Create datatype, such as lists, trees, records, enumerations or unions of records.
The datatype may be recursive. Returns the datatype sort.
mkDatatypes :: Context -> [Symbol] -> [[Constructor]] -> IO [Sort] Source #
Create mutually recursive datatypes, such as a tree and forest.
Returns the datatype sorts
Constants and Applications
Arguments
| :: Context | Logical context. |
| -> Symbol | Name of the function (or constant). |
| -> [Sort] | Function domain (empty for constants). |
| -> Sort | Return sort of the function. |
| -> IO FuncDecl |
Declare a constant or function.
mkConst :: Context -> Symbol -> Sort -> IO AST Source #
Declare and create a constant.
This is a shorthand for:
do xd <- mkFunDecl c x [] s; mkApp c xd []
mkFreshFuncDecl :: Context -> String -> [Sort] -> Sort -> IO FuncDecl Source #
Declare a fresh constant or function.
Declare and create a fresh constant.
Helpers
mkVar :: Context -> Symbol -> Sort -> IO AST Source #
Declare and create a variable (aka constant).
An alias for mkConst.
mkBoolVar :: Context -> Symbol -> IO AST Source #
Declarate and create a variable of sort bool.
See mkVar.
mkRealVar :: Context -> Symbol -> IO AST Source #
Declarate and create a variable of sort real.
See mkVar.
mkIntVar :: Context -> Symbol -> IO AST Source #
Declarate and create a variable of sort int.
See mkVar.
Declarate and create a variable of sort bit-vector.
See mkVar.
mkFreshVar :: Context -> String -> Sort -> IO AST Source #
Declare and create a fresh variable (aka constant).
An alias for mkFreshConst.
mkFreshBoolVar :: Context -> String -> IO AST Source #
Declarate and create a fresh variable of sort bool.
See mkFreshVar.
mkFreshRealVar :: Context -> String -> IO AST Source #
Declarate and create a fresh variable of sort real.
See mkFreshVar.
mkFreshIntVar :: Context -> String -> IO 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 :: Context -> AST -> AST -> AST -> IO AST Source #
Create an AST node representing an if-then-else: ite(t1, t2, t3).
mkAnd :: Context -> [AST] -> IO AST Source #
Create an AST node representing args[0] and ... and args[num_args-1].
mkOr :: Context -> [AST] -> IO AST Source #
Create an AST node representing args[0] or ... or args[num_args-1].
mkDistinct :: Context -> [AST] -> IO AST Source #
The distinct construct is used for declaring the arguments pairwise distinct.
That is, and [ args!!i /= args!!j | i <- [0..length(args)-1], j <- [i+1..length(args)-1] ]
Requires a non-empty list.
mkDistinct1 :: Context -> NonEmpty AST -> IO AST Source #
Same as mkDistinct but type-safe.
Helpers
Arithmetic: Integers and Reals
mkAdd :: Context -> [AST] -> IO AST Source #
Create an AST node representing args[0] + ... + args[num_args-1].
mkMul :: Context -> [AST] -> IO AST Source #
Create an AST node representing args[0] * ... * args[num_args-1].
mkSub :: Context -> [AST] -> IO AST Source #
Create an AST node representing args[0] - ... - args[num_args - 1].
Requires a non-empty list.
Bit-vectors
mkBvredand :: Context -> AST -> IO AST Source #
Take conjunction of bits in vector, return vector of length 1.
mkBvredor :: Context -> AST -> IO AST Source #
Take disjunction of bits in vector, return vector of length 1.
mkBvsrem :: Context -> AST -> AST -> IO AST Source #
Two's complement signed remainder (sign follows dividend).
mkBvsmod :: Context -> AST -> AST -> IO AST Source #
Two's complement signed remainder (sign follows divisor).
mkBvsge :: Context -> AST -> AST -> IO AST Source #
Two's complement signed greater than or equal to.
mkExtract :: Context -> Int -> Int -> AST -> IO 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 :: Context -> Int -> AST -> IO 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 :: Context -> Int -> AST -> IO 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.
mkExtRotateRight :: Context -> AST -> AST -> IO AST Source #
Rotate bits of t1 to the right t2 times.
mkInt2bv :: Context -> Int -> AST -> IO AST Source #
Create an n bit bit-vector from the integer argument t1.
mkBv2int :: Context -> AST -> Bool -> IO 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 :: Context -> AST -> IO AST Source #
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.
mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST Source #
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST Source #
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST Source #
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.
mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST Source #
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.
mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST Source #
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.
mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST Source #
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow.
mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST Source #
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.
Arrays
Array read. The argument a is the array and i is the index of the array that gets read.
Array update.
The result of this function is an array that is equal to the input array (with respect to select) on all indices except for i, where it maps to v.
The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details.
Create the constant array.
The resulting term is an array, such that a select on an arbitrary index produces the value v.
Map a function f on the the argument arrays.
The n nodes args must be of array sorts [domain -> range_i]. The function declaration f must have type range_1 .. range_n -> range. The sort of the result is [domain -> range].
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
Create the empty set.
Remove an element from a set.
Take the set difference between two sets.
Check if the first set is a subset of the second set.
Numerals
Create a real from a fraction.
mkInt :: Context -> Int -> Sort -> IO 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 :: Context -> Word -> Sort -> IO 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 :: Context -> Int64 -> Sort -> IO 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 :: Context -> Word64 -> Sort -> IO 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 :: Integral a => Context -> a -> Sort -> IO AST Source #
Create a numeral of an int, bit-vector, or finite-domain sort.
mkRational :: Context -> Rational -> IO AST Source #
Create a numeral of sort real from a Rational.
mkFixed :: HasResolution a => Context -> Fixed a -> IO AST Source #
Create a numeral of sort real from a Fixed.
mkIntNum :: Integral a => Context -> a -> IO 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 :: Context -> Sort -> IO Sort Source #
Create a sequence sort out of the sort for the elements.
mkReSort :: Context -> Sort -> IO Sort Source #
Create a regular expression sort out of a sequence sort.
mkStringSort :: Context -> IO Sort Source #
Create a sort for 8 bit strings. This function creates a sort for ASCII strings. Each character is 8 bits.
isStringSort :: Context -> Sort -> IO Bool Source #
Check if s is a string sort.
mkString :: Context -> String -> IO AST Source #
Create a string constant out of the string that is passed in.
Check if prefix is a prefix of s.
Check if suffix is a suffix of s.
Check if container contains containee.
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 :: Context -> AST -> IO 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 => Context -> int -> [AST] -> IO AST Source #
Create the union of the regular languages.
mkReConcat :: Integral int => Context -> int -> [AST] -> IO 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 => Context -> int -> [AST] -> IO AST Source #
Create the intersection of the regular languages.
Quantifiers
Create a pattern for quantifier instantiation.
Z3 uses pattern matching to instantiate quantifiers. If a pattern is not provided for a quantifier, then Z3 will automatically compute a set of patterns for it. However, for optimal performance, the user should provide the patterns.
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is a called a multi-pattern.
In general, one can pass in a list of (multi-)patterns in the quantifier constructor.
Create a bound variable.
Bound variables are indexed by de-Bruijn indices.
See http://z3prover.github.io/api/html/group__capi.html#ga1d4da8849fca699b345322f8ee1fa31e
Arguments
| :: Context | |
| -> [Pattern] | Instantiation patterns (see |
| -> [Symbol] | Bound (quantified) variables xs. |
| -> [Sort] | Sorts of the bound variables. |
| -> AST | Body of the quantifier. |
| -> IO AST |
Create a forall formula.
The bound variables are de-Bruijn indices created using mkBound.
Z3 applies the convention that the last element in xs refers to the variable with index 0, the second to last element of xs refers to the variable with index 1, etc.
mkExists :: Context -> [Pattern] -> [Symbol] -> [Sort] -> AST -> IO AST Source #
Create an exists formula.
Similar to mkForall.
Arguments
| :: Context | |
| -> [Pattern] | Instantiation patterns (see |
| -> [App] | Constants to be abstracted into bound variables. |
| -> AST | Quantifier body. |
| -> IO AST |
Create a universal quantifier using a list of constants that will form the set of bound variables.
Arguments
| :: Context | |
| -> [Pattern] | Instantiation patterns (see |
| -> [App] | Constants to be abstracted into bound variables. |
| -> AST | Quantifier body. |
| -> IO AST |
Create a existential quantifier using a list of constants that will form the set of bound variables.
Accessors
getSymbolString :: Context -> Symbol -> IO String Source #
Return the symbol name.
getBvSortSize :: Context -> Sort -> IO Int Source #
Return the size of the given bit-vector sort.
getDatatypeSortConstructors Source #
Get list of constructors for datatype.
getDatatypeSortRecognizers Source #
Get list of recognizers for datatype.
getDatatypeSortConstructorAccessors Source #
Get list of accessors for the datatype constructor.
getDeclName :: Context -> FuncDecl -> IO Symbol Source #
Return the constant declaration name as a symbol.
getArity :: Context -> FuncDecl -> IO 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 :: Context -> App -> IO FuncDecl Source #
Return the declaration of a constant or function application.
getAppNumArgs :: Context -> App -> IO Int Source #
Return the number of argument of an application. If t is an constant, then the number of arguments is 0.
getAppArg :: Context -> App -> Int -> IO AST Source #
Return the i-th argument of the given application.
getAppArgs :: Context -> App -> IO [AST] Source #
Return a list of all the arguments of the given application.
getBoolValue :: Context -> AST -> IO (Maybe Bool) Source #
Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.
toApp :: Context -> AST -> IO App Source #
Convert an ast into an APP_AST. This is just type casting.
getNumeralString :: Context -> AST -> IO String Source #
Return numeral value, as a string of a numeric constant term.
getIndexValue :: Context -> AST -> IO Int Source #
isQuantifierForall :: Context -> AST -> IO Bool Source #
isQuantifierExists :: Context -> AST -> IO Bool Source #
getQuantifierWeight :: Context -> AST -> IO Int Source #
getQuantifierNumPatterns :: Context -> AST -> IO Int Source #
getQuantifierNumNoPatterns :: Context -> AST -> IO Int Source #
getQuantifierNumBound :: Context -> AST -> IO Int Source #
Helpers
Modifiers
Models
Arguments
| :: Context | |
| -> Model | Model m. |
| -> AST | Expression to evaluate t. |
| -> Bool | Model completion? |
| -> IO (Maybe AST) |
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 :: Context -> Model -> AST -> IO (Maybe FuncModel) Source #
Evaluate an array as a function, if possible.
getFuncInterp :: Context -> Model -> FuncDecl -> IO (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 :: Context -> AST -> IO 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 :: Context -> Model -> FuncDecl -> AST -> IO FuncInterp Source #
getAsArrayFuncDecl :: Context -> AST -> IO FuncDecl Source #
Return the function declaration f associated with a (_ as_array f) node.
funcInterpGetNumEntries :: Context -> FuncInterp -> IO Int Source #
Return the number of entries in the given function interpretation.
funcInterpGetEntry :: Context -> FuncInterp -> Int -> IO FuncEntry Source #
Return a _point_ of the given function intepretation. It represents the value of f in a particular point.
funcInterpGetElse :: Context -> FuncInterp -> IO AST Source #
Return the 'else' value of the given function interpretation.
funcInterpGetArity :: Context -> FuncInterp -> IO Int Source #
Return the arity (number of arguments) of the given function interpretation.
funcEntryGetNumArgs :: Context -> FuncEntry -> IO Int Source #
Return the number of arguments in a Z3_func_entry object.
funcEntryGetArg :: Context -> FuncEntry -> Int -> IO AST Source #
Return an argument of a Z3_func_entry object.
modelToString :: Context -> Model -> IO String Source #
Convert the given model into a string.
showModel :: Context -> Model -> IO String Source #
Deprecated: Use modelToString instead.
Alias for modelToString.
Helpers
mapEval :: Traversable t => EvalAst a -> Model -> t AST -> IO (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 c) can be used to obtain
the Integer interpretation of a list of AST of sort int.
evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST)) Source #
Evaluate a collection of AST nodes in the given model.
The interpretation of a function.
evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe FuncModel) Source #
Evaluate a function declaration to a list of argument/value pairs.
Tactics
skipTactic :: Context -> IO Tactic Source #
mkQuantifierEliminationTactic :: Context -> IO Tactic Source #
mkAndInverterGraphTactic :: Context -> IO Tactic Source #
applyTactic :: Context -> Tactic -> Goal -> IO ApplyResult Source #
getApplyResultNumSubgoals :: Context -> ApplyResult -> IO Int Source #
getApplyResultSubgoal :: Context -> ApplyResult -> Int -> IO Goal Source #
getApplyResultSubgoals :: Context -> ApplyResult -> IO [Goal] Source #
getGoalSize :: Context -> Goal -> IO Int 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 :: Context -> ASTPrintMode -> IO () Source #
Set the pretty-printing mode for converting ASTs to strings.
astToString :: Context -> AST -> IO String Source #
Convert an AST to a string.
patternToString :: Context -> Pattern -> IO String Source #
Convert a pattern to a string.
sortToString :: Context -> Sort -> IO String Source #
Convert a sort to a string.
funcDeclToString :: Context -> FuncDecl -> IO String Source #
Convert a FuncDecl to a string.
benchmarkToSMTLibString Source #
Arguments
| :: Context | |
| -> String | name |
| -> String | logic |
| -> String | status |
| -> String | attributes |
| -> [AST] | assumptions |
| -> AST | formula |
| -> IO String |
Convert the given benchmark into SMT-LIB formatted string.
The output format can be configured via setASTPrintMode.
Parser interface
Error Handling
Constructors
| Z3Error | |
Fields
| |
data Z3ErrorCode Source #
Z3 error codes.
Constructors
| SortError | |
| IOB | |
| InvalidArg | |
| ParserError | |
| NoParser | |
| InvalidPattern | |
| MemoutFail | |
| FileAccessError | |
| InternalFatal | |
| InvalidUsage | |
| DecRefError | |
| Z3Exception |
Instances
| Show Z3ErrorCode Source # | |
Miscellaneous
Constructors
| Version | |
Fields
| |
getVersion :: IO Version Source #
Return Z3 version number information.
Fixedpoint
newtype Fixedpoint Source #
Constructors
| Fixedpoint | |
Fields
| |
Instances
| Eq Fixedpoint Source # | |
mkFixedpoint :: Context -> IO Fixedpoint Source #
fixedpointAddRule :: Context -> Fixedpoint -> AST -> Symbol -> IO () Source #
fixedpointSetParams :: Context -> Fixedpoint -> Params -> IO () Source #
fixedpointRegisterRelation :: Context -> Fixedpoint -> FuncDecl -> IO () Source #
fixedpointQueryRelations :: Context -> Fixedpoint -> [FuncDecl] -> IO Result Source #
fixedpointGetAnswer :: Context -> Fixedpoint -> IO AST Source #
fixedpointGetAssertions :: Context -> Fixedpoint -> IO [AST] Source #
Optimization
Constructors
| Optimize | |
Fields
| |
mkOptimize :: Context -> IO Optimize Source #
optimizePush :: Context -> Optimize -> IO () Source #
optimizePop :: Context -> Optimize -> IO () Source #
optimizeGetReasonUnknown :: Context -> Optimize -> IO String Source #
optimizeToString :: Context -> Optimize -> IO String Source #
optimizeFromString :: Context -> Optimize -> String -> IO () Source #
optimizeFromFile :: Context -> Optimize -> String -> IO () Source #
optimizeGetHelp :: Context -> Optimize -> IO String Source #
Solvers
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. |
mkSimpleSolver :: Context -> IO Solver Source #
solverGetHelp :: Context -> Solver -> IO String Source #
Return a string describing all solver available parameters.
solverSetParams :: Context -> Solver -> Params -> IO () Source #
Set the given solver using the given parameters.
solverPush :: Context -> Solver -> IO () Source #
solverReset :: Context -> Solver -> IO () Source #
solverGetNumScopes :: Context -> Solver -> IO Int Source #
Number of backtracking points.
solverCheck :: Context -> Solver -> IO Result Source #
Check whether the assertions in a given solver are consistent or not.
solverCheckAssumptions :: Context -> Solver -> [AST] -> IO Result Source #
Check whether the assertions in the given solver and optional assumptions are consistent or not.
solverGetModel :: Context -> Solver -> IO Model Source #
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.
solverGetProof :: Context -> Solver -> IO 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 :: Context -> Solver -> IO [AST] Source #
Retrieve the unsat core for the last solverCheckAssumptions; the unsat core is a subset of the assumptions
solverGetReasonUnknown :: Context -> Solver -> IO String Source #
Return a brief justification for an Unknown result for the commands solverCheck and solverCheckAssumptions.
solverToString :: Context -> Solver -> IO String Source #
Convert the given solver into a string.