Z3.Monad

A simple monadic interface to Z3 API.

Examples: https://bitbucket.org/iago/z3-haskell/src/tip/examples/Example/Monad

Z3 monad

class (Applicative m, Monad m, MonadIO m) => MonadZ3 m where

Methods

getSolver :: m Solver

getContext :: m Context

Instances

MonadZ3 Z3

data Z3 a

Instances

Monad Z3

Functor Z3

MonadFix Z3

Applicative Z3

MonadIO Z3

MonadZ3 Z3

module Z3.Opts

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

evalZ3 :: Z3 a -> IO a

Eval a Z3 script with default configuration options.

evalZ3With :: Maybe Logic -> Opts -> Z3 a -> IO a

Eval a Z3 script.

Z3 enviroments

data Z3Env

Z3 environment.

newEnv :: Maybe Logic -> Opts -> IO Z3Env

Create a new Z3 environment.

evalZ3WithEnv :: Z3 a -> Z3Env -> IO a

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

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 Context

A Z3 logical context.

Instances

Eq Context

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

Parameters

mkParams :: MonadZ3 z3 => z3 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 :: MonadZ3 z3 => Params -> Symbol -> Bool -> z3 ()

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

paramsSetUInt :: MonadZ3 z3 => Params -> Symbol -> Word -> z3 ()

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

paramsSetDouble :: MonadZ3 z3 => Params -> Symbol -> Double -> z3 ()

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

paramsSetSymbol :: MonadZ3 z3 => Params -> Symbol -> Symbol -> z3 ()

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

paramsToString :: MonadZ3 z3 => Params -> z3 String

Convert a parameter set into a string.

This function is mainly used for printing the contents of a parameter set.

Symbols

mkIntSymbol :: (MonadZ3 z3, Integral i) => i -> z3 Symbol

Create a Z3 symbol using an integer.

mkStringSymbol :: MonadZ3 z3 => String -> z3 Symbol

Create a Z3 symbol using a string.

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

Sorts

mkUninterpretedSort :: MonadZ3 z3 => Symbol -> z3 Sort

Create a free (uninterpreted) type using the given name (symbol).

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

mkBoolSort :: MonadZ3 z3 => z3 Sort

Create the boolean type.

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

mkIntSort :: MonadZ3 z3 => z3 Sort

Create the integer type.

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

mkRealSort :: MonadZ3 z3 => z3 Sort

Create the real type.

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

mkBvSort :: MonadZ3 z3 => Int -> z3 Sort

Create a bit-vector type of the given size.

This type can also be seen as a machine integer.

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

mkArraySort :: MonadZ3 z3 => Sort -> Sort -> z3 Sort

Create an array type

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

mkTupleSort

Arguments

:: MonadZ3 z3

=> Symbol

Name of the sort

-> [(Symbol, Sort)]

Name and sort of each field

-> z3 (Sort, FuncDecl, [FuncDecl])

Resulting sort, and function declarations for the constructor and projections.

Create a tuple type

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

mkConstructor

Arguments

:: MonadZ3 z3

=> Symbol

Name of the sonstructor

-> Symbol

Name of recognizer function

-> [(Symbol, Maybe Sort, Int)]

Name, sort option, and sortRefs

-> z3 Constructor

Create a contructor

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

mkDatatype :: MonadZ3 z3 => Symbol -> [Constructor] -> z3 Sort

Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.

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

Constants and Applications

mkFuncDecl :: MonadZ3 z3 => Symbol -> [Sort] -> Sort -> z3 FuncDecl

A Z3 function

mkApp :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST

Create a constant or function application.

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

mkConst :: MonadZ3 z3 => Symbol -> Sort -> z3 AST

Declare and create a constant.

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

mkFreshConst :: MonadZ3 z3 => String -> Sort -> z3 AST

Declare and create a constant.

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

mkFreshFuncDecl :: MonadZ3 z3 => String -> [Sort] -> Sort -> z3 FuncDecl

Declare a fresh constant or function.

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

