Z3.Lang.Prelude

Z3 script

data Z3 a

Z3 monad.

Instances

Monad Z3

Functor Z3

Applicative Z3

MonadIO Z3

MonadZ3 Z3

data Result

Result of a satisfiability check.

Instances

Eq Result

Ord Result

Read Result

Show Result

evalZ3 :: Z3 a -> IO a

Eval a Z3 script.

data Args

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

stdArgs :: Args

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

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

Eval a Z3 script.

Commands

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

Declare skolem variables.

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

Declare skolem variables with a user specified name.

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

Declare uninterpreted function of arity 1.

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

Declare uninterpreted function of arity 2.

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

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)

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)

Declare uninterpreted function of arity 5.

assert :: Expr Bool -> Z3 ()

Make assertion in current context.

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

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

Check whether the given logical context is consistent or not.

showContext :: MonadZ3 z3 => z3 String

Convert Z3's logical context into a string.

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

Convert an Expr to a string.

push :: MonadZ3 z3 => z3 ()

Create a backtracking point.

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

Backtrack n backtracking points.

Models

data Model a

A computation derived from a model.

Instances

Monad Model

Functor Model

Applicative Model

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

Check satisfiability and evaluate a model if some exists.

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

Check satisfiability and evaluate a model if some exists.

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

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

showModel :: Model String

Show Z3's internal model.

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

Evaluate an expression within a model.

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

Evaluate a collection of expressions within a model.

Expressions

data Expr :: * -> *

Expressions.

Instances

IsReal a => Fractional (Expr a)

IsNum a => Num (Expr a)

Typeable (* -> *) Expr

data Pattern where

Quantifier pattern.

Constructors

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

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

Types for expressions.

Minimal complete definition

typeInv, tc, mkSort, mkLiteral, getValue

Instances

IsTy Bool

IsTy Integer

IsTy Rational

IsTy Nat

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

Numeric types.

Instances

IsNum Integer

IsNum Rational

IsNum Nat

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

Typeclass for Haskell Z3 numbers of int sort in Z3.

Instances

IsInt Integer

IsInt Nat

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

Typeclass for Haskell Z3 numbers of real sort in Z3.

Instances

IsReal Rational

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

Convertible types.

Minimal complete definition

compileCast

Instances

Castable Integer Rational

Castable Rational Integer

Castable Nat Integer

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

literal constructor.

true :: Expr Bool

Boolean literals.

false :: Expr Bool

Boolean literals.

not_ :: Expr Bool -> Expr Bool

Boolean negation

and_ :: [Expr Bool] -> Expr Bool

Boolean variadic and.

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

Boolean binary and.

or_ :: [Expr Bool] -> Expr Bool

Boolean variadic or.

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

Boolean binary or.

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

Boolean variadic distinct.

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

Boolean binary xor.

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

Boolean implication

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

An alias for implies.

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

Boolean if and only if.

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

An alias for iff.

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

Universally quantified formula.

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

Existentially quantified formula.

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

Pattern-based instantiation.

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

Integer division.

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

Integer modulo.

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

Integer remainder.

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

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

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

Equals.

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

Not equals.

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

Less or equals than.

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

Less than.

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

Greater or equals than.

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

Greater than.

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

Minimum.

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

Maximum.

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

if-then-else.

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

Casting between compatible types