mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Updates to ML API.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-06-03 18:51:40 +01:00
parent c1e29dabe7
commit aaa835484f
2 changed files with 86 additions and 83 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/api/ml/z3.ml
View file

@ -323,8 +323,8 @@ struct
else
ast_of_ptr to_ctx (Z3native.translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx))
let unwrap_ast ( x : ast ) = (z3obj_gno x)
let wrap_ast ( ctx : context ) ( ptr : Z3native.ptr ) = ast_of_ptr ctx ptr
let unwrap_ast ( x : ast ) = (z3obj_gno x)
end
open AST
@ -678,6 +678,19 @@ end = struct
res
let to_string ( x : params ) = Z3native.params_to_string (z3obj_gnc x) (z3obj_gno x)
let update_param_value ( ctx : context ) ( id : string) ( value : string )=
Z3native.update_param_value (context_gno ctx) id value
let get_param_value ( ctx : context ) ( id : string ) =
let (r, v) = (Z3native.get_param_value (context_gno ctx) id) in
if not r then
None
else
Some v
let set_print_mode ( ctx : context ) ( value : ast_print_mode ) =
Z3native.set_ast_print_mode (context_gno ctx) (int_of_ast_print_mode value)
end
(** General expressions (terms) *)
@ -1106,7 +1119,7 @@ struct
end
module Array_ =
module Array =
struct
let mk_sort ( ctx : context ) ( domain : sort ) ( range : sort ) =
sort_of_ptr ctx (Z3native.mk_array_sort (context_gno ctx) (Sort.gno domain) (Sort.gno range))
@ -1389,7 +1402,7 @@ struct
end
module List_ =
module List =
struct
let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( elem_sort : sort ) =
let (r, _, _, _, _, _, _) = (Z3native.mk_list_sort (context_gno ctx) (Symbol.gno name) (Sort.gno elem_sort)) in
@ -2558,26 +2571,6 @@ struct
let mk_fixedpoint ( ctx : context ) = create ctx
end
module Options =
struct
let update_param_value ( ctx : context ) ( id : string) ( value : string )=
Z3native.update_param_value (context_gno ctx) id value
let get_param_value ( ctx : context ) ( id : string ) =
let (r, v) = (Z3native.get_param_value (context_gno ctx) id) in
if not r then
None
else
Some v
let set_print_mode ( ctx : context ) ( value : ast_print_mode ) =
Z3native.set_ast_print_mode (context_gno ctx) (int_of_ast_print_mode value)
let toggle_warning_messages ( enabled: bool ) =
Z3native.toggle_warning_messages enabled
end
module SMT =
struct
@ -2692,3 +2685,7 @@ let get_global_param ( id : string ) =
let global_param_reset_all =
Z3native.global_param_reset_all
let toggle_warning_messages ( enabled: bool ) =
Z3native.toggle_warning_messages enabled

126
src/api/ml/z3.mli
View file