Helpers

mkVar :: MonadZ3 z3 => Symbol -> Sort -> z3 AST

Declare and create a variable (aka constant).

An alias for mkConst.

mkBoolVar :: MonadZ3 z3 => Symbol -> z3 AST

Declarate and create a variable of sort bool.

See mkVar.

mkRealVar :: MonadZ3 z3 => Symbol -> z3 AST

Declarate and create a variable of sort real.

See mkVar.

mkIntVar :: MonadZ3 z3 => Symbol -> z3 AST

Declarate and create a variable of sort int.

See mkVar.

mkBvVar

Arguments

:: MonadZ3 z3

=> Symbol

-> Int

bit-width

-> z3 AST

Declarate and create a variable of sort bit-vector.

See mkVar.

mkFreshVar :: MonadZ3 z3 => String -> Sort -> z3 AST

Declare and create a fresh variable (aka constant).

An alias for mkFreshConst.

mkFreshBoolVar :: MonadZ3 z3 => String -> z3 AST

Declarate and create a fresh variable of sort bool.

See mkFreshVar.

mkFreshRealVar :: MonadZ3 z3 => String -> z3 AST

Declarate and create a fresh variable of sort real.

See mkFreshVar.

mkFreshIntVar :: MonadZ3 z3 => String -> z3 AST

Declarate and create a fresh variable of sort int.

See mkFreshVar.

mkFreshBvVar

Arguments

:: MonadZ3 z3

=> String

-> Int

bit-width

-> z3 AST

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

See mkFreshVar.

Propositional Logic and Equality

mkTrue :: MonadZ3 z3 => z3 AST

Create an AST node representing true.

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

mkFalse :: MonadZ3 z3 => z3 AST

Create an AST node representing false.

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

mkEq :: MonadZ3 z3 => AST -> AST -> z3 AST

Create an AST node representing l = r.

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

mkNot :: MonadZ3 z3 => AST -> z3 AST

Create an AST node representing not(a).

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

mkIte :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST

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

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

mkIff :: MonadZ3 z3 => AST -> AST -> z3 AST

Create an AST node representing t1 iff t2.

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

mkImplies :: MonadZ3 z3 => AST -> AST -> z3 AST

Create an AST node representing t1 implies t2.

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

mkXor :: MonadZ3 z3 => AST -> AST -> z3 AST

Create an AST node representing t1 xor t2.

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

mkAnd :: MonadZ3 z3 => [AST] -> z3 AST

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

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

mkOr :: MonadZ3 z3 => [AST] -> z3 AST

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

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

mkDistinct :: MonadZ3 z3 => [AST] -> z3 AST

The distinct construct is used for declaring the arguments pairwise distinct.

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

Helpers

mkBool :: MonadZ3 z3 => Bool -> z3 AST

Create an AST node representing the given boolean.

Arithmetic: Integers and Reals

mkAdd :: MonadZ3 z3 => [AST] -> z3 AST

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

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

mkMul :: MonadZ3 z3 => [AST] -> z3 AST

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

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

mkSub :: MonadZ3 z3 => [AST] -> z3 AST

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

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

mkUnaryMinus :: MonadZ3 z3 => AST -> z3 AST

Create an AST node representing -arg.

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

mkDiv :: MonadZ3 z3 => AST -> AST -> z3 AST

Create an AST node representing arg1 div arg2.

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

mkMod :: MonadZ3 z3 => AST -> AST -> z3 AST

Create an AST node representing arg1 mod arg2.

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

mkRem :: MonadZ3 z3 => AST -> AST -> z3 AST

Create an AST node representing arg1 rem arg2.

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

mkLt :: MonadZ3 z3 => AST -> AST -> z3 AST

Create less than.

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

mkLe :: MonadZ3 z3 => AST -> AST -> z3 AST

Create less than or equal to.

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

mkGt :: MonadZ3 z3 => AST -> AST -> z3 AST

Create greater than.

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

