merge with unstable

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/z3_api.h

@@ -251,6 +251,8 @@ typedef enum
    - Z3_OP_OEQ Binary equivalence modulo namings. This binary predicate is used in proof terms.
         It captures equisatisfiability and equivalence modulo renamings.
 
+   - Z3_OP_INTERP Marks a sub-formula for interpolation.
+
    - Z3_OP_ANUM Arithmetic numeral.
 
    - Z3_OP_AGNUM Arithmetic algebraic numeral. Algebraic numbers are used to represent irrational numbers in Z3.
@@ -901,6 +903,7 @@ typedef enum {
     Z3_OP_NOT,
     Z3_OP_IMPLIES,
     Z3_OP_OEQ,
+    Z3_OP_INTERP,
 
     // Arithmetic
     Z3_OP_ANUM = 0x200,
@@ -2121,6 +2124,16 @@ END_MLAPI_EXCLUDE
     */
     Z3_ast Z3_API Z3_mk_not(__in Z3_context c, __in Z3_ast a);
     
+    /**
+        \brief \mlh mk_interp c a \endmlh 
+        Create an AST node marking a formula position for interpolation.
+        
+        The node \c a must have Boolean sort.
+
+        def_API('Z3_mk_interp', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_interp(__in Z3_context c, __in Z3_ast a);
+    
     /**
        \brief \mlh mk_ite c t1 t2 t2 \endmlh 
        Create an AST node representing an if-then-else: <tt>ite(t1, t2,
@@ -7863,6 +7876,211 @@ END_MLAPI_EXCLUDE
 
     /*@}*/
 
+    /**
+        @name Interpolation
+    */
+    /*@{*/
+
+    /** \brief This function generates a Z3 context suitable for generation of
+	interpolants. Formulas can be generated as abstract syntx trees in
+	this context using the Z3 C API.
+	
+	Interpolants are also generated as AST's in this context.
+
+	If cfg is non-null, it will be used as the base configuration
+	for the Z3 context. This makes it possible to set Z3 options
+	to be used during interpolation. This feature should be used
+	with some caution however, as it may be that certain Z3 options
+	are incompatible with interpolation. 
+
+	def_API('Z3_mk_interpolation_context', CONTEXT, (_in(CONFIG),))
+
+    */
+
+  Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg);
+
+
+/** Constant reprepresenting a root of a formula tree for tree interpolation */
+#define IZ3_ROOT SHRT_MAX
+
+/** This function uses Z3 to determine satisfiability of a set of
+    constraints. If UNSAT, an interpolant is returned, based on the
+    refutation generated by Z3. If SAT, a model is returned.
+
+    If "parents" is non-null, computes a tree interpolant. The tree is
+    defined by the array "parents".  This array maps each formula in
+    the tree to its parent, where formulas are indicated by their
+    integer index in "cnsts". The parent of formula n must have index
+    greater than n. The last formula is the root of the tree. Its
+    parent entry should be the constant IZ3_ROOT.
+
+    If "parents" is null, computes a sequence interpolant. 
+
+    \param ctx The Z3 context. Must be generated by iz3_mk_context
+    \param num The number of constraints in the sequence
+    \param cnsts Array of constraints (AST's in context ctx)
+    \param parents The parents vector defining the tree structure
+    \param options Interpolation options (may be NULL)
+    \param interps Array to return interpolants (size at least num-1, may be NULL)
+    \param model Returns a Z3 model if constraints SAT (may be NULL)
+    \param labels Returns relevant labels if SAT (may be NULL)
+    \param incremental 
+
+    VERY IMPORTANT: All the Z3 formulas in cnsts must be in Z3
+    context ctx. The model and interpolants returned are also
+    in this context. 
+
+    The return code is as in Z3_check_assumptions, that is,
+
+    Z3_L_FALSE = constraints UNSAT (interpolants returned)
+    Z3_L_TRUE = constraints SAT (model returned)
+    Z3_L_UNDEF = Z3 produced no result, or interpolation not possible
+
+    Currently, this function supports integer and boolean variables,
+    as well as arrays over these types, with linear arithmetic,
+    uninterpreted functions and quantifiers over integers (that is
+    AUFLIA). Interpolants are produced in AUFLIA. However, some
+    uses of array operations may cause quantifiers to appear in the
+    interpolants even when there are no quantifiers in the input formulas.
+    Although quantifiers may appear in the input formulas, Z3 may give up in
+    this case, returning Z3_L_UNDEF.
+
+    If "incremental" is true, cnsts must contain exactly the set of
+    formulas that are currently asserted in the context. If false,
+    there must be no formulas currently asserted in the context.
+    Setting "incremental" to true makes it posisble to incrementally
+    add and remove constraints from the context until the context
+    becomes UNSAT, at which point an interpolant is computed. Caution
+    must be used, however. Before popping the context, if you wish to
+    keep the interolant formulas, you *must* preserve them by using
+    Z3_persist_ast. Also, if you want to simplify the interpolant
+    formulas using Z3_simplify, you must first pop all of the
+    assertions in the context (or use a different context). Otherwise,
+    the formulas will be simplified *relative* to these constraints,
+    which is almost certainly not what you want.
+    
+
+    Current limitations on tree interpolants. In a tree interpolation
+    problem, each constant (0-ary function symbol) must occur only
+    along one path from root to leaf. Function symbols (of arity > 0)
+    are considered to have global scope (i.e., may appear in any
+    interpolant formula). 
+
+   
+  */  
+
+
+  Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx, 
+				 __in int num,
+				 __in_ecount(num) Z3_ast *cnsts,
+				 __in_ecount(num) unsigned *parents,
+				 __in Z3_params options,
+				 __out_ecount(num-1) Z3_ast *interps,
+				 __out Z3_model *model,
+				 __out Z3_literals *labels,
+				 __in int incremental,
+				 __in int num_theory,
+				 __in_ecount(num_theory) Z3_ast *theory);
+  
+  /** Return a string summarizing cumulative time used for
+      interpolation.  This string is purely for entertainment purposes
+      and has no semantics.
+      
+      \param ctx The context (currently ignored)
+
+    def_API('Z3_interpolation_profile', STRING, (_in(CONTEXT),))
+  */
+
+  Z3_string Z3_API Z3_interpolation_profile(__in Z3_context ctx);
+  
+  /**
+     \brief Read an interpolation problem from file.
+
+     \param ctx The Z3 context. This resets the error handler of ctx.
+     \param filename The file name to read.
+     \param num Returns length of sequence.
+     \param cnsts Returns sequence of formulas (do not free)
+     \param parents Returns the parents vector (or NULL for sequence)
+     \param error Returns an error message in case of failure (do not free the string)
+
+     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 assiciated 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.
+
+  */
+  
+
+  int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx,
+				__out int *num, 
+				__out_ecount(*num) Z3_ast **cnsts, 
+				__out_ecount(*num) int **parents,
+				__in const char *filename,
+				__out const char **error,
+                                __out int *num_theory,
+				__out_ecount(*num_theory) Z3_ast **theory);
+
+
+
+  /** Check the correctness of an interpolant. The Z3 context must
+      have no constraints asserted when this call is made. That means
+      that after interpolating, you must first fully pop the Z3
+      context before calling this. See Z3_interpolate for meaning of parameters.
+
+      \param ctx The Z3 context. Must be generated by Z3_mk_interpolation_context
+      \param num The number of constraints in the sequence
+      \param cnsts Array of constraints (AST's in context ctx)
+      \param parents The parents vector (or NULL for sequence)
+      \param interps The interpolant to check
+      \param error Returns an error message if interpolant incorrect (do not free the string)
+
+      Return value is Z3_L_TRUE if interpolant is verified, Z3_L_FALSE if
+      incorrect, and Z3_L_UNDEF if unknown.
+
+  */
+  
+  int Z3_API Z3_check_interpolant(Z3_context ctx, int num, Z3_ast *cnsts, int *parents, Z3_ast *interps, const char **error,
+                                       int num_theory, Z3_ast *theory);
+
+  /** 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.
+
+      \param ctx The Z3 context. Must be generated by z3_mk_interpolation_context
+      \param num The number of constraints in the sequence
+      \param cnsts Array of constraints
+      \param parents The parents vector (or NULL for sequence)
+      \param filename The file name to write
+
+  */
+
+  void Z3_API  Z3_write_interpolation_problem(Z3_context ctx,
+				 int num, 
+				 Z3_ast *cnsts, 
+				 int *parents,
+				 const char *filename,
+                                 int num_theory,
+				 Z3_ast *theory);
+
+
+
 #endif