Module Z3

module Z3: sig .. end

The Z3 ML/OCaml Interface.

Author(s): CM Wintersteiger (cwinter) 2012-12-17

exception Error of string

General Z3 exceptions

Many functions in this API may throw an exception; if they do, it is this one.

type context

Context objects.

Most interactions with Z3 are interpreted in some context; many users will only require one such object, but power users may require more than one. To start using Z3, do

let ctx = (mk_context []) in (...)

where a list of pairs of strings may be passed to set options on the context, e.g., like so:

let cfg = [("model", "true"); ("...", "...")] in let ctx = (mk_context cfg) in (...)

val mk_context : (string * string) list -> context

Create a context object The following parameters can be set:

proof (Boolean) Enable proof generation
debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting
trace (Boolean) Tracing support for VCC
trace_file_name (String) Trace out file for VCC traces
timeout (unsigned) default timeout (in milliseconds) used for solvers
well_sorted_check type checker
auto_config use heuristics to automatically select solver and configure it
model model generation for solvers, this parameter can be overwritten when creating a solver
model_validate validate models produced by solvers
unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver

val interrupt : context -> unit

Interrupt the execution of a Z3 procedure.

This procedure can be used to interrupt: solvers, simplifiers and tactics. Note: Tactic.interrupt is an alias for this.

module Log: sig .. end

Interaction logging for Z3 Interaction logs are used to record calls into the API into a text file.

module Version: sig .. end

Version information

module Symbol: sig .. end

Symbols are used to name several term and type constructors

module AST: sig .. end

The abstract syntax tree (AST) module

module Sort: sig .. end

The Sort module implements type information for ASTs

module FuncDecl: sig .. end

Function declarations

module Params: sig .. end

Parameter sets (of Solvers, Tactics, ...)

module Expr: sig .. end

General Expressions (terms)

module Boolean: sig .. end

Boolean expressions; Propositional logic and equality

module Quantifier: sig .. end

Quantifier expressions

module Z3Array: sig .. end

Functions to manipulate Array expressions

module Set: sig .. end

Functions to manipulate Set expressions

module FiniteDomain: sig .. end

Functions to manipulate Finite Domain expressions

module Relation: sig .. end

Functions to manipulate Relation expressions

module Datatype: sig .. end

Functions to manipulate Datatype expressions

module Enumeration: sig .. end

Functions to manipulate Enumeration expressions

module Z3List: sig .. end

Functions to manipulate List expressions

module Tuple: sig .. end

Functions to manipulate Tuple expressions

module Arithmetic: sig .. end

Functions to manipulate arithmetic expressions

module BitVector: sig .. end

Functions to manipulate bit-vector expressions

module Seq: sig .. end

Sequences, Strings and Regular Expressions *

module FloatingPoint: sig .. end

Floating-Point Arithmetic

module Proof: sig .. end

Functions to manipulate proof expressions

module Goal: sig .. end

Goals

module Model: sig .. end

Models

module Probe: sig .. end

Probes

module Tactic: sig .. end

Tactics

module Simplifier: sig .. end

module Statistics: sig .. end

Objects that track statistical information.

module Solver: sig .. end

Solvers

module Fixedpoint: sig .. end

Fixedpoint solving

module Optimize: sig .. end

Optimization

module SMT: sig .. end

Functions for handling SMT and SMT2 expressions and files

module RCF: sig .. end

Real closed field

val set_global_param : string -> string -> unit

Set a global (or module) parameter, which is shared by all Z3 contexts.

When a Z3 module is initialized it will use the value of these parameters when Z3_params objects are not provided. The name of parameter can be composed of characters a-zA-Z, digits 0-9, '-' and '_'. The character '.' is a delimiter (more later). The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'. Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION". This function can be used to set parameters for a specific Z3 module. This can be done by using <module-name>.<parameter-name>. For example: (set_global_param "pp.decimal" "true") will set the parameter "decimal" in the module "pp" to true.

val get_global_param : string -> string option

Get a global (or module) parameter.

Returns None if the parameter does not exist. The caller must invoke #Z3_global_param_del_value to delete the value returned at param_value. This function cannot be invoked simultaneously from different threads without synchronization. The result string stored in param_value is stored in a shared location.

Restore the value of all global (and module) parameters.

This command will not affect already created objects (such as tactics and solvers) set_global_param

val global_param_reset_all : unit -> unit

val toggle_warning_messages : bool -> unit

Enable/disable printing of warning messages to the console.

Note that this function is static and effects the behaviour of all contexts globally.

val enable_trace : string -> unit

Enable tracing messages tagged as `tag' when Z3 is compiled in debug mode.

Remarks: It is a NOOP otherwise.

val disable_trace : string -> unit

Disable tracing messages tagged as `tag' when Z3 is compiled in debug mode.

Remarks: It is a NOOP otherwise.

module Memory: sig .. end

Memory management *