module Z3: sig  end

Summary: Create a configuration.

Configurations are created in order to assign parameters prior to creating contexts for Z3 interaction. For example, if the users wishes to use model generation, then call:

set_param_value cfg "MODEL" "true"

• Remarks: Consider using Z3.mk_context_x instead of using explicit configuration objects. The function Z3.mk_context_x receives an array of string pairs. This array represents the configuration options.

• See also: Z3.set_param_value

Summary: Delete the given configuration object.

• See also: Z3.mk_config

Summary: Set a configuration parameter.

The list of all configuration parameters can be obtained using the Z3 executable:

       z3.exe -ini?
       

• See also: Z3.mk_config

Summary: Create a context using the given configuration.

After a context is created, the configuration cannot be changed, although some parameters can be changed using Z3.update_param_value. All main interaction with Z3 happens in the context of a context.

• Remarks: Consider using Z3.mk_context_x instead of using explicit configuration objects. The function Z3.mk_context_x receives an array of string pairs. This array represents the configuration options.

Summary: Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers, simplifiers and tactics.

Summary: Create a context using the given configuration. This function is similar to Z3.mk_context. However, in the context returned by this function, the user is responsible for managing ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3.inc_ref for any ast returned by Z3, and Z3.dec_ref whenever the ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.

Remark: sort, func_decl, app, pattern are ast's.

After a context is created, the configuration cannot be changed. All main interaction with Z3 happens in the context of a context.

Summary: Delete the given logical context.

• See also: Z3.mk_context

Summary: Increment the reference counter of the given AST. The context c should have been created using Z3.mk_context_rc. This function is a NOOP if c was created using Z3.mk_context.

Summary: Decrement the reference counter of the given AST. The context c should have been created using Z3.mk_context_rc. This function is a NOOP if c was created using Z3.mk_context.

Summary: Update a mutable configuration parameter.

The list of all configuration parameters can be obtained using the Z3 executable:

       z3.exe -ini?
       

Only a few configuration parameters are mutable once the context is created. The error handler is invoked when trying to modify an immutable parameter.

• See also: Z3.set_param_value

Summary: Get a configuration parameter.

Returns None if the parameter value does not exist.

• See also: Z3.mk_config
• See also: Z3.set_param_value

Summary: Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.

Summary: Increment the reference counter of the given parameter set.

Summary: Decrement the reference counter of the given parameter set.

Summary: Add a Boolean parameter k with value v to the parameter set p.

Summary: Add a unsigned int parameter k with value v to the parameter set p.

Summary: Add a double parameter k with value v to the parameter set p.

Summary: Add a symbol parameter k with value v to the parameter set p.

Summary: Convert a parameter set into a string. This function is mainly used for printing the contents of a parameter set.

Summary: Create a Z3 symbol using an integer.

Symbols are used to name several term and type constructors.

NB. Not all integers can be passed to this function. The legal range of unsigned int integers is 0 to 2^30-1.

• See also: Z3.mk_string_symbol

Summary: Create a Z3 symbol using a C string.

Symbols are used to name several term and type constructors.

• See also: Z3.mk_int_symbol

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

Two free types are considered the same iff the have the same name.

Summary: Create the Boolean type.

This type is used to create propositional variables and predicates.

Summary: Create the integer type.

This type is not the int type found in programming languages. A machine integer can be represented using bit-vectors. The function Z3.mk_bv_sort creates a bit-vector type.

• See also: Z3.mk_bv_sort

Summary: Create the real type.

This type is not a floating point number. Z3 does not have support for floating point numbers yet.

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

This type can also be seen as a machine integer.

• Remarks: The size of the bitvector type must be greater than zero.

Summary: Create a named finite domain sort.

To create constants that belong to the finite domain, use the APIs for creating numerals and pass a numeric constant together with the sort returned by this call.

• See also: Z3.get_finite_domain_sort_size.

Summary: Create an array type.

We usually represent the array type as: domain -> range . Arrays are usually used to model the heap/memory in software verification.

• See also: Z3.mk_select
• See also: Z3.mk_store

Summary: Create a tuple type.

mk_tuple_sort c name field_names field_sorts creates a tuple with a constructor named name, a n fields, where n is the size of the arrays field_names and field_sorts.

Summary: Create a enumeration sort.

mk_enumeration_sort c enums creates an enumeration sort with enumeration names enums, it also returns n predicates, where n is the number of enums corresponding to testing whether an element is one of the enumerants.

Summary: Create a list sort

mk_list_sort c name elem_sort creates a list sort of name, over elements of sort elem_sort.

Summary: Create a constructor.

Summary: Reclaim memory allocated to constructor.

Summary: Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.

Summary: Create list of constructors.

Summary: Reclaim memory allocated for constructor list.

Each constructor inside the constructor list must be independently reclaimed using Z3.del_constructor.

Summary: Create mutually recursive datatypes.

Summary: Declare a constant or function.

mk_func_decl c n d r creates a function with name n, domain d, and range r. The arity of the function is the size of the array d.

Summary: Create a constant or function application.

• See also: Z3.mk_func_decl

Summary: Declare and create a constant.

mk_const c s t is a shorthand for mk_app c (mk_func_decl c s [||] t) [||]

• See also: Z3.mk_func_decl
• See also: Z3.mk_app

