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

working on eq-propagate rule in interpolation

Browse source
This commit is contained in:
Ken McMillan 2013-11-12 12:38:30 -08:00
parent 4b0c00969c
commit d73310cfa1
2 changed files with 69 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/interp/iz3proof_itp.cpp
View file

@ -1831,6 +1831,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
itp = mk_true();
break;
default: { // mixed equality
if(get_term_type(x) == LitMixed || get_term_type(y) == LitMixed)
std::cerr << "WARNING: mixed term in leq2eq\n";
std::vector<ast> conjs; conjs.resize(3);
conjs[0] = mk_not(con);
conjs[1] = xleqy;

81
src/interp/iz3translate.cpp
View file

@ -1215,7 +1215,61 @@ public:
return res;
}
bool is_eq_propagate(const ast &proof){
return pr(proof) == PR_TH_LEMMA && get_theory_lemma_theory(proof) == ArithTheory && get_theory_lemma_kind(proof) == EqPropagateKind;
}
ast EqPropagate(const ast &con, const std::vector<ast> &prems, const std::vector<Iproof::node> &args){
Iproof::node fps[2];
ast ineq_con[2];
for(int i = 0; i < 2; i++){
opr o = i == 0 ? Leq : Geq;
ineq_con[i] = make(o, arg(con,0), arg(con,1));
fps[i] = reconstruct_farkas(prems,args,ineq_con[i]);
}
ast res = iproof->make_leq2eq(arg(con,0), arg(con,1), ineq_con[0], ineq_con[1]);
std::vector<Iproof::node> dummy_clause;
for(int i = 0; i < 2; i++)
res = iproof->make_resolution(ineq_con[i],dummy_clause,res,fps[i]);
return res;
}
struct CannotCombineEqPropagate {};
void CombineEqPropagateRec(const ast &proof, std::vector<ast> &prems, std::vector<Iproof::node> &args, ast &eqprem){
if(pr(proof) == PR_TRANSITIVITY && is_eq_propagate(prem(proof,1))){
CombineEqPropagateRec(prem(proof,0), prems, args, eqprem);
ast dummy;
CombineEqPropagateRec(prem(proof,1), prems, args, dummy);
return;
}
if(is_eq_propagate(proof)){
int nprems = num_prems(proof);
for(int i = 0; i < nprems; i++){
prems.push_back(prem(proof,i));
ast ppf = translate_main(prem(proof,i),false);
args.push_back(ppf);
}
return;
}
eqprem = proof;
}
ast CombineEqPropagate(const ast &proof){
std::vector<ast> prems, args;
ast eq1;
CombineEqPropagateRec(proof, prems, args, eq1);
ast eq2con = conc(proof);
if(!eq1.null())
eq2con = make(Equal,arg(conc(eq1),1),arg(conc(proof),1));
ast eq2 = EqPropagate(eq2con,prems,args);
if(!eq1.null()){
Iproof::node foo = translate_main(eq1,false);
eq2 = iproof->make_transitivity(arg(conc(eq1),0), arg(conc(eq1),1), arg(conc(proof),1), foo, eq2);
}
return eq2;
}
// translate a Z3 proof term into interpolating proof system
Iproof::node translate_main(ast proof, bool expect_clause = true){
@ -1290,6 +1344,15 @@ public:
res = make(commute,clause,conc(prem(proof,0))); // HACK -- we depend on Iproof::node being same as ast.
return res;
}
if(dk == PR_TRANSITIVITY && is_eq_propagate(prem(proof,1))){
try {
res = CombineEqPropagate(proof);
return res;
}
catch(const CannotCombineEqPropagate &){
}
}
// translate all the premises
std::vector<Iproof::node> args(nprems);
@ -1412,20 +1475,10 @@ public:
}
case EqPropagateKind: {
std::vector<ast> prems(nprems);
Iproof::node fps[2];
ast ineq_con[2];
for(int i = 0; i < nprems; i++)
for(unsigned i = 0; i < nprems; i++)
prems[i] = prem(proof,i);
for(int i = 0; i < 2; i++){
opr o = i == 0 ? Leq : Geq;
ineq_con[i] = make(o, arg(con,0), arg(con,1));
fps[i] = reconstruct_farkas(prems,args,ineq_con[i]);
}
res = iproof->make_leq2eq(arg(con,0), arg(con,1), ineq_con[0], ineq_con[1]);
std::vector<Iproof::node> dummy_clause;
for(int i = 0; i < 2; i++)
res = iproof->make_resolution(ineq_con[i],dummy_clause,res,fps[i]);
return res;
res = EqPropagate(con,prems,args);
break;
}
default:
throw unsupported();