z3-0.3.0: Bindings for the Z3 Theorem Prover

Copyright(c) Iago Abal, 2012-2013 (c) David Castro, 2012-2013
LicenseBSD3
MaintainerIago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com>
Stabilityexperimental
Safe HaskellNone
LanguageHaskell98

Z3.Lang.Prelude

Contents

Description

 

Synopsis

Z3 script

data Z3 a Source

Z3 monad.

data Result Source

Result of a satisfiability check.

evalZ3 :: Z3 a -> IO a Source

Eval a Z3 script.

data Args Source

Constructors

Args 

Fields

logic :: Maybe Logic

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

the logic to use; see http://smtlib.cs.uiowa.edu/logics.html

softTimeout :: Maybe Int

soft timeout (in milliseconds)

options :: Opts

Z3 options

data Logic Source

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

evalZ3With :: Args -> Z3 a -> IO a Source

Eval a Z3 script.

Commands

var :: IsTy a => Z3 (Expr a) Source

Declare skolem variables.

namedVar :: IsTy a => String -> Z3 (Expr a) Source

Declare skolem variables with a user specified name.

fun1 :: (IsTy a, IsTy b) => Z3 (Expr a -> Expr b) Source

Declare uninterpreted function of arity 1.

fun2 :: (IsTy a, IsTy b, IsTy c) => Z3 (Expr a -> Expr b -> Expr c) Source

Declare uninterpreted function of arity 2.

fun3 :: (IsTy a, IsTy b, IsTy c, IsTy d) => Z3 (Expr a -> Expr b -> Expr c -> Expr d) Source

Declare uninterpreted function of arity 3.

fun4 :: (IsTy a, IsTy b, IsTy c, IsTy d, IsTy e) => Z3 (Expr a -> Expr b -> Expr c -> Expr d -> Expr e) Source

Declare uninterpreted function of arity 4.

fun5 :: (IsTy a, IsTy b, IsTy c, IsTy d, IsTy e, IsTy f) => Z3 (Expr a -> Expr b -> Expr c -> Expr d -> Expr e -> Expr f) Source

Declare uninterpreted function of arity 5.

assert :: Expr Bool -> Z3 () Source

Make assertion in current context.

let_ :: IsTy a => Expr a -> Z3 (Expr a) Source

Introduce an auxiliary declaration to name a given expression.

If you really want sharing use this instead of Haskell's let.

check :: MonadZ3 z3 => z3 Result Source

Check whether the given logical context is consistent or not.

showContext :: MonadZ3 z3 => z3 String Source

Convert Z3's logical context into a string.

exprToString :: Compilable (Expr a) => Expr a -> Z3 String Source

Convert an Expr to a string.

push :: MonadZ3 z3 => z3 () Source

Create a backtracking point.

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

Backtrack n backtracking points.

Models

data Model a Source

A computation derived from a model.

checkModel :: Model a -> Z3 (Maybe a) Source

Check satisfiability and evaluate a model if some exists.

checkModelWith :: (Result -> Maybe a -> b) -> Model a -> Z3 b Source

Check satisfiability and evaluate a model if some exists.

checkModelWithResult :: Model a -> Z3 (Result, Maybe a) Source

Check satisfiability and evaluate a model if some exists, also returning a Result to the reason for any failure.

showModel :: Model String Source

Show Z3's internal model.

eval :: forall a. IsTy a => Expr a -> Model a Source

Evaluate an expression within a model.

evalT :: (IsTy a, Traversable t) => t (Expr a) -> Model (t a) Source

Evaluate a collection of expressions within a model.

Expressions

data Expr :: * -> * Source

Expressions.

Instances

IsReal a => Fractional (Expr a) 
IsNum a => Num (Expr a) 
Typeable (* -> *) Expr 

data Pattern where Source

Quantifier pattern.

Constructors

Pat :: IsTy a => Expr a -> Pattern 

class (Eq a, Show a, Typeable a, Compilable (Expr a)) => IsTy a Source

Types for expressions.

Minimal complete definition

typeInv, tc, mkSort, mkLiteral, getValue

class (IsTy a, Num a) => IsNum a Source

Numeric types.

class (IsNum a, Integral a) => IsInt a Source

Typeclass for Haskell Z3 numbers of int sort in Z3.

Instances

class (IsNum a, Fractional a, Real a) => IsReal a Source

Typeclass for Haskell Z3 numbers of real sort in Z3.

Instances

class (IsTy a, IsTy b) => Castable a b Source

Convertible types.

Minimal complete definition

compileCast

literal :: IsTy a => a -> Expr a Source

literal constructor.

true :: Expr Bool Source

Boolean literals.

false :: Expr Bool Source

Boolean literals.

not_ :: Expr Bool -> Expr Bool Source

Boolean negation

and_ :: [Expr Bool] -> Expr Bool Source

Boolean variadic and.

(&&*) :: Expr Bool -> Expr Bool -> Expr Bool infixr 3 Source

Boolean binary and.

or_ :: [Expr Bool] -> Expr Bool Source

Boolean variadic or.

(||*) :: Expr Bool -> Expr Bool -> Expr Bool infixr 3 Source

Boolean binary or.

distinct :: IsTy a => [Expr a] -> Expr Bool Source

Boolean variadic distinct.

xor :: Expr Bool -> Expr Bool -> Expr Bool infixr 3 Source

Boolean binary xor.

implies :: Expr Bool -> Expr Bool -> Expr Bool infixr 2 Source

Boolean implication

(==>) :: Expr Bool -> Expr Bool -> Expr Bool infixr 2 Source

An alias for implies.

iff :: Expr Bool -> Expr Bool -> Expr Bool infixr 2 Source

Boolean if and only if.

(<=>) :: Expr Bool -> Expr Bool -> Expr Bool infixr 2 Source

An alias for iff.

forall :: QExpr t => t -> Expr Bool Source

Universally quantified formula.

exists :: QExpr t => t -> Expr Bool Source

Existentially quantified formula.

instanceWhen :: Expr Bool -> [Pattern] -> QBody Source

Pattern-based instantiation.

(//) :: IsInt a => Expr a -> Expr a -> Expr a infixl 7 Source

Integer division.

(%*) :: IsInt a => Expr a -> Expr a -> Expr a infixl 7 Source

Integer modulo.

(%%) :: IsInt a => Expr a -> Expr a -> Expr a infixl 7 Source

Integer remainder.

divides :: IsInt a => Expr a -> Expr a -> Expr Bool Source

k divides n == n %* k ==* 0

(==*) :: IsTy a => Expr a -> Expr a -> Expr Bool infix 4 Source

Equals.

(/=*) :: IsTy a => Expr a -> Expr a -> Expr Bool infix 4 Source

Not equals.

(<=*) :: IsNum a => Expr a -> Expr a -> Expr Bool infix 4 Source

Less or equals than.

(<*) :: IsNum a => Expr a -> Expr a -> Expr Bool infix 4 Source

Less than.

(>=*) :: IsNum a => Expr a -> Expr a -> Expr Bool infix 4 Source

Greater or equals than.

(>*) :: IsNum a => Expr a -> Expr a -> Expr Bool infix 4 Source

Greater than.

min_ :: IsNum a => Expr a -> Expr a -> Expr a Source

Minimum.

max_ :: IsNum a => Expr a -> Expr a -> Expr a Source

Maximum.

ite :: IsTy a => Expr Bool -> Expr a -> Expr a -> Expr a Source

if-then-else.

cast :: (IsTy a, IsTy b, Castable a b) => Expr a -> Expr b Source

Casting between compatible types