@ -27,7 +27,20 @@
*)
type context
(** Create a context object *)
(** 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 mk_context : (string * string) list -> context
(** Interaction logging for Z3
@ -220,15 +233,6 @@ sig
@return A copy of the AST which is associated with the other context. *)
val translate : ast -> context -> ast
(** Wraps an AST.
This function is used for transitions between native and
managed objects. Note that the native ast that is passed must be a
native object obtained from Z3 (e.g., through {!unwrap_ast})
and that it must have a correct reference count (see e.g.,
<c>Z3native.inc_ref</c>). *)
val wrap_ast : context -> Z3native.z3_ast -> ast
(** Unwraps an AST.
This function is used for transitions between native and
managed objects. It returns the native pointer to the AST. Note that
@ -238,6 +242,15 @@ sig
<c>Z3native.inc_ref</c>).
{!wrap_ast} *)
val unwrap_ast : ast -> Z3native.ptr
(** Wraps an AST.
This function is used for transitions between native and
managed objects. Note that the native ast that is passed must be a
native object obtained from Z3 (e.g., through {!unwrap_ast})
and that it must have a correct reference count (see e.g.,
<c>Z3native.inc_ref</c>). *)
val wrap_ast : context -> Z3native.z3_ast -> ast
end
(** The Sort module implements type information for ASTs *)
@ -432,6 +445,36 @@ sig
(** A string representation of the parameter set. *)
val to_string : params -> string
(** Update a mutable configuration parameter.
The list of all configuration parameters can be obtained using the Z3 executable:
<c>z3.exe -p</c>
Only a few configuration parameters are mutable once the context is created.
An exception is thrown when trying to modify an immutable parameter.
{!get_param_value} *)
val update_param_value : context -> string -> string -> unit
(** Get a configuration parameter.
Returns None if the parameter value does not exist.
{!update_param_value} *)
val get_param_value : context -> string -> string option
(** Selects the format used for pretty-printing expressions.
The default mode for pretty printing expressions is to produce
SMT-LIB style output where common subexpressions are printed
at each occurrence. The mode is called PRINT_SMTLIB_FULL.
To print shared common subexpressions only once,
use the PRINT_LOW_LEVEL mode.
To print in way that conforms to SMT-LIB standards and uses let
expressions to share common sub-expressions use PRINT_SMTLIB_COMPLIANT.
{!AST.to_string}
{!Quantifier.Pattern.to_string}
{!FuncDecl.to_string}
{!Sort.to_string} *)
val set_print_mode : context -> Z3enums.ast_print_mode -> unit
end
(** General Expressions (terms) *)
@ -737,7 +780,7 @@ sig
end
(** Functions to manipulate Array expressions *)
module Array_ :
module Array :
sig
(** Create a new array sort. *)
val mk_sort : context -> Sort.sort -> Sort.sort -> Sort.sort
@ -790,7 +833,7 @@ sig
The node <c>a</c> must have an array sort <c>[domain -> range]</c>,
and <c>i</c> must have the sort <c>domain</c>.
The sort of the result is <c>range</c>.
{!Array_.mk_sort}
{!Array.mk_sort}
{!mk_store} *)
val mk_select : context -> Expr.expr -> Expr.expr -> Expr.expr
@ -806,7 +849,7 @@ sig
on all indices except for <c>i</c>, where it maps to <c>v</c>
(and the <c>select</c> of <c>a</c> with
respect to <c>i</c> may be a different value).
{!Array_.mk_sort}
{!Array.mk_sort}
{!mk_select} *)
val mk_store : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
@ -814,7 +857,7 @@ sig
The resulting term is an array, such that a <c>select</c>on an arbitrary index
produces the value <c>v</c>.
{!Array_.mk_sort}
{!Array.mk_sort}
{!mk_select} *)
val mk_const_array : context -> Sort.sort -> Expr.expr -> Expr.expr
@ -823,7 +866,7 @@ sig
Eeach element of <c>args</c> must be of an array sort <c>[domain_i -> range_i]</c>.
The function declaration <c>f</c> must have type <c> range_1 .. range_n -> range</c>.
<c>v</c> must have sort range. The sort of the result is <c>[domain_i -> range]</c>.
{!Array_.mk_sort}
{!Array.mk_sort}
{!mk_select}
{!mk_store} *)
val mk_map : context -> FuncDecl.func_decl -> Expr.expr list -> Expr.expr
@ -1069,7 +1112,7 @@ sig
end
(** Functions to manipulate List expressions *)
module List_ :
module List :
sig
(** Create a new list sort. *)
val mk_sort : context -> Symbol.symbol -> Sort.sort -> Sort.sort
@ -2824,50 +2867,6 @@ sig
val mk_fixedpoint : context -> fixedpoint
end
(** Global and context options
Note: This module contains functions that set parameters/options for context
objects as well as functions that set options that are used globally, across
contexts.*)
module Options :
sig
(** Update a mutable configuration parameter.
The list of all configuration parameters can be obtained using the Z3 executable:
<c>z3.exe -ini?</c>
Only a few configuration parameters are mutable once the context is created.
An exception is thrown when trying to modify an immutable parameter.
{!get_param_value} *)
val update_param_value : context -> string -> string -> unit
(** Get a configuration parameter.
Returns None if the parameter value does not exist.
{!update_param_value} *)
val get_param_value : context -> string -> string option
(** Selects the format used for pretty-printing expressions.
The default mode for pretty printing expressions is to produce
SMT-LIB style output where common subexpressions are printed
at each occurrence. The mode is called PRINT_SMTLIB_FULL.
To print shared common subexpressions only once,
use the PRINT_LOW_LEVEL mode.
To print in way that conforms to SMT-LIB standards and uses let
expressions to share common sub-expressions use PRINT_SMTLIB_COMPLIANT.
{!AST.to_string}
{!Quantifier.Pattern.to_string}
{!FuncDecl.to_string}
{!Sort.to_string} *)
val set_print_mode : context -> Z3enums.ast_print_mode -> 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 toggle_warning_messages : bool -> unit
end
(** Functions for handling SMT and SMT2 expressions and files *)
module SMT :
sig
@ -2954,4 +2953,11 @@ val get_global_param : string -> string option
This command will not affect already created objects (such as tactics and solvers)
{!set_global_param}
*)
val global_param_reset_all : 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 toggle_warning_messages : bool -> unit