mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

fix for github issue 54

Browse source
This commit is contained in:
Ken McMillan 2015-05-19 18:47:13 -07:00
parent 69a3590490
commit ccc1f02216
3 changed files with 25 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/interp/iz3mgr.h
View file

@ -279,6 +279,12 @@ class iz3mgr {
res[i] = arg(t,i); res[i] = arg(t,i);
} }
std::vector<ast> args(const ast &t){
std::vector<ast> res;
get_args(t,res);
return res;
}
symb sym(ast t){ symb sym(ast t){
raw_ast *_ast = t.raw(); raw_ast *_ast = t.raw();
return is_app(_ast) ? to_app(_ast)->get_decl() : 0; return is_app(_ast) ? to_app(_ast)->get_decl() : 0;

8
src/interp/iz3proof_itp.cpp
View file

@ -2215,8 +2215,12 @@ class iz3proof_itp_impl : public iz3proof_itp {
} }
else { else {
if(get_term_type(p) == LitA){ if(get_term_type(p) == LitA){
if(get_term_type(q) == LitA) if(get_term_type(q) == LitA){
itp = mk_false(); if(op(q) == Or)
itp = make_assumption(rng.hi,args(q));
else
itp = mk_false();
}
else { else {
if(get_term_type(p_eq_q) == LitA) if(get_term_type(p_eq_q) == LitA)
itp = q; itp = q;

14
src/interp/iz3translate.cpp
View file

@ -1702,14 +1702,16 @@ public:
return res; return res;
} }
} }
if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or){ if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or && op(conc(prem(proof,0))) == Or){
Iproof::node clause = translate_main(prem(proof,0),true); Iproof::node clause = translate_main(prem(proof,0),true);
res = RewriteClause(clause,prem(proof,1)); res = RewriteClause(clause,prem(proof,1));
return res; return res;
} }
#if 0
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";
#endif
// no idea why this shows up // no idea why this shows up
if(dk == PR_MODUS_PONENS_OEQ){ if(dk == PR_MODUS_PONENS_OEQ){
@ -1965,6 +1967,16 @@ public:
res = make(commute,pf,comm_equiv); res = make(commute,pf,comm_equiv);
break; break;
} }
case PR_AND_ELIM: {
std::vector<ast> rule_ax, res_conc;
ast piv = conc(prem(proof,0));
rule_ax.push_back(make(Not,piv));
rule_ax.push_back(con);
ast pf = iproof->make_axiom(rule_ax);
res_conc.push_back(con);
res = iproof->make_resolution(piv,res_conc,pf,args[0]);
break;
}
default: default:
pfgoto(proof); pfgoto(proof);
assert(0 && "translate_main: unsupported proof rule"); assert(0 && "translate_main: unsupported proof rule");