added simple interpolation bindings for python

src/api/api_interp.cpp

@@ -324,17 +324,20 @@ extern "C" {
     Z3_CATCH_RETURN(0);
   }
 
-  Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *out_interp){
+  Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *out_interp, __out Z3_model *model){
     Z3_TRY;
-    LOG_Z3_compute_interpolant(c, pat, p, out_interp);
+    LOG_Z3_compute_interpolant(c, pat, p, out_interp, model);
     RESET_ERROR_CODE();
 
 
-    params_ref &_p = to_params(p)->m_params;
+    // params_ref &_p = to_params(p)->m_params;
+    params_ref _p;
+    _p.set_bool("proof", true); // this is currently useless
+
+    scoped_proof_mode spm(mk_c(c)->m(),PGM_FINE);
     scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
     scoped_ptr<solver> m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null));
     m_solver.get()->updt_params(_p); // why do we have to do this?
-    scoped_proof_mode spm(mk_c(c)->m(),PGM_FINE);
 
     ast *_pat = to_ast(pat);
     
@@ -356,6 +359,8 @@ extern "C" {
     Z3_lbool status = of_lbool(_status);
     
     Z3_ast_vector_ref *v = 0;
+    *model = 0;
+
     if(_status == l_false){
       // copy result back
       v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
@@ -365,6 +370,15 @@ extern "C" {
 	_m.dec_ref(interp[i]);
       }
     }
+    else {
+      model_ref _m;
+      m_solver.get()->get_model(_m);
+      Z3_model_ref *crap = alloc(Z3_model_ref);
+      crap->m_model = _m.get();
+      mk_c(c)->save_object(crap);
+      *model = of_model(crap);
+    }
+
     *out_interp = of_ast_vector(v);
     
     return status;

src/api/python/z3.py

@@ -7253,3 +7253,128 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
     dsz, dnames, ddecls = _dict2darray(decls, ctx)
     return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
    
+def Interp(a,ctx=None):
+    """Create an interpolation operator.
+    
+    The argument is an interpolation pattern (see tree_interpolant). 
+
+    >>> x = Int('x')
+    >>> print Interp(x>0)
+    interp(x > 0)
+    """
+    ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
+    s = BoolSort(ctx)
+    a = s.cast(a)
+    return BoolRef(Z3_mk_interp(ctx.ref(), a.as_ast()), ctx)
+
+def tree_interpolant(pat,p=None,ctx=None):
+    """Compute interpolant for a tree of formulas.
+
+    The input is an interpolation pattern over a set of formulas C.
+    The pattern pat is a formula combining the formulas in C using
+    logical conjunction and the "interp" operator (see Interp). This
+    interp operator is logically the identity operator. It marks the
+    sub-formulas of the pattern for which interpolants should be
+    computed. The interpolant is a map sigma from marked subformulas
+    to formulas, such that, for each marked subformula phi of pat
+    (where phi sigma is phi with sigma(psi) substituted for each
+    subformula psi of phi such that psi in dom(sigma)):
+
+      1) phi sigma implies sigma(phi), and
+
+      2) sigma(phi) is in the common uninterpreted vocabulary between
+      the formulas of C occurring in phi and those not occurring in
+      phi
+
+      and moreover pat sigma implies false. In the simplest case
+      an interpolant for the pattern "(and (interp A) B)" maps A
+      to an interpolant for A /\ B. 
+
+      The return value is a vector of formulas representing sigma. This
+      vector contains sigma(phi) for each marked subformula of pat, in
+      pre-order traversal. This means that subformulas of phi occur before phi
+      in the vector. Also, subformulas that occur multiply in pat will
+      occur multiply in the result vector.
+
+    If pat is satisfiable, raises an object of class ModelRef
+    that represents a model of pat.
+
+    If parameters p are supplied, these are used in creating the
+    solver that determines satisfiability.
+
+    >>> x = Int('x')
+    >>> y = Int('y')
+    >>> print tree_interpolant(And(Interp(x < 0), Interp(y > 2), x == y))
+    [Not(x >= 0), Not(y <= 2)]
+    """
+    f = pat
+    ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
+    ptr = (AstVectorObj * 1)()
+    mptr = (Model * 1)()
+    if p == None:
+        p = ParamsRef(ctx)
+    res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr)
+    if res == Z3_L_FALSE:
+        return AstVector(ptr[0],ctx)
+    raise ModelRef(mptr[0], ctx)
+
+def binary_interpolant(a,b,p=None,ctx=None):
+    """Compute an interpolant for a binary conjunction.
+
+    If a & b is unsatisfiable, returns an interpolant for a & b.
+    This is a formula phi such that
+
+    1) a implies phi
+    2) b implies not phi
+    3) All the uninterpreted symbols of phi occur in both a and b.
+
+    If a & b is satisfiable, raises an object of class ModelRef
+    that represents a model of a &b.
+
+    If parameters p are supplied, these are used in creating the
+    solver that determines satisfiability.
+
+    >>> x = Int('x')
+    >>> print binary_interpolant(x<0,x>2)
+    x <= 2
+    """
+    f = And(Interp(a),b)
+    return tree_interpolant(f,p,ctx)[0]
+
+def sequence_interpolant(v,p=None,ctx=None):
+    """Compute interpolant for a sequence of formulas.
+
+    If len(v) == N, and if the conjunction of the formulas in v is
+    unsatisfiable, the interpolant is a sequence of formulas w
+    such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1:
+
+    1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N)
+    2) All uninterpreted symbols in w[i] occur in both v[0]..v[i]
+    and v[i+1]..v[n]
+    
+    Requires len(v) >= 1. 
+
+    If a & b is satisfiable, raises an object of class ModelRef
+    that represents a model of a & b.
+
+    If parameters p are supplied, these are used in creating the
+    solver that determines satisfiability.
+
+    >>> x = Int('x')
+    >>> y = Int('y')
+    >>> print sequence_interpolant([x < 0, y == x , y > 2])
+    [Not(x >= 0), Not(y >= 0)]
+
+    >>> g = And(Interp(x<0),x<2)
+    >>> try:
+    ...     print tree_interpolant(g).sexpr()
+    ... except ModelRef as m:
+    ...     print m.sexpr()
+    (define-fun x () Int
+      (- 1))
+    """
+    f = v[0]
+    for i in range(1,len(v)):
+        f = And(Interp(f),v[i])
+    return tree_interpolant(f,p,ctx)
+

src/api/z3_api.h

@@ -7790,13 +7790,16 @@ END_MLAPI_EXCLUDE
      
      \param c logical context.
      \param pat an interpolation pattern
-     \param p parameters
+     \param p parameters for solver creation
      \param status returns the status of the sat check
+     \param model returns model if satisfiable
+
+     Return value: status of SAT check
      
-     def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR)))
+     def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR), _out(MODEL)))
   */
   
-  Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *interp);
+  Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *interp, __out Z3_model *model);
 
 
 /** Constant reprepresenting a root of a formula tree for tree interpolation */