Summary: Declare a fresh constant or function.

Z3 will generate an unique name for this function declaration.

• See also: Z3.mk_func_decl

Summary: Declare and create a fresh constant.

mk_fresh_const c p t is a shorthand for mk_app c (mk_fresh_func_decl c p [||] t) [||].

• See also: Z3.mk_func_decl
• See also: Z3.mk_app

Summary: Create an AST node representing true.

Summary: Create an AST node representing false.

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

The nodes l and r must have the same type.

Summary: [ mk_distinct c [| t_1; ...; t_n |] ] Create an AST node represeting a distinct construct. It is used for declaring the arguments t_i pairwise distinct.

The distinct construct is used for declaring the arguments pairwise distinct. That is, Forall 0 <= i < j < num_args. not argsi = argsj .

All arguments must have the same sort.

• Remarks: The number of arguments of a distinct construct must be greater than one.

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

The node a must have Boolean sort.

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

The node t1 must have Boolean sort, t2 and t3 must have the same sort. The sort of the new node is equal to the sort of t2 and t3.

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

The nodes t1 and t2 must have Boolean sort.

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

The nodes t1 and t2 must have Boolean sort.

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

The nodes t1 and t2 must have Boolean sort.

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

All arguments must have Boolean sort.

• Remarks: The number of arguments must be greater than zero.

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

All arguments must have Boolean sort.

• Remarks: The number of arguments must be greater than zero.

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

All arguments must have int or real sort.

• Remarks: The number of arguments must be greater than zero.

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

All arguments must have int or real sort.

• Remarks: Z3 has limited support for non-linear arithmetic.
• Remarks: The number of arguments must be greater than zero.

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

All arguments must have int or real sort.

• Remarks: The number of arguments must be greater than zero.

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

The arguments must have int or real type.

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

The arguments must either both have int type or both have real type. If the arguments have int type, then the result type is an int type, otherwise the the result type is real.

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

The arguments must have int type.

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

The arguments must have int type.

The arguments must have int or real type.

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

The nodes t1 and t2 must have the same sort, and must be int or real.

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

The nodes t1 and t2 must have the same sort, and must be int or real.

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

The nodes t1 and t2 must have the same sort, and must be int or real.

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

The nodes t1 and t2 must have the same sort, and must be int or real.

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

There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.

You can take the floor of a real by creating an auxiliary integer constant k and and asserting mk_int2real(k) <= t1 < mk_int2real(k)+1 .

The node t1 must have sort integer.

• See also: Z3.mk_real2int
• See also: Z3.mk_is_int

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

The semantics of this function follows the SMT-LIB standard for the function to_int

• See also: Z3.mk_int2real
• See also: Z3.mk_is_int

Summary: [ mk_is_int c t1 ] Check if a real number is an integer.

• See also: Z3.mk_int2real
• See also: Z3.mk_real2int

Summary: [ mk_bvnot c t1 ] Bitwise negation.

The node t1 must have a bit-vector sort.

Summary: [ mk_bvredand c t1 ] Take conjunction of bits in vector, return vector of length 1.

The node t1 must have a bit-vector sort.

Summary: [ mk_bvredor c t1 ] Take disjunction of bits in vector, return vector of length 1.

The node t1 must have a bit-vector sort.

Summary: [ mk_bvand c t1 t2 ] Bitwise and.

The nodes t1 and t2 must have the same bit-vector sort.

Summary: [ mk_bvor c t1 t2 ] Bitwise or.

The nodes t1 and t2 must have the same bit-vector sort.

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

The nodes t1 and t2 must have the same bit-vector sort.

Summary: [ mk_bvnand c t1 t2 ] Bitwise nand.

The nodes t1 and t2 must have the same bit-vector sort.

Summary: [ mk_bvnor c t1 t2 ] Bitwise nor.

The nodes t1 and t2 must have the same bit-vector sort.

Summary: [ mk_bvxnor c t1 t2 ] Bitwise xnor.

The nodes t1 and t2 must have the same bit-vector sort.

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

The node t1 must have bit-vector sort.

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

The nodes t1 and t2 must have the same bit-vector sort.

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

The nodes t1 and t2 must have the same bit-vector sort.

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

The nodes t1 and t2 must have the same bit-vector sort.

Summary: [ mk_bvudiv c t1 t2 ] Unsigned division.

It is defined as the floor of t1/t2 if t2 is different from zero. If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector sort.

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

It is defined in the following way:

• The floor of t1/t2 if t2 is different from zero, and t1*t2 >= 0 .

• The ceiling of t1/t2 if t2 is different from zero, and t1*t2 < 0 .

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector sort.

Summary: [ mk_bvurem c t1 t2 ] Unsigned remainder.

It is defined as t1 - (t1 /u t2) * t2 , where /u represents unsigned int division.

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector sort.

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

It is defined as t1 - (t1 /s t2) * t2 , where /s represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of t1.

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector sort.

• See also: Z3.mk_bvsmod

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

If t2 is zero, then the result is undefined.

The nodes t1 and t2 must have the same bit-vector sort.

• See also: Z3.mk_bvsrem

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

The nodes t1 and t2 must have the same bit-vector sort.

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

