Merge branch 'agriggio-ag-iz3_exception'

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<ast> &lits, std::vector<ast> &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<ast,int>::iterator it = frame_map.find(ass);
         if(it == frame_map.end())
-            throw "unknown assertion";
+            throw iz3_exception("unknown assertion");
         return it->second;
     }
   

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

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,

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") {}
 };
 
 // This is thrown if there is some bug in the

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<rational>& 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));
@@ -591,7 +591,7 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& 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
@@ -607,7 +607,7 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& 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];
         }
     }
@@ -661,7 +661,7 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector<rationa
         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 = conc(prem(proof,i-2));
             ast temp = make_real(r); // for debugging
@@ -677,7 +677,7 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector<rationa
     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];
         }
     }
@@ -709,7 +709,7 @@ void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q, bool round_off){
             qstrict = true;
             break;
         default:
-            throw "not an inequality";
+            throw iz3_exception("not an inequality");
         }
     }
     else {
@@ -729,7 +729,7 @@ void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q, bool round_off){
             qstrict = true;
             break;
         default:
-            throw "not an inequality";
+            throw iz3_exception("not an inequality");
         }
     }
     bool pstrict = op(P) == Lt;

src/interp/iz3mgr.h

@@ -26,6 +26,7 @@
 #include <functional>
 
 #include "iz3hash.h"
+#include "iz3exception.h"
 
 #include"well_sorted.h"
 #include"arith_decl_plugin.h"

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,

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;

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<ast,ast> 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<ast> &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<ast> &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<ast> &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){

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.

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;
@@ -1092,10 +1092,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!
     }
 
@@ -1104,7 +1104,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));
@@ -1145,7 +1145,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));
@@ -1447,7 +1447,7 @@ public:
 
         std::vector<ast> vals = cvec;
         if(!is_sat(cnstrs,new_proof,vals))
-            throw "Proof error!";
+            throw iz3_exception("Proof error!");
         std::vector<rational> rat_farkas_coeffs;
         for(unsigned i = 0; i < cvec.size(); i++){
             ast bar = vals[i];
@@ -1455,7 +1455,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<ast> farkas_coeffs;
@@ -1503,7 +1503,7 @@ public:
         ast new_proof;
         std::vector<ast> 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<Iproof::node> my_prems;
@@ -1564,7 +1564,7 @@ public:
         ast new_proof;
         std::vector<ast> 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<Iproof::node> my_prems;

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,

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;