OCaml: Index

Summary: Convert a APP_AST into an AST.

Prove store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3)) .

Show that distinct(a_0, ...

Simple array type construction/deconstruction example.

Summary: Assert a constraing into the logical context.

Assert the axiom: function f is commutative.

Assert the axiom: function f is injective in the i-th argument.

Summary: Convert the given AST node into a string.

Summary: Convert the given benchmark into SMT-LIB formatted string.

Simple bit-vector example.

Find x and y such that: x ^ y - 103 == x * y

Summary: Block subsequent checks using the remaining enabled labels.

Summary: Check whether the given logical context is consistent or not.

Check whether the logical context is satisfiable, and compare the result with the expected result.

Similar to #check, but uses #display_model instead of #Z3_model_to_string.

Summary: Check whether the given logical context is consistent or not.

Summary: Check whether the given logical context and optional assumptions is consistent or not.

Summary: Close interaction log.

Summary: Convert the given logical context into a string.

Summary: Delete the given configuration object.

Summary: Reclaim memory allocated to constructor.

Summary: reclaim memory allocated for constructor list.

Summary: Delete the given logical context.

Summary: Delete a labels context.

Summary: Delete a model object.

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)

Summary: Disable label.

Custom function interpretations pretty printer.

Custom model pretty printer.

Display the given type.

Display a symbol in the given output stream.

Display Z3 version in the standard output.

Auxiliary function to check whether two Z3 types are equal or not.

Demonstrates how error codes can be read insted of registering an error handler.

Demonstrates how Z3 exceptions can be used.

Summary: [ eval c m t ] Evaluate the AST node t in the given model.

Summary: Evaluate declaration given values.

Demonstrate how to use #Z3_eval.

Summary: Return the value of the given constant or function in the given model.

Exit gracefully in case of error.

Find a model for x xor y .

Find a model for x < y + 1, x > 2 .

fprintf

Summary: [ get_app_arg c a i ] Return the i-th argument of the given application.

[ get_app_args c a ] is the array of arguments of an application.

Summary: Return the declaration of a constant or function application.

Summary: [ get_app_num_args c a ] Return the number of argument of an application.

[ get_array_sort c t ] is the domain and the range of t.

Summary: [ get_array_sort_domain c t ] Return the domain of the given array sort.

Summary: [ get_array_sort_range c t ] Return the range of the given array sort.

Summary: [ get_array_value c v ] An array values is represented as a dictionary plus a default (else) value.

Summary: Return the kind of the given AST.

Summary: Return L_TRUE if a is true, L_FALSE if it is false, and L_UNDEF otherwise.

Summary: [ get_bv_sort_size c t ] Return the size of the given bit-vector sort.

Summary: Extract satisfying assignment from context as a conjunction.

Summary: Return idx'th constructor.

Summary: Return idx_a'th accessor for the idx_c'th constructor.

Summary: Return number of constructors for datatype.

Summary: Return idx'th recognizer.

Summary: Return the expresson value associated with an expression parameter.

Summary: Return the double value associated with an double parameter.

Summary: Return the expresson value associated with an expression parameter.

Summary: Return the integer value associated with an integer parameter.

Summary: Return declaration kind corresponding to declaration.

Summary: Return the constant declaration name as a symbol.

Summary: Return the number of parameters associated with a declaration.

Summary: Return the parameter type associated with a declaration.

Summary: Return the rational value, as a string, associated with a rational parameter.

Summary: Return the sort value associated with a sort parameter.

Summary: Return the double value associated with an double parameter.

Summary: [ get_domain c d i ] Return the sort of the i-th parameter of the given function declaration.

Summary: Return the number of parameters of the given declaration.

[ get_app_args c d ] is the array of parameters of d.

Summary: Retrieve the set of literals that whose assignment were guess, but not propagated during the search.

Summary: Retrieve congruence class representatives for terms.

Summary: Return index of de-Brujin bound variable.

Summary: Retrieve label symbol at idx.

Summary: Retrieve literal expression at idx.

Summary: [ get_model_constant c m i ] Return the i-th constant in the given model.

[ get_model_constants c m ] is the array of constants in the model m.

Summary: [ get_model_func_decl c m i ] Return the declaration of the i-th function in the given model.

Summary: [ get_model_func_else c m i ] Return the 'else' value of the i-th function interpretation in the given model.

[ get_model_func_entries c m i ] is the array of entries in the i'th function in the model m.

[ get_model_func_entry c m i j ] is the j'th entry in the i'th function in the model m.

Summary: [ get_model_func_entry_arg c m i j k ] Return the k-th argument of the j-th entry of the i-th function interpretation in the given model.

Summary: [ get_model_func_entry_num_args c m i j ] Return the number of arguments of the j-th entry of the i-th function interpretation in the given model.

