mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

interpolation fix

Browse source
This commit is contained in:
Ken McMillan 2014-03-16 12:09:53 -07:00
parent 675820ff67
commit 663d110b72
1 changed files with 29 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/interp/iz3translate.cpp
View file

@ -1590,6 +1590,27 @@ public:
return res;
}
/* This idiom takes ~P and Q=P, yielding ~Q. It uses a "rewrite"
(Q=false) = ~Q. We eliminate the rewrite by using symmetry,
congruence and modus ponens. */
if(dk == PR_MODUS_PONENS && pr(prem(proof,1)) == PR_REWRITE && pr(prem(proof,0)) == PR_TRANSITIVITY && pr(prem(prem(proof,0),1)) == PR_IFF_FALSE){
if(op(con) == Not && arg(con,0) == arg(conc(prem(proof,0)),0)){
Iproof::node ante1 = translate_main(prem(prem(proof,0),0),false);
Iproof::node ante2 = translate_main(prem(prem(prem(proof,0),1),0),false);
ast ante1_con = conc(prem(prem(proof,0),0));
ast eq0 = arg(ante1_con,0);
ast eq1 = arg(ante1_con,1);
ast symm_con = make(Iff,eq1,eq0);
Iproof::node ante1s = iproof->make_symmetry(symm_con,ante1_con,ante1);
ast cong_con = make(Iff,make(Not,eq1),make(Not,eq0));
Iproof::node ante1sc = iproof->make_congruence(symm_con,cong_con,ante1s);
res = iproof->make_mp(cong_con,ante2,ante1sc);
return res;
}
}
// translate all the premises
std::vector<Iproof::node> args(nprems);
for(unsigned i = 0; i < nprems; i++)
@ -1749,6 +1770,13 @@ public:
res = args[0];
break;
}
case PR_IFF_FALSE: { // turns ~p into p <-> false, noop for us
if(is_local(con))
res = args[0];
else
throw unsupported();
break;
}
case PR_COMMUTATIVITY: {
ast comm_equiv = make(op(con),arg(con,0),arg(con,0));
ast pf = iproof->make_reflexivity(comm_equiv);
@ -1756,6 +1784,7 @@ public:
break;
}
default:
pfgoto(proof);
assert(0 && "translate_main: unsupported proof rule");
throw unsupported();
}