Z3.Base

Low-level bindings to Z3 API.

There is (mostly) a one-to-one correspondence with Z3 C API, thus see http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html for further details.

Note that these bindings still focus on the old Z3 3.x API, and will not handle reference counting for you if you decide to use Z3 4.x API functions. Mixing both API is known to cause some segmentation faults!

Supporting Z3 4.x API (and removing support for 3.x) is planned for the 0.4 version of these bindings.

Types

data Config

A Z3 configuration object.

Instances

Eq Config

data Context

A Z3 logical context.

Instances

Eq Context

data Symbol

A Z3 symbol.

Used to name types, constants and functions.

Instances

Eq Symbol

Ord Symbol

Show Symbol

Storable Symbol

data AST

A Z3 AST node.

This is the data-structure used in Z3 to represent terms, formulas and types.

Instances

Eq AST

Ord AST

Show AST

Storable AST

Typeable * AST

data Sort

A kind of AST representing types.

Instances

Eq Sort

Ord Sort

Show Sort

Storable Sort

data FuncDecl

A kind of AST representing function symbols.

Instances

Eq FuncDecl

Ord FuncDecl

Show FuncDecl

Storable FuncDecl

Typeable * FuncDecl

data App

A kind of AST representing constant and function declarations.

Instances

Eq App

Ord App

Show App

Storable App

data Pattern

A kind of AST representing pattern and multi-patterns to guide quantifier instantiation.

Instances

Eq Pattern

Ord Pattern

Show Pattern

Storable Pattern

data Model

A model for the constraints asserted into the logical context.

Instances

Eq Model

data FuncInterp

An interpretation of a function in a model.

Instances

Eq FuncInterp

data FuncEntry

Representation of the value of a Z3_func_interp at a particular point.

Instances

Eq FuncEntry

data Params

A Z3 parameter set.

Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.

Instances

Eq Params

data Solver

A Z3 solver engine.

A(n) (incremental) solver, possibly specialized by a particular tactic or logic.

Instances

Eq Solver

Satisfiability result

data Result

Result of a satisfiability check.

This corresponds to the z3_lbool type in the C API.

Constructors

Sat

Unsat

Undef

Instances

Eq Result

Ord Result

Read Result

Show Result

Configuration

mkConfig :: IO Config

Create a configuration.

delConfig :: Config -> IO ()

Delete a configuration.

withConfig :: (Config -> IO a) -> IO a

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.

setParamValue :: Config -> String -> String -> IO ()

Set a configuration parameter.

Context

mkContext :: Config -> IO Context

Create a context using the given configuration.

delContext :: Context -> IO ()

Delete the given logical context.

withContext :: Config -> (Context -> IO a) -> IO a

Run a computation using a temporally created context.

contextToString :: Context -> IO String

Convert the given logical context into a string.

showContext :: Context -> IO String

Deprecated: Use contextToString instead.

Alias for contextToString.

Symbols

mkIntSymbol :: Integral int => Context -> int -> IO Symbol

Create a Z3 symbol using an integer.

mkIntSymbol c i requires 0 <= i < 2^30

mkStringSymbol :: Context -> String -> IO Symbol

Create a Z3 symbol using a string.

Sorts

mkUninterpretedSort :: Context -> Symbol -> IO Sort

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

Create the boolean type.

This type is used to create propositional variables and predicates.

mkIntSort :: Context -> IO Sort

Create an 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

Create a real type.

This type is not a floating point number. Z3 does not have support for floating point numbers yet.

mkBvSort :: Context -> Int -> IO Sort

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

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.

mkTupleSort

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.

Constants and Applications

mkFuncDecl

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.

mkApp :: Context -> FuncDecl -> [AST] -> IO AST

Create a constant or function application.

mkConst :: Context -> Symbol -> Sort -> IO AST

Declare and create a constant.

This is a shorthand for: do xd <- mkFunDecl c x [] s; mkApp c xd []

mkTrue :: Context -> IO AST

Create an AST node representing true.

mkFalse :: Context -> IO AST

Create an AST node representing false.

mkEq :: Context -> AST -> AST -> IO AST

Create an AST node representing l = r.

mkNot :: Context -> AST -> IO AST

Create an AST node representing not(a).

mkIte :: Context -> AST -> AST -> AST -> IO AST

Create an AST node representing an if-then-else: ite(t1, t2, t3).

mkIff :: Context -> AST -> AST -> IO AST

Create an AST node representing t1 iff t2.

mkImplies :: Context -> AST -> AST -> IO AST

Create an AST node representing t1 implies t2.

mkXor :: Context -> AST -> AST -> IO AST

Create an AST node representing t1 xor t2.

mkAnd :: Context -> [AST] -> IO AST

Create an AST node representing args[0] and ... and args[num_args-1].

