From 8e772b428bc0f678a76cd885f75fcc4b3c0bdae7 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Thu, 16 Apr 2015 19:14:34 +0200 Subject: [PATCH] use a base iz3_exception class for exceptions raised during interpolation Using a base exception class, derived from z3_exception, makes it possible to recover gracefully if something goes wrong during the computation of interpolants. --- src/interp/iz3base.h | 4 +- src/interp/iz3exception.h | 28 ++++++++++++ src/interp/iz3interp.cpp | 2 +- src/interp/iz3interp.h | 7 ++- src/interp/iz3mgr.cpp | 16 +++---- src/interp/iz3mgr.h | 1 + src/interp/iz3pp.h | 3 +- src/interp/iz3proof.h | 4 +- src/interp/iz3proof_itp.cpp | 68 +++++++++++++++++------------- src/interp/iz3proof_itp.h | 4 +- src/interp/iz3translate.cpp | 18 ++++---- src/interp/iz3translate.h | 3 +- src/interp/iz3translate_direct.cpp | 8 +++- 13 files changed, 109 insertions(+), 57 deletions(-) create mode 100644 src/interp/iz3exception.h diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h index 76ed6e3e2..59cbf3a61 100755 --- a/src/interp/iz3base.h +++ b/src/interp/iz3base.h @@ -117,7 +117,7 @@ class iz3base : public iz3mgr, public scopes { /** Interpolator for clauses, to be implemented */ virtual void interpolate_clause(std::vector &lits, std::vector &itps){ - throw "no interpolator"; + throw iz3_exception("no interpolator"); } ast get_proof_check_assump(range &rng){ @@ -129,7 +129,7 @@ class iz3base : public iz3mgr, public scopes { int frame_of_assertion(const ast &ass){ stl_ext::hash_map::iterator it = frame_map.find(ass); if(it == frame_map.end()) - throw "unknown assertion"; + throw iz3_exception("unknown assertion"); return it->second; } diff --git a/src/interp/iz3exception.h b/src/interp/iz3exception.h new file mode 100644 index 000000000..134c049cf --- /dev/null +++ b/src/interp/iz3exception.h @@ -0,0 +1,28 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + iz3exception.h + +Abstract: + + Base class for exceptions raised by interpolation routines + +Author: + +Notes: + +--*/ +#ifndef _IZ3EXCEPTION_H_ +#define _IZ3EXCEPTION_H_ + +#include "z3_exception.h" +#include "error_codes.h" + +class iz3_exception: public default_exception { +public: + iz3_exception(const std::string &msg): default_exception(msg) {} +}; + +#endif diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 9d90a05c7..ec9fceecc 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -218,7 +218,7 @@ public: iz3secondary *sp = iz3foci::create(this,num,(int *)(parents.empty()?0:&parents[0])); int res = sp->interpolate(cnsts, interps); if(res != 0) - throw "secondary failed"; + throw iz3_exception("secondary failed"); } void proof_to_interpolant(z3pf proof, diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h index 2b1926994..f17b3c405 100644 --- a/src/interp/iz3interp.h +++ b/src/interp/iz3interp.h @@ -21,6 +21,7 @@ #define IZ3_INTERP_H #include "iz3hash.h" +#include "iz3exception.h" #include "solver.h" class iz3base; @@ -35,12 +36,14 @@ public: }; /** This object is thrown if a tree interpolation problem is mal-formed */ -struct iz3_bad_tree { +struct iz3_bad_tree: public iz3_exception { + iz3_bad_tree(): iz3_exception("iz3_bad_tree") {} }; /** This object is thrown when iz3 fails due to an incompleteness in the secondary solver. */ -struct iz3_incompleteness { +struct iz3_incompleteness: public iz3_exception { + iz3_incompleteness(): iz3_exception("iz3_incompleteness") {} }; typedef interpolation_options_struct *interpolation_options; diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index 5a7f71987..845e716ef 100755 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -515,7 +515,7 @@ bool iz3mgr::is_farkas_coefficient_negative(const ast &proof, int n){ symb s = sym(proof); bool ok = s->get_parameter(n+2).is_rational(r); if(!ok) - throw "Bad Farkas coefficient"; + throw iz3_exception("Bad Farkas coefficient"); return r.is_neg(); } @@ -532,7 +532,7 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& rats){ rational r; bool ok = s->get_parameter(i).is_rational(r); if(!ok) - throw "Bad Farkas coefficient"; + throw iz3_exception("Bad Farkas coefficient"); #if 0 { ast con = conc(prem(proof,i-2)); @@ -577,7 +577,7 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector& r rational r; bool ok = s->get_parameter(i).is_rational(r); if(!ok) - throw "Bad Farkas coefficient"; + throw iz3_exception("Bad Farkas coefficient"); { ast con = arg(conc(proof),i-1); ast temp = make_real(r); // for debugging @@ -593,7 +593,7 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector& r if(rats[1].is_neg()){ // work around bug -- if all coeffs negative, negate them for(unsigned i = 1; i < rats.size(); i++){ if(!rats[i].is_neg()) - throw "Bad Farkas coefficients"; + throw iz3_exception("Bad Farkas coefficients"); rats[i] = -rats[i]; } } @@ -623,7 +623,7 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vectorget_parameter(i).is_rational(r); if(!ok) - throw "Bad Farkas coefficient"; + throw iz3_exception("Bad Farkas coefficient"); { ast con = conc(prem(proof,i-2)); ast temp = make_real(r); // for debugging @@ -639,7 +639,7 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector #include "iz3hash.h" +#include "iz3exception.h" #include"well_sorted.h" #include"arith_decl_plugin.h" diff --git a/src/interp/iz3pp.h b/src/interp/iz3pp.h index bbb10a785..c66b4a4fa 100644 --- a/src/interp/iz3pp.h +++ b/src/interp/iz3pp.h @@ -25,7 +25,8 @@ /** Exception thrown in case of mal-formed tree interpoloation specification */ -struct iz3pp_bad_tree { +struct iz3pp_bad_tree: public iz3_exception { + iz3pp_bad_tree(): iz3_exception("iz3pp_bad_tree") {} }; void iz3pp(ast_manager &m, diff --git a/src/interp/iz3proof.h b/src/interp/iz3proof.h index be85702a2..213afce5e 100755 --- a/src/interp/iz3proof.h +++ b/src/interp/iz3proof.h @@ -57,7 +57,9 @@ class iz3proof { typedef prover::ast ast; /** Object thrown in case of a proof error. */ - struct proof_error {}; + struct proof_error: public iz3_exception { + proof_error(): iz3_exception("proof_error") {} + }; /* Null proof node */ static const node null = -1; diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 0bdd51ed8..588ebc2ea 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -250,7 +250,7 @@ class iz3proof_itp_impl : public iz3proof_itp { #if 0 rational r; if(!is_integer(coeff,r)) - throw "ack!"; + throw iz3_exception("ack!"); ast n = make_int(r.numerator()); ast res = make(Times,n,t); if(!r.is_int()) { @@ -433,7 +433,7 @@ class iz3proof_itp_impl : public iz3proof_itp { if(op(foo) == Uninterpreted && sym(foo) == contra){ ast neg_lit = arg(foo,1); if(!is_false(neg_lit) && neg_lits.find(neg_lit) == neg_lits.end()) - throw "lost a literal"; + throw iz3_exception("lost a literal"); return; } else { @@ -506,7 +506,9 @@ class iz3proof_itp_impl : public iz3proof_itp { /* This is where the real work happens. Here, we simplify the proof obtained by cut elimination, obtaining an interpolant. */ - struct cannot_simplify {}; + struct cannot_simplify: public iz3_exception { + cannot_simplify(): iz3_exception("cannot_simplify") {} + }; hash_map simplify_memo; ast simplify(const ast &t){ @@ -582,7 +584,7 @@ class iz3proof_itp_impl : public iz3proof_itp { // if(g == symm) return simplify_rotate_symm(pl,args[0],pf); } if(op(pf) == Leq) - throw "foo!"; + throw iz3_exception("foo!"); throw cannot_simplify(); } @@ -831,7 +833,7 @@ class iz3proof_itp_impl : public iz3proof_itp { return my_implies(cond,ineqs); if(op(ineqs) != And) return my_and(Bconds,my_implies(cond,ineqs)); - throw "help!"; + throw iz3_exception("help!"); } ast add_mixed_eq2ineq(const ast &lhs, const ast &rhs, const ast &equa, const ast &itp){ @@ -871,7 +873,7 @@ class iz3proof_itp_impl : public iz3proof_itp { } } } - throw "help!"; + throw iz3_exception("help!"); } void reverse_modpon(std::vector &args){ @@ -980,7 +982,9 @@ class iz3proof_itp_impl : public iz3proof_itp { return chain; } - struct subterm_normals_failed {}; + struct subterm_normals_failed: public iz3_exception { + subterm_normals_failed(): iz3_exception("subterm_normals_failed") {} + }; void get_subterm_normals(const ast &ineq1, const ast &ineq2, const ast &chain, ast &normals, const ast &pos, hash_set &memo, ast &Aproves, ast &Bproves){ @@ -989,7 +993,7 @@ class iz3proof_itp_impl : public iz3proof_itp { if(o1 == Not || o1 == Leq || o1 == Lt || o1 == Geq || o1 == Gt || o1 == Plus || o1 == Times){ int n = num_args(ineq1); if(o2 != o1 || num_args(ineq2) != n) - throw "bad inequality rewriting"; + throw iz3_exception("bad inequality rewriting"); for(int i = 0; i < n; i++){ ast new_pos = add_pos_to_end(pos,i); get_subterm_normals(arg(ineq1,i), arg(ineq2,i), chain, normals, new_pos, memo, Aproves, Bproves); @@ -1000,7 +1004,7 @@ class iz3proof_itp_impl : public iz3proof_itp { memo.insert(ineq2); ast sub_chain = extract_rewrites(chain,pos); if(is_true(sub_chain)) - throw "bad inequality rewriting"; + throw iz3_exception("bad inequality rewriting"); ast new_normal = make_normal_step(ineq2,ineq1,reverse_chain(sub_chain)); normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves); } @@ -1149,7 +1153,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast interp = contra_chain(Q2,chain); return my_and(Aproves,my_implies(Bproves,interp)); } - throw "bad exmid"; + throw iz3_exception("bad exmid"); } ast simplify_cong(const std::vector &args){ @@ -1163,7 +1167,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast interp = contra_chain(Q2,chain); return my_and(Aproves,my_implies(Bproves,interp)); } - throw "bad cong"; + throw iz3_exception("bad cong"); } bool is_equivrel(const ast &p){ @@ -1171,7 +1175,9 @@ class iz3proof_itp_impl : public iz3proof_itp { return o == Equal || o == Iff; } - struct rewrites_failed{}; + struct rewrites_failed: public iz3_exception { + rewrites_failed(): iz3_exception("rewrites_failed") {} + }; /* Suppose p in Lang(B) and A |- p -> q and B |- q -> r. Return a z in Lang(B) such that B |- p -> z and A |- z -> q. Collect any side conditions in "rules". */ @@ -1414,7 +1420,7 @@ class iz3proof_itp_impl : public iz3proof_itp { rational r; if(is_numeral(arg(pos,0),r)) return r.get_unsigned(); - throw "bad position!"; + throw iz3_exception("bad position!"); } /* substitute y into position pos in x */ @@ -1429,7 +1435,7 @@ class iz3proof_itp_impl : public iz3proof_itp { args[i] = i == p ? subst_in_pos(arg(x,i),arg(pos,1),y) : arg(x,i); return clone(x,args); } - throw "bad term position!"; + throw iz3_exception("bad term position!"); } ast diff_chain(LitType t, const ast &pos, const ast &x, const ast &y, const ast &prefix){ @@ -1448,10 +1454,10 @@ class iz3proof_itp_impl : public iz3proof_itp { ast make_rewrite(LitType t, const ast &pos, const ast &cond, const ast &equality){ #if 0 if(pos == top_pos && op(equality) == Iff && !is_true(arg(equality,0))) - throw "bad rewrite"; + throw iz3_exception("bad rewrite"); #endif if(!is_equivrel(equality)) - throw "bad rewrite"; + throw iz3_exception("bad rewrite"); return make(t == LitA ? rewrite_A : rewrite_B, pos, cond, equality); } @@ -1662,25 +1668,25 @@ class iz3proof_itp_impl : public iz3proof_itp { if(is_true(rest)){ ast old = rewrite_rhs(last); if(!(op(old) == Not)) - throw "bad negative equality chain"; + throw iz3_exception("bad negative equality chain"); ast equ = arg(old,0); if(!is_equivrel(equ)) - throw "bad negative equality chain"; + throw iz3_exception("bad negative equality chain"); last = rewrite_update_rhs(last,top_pos,make(Not,make(op(equ),arg(equ,1),arg(equ,0))),make(True)); return chain_cons(rest,last); } ast pos = rewrite_pos(last); if(pos == top_pos) - throw "bad negative equality chain"; + throw iz3_exception("bad negative equality chain"); int idx = pos_arg(pos); if(idx != 0) - throw "bad negative equality chain"; + throw iz3_exception("bad negative equality chain"); pos = arg(pos,1); if(pos == top_pos){ ast lhs = rewrite_lhs(last); ast rhs = rewrite_rhs(last); if(op(lhs) != Equal || op(rhs) != Equal) - throw "bad negative equality chain"; + throw iz3_exception("bad negative equality chain"); last = make_rewrite(rewrite_side(last),rewrite_pos(last),rewrite_cond(last), make(Iff,make(Equal,arg(lhs,1),arg(lhs,0)),make(Equal,arg(rhs,1),arg(rhs,0)))); } @@ -1691,7 +1697,7 @@ class iz3proof_itp_impl : public iz3proof_itp { else if(idx == 1) idx = 0; else - throw "bad negative equality chain"; + throw iz3_exception("bad negative equality chain"); pos = pos_add(0,pos_add(idx,arg(pos,1))); last = make_rewrite(rewrite_side(last),pos,rewrite_cond(last),rewrite_equ(last)); } @@ -1708,7 +1714,7 @@ class iz3proof_itp_impl : public iz3proof_itp { return chain; } if(is_true(rest)) - throw "bad rewrite chain"; + throw iz3_exception("bad rewrite chain"); ast head = get_head_chain(rest,tail,is_not); tail = chain_cons(tail,last); return head; @@ -1766,7 +1772,9 @@ class iz3proof_itp_impl : public iz3proof_itp { } - struct cannot_split {}; + struct cannot_split: public iz3_exception { + cannot_split(): iz3_exception("cannot_split") {} + }; /** Split a chain of rewrites two chains, operating on positions 0 and 1. Fail if any rewrite in the chain operates on top position. */ @@ -1808,7 +1816,7 @@ class iz3proof_itp_impl : public iz3proof_itp { } case 1: if(rewrite_lhs(last) != rewrite_rhs(last)) - throw "bad rewrite chain"; + throw iz3_exception("bad rewrite chain"); break; default:; } @@ -1853,7 +1861,9 @@ class iz3proof_itp_impl : public iz3proof_itp { return rewrites_from_to(rest,lhs,mid); } - struct bad_ineq_inference {}; + struct bad_ineq_inference: public iz3_exception { + bad_ineq_inference(): iz3_exception("bad_ineq_inference") {} + }; ast chain_ineqs(opr comp_op, LitType t, const ast &chain, const ast &lhs, const ast &rhs){ if(is_true(chain)){ @@ -1907,7 +1917,7 @@ class iz3proof_itp_impl : public iz3proof_itp { rhs = arg(ineq,1); return; } - throw "bad ineq"; + throw iz3_exception("bad ineq"); } ast chain_pos_add(int arg, const ast &chain){ @@ -1974,7 +1984,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast make_normal(const ast &ineq, const ast &nrml){ if(!is_ineq(ineq)) - throw "what?"; + throw iz3_exception("what?"); return make(normal,ineq,nrml); } @@ -1985,7 +1995,7 @@ class iz3proof_itp_impl : public iz3proof_itp { return make_normal_step(lhs,rhs,proof); if(rhst == LitMixed && (lhst != LitMixed || ast_id(rhs) < ast_id(lhs))) return make_normal_step(rhs,lhs,reverse_chain(proof)); - throw "help!"; + throw iz3_exception("help!"); } ast chain_side_proves(LitType side, const ast &chain){ diff --git a/src/interp/iz3proof_itp.h b/src/interp/iz3proof_itp.h index e1e0de5cc..bd9eca441 100644 --- a/src/interp/iz3proof_itp.h +++ b/src/interp/iz3proof_itp.h @@ -50,7 +50,9 @@ class iz3proof_itp : public iz3mgr { typedef ast node; /** Object thrown in case of a proof error. */ - struct proof_error {}; + struct proof_error: public iz3_exception { + proof_error(): iz3_exception("proof_error") {} + }; /** Make a resolution node with given pivot literal and premises. diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 5b420673c..6d1b3f002 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -132,7 +132,7 @@ public: // if(range_is_empty(r)) range r = ast_scope(quanted); if(range_is_empty(r)) - throw "can't skolemize"; + throw iz3_exception("can't skolemize"); if(frame == INT_MAX || !in_range(frame,r)) frame = range_max(r); // this is desperation -- may fail if(frame >= frames) frame = frames - 1; @@ -1086,10 +1086,10 @@ public: rational xcoeff = get_first_coefficient(arg(x,0),xvar); rational ycoeff = get_first_coefficient(arg(y,0),yvar); if(xcoeff == rational(0) || ycoeff == rational(0) || xvar != yvar) - throw "bad assign-bounds lemma"; + throw iz3_exception("bad assign-bounds lemma"); rational ratio = xcoeff/ycoeff; if(denominator(ratio) != rational(1)) - throw "bad assign-bounds lemma"; + throw iz3_exception("bad assign-bounds lemma"); return make_int(ratio); // better be integer! } @@ -1098,7 +1098,7 @@ public: get_assign_bounds_coeffs(proof,farkas_coeffs); int nargs = num_args(con); if(nargs != (int)(farkas_coeffs.size())) - throw "bad assign-bounds theory lemma"; + throw iz3_exception("bad assign-bounds theory lemma"); #if 0 if(farkas_coeffs[0] != make_int(rational(1))) farkas_coeffs[0] = make_int(rational(1)); @@ -1139,7 +1139,7 @@ public: get_assign_bounds_rule_coeffs(proof,farkas_coeffs); int nargs = num_prems(proof)+1; if(nargs != (int)(farkas_coeffs.size())) - throw "bad assign-bounds theory lemma"; + throw iz3_exception("bad assign-bounds theory lemma"); #if 0 if(farkas_coeffs[0] != make_int(rational(1))) farkas_coeffs[0] = make_int(rational(1)); @@ -1415,7 +1415,7 @@ public: std::vector vals = cvec; if(!is_sat(cnstrs,new_proof,vals)) - throw "Proof error!"; + throw iz3_exception("Proof error!"); std::vector rat_farkas_coeffs; for(unsigned i = 0; i < cvec.size(); i++){ ast bar = vals[i]; @@ -1423,7 +1423,7 @@ public: if(is_numeral(bar,r)) rat_farkas_coeffs.push_back(r); else - throw "Proof error!"; + throw iz3_exception("Proof error!"); } rational the_lcd = lcd(rat_farkas_coeffs); std::vector farkas_coeffs; @@ -1471,7 +1471,7 @@ public: ast new_proof; std::vector dummy; if(is_sat(npcons,new_proof,dummy)) - throw "Proof error!"; + throw iz3_exception("Proof error!"); pfrule dk = pr(new_proof); int nnp = num_prems(new_proof); std::vector my_prems; @@ -1532,7 +1532,7 @@ public: ast new_proof; std::vector dummy; if(is_sat(npcons,new_proof,dummy)) - throw "Proof error!"; + throw iz3_exception("Proof error!"); pfrule dk = pr(new_proof); int nnp = num_prems(new_proof); std::vector my_prems; diff --git a/src/interp/iz3translate.h b/src/interp/iz3translate.h index 2fcf406db..86b0b3d2d 100755 --- a/src/interp/iz3translate.h +++ b/src/interp/iz3translate.h @@ -35,7 +35,8 @@ class iz3translation : public iz3base { virtual ~iz3translation(){} /** This is thrown when the proof cannot be translated. */ - struct unsupported { + struct unsupported: public iz3_exception { + unsupported(): iz3_exception("unsupported") {} }; static iz3translation *create(iz3mgr &mgr, diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index c1b751c6f..9b9b46cad 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -595,7 +595,9 @@ public: } - struct invalid_lemma {}; + struct invalid_lemma: public iz3_exception { + invalid_lemma(): iz3_exception("invalid_lemma") {} + }; @@ -846,7 +848,9 @@ public: return 1; } - struct non_lit_local_ante {}; + struct non_lit_local_ante: public iz3_exception { + non_lit_local_ante(): iz3_exception("non_lit_local_ante") {} + }; bool local_antes_simple;