From 81df4932fbc8563befd15775cc960ba906dde1a8 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 25 Oct 2013 18:40:26 -0700 Subject: [PATCH] added quantifiers in new interpolation --- src/api/api_interp.cpp | 4 ++ src/interp/iz3mgr.cpp | 90 ++++++++++++++++++++++++++++++ src/interp/iz3mgr.h | 19 +++++++ src/interp/iz3proof_itp.cpp | 15 +++++ src/interp/iz3proof_itp.h | 3 + src/interp/iz3translate.cpp | 3 +- src/interp/iz3translate_direct.cpp | 80 -------------------------- 7 files changed, 133 insertions(+), 81 deletions(-) diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 926493c6b..00503566e 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -407,6 +407,10 @@ extern "C" { cnsts_vec[i] = a; } Z3_ast tree = parents_vector_to_tree(ctx,num,cnsts,parents); + for(int i = 0; i < num_theory; i++){ + expr *a = to_expr(theory[i]); + cnsts_vec.push_back(a); + } iz3pp(mk_c(ctx)->m(),cnsts_vec,to_expr(tree),f); Z3_dec_ref(ctx,tree); } diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index 376e2a14f..1b91fd521 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -640,3 +640,93 @@ iz3mgr::ast iz3mgr::mk_idiv(const ast& t, const ast &d){ return mk_idiv(t,r); return make(Idiv,t,d); } + + +// does variable occur in expression? +int iz3mgr::occurs_in1(hash_map &occurs_in_memo,ast var, ast e){ + std::pair foo(e,false); + std::pair::iterator,bool> bar = occurs_in_memo.insert(foo); + bool &res = bar.first->second; + if(bar.second){ + if(e == var) res = true; + int nargs = num_args(e); + for(int i = 0; i < nargs; i++) + res |= occurs_in1(occurs_in_memo,var,arg(e,i)); + } + return res; +} + +int iz3mgr::occurs_in(ast var, ast e){ + hash_map memo; + return occurs_in1(memo,var,e); +} + + +// find a controlling equality for a given variable v in a term +// a controlling equality is of the form v = t, which, being +// false would force the formula to have the specifid truth value +// returns t, or null if no such + +iz3mgr::ast iz3mgr::cont_eq(hash_set &cont_eq_memo, bool truth, ast v, ast e){ + if(is_not(e)) return cont_eq(cont_eq_memo, !truth,v,arg(e,0)); + if(cont_eq_memo.find(e) != cont_eq_memo.end()) + return ast(); + cont_eq_memo.insert(e); + if(!truth && op(e) == Equal){ + if(arg(e,0) == v) return(arg(e,1)); + if(arg(e,1) == v) return(arg(e,0)); + } + if((!truth && op(e) == And) || (truth && op(e) == Or)){ + int nargs = num_args(e); + for(int i = 0; i < nargs; i++){ + ast res = cont_eq(cont_eq_memo, truth, v, arg(e,i)); + if(!res.null()) return res; + } + } + if(truth && op(e) == Implies){ + ast res = cont_eq(cont_eq_memo, !truth, v, arg(e,0)); + if(!res.null()) return res; + res = cont_eq(cont_eq_memo, truth, v, arg(e,1)); + if(!res.null()) return res; + } + return ast(); +} + + // substitute a term t for unbound occurrences of variable v in e + +iz3mgr::ast iz3mgr::subst(hash_map &subst_memo, ast var, ast t, ast e){ + if(e == var) return t; + std::pair foo(e,ast()); + std::pair::iterator,bool> bar = subst_memo.insert(foo); + ast &res = bar.first->second; + if(bar.second){ + int nargs = num_args(e); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = subst(subst_memo,var,t,arg(e,i)); + opr f = op(e); + if(f == Equal && args[0] == args[1]) res = mk_true(); + else res = clone(e,args); + } + return res; +} + +iz3mgr::ast iz3mgr::subst(ast var, ast t, ast e){ + hash_map memo; + return subst(memo,var,t,e); +} + + // apply a quantifier to a formula, with some optimizations + // 1) bound variable does not occur -> no quantifier + // 2) bound variable must be equal to some term -> substitute + +iz3mgr::ast iz3mgr::apply_quant(opr quantifier, ast var, ast e){ + if(!occurs_in(var,e))return e; + hash_set cont_eq_memo; + ast cterm = cont_eq(cont_eq_memo, quantifier == Forall, var, e); + if(!cterm.null()){ + return subst(var,cterm,e); + } + std::vector bvs; bvs.push_back(var); + return make_quant(quantifier,bvs,e); +} diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index dc5af9e26..a648c3f84 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -612,6 +612,20 @@ class iz3mgr { z3pf conc(const z3pf &t){return arg(t,num_prems(t));} + + /* quantifier handling */ + + // substitute a term t for unbound occurrences of variable v in e + + ast subst(ast var, ast t, ast e); + + // apply a quantifier to a formula, with some optimizations + // 1) bound variable does not occur -> no quantifier + // 2) bound variable must be equal to some term -> substitute + + ast apply_quant(opr quantifier, ast var, ast e); + + /** For debugging */ void show(ast); @@ -662,6 +676,11 @@ class iz3mgr { ast mki(family_id fid, decl_kind sk, int n, raw_ast **args); ast make(opr op, int n, raw_ast **args); ast make(symb sym, int n, raw_ast **args); + int occurs_in1(stl_ext::hash_map &occurs_in_memo, ast var, ast e); + int occurs_in(ast var, ast e); + ast cont_eq(stl_ext::hash_set &cont_eq_memo, bool truth, ast v, ast e); + ast subst(stl_ext::hash_map &subst_memo, ast var, ast t, ast e); + family_id m_basic_fid; family_id m_array_fid; diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 41237200c..d786f95ab 100644 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -2056,11 +2056,26 @@ class iz3proof_itp_impl : public iz3proof_itp { return new_var; } + ast add_quants(ast e){ + for(int i = localization_vars.size() - 1; i >= 0; i--){ + LocVar &lv = localization_vars[i]; + opr quantifier = (pv->in_range(lv.frame,rng)) ? Exists : Forall; + e = apply_quant(quantifier,lv.var,e); + } + return e; + } + node make_resolution(ast pivot, node premise1, node premise2) { std::vector lits; return make_resolution(pivot,lits,premise1,premise2); } + /* Return an interpolant from a proof of false */ + ast interpolate(const node &pf){ + // proof of false must be a formula, with quantified symbols + return add_quants(pf); + } + ast resolve_with_quantifier(const ast &pivot1, const ast &conj1, const ast &pivot2, const ast &conj2){ if(is_not(arg(pivot1,1))) diff --git a/src/interp/iz3proof_itp.h b/src/interp/iz3proof_itp.h index 1d5579b75..299f391ea 100644 --- a/src/interp/iz3proof_itp.h +++ b/src/interp/iz3proof_itp.h @@ -118,6 +118,9 @@ class iz3proof_itp : public iz3mgr { is an affine term divisble by d and c is an integer constant */ virtual node make_cut_rule(const ast &tleqc, const ast &d, const ast &con, const ast &prem) = 0; + /* Return an interpolant from a proof of false */ + virtual ast interpolate(const node &pf) = 0; + /** Create proof object to construct an interpolant. */ static iz3proof_itp *create(prover *p, const prover::range &r, bool _weak); diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index a41fdcba9..2be7c22e5 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1141,7 +1141,8 @@ public: std::vector itps; for(int i = 0; i < frames -1; i++){ iproof = iz3proof_itp::create(this,range_downward(i),weak_mode()); - ast itp = translate_main(proof); + Iproof::node ipf = translate_main(proof); + ast itp = iproof->interpolate(ipf); itps.push_back(itp); delete iproof; clear_translation(); diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index 7a6238201..037cabee9 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -219,11 +219,8 @@ public: AstToAst localization_map; // maps terms to their localization vars typedef hash_map AstToBool; - AstToBool occurs_in_memo; // memo of occurs_in function - AstHashSet cont_eq_memo; // memo of cont_eq function - AstToAst subst_memo; // memo of subst function iz3secondary *secondary; // the secondary prover @@ -613,83 +610,6 @@ public: } } - // does variable occur in expression? - int occurs_in1(ast var, ast e){ - std::pair foo(e,false); - std::pair bar = occurs_in_memo.insert(foo); - bool &res = bar.first->second; - if(bar.second){ - if(e == var) res = true; - int nargs = num_args(e); - for(int i = 0; i < nargs; i++) - res |= occurs_in1(var,arg(e,i)); - } - return res; - } - - int occurs_in(ast var, ast e){ - occurs_in_memo.clear(); - return occurs_in1(var,e); - } - - // find a controlling equality for a given variable v in a term - // a controlling equality is of the form v = t, which, being - // false would force the formula to have the specifid truth value - // returns t, or null if no such - - ast cont_eq(bool truth, ast v, ast e){ - if(is_not(e)) return cont_eq(!truth,v,arg(e,0)); - if(cont_eq_memo.find(e) != cont_eq_memo.end()) - return ast(); - cont_eq_memo.insert(e); - if(!truth && op(e) == Equal){ - if(arg(e,0) == v) return(arg(e,1)); - if(arg(e,1) == v) return(arg(e,0)); - } - if((!truth && op(e) == And) || (truth && op(e) == Or)){ - int nargs = num_args(e); - for(int i = 0; i < nargs; i++){ - ast res = cont_eq(truth, v, arg(e,i)); - if(!res.null()) return res; - } - } - return ast(); - } - - // substitute a term t for unbound occurrences of variable v in e - - ast subst(ast var, ast t, ast e){ - if(e == var) return t; - std::pair foo(e,ast()); - std::pair bar = subst_memo.insert(foo); - ast &res = bar.first->second; - if(bar.second){ - int nargs = num_args(e); - std::vector args(nargs); - for(int i = 0; i < nargs; i++) - args[i] = subst(var,t,arg(e,i)); - opr f = op(e); - if(f == Equal && args[0] == args[1]) res = mk_true(); - else res = clone(e,args); - } - return res; - } - - // apply a quantifier to a formula, with some optimizations - // 1) bound variable does not occur -> no quantifier - // 2) bound variable must be equal to some term -> substitute - - ast apply_quant(opr quantifier, ast var, ast e){ - if(!occurs_in(var,e))return e; - cont_eq_memo.clear(); - ast cterm = cont_eq(quantifier == Forall, var, e); - if(!cterm.null()){ - subst_memo.clear(); - return subst(var,cterm,e); - } - std::vector bvs; bvs.push_back(var); - return make_quant(quantifier,bvs,e); - } // add quantifiers over the localization vars // to an interpolant for frames lo-hi