Summary: [ get_model_func_entry_value c m i j ] Return the return value of the j-th entry of the i-th function interpretation in the given model.

Summary: [ get_model_func_num_entries c m i ] Return the number of entries of the i-th function interpretation in the given model.

[ get_model_funcs c m ] is the array of functions in the model m.

Summary: Return the number of constants assigned by the given model.

Summary: Return the number of function interpretations in the given model.

Summary: Retrieve the number of label symbols that were returned.

Summary: [ get_numeral_int c v ] Similar to Z3.get_numeral_string, but only succeeds if the value can fit in a machine int.

Summary: Return numeral value, as a pair of 64 bit numbers if the representation fits.

Summary: Return numeral value, as a string of a numeric constant term

Summary: [ get_numeral_uint c v ] Similar to Z3.get_numeral_string, but only succeeds if the value can fit in a machine unsigned int int.

Summary: Return i'th ast in pattern.

Summary: Return number of terms in pattern.

Summary: Return body of quantifier.

Summary: Return symbol of the i'th bound variable.

Summary: Return sort of the i'th bound variable.

Summary: Return number of bound variables of quantifier.

Summary: Return number of patterns used in quantifier.

Summary: Return i'th pattern.

Summary: Obtain weight of quantifier.

Summary: [ get_range c d ] Return the range of the given declaration.

Summary: Retrieve the set of labels that were relevant in the context of the current satisfied context.

Summary: Retrieve the set of literals that satisfy the current context.

Summary: Retrieve reason for search failure.

Summary: [ get_smtlib_assumption c i ] Return the i-th assumption parsed by the last call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.

[ get_smtlib_assumptions c ] is the array of assumptions created by a preceding call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.

Summary: [ get_smtlib_decl c i ] Return the i-th declaration parsed by the last call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.

[ get_smtlib_decls c ] is the array of declarations created by a preceding call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.

Summary: [ get_smtlib_error c ] Retrieve that last error message information generated from parsing.

Summary: [ get_smtlib_formula c i ] Return the i-th formula parsed by the last call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.

[ get_smtlib_formulas c ] is the array of formulas created by a preceding call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.

Summary: Return the number of SMTLIB assumptions parsed by Z3.parse_smtlib_string or Z3.parse_smtlib_file.

Summary: Return the number of declarations parsed by Z3.parse_smtlib_string or Z3.parse_smtlib_file.

Summary: Return the number of SMTLIB formulas parsed by the last call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.

Summary: Return the number of sorts parsed by Z3.parse_smtlib_string or Z3.parse_smtlib_file.

[ get_smtlib_parse_results c ] is the triple (get_smtlib_formulas c, get_smtlib_assumptions c, get_smtlib_decls c).

Summary: [ get_smtlib_sort c i ] Return the i-th sort parsed by the last call to Z3.parse_smtlib_string or Z3.parse_smtlib_file.

Summary: Return the sort of an AST node.

Summary: Return the sort kind (e.g., array, tuple, int, bool, etc).

Summary: Return the sort name as a symbol.

Summary: [ get_symbol_int c s ] Return the symbol int value.

Summary: Return INT_SYMBOL if the symbol was constructed using Z3.mk_int_symbol, and STRING_SYMBOL if the symbol was constructed using Z3.mk_string_symbol.

Summary: [ get_symbol_string c s ] Return the symbol name.

[ get_tuple_sort c ty ] is the pair (mk_decl, fields) where mk_decl is the constructor declaration of ty, and fields is the array of fields in ty.

Summary: [ get_tuple_sort_field_decl c t i ] Return the i-th field declaration (i.e., projection function declaration) of the given tuple sort.

Summary: [ get_tuple_sort_mk_decl c t ] Return the constructor declaration of the given tuple sort.

Summary: [ get_tuple_sort_num_fields c t ] Return the number of fields of the given tuple sort.

Summary: Return Z3 version number information.

Summary: [ is_array_value c v ] Determine whether the term encodes an array value.

Summary: compare terms.

Summary: compare sorts.

Summary: Determine if quantifier is universal.

Example for creating an if-then-else expression.

Summary: [ mk_add c [| t_1; ...; t_n |] ] Create the term: t_1 + ...

Summary: [ mk_and c [| t_1; ...; t_n |] ] Create the conjunction: t_1 and ...

Summary: Create a constant or function application.

Summary: Access the array default value.

Summary: Create an array type.

Create the binary function application: (f x y) .

Summary: Create the Boolean type.

Create a boolean variable using the given name.

Summary: Create a bound variable.

Summary: [ mk_bv2int c t1 is_signed ] Create an integer from the bit-vector argument t1.

Summary: Create a bit-vector type of the given size.

Summary: [ mk_bvadd c t1 t2 ] Standard two's complement addition.

