working on python interp

src/api/api_interp.cpp

@@ -38,6 +38,7 @@ Revision History:
 #include"iz3hash.h"
 #include"iz3pp.h"
 #include"iz3checker.h"
+#include"scoped_proof.h"
 
 using namespace stl_ext;
 
@@ -290,6 +291,85 @@ extern "C" {
     opts->map[name] = value;
   }
 
+  Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p){
+    Z3_TRY;
+    LOG_Z3_get_interpolant(c, pf, pat, p);
+    RESET_ERROR_CODE();
+
+    Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+    mk_c(c)->save_object(v);
+
+    ast *_pf = to_ast(pf);
+    ast *_pat = to_ast(pat);
+    
+    ptr_vector<ast> interp;
+    ptr_vector<ast> cnsts; // to throw away
+    
+    ast_manager &_m = mk_c(c)->m();
+
+    iz3interpolate(_m,
+		   _pf,
+		   cnsts,
+		   _pat,
+		   interp,
+		   (interpolation_options_struct *) 0 // ignore params for now
+		   );
+    
+    // copy result back
+    for(unsigned i = 0; i < interp.size(); i++){
+      v->m_ast_vector.push_back(interp[i]);
+      _m.dec_ref(interp[i]);
+    }
+    RETURN_Z3(of_ast_vector(v));
+    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_TRY;
+    LOG_Z3_compute_interpolant(c, pat, p, out_interp);
+    RESET_ERROR_CODE();
+
+
+    params_ref &_p = to_params(p)->m_params;
+    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);
+    
+    ptr_vector<ast> interp;
+    ptr_vector<ast> cnsts; // to throw away
+    
+    ast_manager &_m = mk_c(c)->m();
+
+    model_ref m;
+    lbool _status = iz3interpolate(_m,
+				   *(m_solver.get()),
+				   _pat,
+				   cnsts,
+				   interp,
+				   m,
+				   0 // ignore params for now
+				   );
+    
+    Z3_lbool status = of_lbool(_status);
+    
+    Z3_ast_vector_ref *v = 0;
+    if(_status == l_false){
+      // copy result back
+      v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+      mk_c(c)->save_object(v);
+      for(unsigned i = 0; i < interp.size(); i++){
+	v->m_ast_vector.push_back(interp[i]);
+	_m.dec_ref(interp[i]);
+      }
+    }
+    *out_interp = of_ast_vector(v);
+    
+    return status;
+    Z3_CATCH_RETURN(Z3_L_UNDEF);
+  }
 
 
 };

src/api/python/z3.py

@@ -7253,3 +7253,18 @@ 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 = main_ctx()
+     s = BoolSort(ctx)
+     a = s.cast(a)
+     return BoolRef(Z3_mk_interp(ctx.ref(), a.as_ast()), ctx)
+
+def tree_interpolant(f,p=None,ctx=None):
+    ctx = _get_ctx(ctx)
+    ptr = (ctypes.POINTER(AstVectorObj) * 1)()
+    if p == None:
+        p = ParamsRef(ctx)
+    res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr[0])
+    if res == Z3_L_FALSE:
+        return AstVector(ptr[0],ctx)
+    raise NoInterpolant()

src/api/python/z3types.py

@@ -109,3 +109,6 @@ class FuncEntryObj(ctypes.c_void_p):
 class RCFNumObj(ctypes.c_void_p):
   def __init__(self, e): self._as_parameter_ = e
   def from_param(obj): return obj
+
+class NoInterpolant():
+    def __init__(self):

src/api/z3_api.h

@@ -7699,6 +7699,105 @@ END_MLAPI_EXCLUDE
 
   Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg);
 
