Function z3_sys::Z3_read_interpolation_problem

pub unsafe extern "C" fn Z3_read_interpolation_problem(
    ctx: Z3_context, 
    num: *mut c_uint, 
    cnsts: *mut *mut Z3_ast, 
    parents: *mut *mut c_uint, 
    filename: Z3_string, 
    error: Z3_string_ptr, 
    num_theory: *mut c_uint, 
    theory: *mut *mut Z3_ast
) -> c_int

Read an interpolation problem from file.

• ctx: The Z3 context. This resets the error handler of ctx.
• filename: The file name to read.
• num: Returns length of sequence.
• cnsts: Returns sequence of formulas (do not free)
• parents: Returns the parents vector (or NULL for sequence)
• error: Returns an error message in case of failure (do not free the string)
• num_theory: Number of theory terms
• theory: Theory terms

Returns true on success.

File formats: Currently two formats are supported, based on SMT-LIB2. For sequence interpolants, the sequence of constraints is represented by the sequence of "assert" commands in the file.

For tree interpolants, one symbol of type bool is associated to each vertex of the tree. For each vertex v there is an "assert" of the form:

(implies (and c1 ... cn f) v)

where c1 .. cn are the children of v (which must precede v in the file) and f is the formula associated to node v. The last formula in the file is the root vertex, and is represented by the predicate "false".

A solution to a tree interpolation problem can be thought of as a valuation of the vertices that makes all the implications true where each value is represented using the common symbols between the formulas in the subtree and the remainder of the formulas.