It abbreviates:

      (or (and (= (extract[|m-1|:|m-1|] t1) bit1)
               (= (extract[|m-1|:|m-1|] t2) bit0))
          (and (= (extract[|m-1|:|m-1|] t1) (extract[|m-1|:|m-1|] t2))
               (bvult t1 t2)))
       

The nodes t1 and t2 must have the same bit-vector sort.

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

The nodes t1 and t2 must have the same bit-vector sort.

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

The nodes t1 and t2 must have the same bit-vector sort.

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

The nodes t1 and t2 must have the same bit-vector sort.

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

The nodes t1 and t2 must have the same bit-vector sort.

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

The nodes t1 and t2 must have the same bit-vector sort.

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

The nodes t1 and t2 must have the same bit-vector sort.

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

The nodes t1 and t2 must have (possibly different) bit-vector sorts

The result is a bit-vector of size n1+n2 , where n1 (n2) is the size of t1 (t2).

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 .

The node t1 must have a bit-vector sort.

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.

The node t1 must have a bit-vector sort.

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.

The node t1 must have a bit-vector sort.

Summary: [ mk_repeat c i t1 ] Repeat the given bit-vector up length i .

The node t1 must have a bit-vector sort.

Summary: [ mk_bvshl c t1 t2 ] Shift left.

It is equivalent to multiplication by 2^x where x is the value of the third argument.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The nodes t1 and t2 must have the same bit-vector sort.

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

It is equivalent to unsigned int division by 2^x where x is the value of the third argument.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The nodes t1 and t2 must have the same bit-vector sort.

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

It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The nodes t1 and t2 must have the same bit-vector sort.

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

The node t1 must have a bit-vector sort.

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

The node t1 must have a bit-vector sort.

Summary: [ mk_ext_rotate_left c t1 t2 ] Rotate bits of t1 to the left t2 times.

The nodes t1 and t2 must have the same bit-vector sort.

Summary: [ mk_ext_rotate_right c t1 t2 ] Rotate bits of t1 to the right t2 times.

The nodes t1 and t2 must have the same bit-vector sort.

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

NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.

The node t1 must have integer sort.

Summary: [ mk_bv2int c t1 is_signed ] Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is treated as unsigned int. So the result is non-negative and in the range 0..2^N-1 , where N are the number of bits in t1. If is_signed is true, t1 is treated as a signed bit-vector.

NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.

The node t1 must have a bit-vector sort.

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.

The nodes t1 and t2 must have the same bit-vector sort.

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.

The nodes t1 and t2 must have the same bit-vector sort.

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.

The nodes t1 and t2 must have the same bit-vector sort.

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.

The nodes t1 and t2 must have the same bit-vector sort.

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.

The nodes t1 and t2 must have the same bit-vector sort.

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

The node t1 must have bit-vector sort.

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.

The nodes t1 and t2 must have the same bit-vector sort.

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.

The nodes t1 and t2 must have the same bit-vector sort.

Summary: [ mk_select c a i ] Array read. The argument a is the array and i is the index of the array that gets read.

The node a must have an array sort domain -> range , and i must have the sort domain. The sort of the result is range.

• See also: Z3.mk_array_sort
• See also: Z3.mk_store

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

The node a must have an array sort domain -> range , i must have sort domain, v must have sort range. The sort of the result is domain -> range . The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http: The result of this function is an array that is equal to a (with respect to select) on all indices except for i, where it maps to v (and the select of a with respect to i may be a different value).

• See also: Z3.mk_array_sort
• See also: Z3.mk_select

Summary: Create the constant array.

The resulting term is an array, such that a select on an arbitrary index produces the value v.

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

The n nodes args must be of array sorts domain_i -> range_i . The function declaration f must have type range_1 .. range_n -> range . v must have sort range. The sort of the result is domain_i -> range .

• See also: Z3.mk_array_sort
• See also: Z3.mk_store
• See also: Z3.mk_select

Summary: Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.

Summary: Create Set type.

Summary: Create the empty set.

Summary: Create the full set.

Summary: Add an element to a set.

The first argument must be a set, the second an element.

Summary: Remove an element to a set.

The first argument must be a set, the second an element.

Summary: Take the union of a list of sets.

Summary: Take the intersection of a list of sets.

Summary: Take the set difference between two sets.

Summary: Take the complement of a set.

Summary: Check for set membership.

The first argument should be an element type of the set.

Summary: Check for subsetness of sets.

Summary: Create a numeral of a given sort.

Summary: Create a real from a fraction.

Summary: Create a numeral of a given sort.

This function can be use to create numerals that fit in a machine integer. It is slightly faster than Z3.mk_numeral since it is not necessary to parse a string.

• See also: Z3.mk_numeral

Summary: Create a numeral of a given sort.

This function can be use to create numerals that fit in a machine long long integer. It is slightly faster than Z3.mk_numeral since it is not necessary to parse a string.

• See also: Z3.mk_numeral

Summary: Create a pattern for quantifier instantiation.

Z3 uses pattern matching to instantiate quantifiers. If a pattern is not provided for a quantifier, then Z3 will automatically compute a set of patterns for it. However, for optimal performance, the user should provide the patterns.

Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is a called a multi-pattern.

In general, one can pass in a list of (multi-)patterns in the quantifier constructor.

• See also: Z3.mk_forall
• See also: Z3.mk_exists

