Z3.Tagged.Eval

Documentation

type EvalAst s a = AST s -> Eval s a

Type of an evaluation function for '(AST s)'.

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

eval :: EvalAst s (AST s)

An alias for modelEval with model completion enabled.

evalT :: Traversable t => t (AST s) -> Eval s (t (AST s))

Evaluate a collection of (AST s) nodes in the given model.

mapEval :: Traversable t => EvalAst s a -> t (AST s) -> Eval s (t a)

Run a evaluation function on a Traversable data structure of '(AST s)'s (e.g. [(AST s)], Vector (AST s), Maybe (AST s), 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 s)' of sort int.

evalBool :: EvalAst s Bool

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

See modelEval and getBool.

evalInt :: EvalAst s Integer

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

See modelEval and getInt.

evalReal :: EvalAst s Rational

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

See modelEval and getReal.

evalBv

Arguments

:: Bool

signed?

-> EvalAst s Integer

Evaluate an (AST s) 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.

evalFunc :: FuncDecl s -> Eval s FuncModel

Get function as a list of argument/value pairs.

runWithModel :: Eval s a -> Z3 s (Maybe a)