mkOr :: Context -> [AST] -> IO AST

Create an AST node representing args[0] or ... or args[num_args-1].

mkDistinct :: Context -> [AST] -> IO AST

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] ]

mkAdd :: Context -> [AST] -> IO AST

Create an AST node representing args[0] + ... + args[num_args-1].

mkMul :: Context -> [AST] -> IO AST

Create an AST node representing args[0] * ... * args[num_args-1].

mkSub :: Context -> [AST] -> IO AST

Create an AST node representing args[0] - ... - args[num_args - 1].

mkUnaryMinus :: Context -> AST -> IO AST

Create an AST node representing -arg.

mkDiv :: Context -> AST -> AST -> IO AST

Create an AST node representing arg1 div arg2.

mkMod :: Context -> AST -> AST -> IO AST

Create an AST node representing arg1 mod arg2.

mkRem :: Context -> AST -> AST -> IO AST

Create an AST node representing arg1 rem arg2.

mkLt :: Context -> AST -> AST -> IO AST

Create less than.

mkLe :: Context -> AST -> AST -> IO AST

Create less than or equal to.

mkGt :: Context -> AST -> AST -> IO AST

Create greater than.

mkGe :: Context -> AST -> AST -> IO AST

Create greater than or equal to.

mkInt2Real :: Context -> AST -> IO AST

Coerce an integer to a real.

mkReal2Int :: Context -> AST -> IO AST

Coerce a real to an integer.

mkIsInt :: Context -> AST -> IO AST

Check if a real number is an integer.

Bit-vectors

mkBvnot :: Context -> AST -> IO AST

Bitwise negation.

mkBvredand :: Context -> AST -> IO AST

Take conjunction of bits in vector, return vector of length 1.

mkBvredor :: Context -> AST -> IO AST

Take disjunction of bits in vector, return vector of length 1.

mkBvand :: Context -> AST -> AST -> IO AST

Bitwise and.

mkBvor :: Context -> AST -> AST -> IO AST

Bitwise or.

mkBvxor :: Context -> AST -> AST -> IO AST

Bitwise exclusive-or.

mkBvnand :: Context -> AST -> AST -> IO AST

Bitwise nand.

mkBvnor :: Context -> AST -> AST -> IO AST

Bitwise nor.

mkBvxnor :: Context -> AST -> AST -> IO AST

Bitwise xnor.

mkBvneg :: Context -> AST -> IO AST

Standard two's complement unary minus.

mkBvadd :: Context -> AST -> AST -> IO AST

Standard two's complement addition.

mkBvsub :: Context -> AST -> AST -> IO AST

Standard two's complement subtraction.

mkBvmul :: Context -> AST -> AST -> IO AST

Standard two's complement multiplication.

mkBvudiv :: Context -> AST -> AST -> IO AST

Unsigned division.

mkBvsdiv :: Context -> AST -> AST -> IO AST

Two's complement signed division.

mkBvurem :: Context -> AST -> AST -> IO AST

Unsigned remainder.

mkBvsrem :: Context -> AST -> AST -> IO AST

Two's complement signed remainder (sign follows dividend).

mkBvsmod :: Context -> AST -> AST -> IO AST

Two's complement signed remainder (sign follows divisor).

mkBvult :: Context -> AST -> AST -> IO AST

Unsigned less than.

mkBvslt :: Context -> AST -> AST -> IO AST

Two's complement signed less than.

mkBvule :: Context -> AST -> AST -> IO AST

Unsigned less than or equal to.

mkBvsle :: Context -> AST -> AST -> IO AST

Two's complement signed less than or equal to.

mkBvuge :: Context -> AST -> AST -> IO AST

Unsigned greater than or equal to.

mkBvsge :: Context -> AST -> AST -> IO AST

Two's complement signed greater than or equal to.

mkBvugt :: Context -> AST -> AST -> IO AST

Unsigned greater than.

mkBvsgt :: Context -> AST -> AST -> IO AST

Two's complement signed greater than.

mkConcat :: Context -> AST -> AST -> IO AST

Concatenate the given bit-vectors.

mkExtract :: Context -> Int -> Int -> AST -> IO AST

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

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

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.

mkRepeat :: Context -> Int -> AST -> IO AST

Repeat the given bit-vector up length i.

mkBvshl :: Context -> AST -> AST -> IO AST

Shift left.

mkBvlshr :: Context -> AST -> AST -> IO AST

Logical shift right.

mkBvashr :: Context -> AST -> AST -> IO AST

Arithmetic shift right.

mkRotateLeft :: Context -> Int -> AST -> IO AST

Rotate bits of t1 to the left i times.

mkRotateRight :: Context -> Int -> AST -> IO AST

Rotate bits of t1 to the right i times.

