module Z3:sig
..end
Copyright (C) 2012 Microsoft Corporation
Author(s): CM Wintersteiger (cwinter) 2012-12-17
exception Error of string
Many functions in this API may throw an exception; if they do, it is this one.
type
context
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
module Log:sig
..end
module Version:sig
..end
module Symbol:sig
..end
module AST:sig
..end
module Sort:sig
..end
module FuncDecl:sig
..end
module Params:sig
..end
module Expr:sig
..end
module Boolean:sig
..end
module Quantifier:sig
..end
module Z3Array:sig
..end
module Set:sig
..end
module FiniteDomain:sig
..end
module Relation:sig
..end
module Datatype:sig
..end
module Enumeration:sig
..end
module Z3List:sig
..end
module Tuple:sig
..end
module Arithmetic:sig
..end
module BitVector:sig
..end
module FloatingPoint:sig
..end
module Proof:sig
..end
module Goal:sig
..end
module Model:sig
..end
module Probe:sig
..end
module Tactic:sig
..end
module Statistics:sig
..end
module Solver:sig
..end
module Fixedpoint:sig
..end
module Optimize:sig
..end
module SMT:sig
..end
module Interpolation:sig
..end
val set_global_param : string -> string -> unit
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-z
A-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
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.
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
Note that this function is static and effects the behaviour of
all contexts globally.
val enable_trace : string -> unit
Remarks: It is a NOOP otherwise.
val disable_trace : string -> unit
Remarks: It is a NOOP otherwise.