Summary: Create a bound variable.

Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from non-de-Bruijn formulas to de-Bruijn format.

 
       abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0)
       abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi))
       abs1(x, x, n) = b_n
       abs1(y, x, n) = y
       abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))
       abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))
       

The last line is significant: the index of a bound variable is different depending on the scope in which it appears. The deeper x appears, the higher is its index.

Summary: Create a forall formula. It takes an expression body that contains bound variables of the same sorts as the sorts listed in the array sorts. The bound variables are de-Bruijn indices created using Z3.mk_bound. The array decl_names contains the names that the quantified formula uses for the bound variables. Z3 applies the convention that the last element in the decl_names and sorts array refers to the variable with index 0, the second to last element of decl_names and sorts refers to the variable with index 1, etc.

mk_forall c w p t n b creates a forall formula, where w is the weight, p is an array of patterns, t is an array with the sorts of the bound variables, n is an array with the 'names' of the bound variables, and b is the body of the quantifier. Quantifiers are associated with weights indicating the importance of using the quantifier during instantiation.

Summary: Create an exists formula. Similar to Z3.mk_forall.

• See also: Z3.mk_pattern
• See also: Z3.mk_bound
• See also: Z3.mk_forall
• See also: Z3.mk_quantifier

Summary: Create a quantifier - universal or existential, with pattern hints. See the documentation for Z3.mk_forall for an explanation of the parameters.

Summary: Create a quantifier - universal or existential, with pattern hints, no patterns, and attributes

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

Summary: Similar to Z3.mk_forall_const.

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

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

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

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_int c s ] Return the symbol int value.

• Precondition: get_symbol_kind s == INT_SYMBOL

• See also: Z3.mk_int_symbol

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

• Precondition: get_symbol_string s == STRING_SYMBOL

• See also: Z3.mk_string_symbol

Summary: Convert a sort into ast.

• Remarks: Z3.sort_to_ast c s can be replaced by (s :> Z3.ast).

Summary: compare sorts.

Summary: Return a unique identifier for s.

Summary: Return the sort name as a symbol.

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

• See also: Z3.sort_kind

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

• Precondition: get_sort_kind c t == BV_SORT

• See also: Z3.mk_bv_sort
• See also: Z3.get_sort_kind

Summary: Return the size of the sort in r. Return None if the call failed. That is, get_sort_kind(s) == FINITE_DOMAIN_SORT

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

• Precondition: get_sort_kind c t == ARRAY_SORT

• See also: Z3.mk_array_sort
• See also: Z3.get_sort_kind

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

• Precondition: get_sort_kind c t == ARRAY_SORT

• See also: Z3.mk_array_sort
• See also: Z3.get_sort_kind

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

• Precondition: get_sort_kind c t == DATATYPE_SORT

• See also: Z3.mk_tuple_sort
• See also: Z3.get_sort_kind

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

• Precondition: get_sort_kind c t == DATATYPE_SORT

• Remarks: Consider using the function Z3.get_tuple_sort, which returns a tuple: tuple constructor, and an array of the tuple sort fields.

• See also: Z3.mk_tuple_sort
• See also: Z3.get_sort_kind

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.

• Remarks: Consider using the function Z3.get_tuple_sort, which returns a tuple: tuple constructor, and an array of the tuple sort fields.

• Precondition: get_sort_kind t == DATATYPE_SORT
• Precondition: i < get_tuple_sort_num_fields c t

• See also: Z3.mk_tuple_sort
• See also: Z3.get_sort_kind

Summary: Return number of constructors for datatype.

• Precondition: get_sort_kind t == DATATYPE_SORT

• See also: Z3.get_datatype_sort_constructor
• See also: Z3.get_datatype_sort_recognizer
• See also: Z3.get_datatype_sort_constructor_accessor

Summary: Return idx'th constructor.

• Precondition: get_sort_kind t == DATATYPE_SORT
• Precondition: idx < get_datatype_sort_num_constructors c t

• See also: Z3.get_datatype_sort_num_constructors
• See also: Z3.get_datatype_sort_recognizer
• See also: Z3.get_datatype_sort_constructor_accessor

Summary: Return idx'th recognizer.

• Precondition: get_sort_kind t == DATATYPE_SORT
• Precondition: idx < get_datatype_sort_num_constructors c t

• See also: Z3.get_datatype_sort_num_constructors
• See also: Z3.get_datatype_sort_constructor
• See also: Z3.get_datatype_sort_constructor_accessor

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

• Precondition: get_sort_kind t == DATATYPE_SORT
• Precondition: idx_c < get_datatype_sort_num_constructors c t
• Precondition: idx_a < get_domain_size c get_datatype_sort_constructor c idx_c

• See also: Z3.get_datatype_sort_num_constructors
• See also: Z3.get_datatype_sort_constructor
• See also: Z3.get_datatype_sort_recognizer

Summary: Query constructor for declared functions.

Summary: Return arity of relation.

• Precondition: get_sort_kind s == RELATION_SORT

• See also: Z3.get_relation_column

Summary: Return sort at i'th column of relation sort.

• Precondition: get_sort_kind c s == RELATION_SORT
• Precondition: col < get_relation_arity c s

• See also: Z3.get_relation_arity

Summary: Convert a func_decl into ast.

