Home • Docs • Download • Mail • FAQ • Awards • Status • MSR

Z3An Efficient SMT Solver

OCaml API examples (Index)

val exitf : string -> 'a
Exit gracefully in case of error.
val mk_context : (string * string) array -> Z3.context
Create a logical context. Enable model construction. Also enable tracing to stderr.
val mk_var : Z3.context -> string -> Z3.sort -> Z3.ast
Create a variable using the given name and type.
val mk_bool_var : Z3.context -> string -> Z3.ast
Create a boolean variable using the given name.
val mk_int_var : Z3.context -> string -> Z3.ast
Create an integer variable using the given name.
val mk_int : Z3.context -> int -> Z3.ast
Create a Z3 integer node using a C int.
val mk_real_var : Z3.context -> string -> Z3.ast
Create a real variable using the given name.
val mk_unary_app : Z3.context -> Z3.func_decl -> Z3.ast -> Z3.ast
Create the unary function application: (f x) .
val mk_binary_app : Z3.context -> Z3.func_decl -> Z3.ast -> Z3.ast -> Z3.ast
Create the binary function application: (f x y) .
val equal_sorts : Z3.context -> Z3.sort -> Z3.sort -> bool
Auxiliary function to check whether two Z3 types are equal or not.
val check : Z3.context -> Z3.lbool -> unit
Check whether the logical context is satisfiable, and compare the result with the expected result. If the context is satisfiable, then display the model.
val prove : Z3.context -> Z3.ast -> bool -> unit
Prove that the constraints already asserted into the logical context implies the given formula. The result of the proof is displayed. Z3 is a satisfiability checker. So, one can prove f by showing that (not f) is unsatisfiable. The context ctx is not modified by this function.
val assert_inj_axiom : Z3.context -> Z3.func_decl -> int -> unit
Assert the axiom: function f is injective in the i-th argument.

The following axiom is asserted into the logical context:

forall (x_1, ..., x_n) finv(f(x_1, ..., x_i, ..., x_n)) = x_i

Where, finv is a fresh function declaration.

val assert_comm_axiom : Z3.context -> Z3.func_decl -> unit
Assert the axiom: function f is commutative.

This example uses the SMT-LIB parser to simplify the axiom construction.

val mk_tuple_update : Z3.context -> Z3.ast -> int -> Z3.ast -> Z3.ast
Z3 does not support explicitly tuple updates. They can be easily implemented as macros. The argument t must have tuple type. A tuple update is a new tuple where field i has value new_val , and all other fields have the value of the respective field of t .

update(t, i, new_val) is equivalent to mk_tuple(proj_0(t), ..., new_val, ..., proj_n(t))

val display_symbol : Z3.context -> Pervasives.out_channel -> Z3.symbol -> unit
Display a symbol in the given output stream.
val display_sort : Z3.context -> Pervasives.out_channel -> Z3.sort -> unit
Display the given type.

Custom ast pretty printer.

This function demonstrates how to use the API to navigate terms.

val display_numeral : 'a -> Pervasives.out_channel -> Z3.numeral_refined -> unit
val display_ast : Z3.context -> Pervasives.out_channel -> Z3.ast -> unit

Custom function for traversing a term and replacing the constant 'x' by the bound variable having index 'idx'. This function illustrates how to walk Z3 terms and reconstruct them. *

val abstract : Z3.context -> Z3.ast -> int -> Z3.ast -> Z3.ast

Example abstraction function. *

val abstract_example : unit -> unit
val display_function_interpretations : Z3.context -> Pervasives.out_channel -> Z3.model -> unit
Custom function interpretations pretty printer.
val display_model : Z3.context -> Pervasives.out_channel -> Z3.model -> unit
Custom model pretty printer.
val check2 : Z3.context -> Z3.lbool -> unit
Similar to #check, but uses #display_model instead of #Z3_model_to_string.
val display_version : unit -> unit
Display Z3 version in the standard output.
val simple_example : unit -> unit
"Hello world" example: create a Z3 logical context, and delete it.
val demorgan : unit -> unit
Demonstration of how Z3 can be used to prove validity of De Morgan's Duality Law: not(x and y) <-> (not x) or ( not y)
val find_model_example1 : unit -> unit
Find a model for x xor y .
val find_model_example2 : unit -> unit
Find a model for x < y + 1, x > 2 . Then, assert not(x = y) , and find another model.
val prove_example1 : unit -> unit
Prove x = y implies g(x) = g(y) , and disprove x = y implies g(g(x)) = g(y) .

This function demonstrates how to create uninterpreted types and functions.

val prove_example2 : unit -> unit
Prove not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0 . Then, show that z < -1 is not implied.

This example demonstrates how to combine uninterpreted functions and arithmetic.

val push_pop_example1 : unit -> unit
Show how push & pop can be used to create "backtracking" points.

This example also demonstrates how big numbers can be created in Z3.

val quantifier_example1 : unit -> unit
Prove that f(x, y) = f(w, v) implies y = v when f is injective in the second argument.
val array_example1 : unit -> unit
Prove store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3)) .

This example demonstrates how to use the array theory.

val array_example2 : unit -> unit
Show that distinct(a_0, ... , a_n) is unsatisfiable when a_i's are arrays from boolean to boolean and n > 4.

This example also shows how to use the distinct construct.

val array_example3 : unit -> unit
Simple array type construction/deconstruction example.
val tuple_example1 : unit -> unit
Simple tuple type example. It creates a tuple that is a pair of real numbers.
val bitvector_example1 : unit -> unit
Simple bit-vector example. This example disproves that x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers
val bitvector_example2 : unit -> unit
Find x and y such that: x ^ y - 103 == x * y
val eval_example1 : unit -> unit
Demonstrate how to use #Z3_eval.
val two_contexts_example1 : unit -> unit
Several logical context can be used simultaneously.
val error_code_example1 : unit -> unit
Demonstrates how error codes can be read insted of registering an error handler.
val error_code_example2 : unit -> unit
Demonstrates how Z3 exceptions can be used.
val parser_example1 : unit -> unit
Demonstrates how to use the SMTLIB parser.
val parser_example2 : unit -> unit
Demonstrates how to initialize the parser symbol table.
val parser_example3 : unit -> unit
Demonstrates how to initialize the parser symbol table.
val parser_example4 : unit -> unit
Display the declarations, assumptions and formulas in a SMT-LIB string.
val parser_example5 : unit -> unit
Demonstrates how to handle parser errors using Z3 exceptions.
val ite_example : unit -> unit
Example for creating an if-then-else expression.
val enum_example : unit -> unit
Create an enumeration data type.

Several more examples of creating and using data-types (lists, trees, records) are provided for the C-based API. The translation from the examples in C to use the OCaml API follow the same pattern that is used here.

val unsat_core_and_proof_example : unit -> unit
Example for extracting unsatisfiable core and proof. The example uses the function check_assumptions which allows passing in additional hypotheses. The unsatisfiable core is a subset of these additional hypotheses.