mkGe :: MonadZ3 z3 => AST -> AST -> z3 AST

Create greater than or equal to.

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

mkInt2Real :: MonadZ3 z3 => AST -> z3 AST

Coerce an integer to a real.

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

mkReal2Int :: MonadZ3 z3 => AST -> z3 AST

Coerce a real to an integer.

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

mkIsInt :: MonadZ3 z3 => AST -> z3 AST

Check if a real number is an integer.

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

Bit-vectors

mkBvnot :: MonadZ3 z3 => AST -> z3 AST

Bitwise negation.

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

mkBvredand :: MonadZ3 z3 => AST -> z3 AST

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

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

mkBvredor :: MonadZ3 z3 => AST -> z3 AST

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

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

mkBvand :: MonadZ3 z3 => AST -> AST -> z3 AST

Bitwise and.

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

mkBvor :: MonadZ3 z3 => AST -> AST -> z3 AST

Bitwise or.

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

mkBvxor :: MonadZ3 z3 => AST -> AST -> z3 AST

Bitwise exclusive-or.

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

mkBvnand :: MonadZ3 z3 => AST -> AST -> z3 AST

Bitwise nand.

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

mkBvnor :: MonadZ3 z3 => AST -> AST -> z3 AST

Bitwise nor.

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

mkBvxnor :: MonadZ3 z3 => AST -> AST -> z3 AST

Bitwise xnor.

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

mkBvneg :: MonadZ3 z3 => AST -> z3 AST

Standard two's complement unary minus.

Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7

mkBvadd :: MonadZ3 z3 => AST -> AST -> z3 AST

Standard two's complement addition.

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

mkBvsub :: MonadZ3 z3 => AST -> AST -> z3 AST

Standard two's complement subtraction.

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

mkBvmul :: MonadZ3 z3 => AST -> AST -> z3 AST

Standard two's complement multiplication.

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

mkBvudiv :: MonadZ3 z3 => AST -> AST -> z3 AST

Unsigned division.

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

mkBvsdiv :: MonadZ3 z3 => AST -> AST -> z3 AST

Two's complement signed division.

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

mkBvurem :: MonadZ3 z3 => AST -> AST -> z3 AST

Unsigned remainder.

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

mkBvsrem :: MonadZ3 z3 => AST -> AST -> z3 AST

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

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

mkBvsmod :: MonadZ3 z3 => AST -> AST -> z3 AST

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

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

mkBvult :: MonadZ3 z3 => AST -> AST -> z3 AST

Unsigned less than.

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

mkBvslt :: MonadZ3 z3 => AST -> AST -> z3 AST

Two's complement signed less than.

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

mkBvule :: MonadZ3 z3 => AST -> AST -> z3 AST

Unsigned less than or equal to.

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

mkBvsle :: MonadZ3 z3 => AST -> AST -> z3 AST

Two's complement signed less than or equal to.

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

mkBvuge :: MonadZ3 z3 => AST -> AST -> z3 AST

Unsigned greater than or equal to.

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

mkBvsge :: MonadZ3 z3 => AST -> AST -> z3 AST

Two's complement signed greater than or equal to.

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

mkBvugt :: MonadZ3 z3 => AST -> AST -> z3 AST

Unsigned greater than.

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

mkBvsgt :: MonadZ3 z3 => AST -> AST -> z3 AST

Two's complement signed greater than.

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

mkConcat :: MonadZ3 z3 => AST -> AST -> z3 AST

Concatenate the given bit-vectors.

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

mkExtract :: MonadZ3 z3 => Int -> Int -> AST -> z3 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.

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

mkSignExt :: MonadZ3 z3 => Int -> AST -> z3 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.

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

mkZeroExt :: MonadZ3 z3 => Int -> AST -> z3 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.

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

mkRepeat :: MonadZ3 z3 => Int -> AST -> z3 AST

Repeat the given bit-vector up length i.

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

mkBvshl :: MonadZ3 z3 => AST -> AST -> z3 AST

Shift left.

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