Summary: [ mk_bvadd_no_overflow c t1 t2 is_signed ] Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

Summary: [ mk_bvadd_no_underflow c t1 t2 ] Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.

Summary: [ mk_bvand c t1 t2 ] Bitwise and.

Summary: [ mk_bvashr c t1 t2 ] Arithmetic shift right.

Summary: [ mk_bvlshr c t1 t2 ] Logical shift right.

Summary: [ mk_bvmul c t1 t2 ] Standard two's complement multiplication.

Summary: [ mk_bvmul_no_overflow c t1 t2 is_signed ] Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.

Summary: [ mk_bvmul_no_underflow c t1 t2 ] Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow.

Summary: [ mk_bvnand c t1 t2 ] Bitwise nand.

Summary: [ mk_bvneg c t1 ] Standard two's complement unary minus.

Summary: [ mk_bvneg_no_overflow c t1 ] Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.

Summary: [ mk_bvnor c t1 t2 ] Bitwise nor.

Summary: [ mk_bvneg c t1 ] Bitwise negation.

Summary: [ mk_bvor c t1 t2 ] Bitwise or.

Summary: [ mk_bvsdiv c t1 t2 ] Two's complement signed division.

Summary: [ mk_bvsdiv_no_overflow c t1 t2 ] Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.

Summary: [ mk_bvsge c t1 t2 ] Two's complement signed greater than or equal to.

Summary: [ mk_bvsgt c t1 t2 ] Two's complement signed greater than.

Summary: [ mk_bvshl c t1 t2 ] Shift left.

Summary: [ mk_bvsle c t1 t2 ] Two's complement signed less than or equal to.

Summary: [ mk_bvslt c t1 t2 ] Two's complement signed less than.

Summary: [ mk_bvsmod c t1 t2 ] Two's complement signed remainder (sign follows divisor).

Summary: [ mk_bvsrem c t1 t2 ] Two's complement signed remainder (sign follows dividend).

Summary: [ mk_bvsub c t1 t2 ] Standard two's complement subtraction.

Summary: [ mk_bvsub_no_overflow c t1 t2 ] Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.

Summary: [ mk_bvsub_no_underflow c t1 t2 is_signed ] Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.

Summary: [ mk_bvudiv c t1 t2 ] Unsigned division.

Summary: [ mk_bvuge c t1 t2 ] Unsigned greater than or equal to.

Summary: [ mk_bvugt c t1 t2 ] Unsigned greater than.

Summary: [ mk_bvule c t1 t2 ] Unsigned less than or equal to.

Summary: [ mk_bvult c t1 t2 ] Unsigned less than.

Summary: [ mk_bvurem c t1 t2 ] Unsigned remainder.

Summary: [ mk_bvxnor c t1 t2 ] Bitwise xnor.

Summary: [ mk_bvxor c t1 t2 ] Bitwise exclusive-or.

Summary: [ mk_concat c t1 t2 ] Concatenate the given bit-vectors.

Summary: Create a configuration.

Summary: Declare and create a constant.

Summary: Create the constant array.

Summary: Create a constructor.

Summary: Create list of constructors.

Summary: Create a logical context using the given configuration.

Create a logical context.

[ mk_context_x configs ] is a shorthand for the context with configurations in configs.

Summary: Create recursive datatype.

Summary: Create mutually recursive datatypes.

Summary: [ mk_distinct c [| t_1; ...; t_n |] ] Create an AST node represeting a distinct construct.

Summary: [ mk_div c t_1 t_2 ] Create the term: t_1 div t_2.

Summary: Create a enumeration sort.

Summary: [ mk_eq c l r ] Create an AST node representing l = r .

Summary: Create an exists formula.

Summary: Similar to Z3.mk_forall_const.

Summary: [ mk_extract c high low t1 ] Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1 .

Summary: Create an AST node representing false.

Summary: Create a forall formula.

Summary: Create a universal quantifier using a list of constants that will form the set of bound variables.

Summary: Declare and create a fresh constant.

Summary: Declare a fresh constant or function.

Summary: Declare a constant or function.

Summary: [ mk_ge c t1 t2 ] Create greater than or equal to.

Summary: [ mk_gt c t1 t2 ] Create greater than.

Summary: [ mk_iff c t1 t2 ] Create an AST node representing t1 iff t2 .

Summary: [ mk_implies c t1 t2 ] Create an AST node representing t1 implies t2 .

Summary: Create injective function declaration

Summary: Create a numeral of a given sort.

Create a Z3 integer node using a C int.

Summary: [ mk_int2bv c n t1 ] Create an n bit bit-vector from the integer argument t1.

Summary: [ mk_int2real c t1 ] Coerce an integer to a real.

Summary: Create an integer type.

Summary: Create a Z3 symbol using an integer.

Create an integer variable using the given name.