mkExtRotateLeft :: Context -> AST -> AST -> IO AST

Rotate bits of t1 to the left t2 times.

mkExtRotateRight :: Context -> AST -> AST -> IO AST

Rotate bits of t1 to the right t2 times.

mkInt2bv :: Context -> Int -> AST -> IO AST

Create an n bit bit-vector from the integer argument t1.

mkBv2int :: Context -> AST -> Bool -> IO AST

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

Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.

mkBvaddNoOverflow :: Context -> AST -> AST -> Bool -> IO AST

Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

mkBvaddNoUnderflow :: Context -> AST -> AST -> IO AST

Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.

mkBvsubNoOverflow :: Context -> AST -> AST -> IO AST

Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.

mkBvsubNoUnderflow :: Context -> AST -> AST -> IO AST

Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.

mkBvmulNoOverflow :: Context -> AST -> AST -> Bool -> IO AST

Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.

mkBvmulNoUnderflow :: Context -> AST -> AST -> IO AST

Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow.

mkBvsdivNoOverflow :: Context -> AST -> AST -> IO AST

Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.

Arrays

mkSelect

Arguments

:: Context

-> AST

Array.

-> AST

Index of the array to read.

-> IO AST

Array read. The argument a is the array and i is the index of the array that gets read.

mkStore

Arguments

:: Context

-> AST

Array.

-> AST

Index i of the array.

-> AST

New value for i.

-> IO AST

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.

mkConstArray

Arguments

:: Context

-> Sort

Domain sort of the array.

-> AST

Value v that the array maps to.

-> IO AST

Create the constant array.

The resulting term is an array, such that a select on an arbitrary index produces the value v.

mkMap

Arguments

:: Context

-> FuncDecl

Function f.

-> [AST]

List of arrays.

-> IO AST

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].

mkArrayDefault

Arguments

:: Context

-> AST

Array.

-> IO AST

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

mkNumeral :: Context -> String -> Sort -> IO AST

Create a numeral of a given sort.

mkInt :: Integral a => Context -> a -> IO AST

Create a numeral of sort int.

mkReal :: Real r => Context -> r -> IO AST

Create a numeral of sort real.

Quantifiers

mkPattern

Arguments

:: Context

-> [AST]

Terms.

-> IO Pattern

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.

mkBound

Arguments

:: Context

-> Int

de-Bruijn index.

-> Sort

-> IO AST

Create a bound variable.

Bound variables are indexed by de-Bruijn indices.

See http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1d4da8849fca699b345322f8ee1fa31e

mkForall

Arguments

:: Context

-> [Pattern]

Instantiation patterns (see mkPattern).