mkBvlshr :: MonadZ3 z3 => AST -> AST -> z3 AST

Logical shift right.

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

mkBvashr :: MonadZ3 z3 => AST -> AST -> z3 AST

Arithmetic shift right.

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

mkRotateLeft :: MonadZ3 z3 => Int -> AST -> z3 AST

Rotate bits of t1 to the left i times.

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

mkRotateRight :: MonadZ3 z3 => Int -> AST -> z3 AST

Rotate bits of t1 to the right i times.

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

mkExtRotateLeft :: MonadZ3 z3 => AST -> AST -> z3 AST

Rotate bits of t1 to the left t2 times.

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

mkExtRotateRight :: MonadZ3 z3 => AST -> AST -> z3 AST

Rotate bits of t1 to the right t2 times.

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

mkInt2bv :: MonadZ3 z3 => Int -> AST -> z3 AST

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

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

mkBv2int :: MonadZ3 z3 => AST -> Bool -> z3 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.

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

mkBvnegNoOverflow :: MonadZ3 z3 => AST -> z3 AST

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

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

mkBvaddNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST

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

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

mkBvaddNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST

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

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

mkBvsubNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST

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

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

mkBvsubNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST

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

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

mkBvmulNoOverflow :: MonadZ3 z3 => AST -> AST -> Bool -> z3 AST

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

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

mkBvmulNoUnderflow :: MonadZ3 z3 => AST -> AST -> z3 AST

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

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

mkBvsdivNoOverflow :: MonadZ3 z3 => AST -> AST -> z3 AST

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

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

Arrays

mkSelect :: MonadZ3 z3 => AST -> AST -> z3 AST

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

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

mkStore :: MonadZ3 z3 => AST -> AST -> AST -> z3 AST

Array update.  

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

mkConstArray :: MonadZ3 z3 => Sort -> AST -> z3 AST

Create the constant array.

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

mkMap :: MonadZ3 z3 => FuncDecl -> [AST] -> z3 AST

map f on the the argument arrays.

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

mkArrayDefault :: MonadZ3 z3 => AST -> z3 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.

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

Numerals

mkNumeral :: MonadZ3 z3 => String -> Sort -> z3 AST

Create a numeral of a given sort.

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

mkInt :: MonadZ3 z3 => Int -> Sort -> z3 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.

mkReal :: MonadZ3 z3 => Int -> Int -> z3 AST

Create a numeral of sort real.

mkUnsignedInt :: MonadZ3 z3 => Word -> Sort -> z3 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 :: MonadZ3 z3 => Int64 -> Sort -> z3 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 :: MonadZ3 z3 => Word64 -> Sort -> z3 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 :: (MonadZ3 z3, Integral a) => a -> Sort -> z3 AST

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

mkRational :: MonadZ3 z3 => Rational -> z3 AST

Create a numeral of sort real from a Rational.

mkFixed :: (MonadZ3 z3, HasResolution a) => Fixed a -> z3 AST

Create a numeral of sort real from a Fixed.

mkRealNum :: (MonadZ3 z3, Real r) => r -> z3 AST

Create a numeral of sort real from a Real.

mkInteger :: MonadZ3 z3 => Integer -> z3 AST

Create a numeral of sort int from an Integer.

mkIntNum :: (MonadZ3 z3, Integral a) => a -> z3 AST

Create a numeral of sort int from an Integral.

mkBitvector

Arguments

:: MonadZ3 z3

=> Int

bit-width

-> Integer

integer value

-> z3 AST

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

mkBvNum

Arguments

:: (MonadZ3 z3, Integral i)

=> Int

bit-width

-> i

integer value

-> z3 AST

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

Quantifiers

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

Accessors

getSymbolString :: MonadZ3 z3 => Symbol -> z3 String

Return the symbol name.

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

getBvSortSize :: MonadZ3 z3 => Sort -> z3 Int

Return the size of the given bit-vector sort.

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

getDatatypeSortConstructors

Arguments

