diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 2c88a1978..4ea0f5d77 100644 --- a/src/api/api_interp.cpp +++ b/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 interp; + ptr_vector 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 sf = mk_smt_solver_factory(); + scoped_ptr 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 interp; + ptr_vector 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); + } }; diff --git a/src/api/python/z3.py b/src/api/python/z3.py index ce53a4c1f..533a71956 100644 --- a/src/api/python/z3.py +++ b/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() diff --git a/src/api/python/z3types.py b/src/api/python/z3types.py index a26a958c0..56316eb46 100644 --- a/src/api/python/z3types.py +++ b/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): diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 94e20eceb..554c792e3 100644 --- a/src/api/z3_api.h +++ b/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 diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 1ae3e3a1b..0d394090f 100755 --- a/src/interp/iz3interp.cpp +++ b/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::iterator it = map.begin(), en = map.end(); it != en; diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h index 52aa716c3..1c6f9513e 100644 --- a/src/interp/iz3interp.h +++ b/src/interp/iz3interp.h @@ -76,6 +76,7 @@ void iz3interpolate(ast_manager &_m_manager, ptr_vector &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