From 0696a7ef500bce553d7cb8b0ded1bef6cd6d8bfe Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Wed, 6 Nov 2013 11:41:17 -0800
Subject: [PATCH] interpolation fix
---
src/interp/iz3proof_itp.cpp | 35 ++++++++++++++++++++++++-----------
1 file changed, 24 insertions(+), 11 deletions(-)
diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp
index 21a455a3a..07f5f0cf5 100644
--- a/src/interp/iz3proof_itp.cpp
+++ b/src/interp/iz3proof_itp.cpp
@@ -636,12 +636,22 @@ class iz3proof_itp_impl : public iz3proof_itp {
throw cannot_simplify();
}
+ void reverse_modpon(std::vector<ast> &args){
+ std::vector<ast> sargs(1); sargs[0] = args[1];
+ args[1] = simplify_symm(sargs);
+ if(is_equivrel_chain(args[2]))
+ args[1] = down_chain(args[1]);
+ std::swap(args[0],args[2]);
+ }
+
ast simplify_rotate_modpon(const ast &pl, const ast &neg_equality, const ast &pf){
- if(pl == arg(pf,2)){
- std::vector<ast> args; args.resize(3);
- args[0] = arg(pf,0);
- args[1] = arg(pf,1);
- args[2] = mk_true();
+ std::vector<ast> args; args.resize(3);
+ args[0] = arg(pf,0);
+ args[1] = arg(pf,1);
+ args[2] = arg(pf,2);
+ if(pl == args[0])
+ reverse_modpon(args);
+ if(pl == args[2]){
ast cond = mk_true();
ast chain = simplify_modpon_fwd(args, cond);
return my_implies(cond,chain);
@@ -1410,7 +1420,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
return chain_cons(mk_true(),make_rewrite(t, top_pos, mk_true(), rew));
}
- ast triv_interp(const symb &rule, const std::vector<ast> &premises){
+ ast triv_interp(const symb &rule, const std::vector<ast> &premises, int mask_in){
std::vector<ast> ps; ps.resize(premises.size());
std::vector<ast> conjs;
int mask = 0;
@@ -1424,7 +1434,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
break;
default:
ps[i] = get_placeholder(p); // can only prove consequent!
- if(i == ps.size()-1)
+ if(mask_in & (1 << i))
mask |= (1 << conjs.size());
conjs.push_back(p);
}
@@ -1434,12 +1444,12 @@ class iz3proof_itp_impl : public iz3proof_itp {
return res;
}
- ast triv_interp(const symb &rule, const ast &p0, const ast &p1, const ast &p2){
+ ast triv_interp(const symb &rule, const ast &p0, const ast &p1, const ast &p2, int mask){
std::vector<ast> ps; ps.resize(3);
ps[0] = p0;
ps[1] = p1;
ps[2] = p2;
- return triv_interp(rule,ps);
+ return triv_interp(rule,ps,mask);
}
/** Make a modus-ponens node. This takes derivations of |- x
@@ -1452,7 +1462,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
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));
+ int mask = 1 << 2;
+ if(op(p) == Not && is_equivrel(arg(p,0)))
+ mask |= 1; // we may need to run this rule backward if first premise is negative equality
+ itp = triv_interp(modpon,p,p_eq_q,mk_not(q),mask);
}
else {
if(get_term_type(p) == LitA){
@@ -1850,7 +1863,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
conjs[0] = make(Equal,x,y);
conjs[1] = mk_not(xleqy);
itp = make(eq2leq,get_placeholder(conjs[0]),get_placeholder(conjs[1]));
- itp = make_contra_node(itp,conjs);
+ itp = make_contra_node(itp,conjs,2);
}
}
return itp;