:: MonadZ3 z3

=> Sort

Datatype sort.

-> z3 [FuncDecl]

Constructor declarations.

Get list of constructors for datatype.

getDatatypeSortRecognizers

Arguments

:: MonadZ3 z3

=> Sort

Datatype sort.

-> z3 [FuncDecl]

Constructor recognizers.

Get list of recognizers for datatype.

getDeclName :: MonadZ3 z3 => FuncDecl -> z3 Symbol

Return the constant declaration name as a symbol.

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

getSort :: MonadZ3 z3 => AST -> z3 Sort

Return the sort of an AST node.

getBoolValue :: MonadZ3 z3 => AST -> z3 (Maybe Bool)

Returns Just True, Just False, or Nothing for undefined.

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

getAstKind :: MonadZ3 z3 => AST -> z3 ASTKind

Return the kind of the given AST.

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

toApp :: MonadZ3 z3 => AST -> z3 App

Cast AST into an App.

getNumeralString :: MonadZ3 z3 => AST -> z3 String

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

Helpers

getBool :: MonadZ3 z3 => AST -> z3 Bool

Read a Bool value from an AST

getInt :: MonadZ3 z3 => AST -> z3 Integer

Return the integer value

getReal :: MonadZ3 z3 => AST -> z3 Rational

Return rational value

getBv

Arguments

:: MonadZ3 z3

=> AST

-> Bool

signed?

-> z3 Integer

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

See mkBv2int.

Models

modelEval :: MonadZ3 z3 => Model -> AST -> z3 (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 :: MonadZ3 z3 => Model -> AST -> z3 (Maybe FuncModel)

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)

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.

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

isAsArray :: MonadZ3 z3 => AST -> z3 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.

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

getAsArrayFuncDecl :: MonadZ3 z3 => AST -> z3 FuncDecl

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

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

funcInterpGetNumEntries :: MonadZ3 z3 => FuncInterp -> z3 Int

Return the number of entries in the given function interpretation.

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

funcInterpGetEntry :: MonadZ3 z3 => FuncInterp -> Int -> z3 FuncEntry

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

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

funcInterpGetElse :: MonadZ3 z3 => FuncInterp -> z3 AST

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

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

funcInterpGetArity :: MonadZ3 z3 => FuncInterp -> z3 Int

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

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

funcEntryGetValue :: MonadZ3 z3 => FuncEntry -> z3 AST

Return the value of this point.

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

funcEntryGetNumArgs :: MonadZ3 z3 => FuncEntry -> z3 Int

Return the number of arguments in a Z3_func_entry object.

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

funcEntryGetArg :: MonadZ3 z3 => FuncEntry -> Int -> z3 AST

Return an argument of a Z3_func_entry object.

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

modelToString :: MonadZ3 z3 => Model -> z3 String

Convert the given model into a string.

showModel :: MonadZ3 z3 => Model -> z3 String

Alias for modelToString.

Helpers

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

Type of an evaluation function for AST.

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

eval :: MonadZ3 z3 => EvalAst z3 AST

An alias for modelEval.

evalBool :: MonadZ3 z3 => EvalAst z3 Bool

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

See modelEval and getBool.

evalInt :: MonadZ3 z3 => EvalAst z3 Integer

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

See modelEval and getInt.

evalReal :: MonadZ3 z3 => EvalAst z3 Rational

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

See modelEval and getReal.

evalBv

Arguments

:: MonadZ3 z3

=> Bool

signed?

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

evalT :: (MonadZ3 z3, Traversable t) => Model -> t AST -> z3 (Maybe (t AST))

Evaluate a collection of AST nodes in the given model.

mapEval :: (MonadZ3 z3, Traversable t) => EvalAst z3 a -> Model -> t AST -> z3 (Maybe (t a))

Run a evaluation function on a Traversable data structure of ASTs (e.g. [AST], Vector AST, Maybe AST, etc).

This a generic version of evalT which can be used in combination with other helpers. For instance, mapEval evalInt can be used to obtain the Integer interpretation of a list of AST of sort int.