• Remarks: Z3.func_decl_to_ast c f can be replaced by (f :> Z3.ast).

Summary: compare terms.

Summary: Return a unique identifier for f.

Summary: Return the constant declaration name as a symbol.

Summary: Return declaration kind corresponding to declaration.

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

• See also: Z3.get_arity

Summary: Alias for get_domain_size.

• See also: Z3.get_domain_size

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

• Precondition: i < get_domain_size d

• See also: Z3.get_domain_size

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

If d is a constant (i.e., has zero arguments), then this function returns the sort of the constant.

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

Summary: Return the parameter type associated with a declaration.

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

• Precondition: get_decl_parameter_kind c d idx == PARAMETER_INT

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

• Precondition: get_decl_parameter_kind c d idx == PARAMETER_DOUBLE

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

• Precondition: get_decl_parameter_kind c d idx == PARAMETER_SYMBOL

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

• Precondition: get_decl_parameter_kind c d idx == PARAMETER_SORT

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

• Precondition: get_decl_parameter_kind c d idx == PARAMETER_AST

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

• Precondition: get_decl_parameter_kind c d idx == PARAMETER_FUNC_DECL

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

• Precondition: get_decl_parameter_kind c d idx == PARAMETER_RATIONAL

Summary: Convert a app into ast.

• Remarks: Z3.app_to_ast c a can be replaced by (a :> Z3.ast).

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. If t is an constant, then the number of arguments is 0.

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

• Precondition: i < get_num_args c a

Summary: compare terms.

Summary: Return a unique identifier for t. Implicitly used by Pervasives.compare for values of type ast, app, sort, func_decl, and pattern.

Summary: Return a hash code for the given AST. Implicitly used by Hashtbl.hash for values of type ast, app, sort, func_decl, and pattern.

Summary: Return the sort of an AST node.

The AST node must be a constant, application, numeral, bound variable, or quantifier.

Summary: Return true if the given expression t is well sorted.

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

Summary: Return the kind of the given AST.

val is_numeral_ast : context -> ast -> bool

val is_algebraic_number : context -> ast -> bool

Summary: Return true if the give AST is a real algebraic number.

Summary: Convert an ast into an APP_AST.

• Precondition:

   get_ast_kind c a == [APP_AST] 

Summary: Convert an AST into a FUNC_DECL_AST. This is just type casting.

• Precondition:

   get_ast_kind c a == FUNC_DECL_AST 

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

• Precondition: get_ast_kind c a == NUMERAL_AST

Summary: Return numeral as a string in decimal notation. The result has at most precision decimal places.

• Precondition: get_ast_kind c a == NUMERAL_AST || is_algebraic_number c a

Summary: Return the numerator (as a numeral AST) of a numeral AST of sort Real.

• Precondition: get_ast_kind c a == NUMERAL_AST

Summary: Return the denominator (as a numeral AST) of a numeral AST of sort Real.

• Precondition: get_ast_kind c a == NUMERAL_AST

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

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

• Precondition: get_ast_kind c v == NUMERAL_AST

• See also: Z3.get_numeral_string

Summary: [ get_numeral_int64 c v ] Similar to Z3.get_numeral_string, but only succeeds if the value can fit in a machine long long int. Return TRUE if the call succeeded.

• Precondition: get_ast_kind c v == NUMERAL_AST

• See also: Z3.get_numeral_string

Summary: [ get_numeral_rational_int64 c x y ] Similar to Z3.get_numeral_string, but only succeeds if the value can fit as a reational number as machine long long int. Return TRUE if the call succeeded.

• Precondition: get_ast_kind c v == NUMERAL_AST

• See also: Z3.get_numeral_string

Summary: Return a lower bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision. The result is a numeral AST of sort Real.

• Precondition: is_algebraic_number c a

Summary: Return a upper bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision. The result is a numeral AST of sort Real.

• Precondition: is_algebraic_number c a

Summary: Convert a pattern into ast.

• Remarks: Z3.pattern_to_ast c p can be replaced by (p :> Z3.ast).

Summary: Return number of terms in pattern.

Summary: Return i'th ast in pattern.

Summary: Return index of de-Brujin bound variable.

• Precondition: get_ast_kind a == VAR_AST

Summary: Determine if quantifier is universal.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Obtain weight of quantifier.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Return number of patterns used in quantifier.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Return i'th pattern.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Return number of no_patterns used in quantifier.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Return i'th no_pattern.

• Precondition: get_ast_kind a == QUANTIFIER_AST

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

• Precondition: get_ast_kind a == QUANTIFIER_AST

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

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Return body of quantifier.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Return number of bound variables of quantifier.

• Precondition: get_ast_kind a == QUANTIFIER_AST

Summary: Interface to simplifier.

Provides an interface to the AST simplifier used by Z3.

Summary: Interface to simplifier.

Provides an interface to the AST simplifier used by Z3. This procedure is similar to Z3.simplify, but the behavior of the simplifier can be configured using the given parameter set.

Summary: Return a string describing all available parameters.

Summary: Update the arguments of term a using the arguments args. The number of arguments num_args should coincide with the number of arguments to a. If a is a quantifier, then num_args has to be 1.

Summary: Substitute every occurrence of fromi in a with toi , for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of fromi must be equal to sort of toi .

