mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix for possible problem in Farkas proofs in interp

Browse source
This commit is contained in:
Ken McMillan 2014-05-13 14:59:09 -07:00
parent aa35f988fc
commit 669fded98a
1 changed files with 22 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/interp/iz3proof_itp.cpp
View file

@ -607,7 +607,29 @@ class iz3proof_itp_impl : public iz3proof_itp {
return res; return res;
} }
ast distribute_coeff(const ast &coeff, const ast &s){
if(sym(s) == sum){
if(sym(arg(s,2)) == sum)
return make(sum,
distribute_coeff(coeff,arg(s,0)),
make_int(rational(1)),
distribute_coeff(make(Times,coeff,arg(s,1)), arg(s,2)));
else
return make(sum,
distribute_coeff(coeff,arg(s,0)),
make(Times,coeff,arg(s,1)),
arg(s,2));
}
if(op(s) == Leq && arg(s,1) == make_int(rational(0)) && arg(s,2) == make_int(rational(0)))
return s;
return make(sum,make(Leq,make_int(rational(0)),make_int(rational(0))),coeff,s);
}
ast simplify_sum(std::vector<ast> &args){ ast simplify_sum(std::vector<ast> &args){
if(args[1] != make_int(rational(1))){
if(sym(args[2]) == sum)
return make(sum,args[0],make_int(rational(1)),distribute_coeff(args[1],args[2]));
}
ast Aproves = mk_true(), Bproves = mk_true(); ast Aproves = mk_true(), Bproves = mk_true();
ast ineq = destruct_cond_ineq(args[0],Aproves,Bproves); ast ineq = destruct_cond_ineq(args[0],Aproves,Bproves);
if(!is_normal_ineq(ineq)) throw cannot_simplify(); if(!is_normal_ineq(ineq)) throw cannot_simplify();