data FuncModel

The interpretation of a function.

Constructors

FuncModel

Fields

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

Mapping from arguments to values.

interpElse :: AST

Default value.

evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel)

Get function as 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 :: MonadZ3 z3 => ASTPrintMode -> z3 ()

Set the mode for converting expressions to strings.

astToString :: MonadZ3 z3 => AST -> z3 String

Convert an AST to a string.

patternToString :: MonadZ3 z3 => Pattern -> z3 String

Convert a pattern to a string.

sortToString :: MonadZ3 z3 => Sort -> z3 String

Convert a sort to a string.

funcDeclToString :: MonadZ3 z3 => FuncDecl -> z3 String

Convert a FuncDecl to a string.

benchmarkToSMTLibString

Arguments

:: MonadZ3 z3

=> String

name

-> String

logic

-> String

status

-> String

attributes

-> [AST]

assumptions1

-> AST

formula

-> z3 String

Convert the given benchmark into SMT-LIB formatted string.

The output format can be configured via setASTPrintMode.

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 :: MonadZ3 z3 => z3 Version

Return Z3 version number information.

Solvers

solverGetHelp :: MonadZ3 z3 => z3 String

Return a string describing all solver available parameters.

solverSetParams :: MonadZ3 z3 => Params -> z3 ()

Set the solver using the given parameters.

solverPush :: MonadZ3 z3 => z3 ()

Create a backtracking point.

solverPop :: MonadZ3 z3 => Int -> z3 ()

Backtrack n backtracking points.

solverReset :: MonadZ3 z3 => z3 ()

solverGetNumScopes :: MonadZ3 z3 => z3 Int

Number of backtracking points.

solverAssertCnstr :: MonadZ3 z3 => AST -> z3 ()

Assert a constraing into the logical context.

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

solverAssertAndTrack :: MonadZ3 z3 => AST -> AST -> z3 ()

Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.

This API is an alternative to Z3_solver_check_assumptions for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination of the Boolean variables provided using Z3_solver_assert_and_track and the Boolean literals provided using Z3_solver_check_assumptions.

solverCheck :: MonadZ3 z3 => z3 Result

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

solverCheckAssumptions :: MonadZ3 z3 => [AST] -> z3 Result

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

solverGetModel :: MonadZ3 z3 => z3 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 :: MonadZ3 z3 => z3 [AST]

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

solverGetReasonUnknown :: MonadZ3 z3 => z3 String

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

solverToString :: MonadZ3 z3 => z3 String

Convert the given solver into a string.

Helpers

assert :: MonadZ3 z3 => AST -> z3 ()

check :: MonadZ3 z3 => z3 Result

Check whether the given logical context is consistent or not.

checkAssumptions :: MonadZ3 z3 => [AST] -> z3 Result

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

solverCheckAndGetModel :: MonadZ3 z3 => z3 (Result, Maybe Model)

getModel :: MonadZ3 z3 => z3 (Result, Maybe Model)

Get model.

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

withModel :: (Applicative z3, MonadZ3 z3) => (Model -> z3 a) -> z3 (Result, Maybe a)

Check satisfiability and, if sat, compute a value from the given model.

E.g. withModel $ \m -> fromJust <$> evalInt m x

getUnsatCore :: MonadZ3 z3 => z3 [AST]

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

push :: MonadZ3 z3 => z3 ()

Create a backtracking point.

For push; m; pop 1 see local.

pop :: MonadZ3 z3 => Int -> z3 ()

Backtrack n backtracking points.

Contrary to solverPop this funtion checks whether n is within the size of the solver scope stack.

local :: MonadZ3 z3 => z3 a -> z3 a

Run a query and restore the initial logical context.

This is a shorthand for push, run the query, and pop.

reset :: MonadZ3 z3 => z3 ()

Backtrack all the way.

getNumScopes :: MonadZ3 z3 => z3 Int

Get number of backtracking points.