Summary: Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs, the variable with de-Bruijn index i is replaced with term toi .

Summary: Translate/Copy the AST a from context source to context target. AST a must have been created using context source.

• Precondition: source != target

Summary: Increment the reference counter of the given model.

Summary: Decrement the reference counter of the given model.

Summary: Return the interpretation (i.e., assignment) of constant a in the model m. Return None, if the model does not assign an interpretation for a. That should be interpreted as: the value of a does not matter.

• Precondition: get_arity c a == 0

Summary: Return the interpretation of the function f in the model m. Return None, if the model does not assign an interpretation for f. That should be interpreted as: the f does not matter.

• Precondition: get_arity c f > 0

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

• Remarks: Consider using Z3.get_model_constants.

• See also: Z3.model_get_const_decl

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

• Precondition: i < model_get_num_consts c m

• See also: Z3.eval

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

A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments.

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

• Precondition: i < model_get_num_funcs c m

• See also: Z3.model_get_num_funcs

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

Return None if the term was not successfully evaluated.

If model_completion is TRUE, then Z3 will assign an interpretation for any constant or function that does not have an interpretation in m. These constants and functions were essentially don't cares.

The evaluation may fail for the following reasons:

• t contains a quantifier.

• the model m is partial, that is, it doesn't have a complete interpretation for uninterpreted functions. That is, the option MODEL_PARTIAL=true was used.

• t is type incorrect.

Summary: Return the number of uninterpreted sorts that m assigs an interpretation to.

Z3 also provides an intepretation for uninterpreted sorts used in a formua. The interpretation for a sort s is a finite set of distinct values. We say this finite set is the "universe" of s.

• See also: Z3.model_get_sort
• See also: Z3.model_get_sort_universe

Summary: Return a uninterpreted sort that m assigns an interpretation.

• Precondition: i < model_get_num_sorts c m

• See also: Z3.model_get_num_sorts
• See also: Z3.model_get_sort_universe

Summary: Return the finite set of distinct values that represent the interpretation for sort s.

• See also: Z3.model_get_num_sorts
• See also: Z3.model_get_sort

Summary: The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3. It is the array such that forall indices i we have that (select (_ as-array f) i) is equal to (f i) . This procedure returns TRUE if the a is an as-array AST node.

Z3 current solvers have minimal support for as_array nodes.

• See also: Z3.get_as_array_func_decl

Summary: Return the function declaration f associated with a (_ as_array f) node.

• See also: Z3.is_as_array

Summary: Increment the reference counter of the given func_interp object.

Summary: Decrement the reference counter of the given func_interp object.

Summary: Return the number of entries in the given function interpretation.

A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments. This procedure return the number of element in the finite map of f.

Summary: Return a "point" of the given function intepretation. It represents the value of f in a particular point.

• Precondition: i < func_interp_get_num_entries c f

• See also: Z3.func_interp_get_num_entries

Summary: Return the 'else' value of the given function interpretation.

A function interpretation is represented as a finite map and an 'else' value. This procedure returns the 'else' value.

Summary: Return the arity (number of arguments) of the given function interpretation.

Summary: Increment the reference counter of the given func_entry object.

Summary: Decrement the reference counter of the given func_entry object.

Summary: Return the value of this point.

A func_entry object represents an element in the finite map used to encode a function interpretation.

• See also: Z3.func_interp_get_entry

Summary: Return the number of arguments in a func_entry object.

• See also: Z3.func_interp_get_entry

Summary: Return an argument of a func_entry object.

• Precondition: i < func_entry_get_num_args c e

• See also: Z3.func_interp_get_entry

Summary: Log interaction to a file.

Summary: Append user-defined string to interaction log.

The interaction log is opened using open_log. It contains the formulas that are checked using Z3. You can use this command to append comments, for instance.

Summary: Close interaction log.

Summary: Enable/disable printing warning messages to the console.

Warnings are printed after passing true, warning messages are suppressed after calling this method with false.

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

The default mode for pretty printing AST nodes 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.

• See also: Z3.ast_to_string
• See also: Z3.pattern_to_string
• See also: Z3.func_decl_to_string

Summary: Convert the given AST node into a string.

• See also: Z3.pattern_to_string
• See also: Z3.sort_to_string

val sort_to_string : context -> sort -> string

val func_decl_to_string : context -> func_decl -> string

val model_to_string : context -> model -> string

Summary: Convert the given model into a string.

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

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

The symbol table of the parser can be initialized using the given sorts and declarations. The symbols in the arrays sort_names and decl_names don't need to match the names of the sorts and declarations in the arrays sorts and decls. This is an useful feature since we can use arbitrary names to reference sorts and declarations defined using the C API.

The formulas, assumptions and declarations defined in str can be extracted using the functions: Z3.get_smtlib_num_formulas, Z3.get_smtlib_formula, Z3.get_smtlib_num_assumptions, Z3.get_smtlib_assumption, Z3.get_smtlib_num_decls, and Z3.get_smtlib_decl.

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

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

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.

• Precondition: i < get_smtlib_num_formulas c

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

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.

• Precondition: i < get_smtlib_num_assumptions c

Summary: Return the number of declarations parsed by 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.

• Precondition: i < get_smtlib_num_decls c

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

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.

