From 2c9c5ba1f0f44e0b07efbe58042d77b1d2276443 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sun, 15 Sep 2013 13:33:20 -0700 Subject: [PATCH] still working on interpolation of full z3 proofs --- scripts/mk_util.py | 1 + src/interp/iz3foci.cpp | 4 + src/interp/iz3mgr.cpp | 9 +- src/interp/iz3mgr.h | 29 +- src/interp/iz3proof_itp.cpp | 610 +++++++++++++++++++++++++++++------- src/interp/iz3proof_itp.h | 6 +- src/interp/iz3translate.cpp | 18 +- src/interp/iz3translate.h | 5 +- 8 files changed, 547 insertions(+), 135 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 4a042d37f..79c1877ff 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1496,6 +1496,7 @@ def mk_config(): if test_foci2(CXX,FOCI2LIB): LDFLAGS = '%s %s' % (LDFLAGS,FOCI2LIB) SLIBEXTRAFLAGS = '%s %s' % (SLIBEXTRAFLAGS,FOCI2LIB) + CPPFLAGS = '%s -D_FOCI2' % CPPFLAGS else: print "FAILED\n" FOCI2 = False diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp index 251599041..85e090c5b 100755 --- a/src/interp/iz3foci.cpp +++ b/src/interp/iz3foci.cpp @@ -308,7 +308,11 @@ public: int interpolate(const std::vector &cnsts, std::vector &itps){ assert((int)cnsts.size() == frames); std::string lia("lia"); +#ifdef _FOCI2 foci = foci2::create(lia); +#else + foci = 0; +#endif if(!foci){ std::cerr << "iZ3: cannot find foci lia solver.\n"; assert(0); diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index 7a787fdea..0cff3b970 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -494,6 +494,12 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& rats){ } rats[i-2] = r; } + if(rats.size() != 0 && rats[0].is_neg()){ + for(unsigned i = 0; i < rats.size(); i++){ + assert(rats[i].is_neg()); + rats[i] = -rats[i]; + } + } extract_lcd(rats); } @@ -519,11 +525,10 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector& r { ast con = arg(conc(proof),i-1); ast temp = make_real(r); // for debugging -#if 0 opr o = is_not(con) ? op(arg(con,0)) : op(con); if(is_not(con) ? (o == Leq || o == Lt) : (o == Geq || o == Gt)) -#endif r = -r; + r = -r; } rats[i-1] = r; } diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 83cd573f3..e49182073 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -460,6 +460,17 @@ class iz3mgr { return make(Or,x,y); } + ast mk_implies(ast x, ast y){ + opr ox = op(x); + opr oy = op(y); + if(ox == True) return y; + if(oy == False) return mk_not(x); + if(ox == False) return mk_true(); + if(oy == True) return y; + if(x == y) return mk_true(); + return make(Implies,x,y); + } + ast mk_or(const std::vector &x){ ast res = mk_false(); for(unsigned i = 0; i < x.size(); i++) @@ -468,10 +479,20 @@ class iz3mgr { } ast mk_and(const std::vector &x){ - ast res = mk_true(); - for(unsigned i = 0; i < x.size(); i++) - res = mk_and(res,x[i]); - return res; + std::vector conjs; + for(unsigned i = 0; i < x.size(); i++){ + const ast &e = x[i]; + opr o = op(e); + if(o == False) + return mk_false(); + if(o != True) + conjs.push_back(e); + } + if(conjs.size() == 0) + return mk_true(); + if(conjs.size() == 1) + return conjs[0]; + return make(And,conjs); } ast mk_equal(ast x, ast y){ diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 5cd75bc26..a4b742d7d 100644 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -33,7 +33,60 @@ class iz3proof_itp_impl : public iz3proof_itp { enum LitType {LitA,LitB,LitMixed}; hash_map placeholders; - symb farkas; + + // These symbols represent deduction rules + + /* This symbol represents a proof by contradiction. That is, + contra(p,l1 /\ ... /\ lk) takes a proof p of + + l1,...,lk |- false + + and returns a proof of + + |- ~l1,...,~l2 + */ + symb contra; + + /* The summation rule. The term sum(p,c,i) takes a proof p of an + inequality i', an integer coefficient c and an inequality i, and + yieds a proof of i' + ci. */ + symb sum; + + /* Proof rotation. The proof term rotate(q,p) takes a + proof p of: + + Gamma, q |- false + + and yields a proof of: + + Gamma |- ~q + */ + symb rotate_sum; + + /* Inequalities to equality. leq2eq(p, q, r) takes a proof + p of ~x=y, a proof q of x <= y and a proof r of y <= x + and yields a proof of false. */ + symb leq2eq; + + /* Proof term cong(p,q) takes a proof p of x=y and a proof + q of t != t and returns a proof of false. */ + symb cong; + + + /* Excluded middle. exmid(phi,p,q) takes a proof p of phi and a + proof q of ~\phi and returns a proof of false. */ + symb exmid; + + /* Symmetry. symm(p) takes a proof p of x=y and produces + a proof of y=x. */ + symb symm; + + /* Modus ponens. modpon(p,e,q) takes proofs p of P, e of P=Q + and q of ~Q and returns a proof of false. */ + symb modpon; + + // This is used to represent an infinitessimal value + ast epsilon; ast get_placeholder(ast t){ hash_map::iterator it = placeholders.find(t); @@ -49,8 +102,17 @@ class iz3proof_itp_impl : public iz3proof_itp { return res; } - ast make_farkas(ast &coeff, ast &ineq){ - return make(farkas,coeff,ineq); + ast make_contra_node(const ast &pf, const std::vector &lits){ + if(lits.size() == 0) + return pf; + std::vector reslits; + reslits.push_back(make(contra,pf,mk_false())); + for(unsigned i = 0; i < lits.size(); i++){ + ast bar = make(rotate_sum,lits[i],pf); + ast foo = make(contra,bar,lits[i]); + reslits.push_back(foo); + } + return make(And,reslits); } LitType get_term_type(const ast &lit){ @@ -81,24 +143,10 @@ class iz3proof_itp_impl : public iz3proof_itp { /* the mixed case is a bit complicated */ - ast atom = get_lit_atom(pivot); - switch(op(atom)){ - case Equal: - return resolve_equality(pivot,conc,premise1,premise2); - case Leq: - case Geq: - case Lt: - case Gt: - return resolve_arith(pivot,conc,premise1,premise2); - break; - default:; - } - - /* we can resolve on mixed equality and inequality literals, - but nothing else. */ - throw proof_error(); + return resolve_arith(pivot,conc,premise1,premise2); } +#if 0 /* Handles the case of resolution on a mixed equality atom. */ ast resolve_equality(const ast &pivot, const std::vector &conc, node premise1, node premise2){ @@ -134,7 +182,8 @@ class iz3proof_itp_impl : public iz3proof_itp { else { switch(op(premise1)){ case Or: - case And: { + case And: + case Implies: { unsigned nargs = num_args(premise1); std::vector args; args.resize(nargs); for(unsigned i = 0; i < nargs; i++) @@ -149,6 +198,7 @@ class iz3proof_itp_impl : public iz3proof_itp { } return res; } +#endif /* Handles the case of resolution on a mixed arith atom. */ @@ -161,15 +211,21 @@ class iz3proof_itp_impl : public iz3proof_itp { return resolve_arith_rec1(memo, neg_pivot_lit, premise1, premise2); } - void collect_farkas_resolvents(const ast &pivot, const ast &coeff, const ast &conj, std::vector &res){ - int nargs = num_args(conj); - for(int i = 1; i < nargs; i++){ - ast f = arg(conj,i); - if(!(f == pivot)){ - ast newf = make(farkas,make(Times,arg(f,0),coeff),arg(f,1)); - res.push_back(newf); - } + + ast apply_coeff(const ast &coeff, const ast &t){ +#if 0 + rational r; + if(!is_integer(coeff,r)) + throw "ack!"; + ast n = make_int(r.numerator()); + ast res = make(Times,n,t); + if(!r.is_int()) { + ast d = make_int(r.numerator()); + res = mk_idiv(res,d); } + return res; +#endif + return make(Times,coeff,t); } ast sum_ineq(const ast &coeff1, const ast &ineq1, const ast &coeff2, const ast &ineq2){ @@ -178,29 +234,63 @@ class iz3proof_itp_impl : public iz3proof_itp { sum_op = Lt; ast sum_sides[2]; for(int i = 0; i < 2; i++){ - sum_sides[i] = make(Plus,make(Times,coeff1,arg(ineq1,i)),make(Times,coeff2,arg(ineq2,i))); + sum_sides[i] = make(Plus,apply_coeff(coeff1,arg(ineq1,i)),apply_coeff(coeff2,arg(ineq2,i))); sum_sides[i] = z3_simplify(sum_sides[i]); } return make(sum_op,sum_sides[0],sum_sides[1]); } - - ast resolve_farkas(const ast &pivot1, const ast &conj1, const ast &pivot2, const ast &conj2){ +#if 0 + ast resolve_farkas(const ast &pivot1, const ast &conj1, const ast &implicant1, + const ast &pivot2, const ast &conj2, const ast &implicant2){ std::vector resolvent; ast coeff1 = get_farkas_coeff(pivot1); ast coeff2 = get_farkas_coeff(pivot2); - resolvent.push_back(sum_ineq(coeff2,arg(conj1,0),coeff1,arg(conj2,0))); + ast s1 = resolve_arith_placeholders(pivot2,conj2,arg(conj1,0)); + ast s2 = resolve_arith_placeholders(pivot1,conj1,arg(conj2,0)); + resolvent.push_back(sum_ineq(coeff2,s1,coeff1,s2)); collect_farkas_resolvents(pivot1,coeff2,conj1,resolvent); collect_farkas_resolvents(pivot2,coeff1,conj2,resolvent); + ast res = make(And,resolvent); + if(implicant1.null() && implicant2.null()) + return res; + ast i1 = implicant1.null() ? mk_false() : resolve_arith_placeholders(pivot2,conj2,implicant1); + ast i2 = implicant2.null() ? mk_false() : resolve_arith_placeholders(pivot1,conj1,implicant2); + return make(Implies,res,my_or(i1,i2)); + } +#endif + + void collect_contra_resolvents(int from, const ast &pivot1, const ast &pivot, const ast &conj, std::vector &res){ + int nargs = num_args(conj); + for(int i = from; i < nargs; i++){ + ast f = arg(conj,i); + if(!(f == pivot)){ + ast ph = get_placeholder(mk_not(arg(pivot1,1))); + ast pf = arg(pivot1,0); + ast thing = subst_term_and_simp(ph,pf,arg(f,0)); + ast newf = make(contra,thing,arg(f,1)); + res.push_back(newf); + } + } + } + + ast resolve_contra(const ast &pivot1, const ast &conj1, + const ast &pivot2, const ast &conj2){ + std::vector resolvent; + collect_contra_resolvents(0,pivot1,pivot2,conj2,resolvent); + collect_contra_resolvents(1,pivot2,pivot1,conj1,resolvent); + if(resolvent.size() == 1) // we have proved a contradiction + return simplify(arg(resolvent[0],0)); // this is the proof -- get interpolant return make(And,resolvent); } + - bool is_farkas_itp(const ast &pivot1, const ast &itp2, ast &pivot2){ + bool is_contra_itp(const ast &pivot1, ast itp2, ast &pivot2){ if(op(itp2) == And){ int nargs = num_args(itp2); for(int i = 1; i < nargs; i++){ ast foo = arg(itp2,i); - if(op(foo) == Uninterpreted && sym(foo) == farkas){ + if(op(foo) == Uninterpreted && sym(foo) == contra){ if(arg(foo,1) == pivot1){ pivot2 = foo; return true; @@ -218,12 +308,13 @@ class iz3proof_itp_impl : public iz3proof_itp { return res; ast pivot2; - if(is_farkas_itp(mk_not(arg(pivot1,1)),itp2,pivot2)) - res = resolve_farkas(pivot1,conj1,pivot2,itp2); + if(is_contra_itp(mk_not(arg(pivot1,1)),itp2,pivot2)) + res = resolve_contra(pivot1,conj1,pivot2,itp2); else { switch(op(itp2)){ case Or: - case And: { + case And: + case Implies: { unsigned nargs = num_args(itp2); std::vector args; args.resize(nargs); for(unsigned i = 0; i < nargs; i++) @@ -244,15 +335,15 @@ class iz3proof_itp_impl : public iz3proof_itp { if(!res.null()) return res; ast pivot1; - if(is_farkas_itp(neg_pivot_lit,itp1,pivot1)){ + if(is_contra_itp(neg_pivot_lit,itp1,pivot1)){ hash_map memo2; res = resolve_arith_rec2(memo2,pivot1,itp1,itp2); - res = resolve_arith_placeholders(pivot1,itp1,res); } else { switch(op(itp1)){ case Or: - case And: { + case And: + case Implies: { unsigned nargs = num_args(itp1); std::vector args; args.resize(nargs); for(unsigned i = 0; i < nargs; i++) @@ -268,21 +359,26 @@ class iz3proof_itp_impl : public iz3proof_itp { return res; } +#if 0 ast resolve_arith_placeholders(const ast &pivot1, const ast &conj1, const ast &itp2){ ast coeff = arg(pivot1,0); + ast val = arg(arg(conj1,0),1); + if(op(conj1)==Lt) + val = make(Sub,val,epsilon); // represent x < c by x <= c - epsilon coeff = z3_simplify(coeff); - ast soln = mk_idiv(arg(arg(conj1,0),1),coeff); + ast soln = mk_idiv(val,coeff); int nargs = num_args(conj1); for(int i = 1; i < nargs; i++){ ast c = arg(conj1,i); if(!(c == pivot1)){ - soln = make(Plus,soln,get_placeholder(mk_not(c))); + soln = make(Plus,soln,get_placeholder(arg(c,1))); } } ast pl = get_placeholder(mk_not(arg(pivot1,1))); ast res = subst_term_and_simp(pl,soln,itp2); return res; } +#endif hash_map subst_memo; // memo of subst function @@ -311,6 +407,197 @@ class iz3proof_itp_impl : public iz3proof_itp { return res; } + /* This is where the real work happens. Here, we simplify the + proof obtained by cut elimination, obtaining a interpolant. */ + + struct cannot_simplify {}; + hash_map simplify_memo; + + ast simplify(const ast &t){ + return simplify_rec(t); + } + + ast simplify_rec(const ast &e){ + std::pair foo(e,ast()); + std::pair::iterator,bool> bar = simplify_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] = simplify_rec(arg(e,i)); + try { + opr f = op(e); + if(f == Equal && args[0] == args[1]) res = mk_true(); + else if(f == And) res = my_and(args); + else if(f == Or) res = my_or(args); + else if(f == Idiv) res = mk_idiv(args[0],args[1]); + else if(f == Uninterpreted){ + symb g = sym(e); + if(g == rotate_sum) res = simplify_rotate(args); + else if(g == symm) res = simplify_symm(args); + else if(g == modpon) res = simplify_modpon(args); +#if 0 + else if(g == cong) res = simplify_cong(args); + else if(g == modpon) res = simplify_modpon(args); + else if(g == leq2eq) res = simplify_leq2eq(args); + else if(g == eq2leq) res = simplify_eq2leq(args); +#endif + else res = clone(e,args); + } + else res = clone(e,args); + } + catch (const cannot_simplify &){ + res = clone(e,args); + } + } + return res; + } + + + ast simplify_rotate(const std::vector &args){ + const ast &pf = args[1]; + ast pl = get_placeholder(args[0]); + if(op(pf) == Uninterpreted){ + symb g = sym(pf); + if(g == sum) return simplify_rotate_sum(pl,pf); + if(g == leq2eq) return simplify_rotate_leq2eq(pl,args[0],pf); + if(g == cong) return simplify_rotate_cong(pl,args[0],pf); + // if(g == symm) return simplify_rotate_symm(pl,args[0],pf); + } + throw cannot_simplify(); + } + + ast simplify_rotate_sum(const ast &pl, const ast &pf){ + ast cond = mk_true(); + ast ineq = make(Leq,make_int("0"),make_int("0")); + rotate_sum_rec(pl,pf,cond,ineq); + return ineq; + } + + void sum_cond_ineq(ast &ineq, ast &cond, const ast &coeff2, const ast &ineq2){ + opr o = op(ineq2); + if(o == Implies){ + sum_cond_ineq(ineq,cond,coeff2,arg(ineq2,1)); + cond = my_and(cond,arg(ineq2,0)); + } + else if(o == Leq || o == Lt) + ineq = sum_ineq(make_int("1"),ineq,coeff2,ineq2); + else + throw cannot_simplify(); + } + + // divide both sides of inequality by a non-negative integer divisor + ast idiv_ineq(const ast &ineq, const ast &divisor){ + return make(op(ineq),mk_idiv(arg(ineq,0),divisor),mk_idiv(arg(ineq,1),divisor)); + } + + ast rotate_sum_rec(const ast &pl, const ast &pf, ast &cond, ast &ineq){ + if(op(pf) == Uninterpreted && sym(pf) == sum){ + if(arg(pf,2) == pl){ + sum_cond_ineq(ineq,cond,make_int("1"),arg(pf,0)); + ineq = idiv_ineq(ineq,arg(pf,1)); + return my_implies(cond,ineq); + } + sum_cond_ineq(ineq,cond,arg(pf,1),arg(pf,2)); + return rotate_sum_rec(pl,arg(pf,0),cond,ineq); + } + throw cannot_simplify(); + } + + ast simplify_rotate_leq2eq(const ast &pl, const ast &neg_equality, const ast &pf){ + if(pl == arg(pf,0)){ + ast equality = arg(neg_equality,0); + ast x = arg(equality,0); + ast y = arg(equality,1); + ast xleqy = arg(pf,1); + ast yleqx = arg(pf,2); + ast itpeq; + if(get_term_type(x) == LitA) + itpeq = make(Equal,x,make(Plus,x,get_ineq_rhs(xleqy))); + else if(get_term_type(y) == LitA) + itpeq = make(Equal,make(Plus,y,get_ineq_rhs(yleqx)),y); + else + throw cannot_simplify(); + ast cond = mk_true(); + ast ineq = make(Leq,make_int("0"),make_int("0")); + sum_cond_ineq(ineq,cond,make_int("-1"),xleqy); + sum_cond_ineq(ineq,cond,make_int("-1"),yleqx); + cond = my_and(cond,ineq); + return my_implies(cond,itpeq); + } + throw cannot_simplify(); + } + + ast get_ineq_rhs(const ast &ineq2){ + opr o = op(ineq2); + if(o == Implies) + return get_ineq_rhs(arg(ineq2,1)); + else if(o == Leq || o == Lt) + return arg(ineq2,1); + throw cannot_simplify(); + } + + ast simplify_rotate_cong(const ast &pl, const ast &neg_equality, const ast &pf){ + if(pl == arg(pf,2)){ + if(op(arg(pf,0)) == True) + return mk_true(); + rational pos; + if(is_numeral(arg(pf,1),pos)){ + int ipos = pos.get_unsigned(); + ast cond = mk_true(); + ast equa = sep_cond(arg(pf,0),cond); + if(op(equa) == Equal){ + ast pe = mk_not(neg_equality); + ast lhs = subst_in_arg_pos(ipos,arg(equa,0),arg(pe,0)); + ast rhs = subst_in_arg_pos(ipos,arg(equa,1),arg(pe,1)); + ast res = make(Equal,lhs,rhs); + return my_implies(cond,res); + } + } + } + throw cannot_simplify(); + } + + ast simplify_symm(const std::vector &args){ + if(op(args[0]) == True) + return mk_true(); + ast cond = mk_true(); + ast equa = sep_cond(args[0],cond); + if(op(equa) == Equal) + return my_implies(cond,make(Equal,arg(equa,1),arg(equa,0))); + throw cannot_simplify(); + } + + ast simplify_modpon(const std::vector &args){ + if(op(args[1]) == True){ + ast cond = mk_true(); + ast P = sep_cond(args[0],cond); + ast notQ = sep_cond(args[2],cond); + ast Q = mk_not(notQ); + ast d = mk_not(delta(P,Q)); + return my_implies(cond,d); + } + throw cannot_simplify(); + } + + ast delta(const ast &x, const ast &y){ + if(op(x) != op(y) || (op(x) == Uninterpreted && sym(x) != sym(y)) || num_args(x) != num_args(y)) + return make(Equal,x,y); + ast res = mk_true(); + int nargs = num_args(x); + for(int i = 0; i < nargs; i++) + res = my_and(res,delta(arg(x,i),arg(y,i))); + return res; + } + + ast sep_cond(const ast &t, ast &cond){ + if(op(t) == Implies){ + cond = my_and(cond,arg(t,0)); + return arg(t,1); + } + return t; + } /** Make an assumption node. The given clause is assumed in the given frame. */ virtual node make_assumption(int frame, const std::vector &assumption){ @@ -327,39 +614,76 @@ class iz3proof_itp_impl : public iz3proof_itp { } } - /** Make a modus-ponens node. This takes derivations of |- x - and |- x = y and produces |- y */ - - virtual node make_mp(const ast &p, const ast &q, const ast &prem1, const ast &prem2){ - - /* Interpolate the axiom p, p=q -> q */ - ast itp; - if(get_term_type(p) == LitA){ - if(get_term_type(q) == LitA) - itp = mk_false(); - else { - if(get_term_type(make(Equal,p,q)) == LitA) - itp = q; - else - itp = get_placeholder(make(Equal,p,q)); + ast triv_interp(const symb &rule, const std::vector &premises){ + std::vector ps; ps.resize(premises.size()); + std::vector conjs; + for(unsigned i = 0; i < ps.size(); i++){ + ast p = premises[i]; + switch(get_term_type(p)){ + case LitA: + ps[i] = p; + break; + case LitB: + ps[i] = mk_true(); + break; + default: + ps[i] = get_placeholder(p); + conjs.push_back(p); } } + ast ref = make(rule,ps); + ast res = make_contra_node(ref,conjs); + return res; + } + + ast triv_interp(const symb &rule, const ast &p0, const ast &p1, const ast &p2){ + std::vector ps; ps.resize(3); + ps[0] = p0; + ps[1] = p1; + ps[2] = p2; + return triv_interp(rule,ps); + } + + /** Make a modus-ponens node. This takes derivations of |- x + and |- x = y and produces |- y */ + + virtual node make_mp(const ast &p_eq_q, const ast &prem1, const ast &prem2){ + + /* Interpolate the axiom p, p=q -> q */ + ast p = arg(p_eq_q,0); + ast q = arg(p_eq_q,1); + ast itp; + if(get_term_type(p_eq_q) == LitMixed){ + itp = triv_interp(modpon,p,p_eq_q,mk_not(q)); + } else { - if(get_term_type(q) == LitA){ - if(get_term_type(make(Equal,p,q)) == LitA) - itp = mk_not(p); - else - itp = mk_not(get_placeholder(make(Equal,p,q))); + if(get_term_type(p) == LitA){ + if(get_term_type(q) == LitA) + itp = mk_false(); + else { + if(get_term_type(p_eq_q) == LitA) + itp = q; + else + throw proof_error(); + } + } + else { + if(get_term_type(q) == LitA){ + if(get_term_type(make(Equal,p,q)) == LitA) + itp = mk_not(p); + else + throw proof_error(); } else itp = mk_true(); + } } /* Resolve it with the premises */ std::vector conc; conc.push_back(q); conc.push_back(mk_not(make(Equal,p,q))); itp = make_resolution(p,conc,itp,prem1); conc.pop_back(); - itp = make_resolution(make(Equal,p,q),conc,itp,prem2); + itp = make_resolution(p_eq_q,conc,itp,prem2); return itp; } @@ -387,26 +711,25 @@ class iz3proof_itp_impl : public iz3proof_itp { return mk_true(); default: // mixed hypothesis switch(op(P)){ - case Equal: - { - ast x = arg(P,0); - ast y = arg(P,1); - ast A_term = (get_term_type(y) == LitA) ? y : x; - ast res = make(And,make(Equal,A_term,get_placeholder(P)),mk_not(P)); - return res; - } case Geq: case Leq: case Gt: case Lt: { ast zleqz = make(Leq,make_int("0"),make_int("0")); - ast fark1 = make(farkas,make_int("1"),P); - ast fark2 = make(farkas,make_int("1"),mk_not(P)); - ast res = make(And,zleqz,fark1,fark2); + ast fark1 = make(sum,zleqz,make_int("1"),get_placeholder(P)); + ast fark2 = make(sum,fark1,make_int("1"),get_placeholder(mk_not(P))); + ast res = make(And,make(contra,fark2,mk_false()), + make(contra,get_placeholder(mk_not(P)),P), + make(contra,get_placeholder(P),mk_not(P))); + return res; + } + default: { + ast em = make(exmid,P,get_placeholder(P),get_placeholder(mk_not(P))); + ast res = make(And,make(contra,em,mk_false()), + make(contra,get_placeholder(mk_not(P)),P), + make(contra,get_placeholder(P),mk_not(P))); return res; } - default: - throw proof_error(); } } } @@ -420,20 +743,31 @@ class iz3proof_itp_impl : public iz3proof_itp { /** Make a Symmetry node. This takes a derivation of |- x = y and produces | y = x */ - virtual node make_symmetry(ast con, node prem){ + virtual node make_symmetry(ast con, const ast &premcon, node prem){ ast x = arg(con,0); ast y = arg(con,1); - ast p = make(Equal,y,x); + ast p = make(op(con),y,x); + if(p == premcon) + std::cout << "ok\n"; + if(get_term_type(con) != LitMixed) + return prem; // symmetry shmymmetry... +#if 0 LitType xt = get_term_type(x); LitType yt = get_term_type(y); ast A_term; + if(xt == LitA && yt == LitB) A_term = x; else if(yt == LitA && xt == LitB) A_term = y; else - return prem; // symmetry shmymmetry... ast itp = make(And,make(Equal,A_term,get_placeholder(p)),mk_not(con)); +#endif + ast em = make(exmid,con,make(symm,get_placeholder(p)),get_placeholder(mk_not(con))); + ast itp = make(And,make(contra,em,mk_false()), + make(contra,make(symm,get_placeholder(mk_not(con))),p), + make(contra,make(symm,get_placeholder(p)),mk_not(con))); + std::vector conc; conc.push_back(con); itp = make_resolution(p,conc,itp,prem); return itp; @@ -448,7 +782,13 @@ class iz3proof_itp_impl : public iz3proof_itp { ast p = make(Equal,x,y); ast q = make(Equal,y,z); ast r = make(Equal,x,z); + ast equiv = make(Iff,p,r); ast itp; + + itp = make_congruence(q,equiv,prem2); + itp = make_mp(equiv,prem1,itp); + +#if 0 if(get_term_type(p) == LitA){ if(get_term_type(q) == LitA){ if(get_term_type(r) == LitA) @@ -506,21 +846,24 @@ class iz3proof_itp_impl : public iz3proof_itp { itp = make_resolution(p,conc,itp,prem1); conc.pop_back(); itp = make_resolution(q,conc,itp,prem2); +#endif + + return itp; - + } /** Make a congruence node. This takes derivations of |- x_i = y_i and produces |- f(x_1,...,x_n) = f(y_1,...,y_n) */ - virtual node make_congruence(const ast &x, const ast &y, const ast &con, const std::vector &hyps, const ast &prem1){ - ast p = make(Equal,x,y); + virtual node make_congruence(const ast &p, const ast &con, const ast &prem1){ + ast x = arg(p,0), y = arg(p,1); ast itp; if(get_term_type(p) == LitA){ if(get_term_type(con) == LitA) itp = mk_false(); else - throw proof_error(); // itp = p; + itp = make_mixed_congruence(x, y, p, con, prem1); } else { if(get_term_type(con) == LitA) @@ -529,7 +872,7 @@ class iz3proof_itp_impl : public iz3proof_itp { if(get_term_type(con) == LitB) itp = mk_true(); else - itp = make_mixed_congruence(x, y, con, hyps, prem1); + itp = make_mixed_congruence(x, y, p, con, prem1); } } std::vector conc; conc.push_back(con); @@ -539,14 +882,19 @@ class iz3proof_itp_impl : public iz3proof_itp { /* Interpolate a mixed congruence axiom. */ - virtual ast make_mixed_congruence(const ast &x, const ast &y, const ast &con, const std::vector &hyps, const ast &prem1){ - ast A_term = x; - ast f_A_term = arg(con,0); - if(get_term_type(y) == LitA){ - A_term = y; - f_A_term = arg(con,1); + virtual ast make_mixed_congruence(const ast &x, const ast &y, const ast &p, const ast &con, const ast &prem1){ + ast foo = p; + std::vector conjs; + switch(get_term_type(foo)){ + case LitA: + break; + case LitB: + foo = mk_true(); + break; + case LitMixed: + conjs.push_back(foo); + foo = get_placeholder(foo); } - // find the argument position of x and y int pos = -1; int nargs = num_args(arg(con,0)); @@ -555,10 +903,22 @@ class iz3proof_itp_impl : public iz3proof_itp { pos = i; if(pos == -1) throw proof_error(); + ast bar = make(cong,foo,make_int(rational(pos)),get_placeholder(mk_not(con))); + conjs.push_back(mk_not(con)); + return make_contra_node(bar,conjs); +#if 0 + ast A_term = x; + ast f_A_term = arg(con,0); + if(get_term_type(y) == LitA){ + A_term = y; + f_A_term = arg(con,1); + } + ast res = make(Equal,f_A_term,subst_in_arg_pos(pos,get_placeholder(make(Equal,x,y)),f_A_term)); res = make(And,res,mk_not(con)); return res; +#endif } ast subst_in_arg_pos(int pos, ast term, ast app){ @@ -576,20 +936,22 @@ class iz3proof_itp_impl : public iz3proof_itp { /* Compute the interpolant for the clause */ ast zero = make_int("0"); - std::vector conjs; conjs.resize(1); + std::vector conjs; ast thing = make(Leq,zero,zero); for(unsigned i = 0; i < prem_cons.size(); i++){ const ast &lit = prem_cons[i]; if(get_term_type(lit) == LitA) linear_comb(thing,coeffs[i],lit); - else if(get_term_type(lit) != LitB) - conjs.push_back(make(farkas,coeffs[i],prem_cons[i])); } thing = simplify_ineq(thing); - if(conjs.size() > 1){ - conjs[0] = thing; - thing = make(And,conjs); + for(unsigned i = 0; i < prem_cons.size(); i++){ + const ast &lit = prem_cons[i]; + if(get_term_type(lit) == LitMixed){ + thing = make(sum,thing,coeffs[i],get_placeholder(lit)); + conjs.push_back(lit); + } } + thing = make_contra_node(thing,conjs); /* Resolve it with the premises */ std::vector conc; conc.resize(prem_cons.size()); @@ -667,24 +1029,15 @@ class iz3proof_itp_impl : public iz3proof_itp { itp = mk_true(); break; default: { // mixed equality - ast mid,ante; - if(get_term_type(y) == LitA){ - std::swap(x,y); - mid = make(Plus,x,get_placeholder(yleqx)); - } - else { - mid = make(Plus,x,get_placeholder(xleqy)); - } - ante = make(Uminus,make(Plus,get_placeholder(xleqy),get_placeholder(yleqx))); - ante = mk_not(make(Leq,make_int("0"),ante)); -#if 0 - ast zleqz = make(Leq,make_int("0"),make_int("0")); - ast fark1 = make(farkas,make_int("1"),xleqy); - ast fark2 = make(farkas,make_int("1"),yleqx); - ast ante = make(And,zleqz,fark1,fark2); -#endif - ast conc = make(And,make(Equal,x,mid),mk_not(con)); - itp = my_or(ante,conc); + std::vector conjs; conjs.resize(3); + conjs[0] = mk_not(con); + conjs[1] = xleqy; + conjs[2] = yleqx; + itp = make_contra_node(make(leq2eq, + get_placeholder(mk_not(con)), + get_placeholder(xleqy), + get_placeholder(yleqx)), + conjs); } } return itp; @@ -710,7 +1063,7 @@ class iz3proof_itp_impl : public iz3proof_itp { mid = make(Sub,mid,x); } ast zleqmid = make(Leq,make_int("0"),mid); - ast fark = make(farkas,make_int("1"),mk_not(xleqy)); + ast fark = make(contra,make_int("1"),mk_not(xleqy)); itp = make(And,zleqmid,fark); } } @@ -732,7 +1085,7 @@ class iz3proof_itp_impl : public iz3proof_itp { default: { ast t = arg(tleqc,0); ast c = arg(tleqc,1); - ast thing = make(farkas,make_int("1"),mk_not(con)); + ast thing = make(contra,make_int("1"),mk_not(con)); itp = make(And,make(Leq,make_int("0"),make(Idiv,get_placeholder(tleqc),d)),thing); } } @@ -741,7 +1094,9 @@ class iz3proof_itp_impl : public iz3proof_itp { return itp; } - ast get_farkas_coeff(const ast &f){ + + + ast get_contra_coeff(const ast &f){ ast c = arg(f,0); // if(!is_not(arg(f,1))) // c = make(Uminus,c); @@ -755,6 +1110,10 @@ class iz3proof_itp_impl : public iz3proof_itp { ast my_and(const ast &a, const ast &b){ return mk_and(a,b); } + + ast my_implies(const ast &a, const ast &b){ + return mk_implies(a,b); + } ast my_or(const std::vector &a){ return mk_or(a); @@ -777,8 +1136,19 @@ public: pv = p; rng = r; weak = w; - type domain[2] = {int_type(),bool_type()}; - farkas = function("@farkas",2,domain,bool_type()); + type boolintbooldom[3] = {bool_type(),int_type(),bool_type()}; + type booldom[1] = {bool_type()}; + type boolbooldom[2] = {bool_type(),bool_type()}; + type boolboolbooldom[3] = {bool_type(),bool_type(),bool_type()}; + contra = function("@contra",2,boolbooldom,bool_type()); + sum = function("@sum",3,boolintbooldom,bool_type()); + rotate_sum = function("@rotsum",2,boolbooldom,bool_type()); + leq2eq = function("@leq2eq",3,boolboolbooldom,bool_type()); + cong = function("@cong",3,boolintbooldom,bool_type()); + exmid = function("@exmid",3,boolboolbooldom,bool_type()); + symm = function("@symm",1,booldom,bool_type()); + epsilon = make_var("@eps",int_type()); + modpon = function("@mp",3,boolboolbooldom,bool_type()); } }; diff --git a/src/interp/iz3proof_itp.h b/src/interp/iz3proof_itp.h index 692fb7772..a50fa184a 100644 --- a/src/interp/iz3proof_itp.h +++ b/src/interp/iz3proof_itp.h @@ -82,7 +82,7 @@ class iz3proof_itp : public iz3mgr { /** Make a Symmetry node. This takes a derivation of |- x = y and produces | y = x */ - virtual node make_symmetry(ast con, node prem) = 0; + virtual node make_symmetry(ast con, const ast &premcon, node prem) = 0; /** Make a transitivity node. This takes derivations of |- x = y and |- y = z produces | x = z */ @@ -92,12 +92,12 @@ class iz3proof_itp : public iz3mgr { /** Make a congruence node. This takes a derivation of |- x_i = y_i and produces |- f(...x_i,...) = f(...,y_i,...) */ - virtual node make_congruence(const ast &x, const ast &y, const ast &con, const std::vector &hyps, const ast &prem1) = 0; + virtual node make_congruence(const ast &xi_eq_yi, const ast &con, const ast &prem1) = 0; /** Make a modus-ponens node. This takes derivations of |- x and |- x = y and produces |- y */ - virtual node make_mp(const ast &x, const ast &y, const ast &prem1, const ast &prem2) = 0; + virtual node make_mp(const ast &x_eq_y, const ast &prem1, const ast &prem2) = 0; /** Make a farkas proof node. */ diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 8220fb214..ceacb18bf 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -888,15 +888,21 @@ public: for(unsigned i = 0; i < farkas_coeffs.size(); i++) my_coeffs.push_back(farkas_coeffs[i]); #else - std::vector &my_coeffs = farkas_coeffs; + std::vector my_coeffs; #endif std::vector my_cons; - for(int i = 0; i < nargs; i++) + for(int i = 1; i < nargs; i++){ my_cons.push_back(mk_not(arg(con,i))); + my_coeffs.push_back(farkas_coeffs[i]); + } + ast farkas_con = normalize_inequality(sum_inequalities(farkas_coeffs,my_cons)); + my_cons.push_back(mk_not(farkas_con)); + my_coeffs.push_back(make_int("1")); std::vector my_hyps; for(int i = 0; i < nargs; i++) my_hyps.push_back(iproof->make_hypothesis(my_cons[i])); ast res = iproof->make_farkas(mk_false(),my_hyps,my_cons,my_coeffs); + res = iproof->make_cut_rule(farkas_con,farkas_coeffs[0],arg(con,0),res); return res; } @@ -973,10 +979,12 @@ public: // assume the premise is x = y ast x = arg(conc(prem(proof,0)),0); ast y = arg(conc(prem(proof,0)),1); +#if 0 AstSet &hyps = get_hyps(proof); std::vector hyps_vec; hyps_vec.resize(hyps.size()); std::copy(hyps.begin(),hyps.end(),hyps_vec.begin()); - res = iproof->make_congruence(x,y,con,hyps_vec,args[0]); +#endif + res = iproof->make_congruence(conc(prem(proof,0)),con,args[0]); break; } case PR_REFLEXIVITY: { @@ -984,11 +992,11 @@ public: break; } case PR_SYMMETRY: { - res = iproof->make_symmetry(con,args[0]); + res = iproof->make_symmetry(con,conc(prem(proof,0)),args[0]); break; } case PR_MODUS_PONENS: { - res = iproof->make_mp(conc(prem(proof,0)),arg(conc(prem(proof,1)),1),args[0],args[1]); + res = iproof->make_mp(conc(prem(proof,1)),args[0],args[1]); break; } case PR_TH_LEMMA: { diff --git a/src/interp/iz3translate.h b/src/interp/iz3translate.h index 6663f406b..afb9df9bc 100755 --- a/src/interp/iz3translate.h +++ b/src/interp/iz3translate.h @@ -53,8 +53,11 @@ public: }; //#define IZ3_TRANSLATE_DIRECT2 +#ifndef _FOCI2 #define IZ3_TRANSLATE_DIRECT -// #define IZ3_TRANSLATE_FULL +#else +#define IZ3_TRANSLATE_FULL +#endif #endif