mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

use a base iz3_exception class for exceptions raised during interpolation

Browse source 
Using a base exception class, derived from z3_exception, makes it possible to
recover gracefully if something goes wrong during the computation of
interpolants.
This commit is contained in:
Alberto Griggio 2015-04-16 19:14:34 +02:00
parent af444beb2e
commit 8e772b428b
13 changed files with 109 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/interp/iz3base.h
View file

@ -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;
}

28
src/interp/iz3exception.h Normal file
View file

@ -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

2
src/interp/iz3interp.cpp
View file

@ -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,

7
src/interp/iz3interp.h
View file

@ -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;

16
src/interp/iz3mgr.cpp
View file

@ -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));
@ -577,7 +577,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
@ -593,7 +593,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];
}
}
@ -623,7 +623,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
@ -639,7 +639,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];
}
}
@ -671,7 +671,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 {
@ -691,7 +691,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;

1
src/interp/iz3mgr.h
View file

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

3
src/interp/iz3pp.h
View file

@ -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,

4
src/interp/iz3proof.h
View file

@ -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;

68
src/interp/iz3proof_itp.cpp
View file

@ -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){

4
src/interp/iz3proof_itp.h
View file

@ -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.

18
src/interp/iz3translate.cpp
View file

@ -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<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];
@ -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<ast> farkas_coeffs;
@ -1471,7 +1471,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;
@ -1532,7 +1532,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;

3
src/interp/iz3translate.h
View file

@ -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,

8
src/interp/iz3translate_direct.cpp
View file

@ -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;