• Precondition: i < get_smtlib_num_sorts c

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

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

Return the conjunction of asserts made in the input.

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

Summary: [ parse_smtlib2_string c str ] Parse the given string using the SMT-LIB2 parser.

It returns a formula comprising of the conjunction of assertions in the scope (up to push/pop) at the end of the string.

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

Summary: Return Z3 version number information.

Summary: Reset all allocated resources.

Use this facility on out-of memory errors. It allows discharging the previous state and resuming afresh. Any pointers previously returned by the API become invalid.

Summary: Create a new user defined theory. The new theory will be identified by the name th_name. A theory must be created before asserting any assertion to the given context.

Summary: Create an interpreted theory sort.

Summary: Create an interpreted theory constant value. Values are assumed to be different from each other.

Summary: Create an interpreted constant for the given theory.

Summary: Create an interpreted function declaration for the given theory.

Summary: Return the context where the given theory is installed.

Summary: Set a callback that is invoked when theory t is deleted. This callback should be used to delete external data-structures associated with the given theory.

• See: Z3.mk_theory

Summary: Set a callback for simplifying operators of the given theory. The callback f is invoked by Z3's simplifier.

Summary: Set a callback for simplifying the atom s_1 = s_2 , when the sort of s_1 and s_2 is an interpreted sort of the given theory. The callback f is invoked by Z3's simplifier.

Summary: Set a callback for simplifying the atom distinct(s_1, ..., s_n) , when the sort of s_1, ..., s_n is an interpreted sort of the given theory. The callback f is invoked by Z3's simplifier.

Summary: Set a callback that is invoked when a theory application is finally added into the logical context. Note that, not every application contained in an asserted expression is actually added into the logical context because it may be simplified during a preprocessing step.

• Remarks: An expression n added to the logical context at search level n, will remain in the logical context until this level is backtracked.

Summary: Set a callback that is invoked when an expression of sort s, where s is an interpreted sort of the theory \c t, is finally added into the logical context. Note that, not every expression contained in an asserted expression is actually added into the logical context because it may be simplified during a preprocessing step.

• Remarks: An expression n added to the logical context at search level n, will remain in the logical context until this level is backtracked.

Summary: Set a callback that is invoked when Z3 starts searching for a satisfying assignment.

Summary: Set a callback that is invoked when Z3 creates a case-split (aka backtracking point).

When a case-split is created we say the search level is increased.

Summary: Set a callback that is invoked when Z3 backtracks a case-split.

When a case-split is backtracked we say the search level is decreased.

Summary: Set a callback that is invoked when Z3 restarts the search for a satisfying assignment.

Summary: Set a callback that is invoked when the logical context is reset by the user. This callback is useful for reseting any data-structure maintained by the user theory solver.

Summary: Set a callback that is invoked before Z3 starts building a model. A theory may use this callback to perform expensive operations.

If the theory returns false, Z3 will assume that theory is giving up, and it will assume that it was not possible to decide if the asserted constraints are satisfiable or not.

Summary: Set a callback that is invoked when an equality s_1 = s_2 is found by the logical context.

Summary: Set a callback that is invoked when a disequality s_1 != s_2 is found by the logical context.

Summary: Set a callback that is invoked when a theory predicate is assigned to true/false by Z3.

Summary: Set a callback that is invoked when an expression is marked as relevant during the search. This callback is only invoked when relevancy propagation is enabled.

Summary: Assert a theory axiom/lemmas during the search.

An axiom added at search level n will remain in the logical context until level n is backtracked.

The callbacks for push (Z3.set_push_callback) and pop (Z3.set_pop_callback) can be used to track when the search level is increased (i.e., new case-split) and decreased (i.e., case-split is backtracked).

Z3 tracks the theory axioms asserted. So, multiple assertions of the same axiom are ignored.

Summary: Inform to the logical context that lhs and rhs have the same interpretation in the model being built by theory t. If lhs = rhs is inconsistent with other theories, then the logical context will backtrack.

For more information, see the paper "Model-Based Theory Combination" in the Z3 website.

Summary: Enable/disable the simplification of theory axioms asserted using Z3.theory_assert_axiom. By default, the simplification of theory specific operators is disabled. That is, the reduce theory callbacks are not invoked for theory axioms. The default behavior is useful when asserting axioms stating properties of theory operators.

Summary: Return the root of the equivalence class containing n.

Summary: Return the next element in the equivalence class containing n.

The elements in an equivalence class are organized in a circular list. You can traverse the list by calling this function multiple times using the result from the previous call. This is illustrated in the code snippet below.

           ast curr = n;
           do
             curr = theory_get_eqc_next(theory, curr);
           while (curr != n);
       

Summary: Return the number of parents of n that are operators of the given theory.

Summary: Return the i-th parent of n. See Z3.theory_get_num_parents.

Summary: Return TRUE if n is an interpreted theory value.

Summary: Return TRUE if d is an interpreted theory declaration.

Summary: Return the number of expressions of the given theory in the logical context. These are the expressions notified using the callback Z3.set_new_elem_callback.

Summary: Return the i-th elem of the given theory in the logical context.

• See: Z3.theory_get_num_elems

Summary: Return the number of theory applications in the logical context. These are the expressions notified using the callback Z3.set_new_app_callback.

Summary: Return the i-th application of the given theory in the logical context.

