Copyright | (c) Iago Abal, 2013 (c) David Castro, 2013 |
---|---|
License | BSD3 |
Maintainer | Iago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com> |
Safe Haskell | None |
Language | Haskell98 |
A simple monadic wrapper for Base
.
- class (Monad m, MonadIO m) => MonadZ3 m where
- getSolver :: m (Maybe 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
- delEnv :: Z3Env -> IO ()
- evalZ3WithEnv :: Z3 a -> Z3Env -> IO a
- data Symbol
- data AST
- data Sort
- data FuncDecl
- data App
- data Pattern
- data Model
- data Context
- data FuncInterp
- data FuncEntry
- data FuncModel = FuncModel {
- interpMap :: [([AST], AST)]
- interpElse :: AST
- data Solver
- data Result
- contextToString :: MonadZ3 z3 => z3 String
- showContext :: MonadZ3 z3 => 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
- mkArraySort :: MonadZ3 z3 => Sort -> Sort -> z3 Sort
- mkTupleSort :: MonadZ3 z3 => Symbol -> [(Symbol, Sort)] -> z3 (Sort, FuncDecl, [FuncDecl])
- mkFuncDecl :: MonadZ3 z3 => Symbol -> [Sort] -> Sort -> z3 FuncDecl
- mkApp :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST
- mkConst :: MonadZ3 z3 => Symbol -> Sort -> 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
- mkAdd :: MonadZ3 z3 => [AST] -> z3 AST
- mkMul :: MonadZ3 z3 => [AST] -> z3 AST
- mkSub :: MonadZ3 z3 => [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
- 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
- mkNumeral :: MonadZ3 z3 => String -> Sort -> z3 AST
- mkInt :: (MonadZ3 z3, Integral a) => a -> z3 AST
- mkReal :: (MonadZ3 z3, Real r) => r -> z3 AST
- mkPattern :: MonadZ3 z3 => [AST] -> z3 Pattern
- mkBound :: MonadZ3 z3 => Int -> Sort -> z3 AST
- mkForall :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST
- mkExists :: MonadZ3 z3 => [Pattern] -> [Symbol] -> [Sort] -> AST -> z3 AST
- mkForallConst :: MonadZ3 z3 => [Pattern] -> [App] -> AST -> z3 AST
- mkExistsConst :: MonadZ3 z3 => [Pattern] -> [App] -> AST -> z3 AST
- getBvSortSize :: MonadZ3 z3 => Sort -> z3 Int
- getBool :: MonadZ3 z3 => AST -> z3 (Maybe Bool)
- getInt :: MonadZ3 z3 => AST -> z3 Integer
- getReal :: MonadZ3 z3 => AST -> z3 Rational
- toApp :: MonadZ3 z3 => AST -> z3 App
- eval :: MonadZ3 z3 => Model -> AST -> z3 (Maybe AST)
- evalT :: (MonadZ3 z3, Traversable t) => Model -> t AST -> z3 (Maybe (t AST))
- evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel)
- evalArray :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel)
- getFuncInterp :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncInterp)
- isAsArray :: MonadZ3 z3 => AST -> z3 Bool
- 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
- assertCnstr :: MonadZ3 z3 => AST -> z3 ()
- check :: MonadZ3 z3 => z3 Result
- getModel :: MonadZ3 z3 => z3 (Result, Maybe Model)
- delModel :: MonadZ3 z3 => Model -> z3 ()
- withModel :: (Applicative z3, MonadZ3 z3) => (Model -> z3 a) -> z3 (Result, Maybe a)
- 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
- 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
- solverToString :: MonadZ3 z3 => z3 String
- benchmarkToSMTLibString :: MonadZ3 z3 => String -> String -> String -> String -> [AST] -> AST -> z3 String
- data Version = Version {}
- getVersion :: MonadZ3 z3 => z3 Version
Z3 monad
module Z3.Opts
Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!
Solvers available in Z3.
These are described at http://smtlib.cs.uiowa.edu/logics.html
WARNING: Support for solvers is fragile, you may experience segmentation faults!
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
newEnv :: Maybe Logic -> Opts -> IO Z3Env Source
Create a new Z3 environment.
Until we move to Z3 API 4.0 you need to manually freed this
environment using delEnv
.
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.
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.
Representation of the value of a Z3_func_interp
at a particular point.
The interpretation of a function.
A Z3 solver engine.
A(n) (incremental) solver, possibly specialized by a particular tactic or logic.
Satisfiability result
Result of a satisfiability check.
This corresponds to the z3_lbool type in the C API.
Context
contextToString :: MonadZ3 z3 => z3 String Source
Convert Z3's logical context into a string.
showContext :: MonadZ3 z3 => z3 String Source
Alias for contextToString
.
Symbols
mkIntSymbol :: (MonadZ3 z3, Integral i) => i -> z3 Symbol Source
Create a Z3 symbol using an integer.
mkStringSymbol :: MonadZ3 z3 => String -> z3 Symbol Source
Create a Z3 symbol using a string.
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.
:: 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
Constants and Applications
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.
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].
mkUnaryMinus :: MonadZ3 z3 => AST -> z3 AST Source
Create an AST node representing -arg.
mkInt2Real :: MonadZ3 z3 => AST -> z3 AST Source
Coerce an integer to a real.
mkReal2Int :: MonadZ3 z3 => AST -> z3 AST Source
Coerce a real to an integer.
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).
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.
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.
Numerals
Quantifiers
Accessors
getBvSortSize :: MonadZ3 z3 => Sort -> z3 Int Source
Return the size of the given bit-vector sort.
getBool :: MonadZ3 z3 => AST -> z3 (Maybe Bool) Source
Returns Just True
, Just False
, or Nothing
for undefined.
Models
evalT :: (MonadZ3 z3, Traversable t) => Model -> t AST -> z3 (Maybe (t AST)) Source
Evaluate a collection of AST nodes in the given model.
evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel) Source
Get function as a list of argument/value pairs.
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.
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.
funcEntryGetValue :: MonadZ3 z3 => FuncEntry -> z3 AST Source
Return the value of this point.
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.
modelToString :: MonadZ3 z3 => Model -> z3 String Source
Convert the given model into a string.
Constraints
assertCnstr :: MonadZ3 z3 => AST -> z3 () Source
Assert a constraing into the logical context.
check :: MonadZ3 z3 => z3 Result Source
Check whether the given logical context is consistent or not.
getNumScopes :: MonadZ3 z3 => z3 Int Source
Get number of backtracking points.
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.
astToString :: MonadZ3 z3 => AST -> z3 String Source
Convert an AST to a string.
patternToString :: MonadZ3 z3 => Pattern -> z3 String Source
Convert a pattern to a string.
sortToString :: MonadZ3 z3 => Sort -> z3 String Source
Convert a sort to a string.
funcDeclToString :: MonadZ3 z3 => FuncDecl -> z3 String Source
Convert a FuncDecl to a string.
solverToString :: MonadZ3 z3 => z3 String Source
Convert the solver to a string.
benchmarkToSMTLibString Source
:: 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
.
Miscellaneous
getVersion :: MonadZ3 z3 => z3 Version Source
Return Z3 version number information.