+  /** Compute an interpolant from a refutation. This takes a proof of
+      "false" from a set of formulas C, and an interpolation
+      pattern. The pattern pat is a formula combining the formulas in C
+      using logical conjunction and the "interp" operator (see
+      #Z3_mk_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. The
+      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.
+
+      In particular, calling Z3_get_interpolant on a pattern of the
+      form (interp ... (interp (and (interp A_1) A_2)) ... A_N) will
+      result in a sequence interpolant for A_1, A_2,... A_N. 
+
+      Neglecting interp markers, the pattern must be a conjunction of
+      formulas in C, the set of premises of the proof. Otherwise an
+      error is flagged.
+
+      Any premises of the proof not present in the pattern are
+      treated as "background theory". Predicate and function symbols
+      occurring in the background theory are treated as interpreted and
+      thus always allowed in the interpolant.
+
+      Interpolant may not necessarily be computable from all
+      proofs. To be sure an interpolant can be computed, the proof
+      must be generated by an SMT solver for which interpoaltion is
+      supported, and the premises must be expressed using only
+      theories and operators for which interpolation is supported.
+
+      Currently, the only SMT solver that is supported is the legacy
+      SMT solver. Such a solver is available as the default solver in
+      #Z3_context objects produced by #Z3_mk_interpolation_context.
+      Currently, the theories supported are equality with
+      uninterpreted functions, linear integer arithmetic, and the
+      theory of arrays (in SMT-LIB terms, this is AUFLIA).
+      Quantifiers are allowed. Use of any other operators (including
+      "labels") may result in failure to compute an interpolant from a
+      proof.
+
+      Parameters:
+
+      \param c logical context.
+      \param pf a refutation from premises (assertions) C
+      \param pat an interpolation pattern over C
+      \param p parameters
+
+       def_API('Z3_get_interpolant', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(PARAMS)))
+    */
+
+  Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p);
+
+  /* Compute an interpolant for an unsatisfiable conjunction of formulas.
+
+     This takes as an argument an interpolation pattern as in
+     #Z3_get_interpolant. This is a conjunction, some subformulas of
+     which are marked with the "interp" operator (see #Z3_mk_interp).
+     
+     The conjunction is first checked for unsatisfiability. The result
+     of this check is returned in the out parameter "status". If the result
+     is unsat, an interpolant is computed from the refutation as in #Z3_get_interpolant
+     and returned as a vector of formulas. Otherwise the return value is
+     an empty formula. 
+
+     See #Z3_get_interpolant for a discussion of supported theories.
+
+     The advantage of this function over #Z3_get_interpolant is that
+     it is not necessary to create a suitable SMT solver and generate
+     a proof. The disadvantage is that it is not possible to use the
+     solver incrementally.
+
+     Parameters:
+     
+     \param c logical context.
+     \param pat an interpolation pattern
+     \param p parameters
+     \param status returns the status of the sat check
+     
+     def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR)))
+  */
+  
+  Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *interp);
+
 
 /** Constant reprepresenting a root of a formula tree for tree interpolation */
 #define IZ3_ROOT SHRT_MAX

src/interp/iz3interp.cpp

@@ -41,6 +41,7 @@ Revision History:
 #include "iz3hash.h"
 #include "iz3interp.h"
 
+#include"scoped_proof.h"
 
 
 using namespace stl_ext;
@@ -503,6 +504,8 @@ lbool iz3interpolate(ast_manager &_m_manager,
   return res;
 }
 
+
+
 void interpolation_options_struct::apply(iz3base &b){
   for(stl_ext::hash_map<std::string,std::string>::iterator it = map.begin(), en = map.end();
       it != en;

src/interp/iz3interp.h

@@ -76,6 +76,7 @@ void iz3interpolate(ast_manager &_m_manager,
 		    ptr_vector<ast> &interps,
 		    interpolation_options_struct * options);
 
+
 /* Compute an interpolant from an ast representing an interpolation
    problem, if unsat, else return a model (if enabled). Uses the
    given solver to produce the proof/model. Also returns a vector
@@ -90,4 +91,5 @@ lbool iz3interpolate(ast_manager &_m_manager,
 		     model_ref &m,
 		     interpolation_options_struct * options);
 
+
 #endif