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.

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

Typeable * AST

data Sort

A kind of AST representing types.

Instances

Eq Sort

Ord Sort

Show Sort

data FuncDecl

A kind of AST representing function symbols.

Instances

Eq FuncDecl

Ord FuncDecl

Show FuncDecl

Typeable * FuncDecl

data App

A kind of AST representing constant and function declarations.

Instances

Eq App

Ord App

Show App

data Pattern

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

Instances

Eq Pattern

Ord Pattern

Show Pattern

data Constructor

A type contructor for a (recursive) datatype.

Instances

Eq Constructor

Ord Constructor

Show Constructor

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

data ASTKind

Different kinds of Z3 AST nodes.

Constructors

Z3_NUMERAL_AST

Z3_APP_AST

Z3_VAR_AST

Z3_QUANTIFIER_AST

Z3_SORT_AST

Z3_FUNC_DECL_AST

Z3_UNKNOWN_AST

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

Create configuration

mkConfig :: IO Config

Create a configuration.

See withConfig.

delConfig :: Config -> IO ()

Delete a configuration.

See withConfig.

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

Set a configuration parameter.

Helpers

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.

Create context

mkContext :: Config -> IO Context

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

Parameters

mkParams :: Context -> IO Params

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 ()

Add a Boolean parameter k with value v to the parameter set p.

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

Add a unsigned parameter k with value v to the parameter set p.

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

Add a double parameter k with value v to the parameter set p.

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

Add a symbol parameter k with value v to the parameter set p.

paramsToString :: Context -> Params -> IO String

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

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

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

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.

mkConstructor

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

Create datatype, such as lists, trees, records, enumerations or unions of records.

The datatype may be recursive. Returns the datatype sort.

mkSetSort :: Context -> Sort -> IO Sort

Create an set type with a given domain type

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

mkFreshFuncDecl :: Context -> String -> [Sort] -> Sort -> IO FuncDecl

Declare a fresh constant or function.

mkFreshConst

Arguments

:: Context

Logical context.

-> String

Prefix.

-> Sort

Sort of the constant.

-> IO AST

Declare and create a fresh constant.

Helpers

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

Declare and create a variable (aka constant).

An alias for mkConst.

mkBoolVar :: Context -> Symbol -> IO AST

Declarate and create a variable of sort bool.

See mkVar.

mkRealVar :: Context -> Symbol -> IO AST

Declarate and create a variable of sort real.

See mkVar.

mkIntVar :: Context -> Symbol -> IO AST

Declarate and create a variable of sort int.

See mkVar.

mkBvVar

Arguments

:: Context

-> Symbol

-> Int

bit-width

-> IO AST

Declarate and create a variable of sort bit-vector.

See mkVar.

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

Declare and create a fresh variable (aka constant).

An alias for mkFreshConst.

mkFreshBoolVar :: Context -> String -> IO AST

Declarate and create a fresh variable of sort bool.

See mkFreshVar.

mkFreshRealVar :: Context -> String -> IO AST

Declarate and create a fresh variable of sort real.

See mkFreshVar.

mkFreshIntVar :: Context -> String -> IO AST

Declarate and create a fresh variable of sort int.

See mkFreshVar.

mkFreshBvVar

Arguments

:: Context

-> String

-> Int

bit-width

-> IO AST

Declarate and create a fresh variable of sort bit-vector.

See mkFreshVar.

Propositional Logic and Equality

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

Helpers

mkBool :: Context -> Bool -> IO AST

Create an AST node representing the given boolean.

Arithmetic: Integers and Reals

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.

Sets

mkEmptySet

Arguments

:: Context

-> Sort

Domain sort of the set.

-> IO AST

Create the empty set.

mkFullSet

Arguments

:: Context

-> Sort

Domain sort of the set.

-> IO AST

Create the full set.

mkSetAdd

Arguments

:: Context

-> AST

Set.

-> AST

Element.

-> IO AST

Add an element to a set.

mkSetDel

Arguments

:: Context

-> AST

Set.

-> AST

Element.

-> IO AST

Remove an element from a set.

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

Take the union of a list of sets.

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

Take the intersection of a list of sets.

mkSetDifference

Arguments

:: Context

-> AST

First set.

-> AST

Second set.

-> IO AST

Take the set difference between two sets.

mkSetComplement

Arguments

:: Context

-> AST

Set.

-> IO AST

Take the complement of a set.

mkSetMember

Arguments

:: Context

-> AST

Element.

-> AST

Set.

-> IO AST

Check for set membership.

mkSetSubset

Arguments

:: Context

-> AST

First set.

-> AST

Second set.

-> IO AST

Check if the first set is a subset of the second set.

Numerals

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

Create a numeral of a given sort.

mkReal

Arguments

:: Context

-> Int

numerator

-> Int

denominator (/= 0)

-> IO AST

Create a real from a fraction.

mkInt :: Context -> Int -> Sort -> IO AST

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

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

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

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

Create a numeral of an int, bit-vector, or finite-domain sort.

mkRational :: Context -> Rational -> IO AST

Create a numeral of sort real from a Rational.