Summary: [ mk_ite c t1 t2 t2 ] Create an AST node representing an if-then-else: ite(t1, t2, t3) .

Summary: Create a labeled formula.

Summary: [ mk_le c t1 t2 ] Create less than or equal to.

Summary: Create a list sort

Summary: [ mk_lt c t1 t2 ] Create less than.

Summary: [ mk_map f n args ] map f on the the argument arrays.

Summary: [ mk_mod c t_1 t_2 ] Create the term: t_1 mod t_2.

Summary: [ mk_mul c [| t_1; ...; t_n |] ] Create the term: t_1 * ...

Summary: [ mk_not c a ] Create an AST node representing not(a) .

Summary: Create a numeral of a given sort.

Summary: [ mk_or c [| t_1; ...; t_n |] ] Create the disjunction: t_1 or ...

Summary: Create a pattern for quantifier instantiation.

Summary: Create a quantifier - universal or existential, with pattern hints.

Summary: Create a real from a fraction.

Summary: Create a real type.

Create a real variable using the given name.

Summary: [ mk_rem c t_1 t_2 ] Create the term: t_1 rem t_2.

Summary: [ mk_rotate_left c i t1 ] Rotate bits of t1 to the left i times.

Summary: [ mk_rotate_right c i t1 ] Rotate bits of t1 to the right i times.

Summary: [ mk_select c a i ] Array read.

Summary: [ mk_sign_ext c i t1 ] Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i , where m is the size of the given bit-vector.

Summary: [ mk_store c a i v ] Array update.

Summary: Create a Z3 symbol using a C string.

Summary: [ mk_sub c [| t_1; ...; t_n |] ] Create the term: t_1 - ...

Summary: Create an AST node representing true.

Summary: Create a tuple type.

Z3 does not support explicitly tuple updates.

Create the unary function application: (f x) .

Summary: [ mk_unary_minus c arg ] Create the term: - arg.

Summary: Create a free (uninterpreted) type using the given name (symbol).

Summary: Create a numeral of a given sort.

Create a variable using the given name and type.

Summary: [ mk_xor c t1 t2 ] Create an AST node representing t1 xor t2 .

Summary: [ mk_zero_ext c i t1 ] Extend the given bit-vector with zeros to the (unsigned int) equivalent bitvector of size m+i , where m is the size of the given bit-vector.

Summary: Convert the given model into a string.

Summary: Log interaction to a file.

Summary: Similar to Z3.parse_smtlib_string, but reads the benchmark from a file.

[ parse_smtlib_file_formula c ... ] calls (parse_smtlib_file c ...) and returns the single formula produced.

[ parse_smtlib_file_x c ... ] is (parse_smtlib_file c ...; get_smtlib_parse_results c)

Summary: [ parse_smtlib_string c str sort_names sorts decl_names decls ] Parse the given string using the SMT-LIB parser.

[ parse_smtlib_string_formula c ... ] calls (parse_smtlib_string c ...) and returns the single formula produced.

[ parse_smtlib_string_x c ... ] is (parse_smtlib_string c ...; get_smtlib_parse_results c)

Summary: Similar to Z3.parse_z3_string, but reads the benchmark from a file.

Summary: [ parse_z3_string c str ] Parse the given string using the Z3 native parser.

Demonstrates how to use the SMTLIB parser.

Demonstrates how to initialize the parser symbol table.

Demonstrates how to initialize the parser symbol table.

Display the declarations, assumptions and formulas in a SMT-LIB string.

Demonstrates how to handle parser errors using Z3 exceptions.

Summary: Persist AST through num_scopes pops.

Summary: Backtrack.

printf

Prove that the constraints already asserted into the logical context implies the given formula.

Prove x = y implies g(x) = g(y) , and disprove x = y implies g(g(x)) = g(y) .

Prove not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0 .

Summary: Create a backtracking point.

Show how push & pop can be used to create "backtracking" points.

Prove that f(x, y) = f(w, v) implies y = v when f is injective in the second argument.

Summary: Query constructor for declared funcions.

Summary: Reset all allocated resources.

Summary: Select mode for the format used for pretty-printing AST nodes.

Summary: Set a configuration parameter.

"Hello world" example: create a Z3 logical context, and delete it.

Summary: Interface to simplifier.

Summary: Cancel an ongoing check.

[ sort_refine c t ] is the refined sort of t.

[ symbol_refine c s ] is the refined symbol of s.

[ term_refine c a ] is the refined term of a.

Summary: Convert an AST into a APP_AST.

Summary: Disable trace messages.

Summary: Enable trace messages to a file

Summary: Enable trace messages to a standard error.

Summary: Enable trace messages to a standard output.

Simple tuple type example.

Several logical context can be used simultaneously.

Example for extracting unsatisfiable core and proof.