-> [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

Create an exists formula.

Similar to mkForall.

mkForallConst

Arguments

:: Context

-> [Pattern]

Instantiation patterns (see mkPattern).

-> [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.

mkExistsConst

Arguments

:: Context

-> [Pattern]

Instantiation patterns (see mkPattern).

-> [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

getBvSortSize :: Context -> Sort -> IO Int

Return the size of the given bit-vector sort.

getSort :: Context -> AST -> IO Sort

Return the sort of an AST node.

getBool :: Context -> AST -> IO (Maybe Bool)

Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.

getInt :: Context -> AST -> IO Integer

Return Z3Int value

getReal :: Context -> AST -> IO Rational

Return Z3Real value

toApp :: Context -> AST -> IO App

Convert an ast into an APP_AST. This is just type casting.

Models

data FuncModel

The interpretation of a function.

Constructors

FuncModel

Fields

interpMap :: [([AST], AST)]

Mapping from arguments to values.

interpElse :: AST

Default value.

eval

Arguments

:: Context

-> Model

Model m.

-> AST

Expression to evaluate t.

-> 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.

evalT :: Traversable t => Context -> Model -> t AST -> IO (Maybe (t AST))

Evaluate a collection of AST nodes in the given model.

evalFunc :: Context -> Model -> FuncDecl -> IO (Maybe FuncModel)

Evaluate a function declaration to a list of argument/value pairs.

evalArray :: Context -> Model -> AST -> IO (Maybe FuncModel)

Evaluate an array as a function, if possible.

getFuncInterp :: Context -> Model -> FuncDecl -> IO (Maybe FuncInterp)

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

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 :: Context -> AST -> IO FuncDecl

Return the function declaration f associated with a (_ as_array f) node.

funcInterpGetNumEntries :: Context -> FuncInterp -> IO Int

Return the number of entries in the given function interpretation.

funcInterpGetEntry :: Context -> FuncInterp -> Int -> IO FuncEntry

Return a _point_ of the given function intepretation. It represents the value of f in a particular point.

funcInterpGetElse :: Context -> FuncInterp -> IO AST

Return the 'else' value of the given function interpretation.

funcInterpGetArity :: Context -> FuncInterp -> IO Int

Return the arity (number of arguments) of the given function interpretation.

funcEntryGetValue :: Context -> FuncEntry -> IO AST

Return the value of this point.

funcEntryGetNumArgs :: Context -> FuncEntry -> IO Int

Return the number of arguments in a Z3_func_entry object.

funcEntryGetArg :: Context -> FuncEntry -> Int -> IO AST

Return an argument of a Z3_func_entry object.

modelToString :: Context -> Model -> IO String

Convert the given model into a string.

showModel :: Context -> Model -> IO String

Deprecated: Use modelToString instead.

Alias for modelToString.

Constraints

assertCnstr :: Context -> AST -> IO ()

Assert a constraing into the logical context.

check :: Context -> IO Result

Check whether the given logical context is consistent or not.

checkAndGetModel :: Context -> IO (Result, Maybe Model)

Check whether the given logical context is consistent or not.

If the logical context is not unsatisfiable and model construction is enabled (via mkConfig), then a model is returned. The caller is responsible for deleting the model using the function delModel.

getModel :: Context -> IO (Result, Maybe Model)

Deprecated: Use checkAndGetModel instead.

Check whether the given logical context is consistent or not.

delModel :: Context -> Model -> IO ()

Delete a model object.

push :: Context -> IO ()

Create a backtracking point.

pop :: Context -> Int -> IO ()

Backtrack n backtracking points.

Parameters

mkParams :: Context -> IO Params

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

paramsSetBool :: Context -> Params -> Symbol -> Bool -> IO ()

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

paramsSetUInt :: Context -> Params -> Symbol -> Int -> IO ()

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

paramsSetDouble :: Context -> Params -> Symbol -> Double -> IO ()

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

paramsSetSymbol :: Context -> Params -> Symbol -> Symbol -> IO ()

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

paramsToString :: Context -> Params -> IO String

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

Solvers

data Logic

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!

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.

Instances

Show Logic

mkSolver :: Context -> IO Solver

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

mkSimpleSolver :: Context -> IO Solver

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

mkSolverForLogic :: Context -> Logic -> IO Solver

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

solverSetParams :: Context -> Solver -> Params -> IO ()

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

solverPush :: Context -> Solver -> IO ()

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

solverPop :: Context -> Solver -> Int -> IO ()

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

solverReset :: Context -> Solver -> IO ()

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

solverGetNumScopes :: Context -> Solver -> IO Int

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

Number of backtracking points.

solverAssertCnstr :: Context -> Solver -> AST -> IO ()

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

solverAssertAndTrack :: Context -> Solver -> AST -> AST -> IO ()

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

solverCheck :: Context -> Solver -> IO Result

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

Check whether the assertions in a given solver are consistent or not.

solverGetModel :: Context -> Solver -> IO Model

solverCheckAndGetModel :: Context -> Solver -> IO (Result, Maybe Model)

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

solverGetReasonUnknown :: Context -> Solver -> IO String

Warning: New Z3 API support is still incomplete and fragile: you may experience segmentation faults!

solverToString :: Context -> Solver -> IO String

Convert the given solver into a string.

String Conversion

data ASTPrintMode

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.

Constructors

Z3_PRINT_SMTLIB_FULL

Z3_PRINT_LOW_LEVEL

Z3_PRINT_SMTLIB_COMPLIANT

Z3_PRINT_SMTLIB2_COMPLIANT

setASTPrintMode :: Context -> ASTPrintMode -> IO ()

Set the pretty-printing mode for converting ASTs to strings.

astToString :: Context -> AST -> IO String

Convert an AST to a string.

patternToString :: Context -> Pattern -> IO String

Convert a pattern to a string.

sortToString :: Context -> Sort -> IO String

Convert a sort to a string.

funcDeclToString :: Context -> FuncDecl -> IO String

Convert a FuncDecl to a string.

benchmarkToSMTLibString

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.

Miscellaneous

data Version

Constructors

Version

Fields

z3Major :: !Int

z3Minor :: !Int

z3Build :: !Int

z3Revision :: !Int

Instances

Eq Version

Ord Version

Show Version

getVersion :: IO Version

Return Z3 version number information.

Error Handling

data Z3Error

Z3 exceptions.

Constructors

Z3Error

Fields

errCode :: Z3ErrorCode

errMsg :: String

Instances

Show Z3Error

Exception Z3Error

Typeable * Z3Error

data Z3ErrorCode

Constructors

SortError

IOB

InvalidArg

ParserError

NoParser

InvalidPattern

MemoutFail

FileAccessError

InternalFatal

InvalidUsage

DecRefError

Z3Exception

Instances

Show Z3ErrorCode

Typeable * Z3ErrorCode