Z3.Monad

A simple monadic wrapper for Base.

Documentation

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

Methods

getSolver :: m (Maybe Solver)

getContext :: m Context

Instances

MonadZ3 Z3

MonadZ3 Z3

data Z3 a

Instances

Monad Z3

Functor Z3

Applicative Z3

MonadIO Z3

MonadZ3 Z3

module Z3.Opts

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

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.

Types

data Symbol

A Z3 Lisp-link symbol.

Instances

Eq Symbol

Ord Symbol

Show Symbol

Storable Symbol

data AST

A Z3 AST node.

Instances

Eq AST

Ord AST

Show AST

Storable AST

Typeable * AST

data Sort

Kind of Z3 AST representing types.

Instances

Eq Sort

Ord Sort

Show Sort

Storable Sort

data FuncDecl

Kind of AST used to represent function symbols.

Instances

Eq FuncDecl

Ord FuncDecl

Show FuncDecl

Storable FuncDecl

Typeable * FuncDecl

data App

A kind of Z3 AST used to represent constant and function declarations.

Instances

Eq App

Ord App

Show App

Storable App

data Pattern

A kind of AST used to represent pattern and multi-patterns used 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

Satisfiability result

data Result

Result of a satisfiability check.

Constructors

Sat

Unsat

Undef

Instances

Eq Result

Ord Result

Read Result

Show Result

Symbols

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

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

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

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

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

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, Integral a) => a -> z3 AST

Create a numeral of sort int.

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

Create a numeral of sort real.

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

Accessors

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

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

Return the integer value

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

Return rational value

Models

eval :: MonadZ3 z3 => Model -> AST -> z3 (Maybe AST)

Evaluate an AST node in the given model.

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

Evaluate a collection of AST nodes in the given model.

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

Convert the given model into a string.

showContext :: MonadZ3 z3 => z3 String

Convert Z3's logical context into a string.

Constraints

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

check :: MonadZ3 z3 => z3 Result

Check whether the given logical context is consistent or not.

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

Get model.

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

delModel :: MonadZ3 z3 => Model -> z3 ()

Delete a model object.

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

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

push :: MonadZ3 z3 => z3 ()

Create a backtracking point.

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

Backtrack n backtracking points.

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.