• See: Z3.theory_get_num_apps

Summary: Create a new fixedpoint context.

Summary: Increment the reference counter of the given fixedpoint context

Summary: Decrement the reference counter of the given fixedpoint context.

Summary: Add a universal Horn clause as a named rule. The horn_rule should be of the form:

           horn_rule ::= (forall (bound-vars) horn_rule)
                      |  (=> atoms horn_rule)
                      |  atom
       

Summary: Assert a constraint to the fixedpoint context.

The constraints are used as background axioms when the fixedpoint engine uses the PDR mode. They are ignored for standard Datalog mode.

Summary: Pose a query against the asserted rules.

           query ::= (exists (bound-vars) query)
                 |  literals 
        

query returns

• L_FALSE if the query is unsatisfiable.
• L_TRUE if the query is satisfiable. Obtain the answer by calling Z3.fixedpoint_get_answer.
• L_UNDEF if the query was interrupted, timed out or otherwise failed.

Summary: Pose multiple queries against the asserted rules.

The queries are encoded as relations (function declarations).

query returns

• L_FALSE if the query is unsatisfiable.
• L_TRUE if the query is satisfiable. Obtain the answer by calling Z3.fixedpoint_get_answer.
• L_UNDEF if the query was interrupted, timed out or otherwise failed.

Summary: Retrieve a formula that encodes satisfying answers to the query.

When used in Datalog mode, the returned answer is a disjunction of conjuncts. Each conjunct encodes values of the bound variables of the query that are satisfied. In PDR mode, the returned answer is a single conjunction.

The previous call to fixedpoint_query must have returned L_TRUE.

Summary: Retrieve a string that describes the last status returned by Z3.fixedpoint_query.

Use this method when Z3.fixedpoint_query returns L_UNDEF.

Summary: Retrieve statistics information from the last call to Z3.fixedpoint_query.

Summary: Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics. For example, the relation is empty if it does not occur in a head or a fact.

Summary: Configure the predicate representation.

It sets the predicate to use a set of domains given by the list of symbols. The domains given by the list of symbols must belong to a set of built-in domains.

Summary: Simplify rules into a set of new rules that are returned. The simplification routines apply inlining, quantifier elimination, and other algebraic simplifications.

Summary: Print the current rules and background axioms as a string.

Summary: Return an empty AST vector.

Summary: Increment the reference counter of the given AST vector.

Summary: Decrement the reference counter of the given AST vector.

Summary: Return the size of the given AST vector.

Summary: Return the AST at position i in the AST vector v.

• Precondition: i < ast_vector_size c v

Summary: Update position i of the AST vector v with the AST a.

• Precondition: i < ast_vector_size c v

Summary: Resize the AST vector v.

Summary: Add the AST a in the end of the AST vector v. The size of v is increased by one.

Summary: Translate the AST vector v from context s into an AST vector in context t.

Summary: Convert AST vector into a string.

Summary: Return an empty mapping from AST to AST

Summary: Increment the reference counter of the given AST map.

Summary: Decrement the reference counter of the given AST map.

Summary: Return true if the map m contains the AST key k.

Summary: Return the value associated with the key k.

The procedure invokes the error handler if k is not in the map.

Summary: Store/Replace a new key, value pair in the given map.

Summary: Erase a key from the map.

Summary: Remove all keys from the given map.

Summary: Return the size of the given map.

Summary: Return the keys stored in the given map.

Summary: Convert the given map into a string.

Summary: Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.

If models == true, then model generation is enabled for the new goal.

If unsat_cores == true, then unsat core generation is enabled for the new goal.

If proofs == true, then proof generation is enabled for the new goal. Remark, the Z3 context c must have been created with proof generation support.

Summary: Increment the reference counter of the given goal.

Summary: Decrement the reference counter of the given goal.

Summary: Return the "precision" of the given goal. Goals can be transformed using over and under approximations. A under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.

Summary: Add a new formula a to the given goal.

Summary: Return true if the given goal contains the formula false.

Summary: Return the depth of the given goal. It tracks how many transformations were applied to it.

Summary: Erase all formulas from the given goal.

Summary: Return the number of formulas in the given goal.

Summary: Return a formula from the given goal.

• Precondition: idx < goal_size c g

Summary: Return the number of formulas, subformulas and terms in the given goal.

Summary: Return true if the goal is empty, and it is precise or the product of a under approximation.

Summary: Return true if the goal contains false, and it is precise or the product of an over approximation.

Summary: Copy a goal g from the context source to a the context target.

Summary: Convert a goal into a string.

Summary: Return a tactic associated with the given name. The complete list of tactics may be obtained using the procedures Z3.get_num_tactics and Z3.get_tactic_name. It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end.

Tactics are the basic building block for creating custom solvers for specific problem domains.

Summary: Increment the reference counter of the given tactic.

Summary: Decrement the reference counter of the given tactic.

Summary: Return a probe associated with the given name. The complete list of probes may be obtained using the procedures Z3.get_num_probes and Z3.get_probe_name. It may also be obtained using the command (help-tactics) in the SMT 2.0 front-end.

Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used.

Summary: Increment the reference counter of the given probe.

Summary: Decrement the reference counter of the given probe.

Summary: Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1.

Summary: Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 applied to the given goal.