mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

interpolation fix for commutativity

Browse source
This commit is contained in:
Ken McMillan 2014-02-19 13:56:16 -08:00
parent 928d419138
commit 76fb66314b
1 changed files with 14 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/interp/iz3translate.cpp
View file

@ -1547,12 +1547,20 @@ public:
if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or) if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or)
std::cout << "foo!\n"; std::cout << "foo!\n";
#if 0
if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){ if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){
Iproof::node clause = translate_main(prem(proof,0),true); Iproof::node clause = translate_main(prem(proof,0),true);
res = make(commute,clause,conc(prem(proof,0))); // HACK -- we depend on Iproof::node being same as ast. res = make(commute,clause,conc(prem(proof,0))); // HACK -- we depend on Iproof::node being same as ast.
return res; return res;
} }
if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,0)) == PR_COMMUTATIVITY){
Iproof::node clause = translate_main(prem(proof,1),true);
res = make(commute,clause,conc(prem(proof,1))); // HACK -- we depend on Iproof::node being same as ast.
return res;
}
#endif
if(dk == PR_TRANSITIVITY && is_eq_propagate(prem(proof,1))){ if(dk == PR_TRANSITIVITY && is_eq_propagate(prem(proof,1))){
try { try {
res = CombineEqPropagate(proof); res = CombineEqPropagate(proof);
@ -1736,6 +1744,12 @@ public:
res = args[0]; res = args[0];
break; break;
} }
case PR_COMMUTATIVITY: {
ast comm_equiv = make(op(con),arg(con,0),arg(con,0));
ast pf = iproof->make_reflexivity(comm_equiv);
res = make(commute,pf,comm_equiv);
break;
}
default: default:
assert(0 && "translate_main: unsupported proof rule"); assert(0 && "translate_main: unsupported proof rule");
throw unsupported(); throw unsupported();