mkFixed :: HasResolution a => Context -> Fixed a -> IO AST

Create a numeral of sort real from a Fixed.

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

Create a numeral of sort real from a Real.

mkInteger :: Context -> Integer -> IO AST

Create a numeral of sort int from an Integer.

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

Create a numeral of sort int from an Integral.

mkBitvector

Arguments

:: Context

-> Int

bit-width

-> Integer

integer value

-> IO AST

Create a numeral of sort Bit-vector from an Integer.

mkBvNum

Arguments

:: Integral i

=> Context

-> Int

bit-width

-> i

integer value

-> IO AST

Create a numeral of sort Bit-vector from an Integral.

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

getSymbolString :: Context -> Symbol -> IO String

Return the symbol name.

getBvSortSize :: Context -> Sort -> IO Int

Return the size of the given bit-vector sort.

getDatatypeSortConstructors

Arguments

:: Context

-> Sort

Datatype sort.

-> IO [FuncDecl]

Constructor declarations.

Get list of constructors for datatype.

getDatatypeSortRecognizers

Arguments

:: Context

-> Sort

Datatype sort.

-> IO [FuncDecl]

Constructor recognizers.

Get list of recognizers for datatype.

getDeclName :: Context -> FuncDecl -> IO Symbol

Return the constant declaration name as a symbol.

getSort :: Context -> AST -> IO Sort

Return the sort of an AST node.

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

getAstKind :: Context -> AST -> IO ASTKind

Return the kind of the given AST.

toApp :: Context -> AST -> IO App

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

getNumeralString :: Context -> AST -> IO String

Return numeral value, as a string of a numeric constant term.

Helpers

getBool :: Context -> AST -> IO Bool

Read a Bool value from an AST

getInt :: Context -> AST -> IO Integer

Read an Integer value from an AST

getReal :: Context -> AST -> IO Rational

Read a Rational value from an AST

getBv

Arguments

:: Context

-> AST

-> Bool

signed?

-> IO Integer

Read the Integer value from an AST of sort bit-vector.

See mkBv2int.

Models

modelEval

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)

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.

Helpers

type EvalAst a = Model -> AST -> IO (Maybe a)

Type of an evaluation function for AST.

Evaluation may fail (i.e. return Nothing) for a few reasons, see modelEval.

eval :: Context -> EvalAst AST

An alias for modelEval with model completion enabled.

evalBool :: Context -> EvalAst Bool

Evaluate an AST node of sort bool in the given model.

See modelEval and getBool.

evalInt :: Context -> EvalAst Integer

Evaluate an AST node of sort int in the given model.

See modelEval and getInt.

evalReal :: Context -> EvalAst Rational

Evaluate an AST node of sort real in the given model.

See modelEval and getReal.

evalBv

Arguments

:: Context

-> Bool

signed?

-> EvalAst Integer

Evaluate an AST node of sort bit-vector in the given model.

The flag signed decides whether the bit-vector value is interpreted as a signed or unsigned integer.

See modelEval and getBv.

mapEval :: Traversable t => EvalAst a -> Model -> t AST -> IO (Maybe (t a))

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

Evaluate a collection of AST nodes in the given model.

data FuncModel

The interpretation of a function.

Constructors

FuncModel

Fields

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

Mapping from arguments to values.

interpElse :: AST

Default value.

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

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

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.

Error Handling

data Z3Error

Z3 exceptions.

Z3 errors are re-thrown as Haskell Z3Error exceptions, see Exception.

Constructors

Z3Error

Fields

errCode :: Z3ErrorCode

errMsg :: String

Instances

Show Z3Error

Exception Z3Error

Typeable * Z3Error

data Z3ErrorCode

Z3 error codes.

Constructors

SortError

IOB

InvalidArg

ParserError

NoParser

InvalidPattern

MemoutFail

FileAccessError

InternalFatal

InvalidUsage

DecRefError

Z3Exception

Instances

Show Z3ErrorCode

Typeable * Z3ErrorCode

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.

Solvers

data Logic

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.

Instances

Show Logic

mkSolver :: Context -> IO Solver

mkSimpleSolver :: Context -> IO Solver

mkSolverForLogic :: Context -> Logic -> IO Solver

solverGetHelp :: Context -> Solver -> IO String

Return a string describing all solver available parameters.

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

Set the given solver using the given parameters.

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

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

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

solverGetNumScopes :: Context -> Solver -> IO Int

Number of backtracking points.

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

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

solverCheck :: Context -> Solver -> IO Result

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

solverCheckAssumptions :: Context -> Solver -> [AST] -> IO Result

Check whether the assertions in the given solver and optional assumptions are consistent or not.

solverGetModel :: Context -> Solver -> IO Model

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.

solverGetUnsatCore :: Context -> Solver -> IO [AST]

Retrieve the unsat core for the last solverCheckAssumptions; the unsat core is a subset of the assumptions

solverGetReasonUnknown :: Context -> Solver -> IO String

Return a brief justification for an Unknown result for the commands solverCheck and solverCheckAssumptions.

solverToString :: Context -> Solver -> IO String

Convert the given solver into a string.

Helpers

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