Function z3_sys::Z3_write_interpolation_problem [−] [src]

pub unsafe extern "C" fn Z3_write_interpolation_problem(
    ctx: Z3_context, 
    num: c_uint, 
    cnsts: *mut Z3_ast, 
    parents: *mut c_uint, 
    filename: Z3_string, 
    num_theory: c_uint, 
    theory: *mut Z3_ast
)

Write an interpolation problem to file suitable for reading with Z3_read_interpolation_problem. The output file is a sequence of SMT-LIB2 format commands, suitable for reading with command-line Z3 or other interpolating solvers.

  • ctx: The Z3 context. Must be generated by z3_mk_interpolation_context
  • num: The number of constraints in the sequence
  • cnsts: Array of constraints
  • parents: The parents vector (or NULL for sequence)
  • filename: The file name to write
  • num_theory: Number of theory terms
  • theory: Theory terms