mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

attempted interp fixes

Browse source
This commit is contained in:
Ken McMillan 2014-12-08 15:46:55 -08:00
parent a6f58bdd17
commit 8181b15a1b
2 changed files with 11 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/interp/iz3proof_itp.cpp
View file

@ -1027,7 +1027,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
linear_comb(Aineqs,coeff,make(Leq,make_int(rational(0)),make(Sub,term2,term1)));
}
else {
ast pf = extract_rewrites(make(concat,mk_true(),rest),p1);
ast pf = extract_rewrites(make(concat,mk_true(),last),p1);
ast new_normal = fix_normal(term1,term2,pf);
normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves);
}

12
src/interp/iz3translate.cpp
View file

@ -1712,11 +1712,17 @@ public:
std::cout << "foo!\n";
// no idea why this shows up
if(dk == PR_MODUS_PONENS_OEQ)
if(dk == PR_MODUS_PONENS_OEQ){
if(conc(prem(proof,0)) == con){
res = translate_main(prem(proof,0),expect_clause);
return res;
}
if(expect_clause && op(con) == Or){ // skolemization does this
Iproof::node clause = translate_main(prem(proof,0),true);
res = RewriteClause(clause,prem(proof,1));
return res;
}
}
#if 0
if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){
@ -1800,7 +1806,9 @@ public:
}
break;
}
case PR_MONOTONICITY: {
case PR_QUANT_INTRO:
case PR_MONOTONICITY:
{
std::vector<ast> eqs; eqs.resize(args.size());
for(unsigned i = 0; i < args.size(); i++)
eqs[i] = conc(prem(proof,i));