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

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2018-02-04 22:43:43 +00:00
parent 333374229d caaaa23438
commit 175273fe27
5 changed files with 29 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/interp/iz3interp.cpp
View file

@ -255,9 +255,11 @@ public:
throw interpolation_failure(msg);
}
catch (const iz3translation::unsupported &) {
TRACE("iz3", tout << "unsupported\n";);
throw interpolation_error();
}
catch (const iz3proof::proof_error &) {
TRACE("iz3", tout << "proof error\n";);
throw interpolation_error();
}
profiling::timer_stop("Proof translation");
@ -304,9 +306,11 @@ public:
throw interpolation_failure(msg);
}
catch (const iz3translation::unsupported &) {
TRACE("iz3", tout << "unsupported\n";);
throw interpolation_error();
}
catch (const iz3proof::proof_error &) {
TRACE("iz3", tout << "proof error\n";);
throw interpolation_error();
}
profiling::timer_stop("Proof translation");

36
src/interp/iz3translate.cpp
View file

@ -49,6 +49,9 @@ using namespace stl_ext;
prover is used.
*/
#define throw_unsupported(_e_) { TRACE("iz3", tout << expr_ref((expr*)_e_.raw(), *_e_.mgr()) << "\n";); throw unsupported(_e_); }
class iz3translation_full : public iz3translation {
public:
@ -983,6 +986,7 @@ public:
ast get_bounded_variable(const ast &ineq, bool &lb){
ast nineq = normalize_inequality(ineq);
ast lhs = arg(nineq,0);
lhs.raw();
switch(op(lhs)){
case Uninterpreted:
lb = false;
@ -993,10 +997,10 @@ public:
else if(arg(lhs,0) == make_int(rational(-1)))
lb = true;
else
throw unsupported();
throw_unsupported(lhs);
return arg(lhs,1);
default:
throw unsupported();
throw_unsupported(lhs);
}
}
@ -1101,10 +1105,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 unsupported(); // can be caused by non-linear arithmetic
throw_unsupported(x); // can be caused by non-linear arithmetic
rational ratio = xcoeff/ycoeff;
if(denominator(ratio) != rational(1))
throw unsupported(); // can this ever happen?
throw_unsupported(y); // can this ever happen?
return make_int(ratio); // better be integer!
}
@ -1113,7 +1117,7 @@ public:
get_assign_bounds_coeffs(proof,farkas_coeffs);
int nargs = num_args(con);
if(nargs != (int)(farkas_coeffs.size()))
throw unsupported(); // should never happen
throw_unsupported(proof); // should never happen
#if 0
if(farkas_coeffs[0] != make_int(rational(1)))
farkas_coeffs[0] = make_int(rational(1));
@ -1237,7 +1241,7 @@ public:
if(pr(rew) == PR_REWRITE){
return clause; // just hope the rewrite does nothing!
}
throw unsupported();
throw_unsupported(rew);
}
@ -1311,7 +1315,7 @@ public:
ast commute_equality_iff(const ast &con){
if(op(con) != Iff || op(arg(con,0)) != Equal)
throw unsupported();
throw_unsupported(con);
return make(Iff,commute_equality(arg(con,0)),commute_equality(arg(con,1)));
}
@ -1337,7 +1341,7 @@ public:
prs.push_back(con);
return clone(proof,prs);
default:
throw unsupported();
throw_unsupported(proof);
}
}
@ -1837,7 +1841,7 @@ public:
for(unsigned i = 0; i < nprems; i++)
if(sym(args[i]) == commute
&& !(dk == PR_TRANSITIVITY || dk == PR_MODUS_PONENS || dk == PR_SYMMETRY || (dk == PR_MONOTONICITY && op(arg(con,0)) == Not)))
throw unsupported();
throw_unsupported(proof);
switch(dk){
case PR_TRANSITIVITY: {
@ -1908,7 +1912,7 @@ public:
int nargs = num_args(con);
if(farkas_coeffs.size() != (unsigned)nargs){
pfgoto(proof);
throw unsupported();
throw_unsupported(proof);
}
for(int i = 0; i < nargs; i++){
ast lit = mk_not(arg(con,i));
@ -1946,7 +1950,7 @@ public:
get_broken_gcd_test_coeffs(proof,farkas_coeffs);
if(farkas_coeffs.size() != nprems){
pfgoto(proof);
throw unsupported();
throw_unsupported(proof);
}
std::vector<Iproof::node> my_prems; my_prems.resize(2);
std::vector<ast> my_prem_cons; my_prem_cons.resize(2);
@ -1969,7 +1973,7 @@ public:
if(args.size() > 0)
res = GomoryCutRule2Farkas(proof, conc(proof), args);
else
throw unsupported();
throw_unsupported(proof);
break;
}
case EqPropagateKind: {
@ -1988,7 +1992,7 @@ public:
break;
}
default:
throw unsupported();
throw_unsupported(proof);
}
break;
case ArrayTheory: {// nothing fancy for this
@ -2000,7 +2004,7 @@ public:
break;
}
default:
throw unsupported();
throw_unsupported(proof);
}
break;
}
@ -2024,7 +2028,7 @@ public:
if(is_local(con))
res = args[0];
else
throw unsupported();
throw_unsupported(con);
break;
}
case PR_COMMUTATIVITY: {
@ -2048,7 +2052,7 @@ public:
IF_VERBOSE(0, verbose_stream() << "Unsupported proof rule: " << expr_ref((expr*)proof.raw(), *proof.mgr()) << "\n";);
// pfgoto(proof);
// SASSERT(0 && "translate_main: unsupported proof rule");
throw unsupported();
throw_unsupported(proof);
}
}

3
src/interp/iz3translate.h
View file

@ -36,7 +36,8 @@ class iz3translation : public iz3base {
/** This is thrown when the proof cannot be translated. */
struct unsupported: public iz3_exception {
unsupported(): iz3_exception("unsupported") { }
raw_ast* m_ast;
unsupported(ast const& a): iz3_exception("unsupported"), m_ast(a.raw()) { }
};
static iz3translation *create(iz3mgr &mgr,

2
src/sat/sat_clause.cpp
View file

@ -33,6 +33,8 @@ namespace sat {
m_frozen(false),
m_reinit_stack(false),
m_inact_rounds(0) {
m_psm = 0;
m_glue = 0;
memcpy(m_lits, lits, sizeof(literal) * sz);
mark_strengthened();
SASSERT(check_approx());

5
src/sat/sat_solver.cpp
View file

@ -2460,10 +2460,7 @@ namespace sat {
// try to use cached implication if available
literal_vector * implied_lits = m_probing.cached_implied_lits(~l);
if (implied_lits) {
literal_vector::iterator it = implied_lits->begin();
literal_vector::iterator end = implied_lits->end();
for (; it != end; ++it) {
literal l2 = *it;
for (literal l2 : *implied_lits) {
// Here, we must check l0 != ~l2.
// l \/ l2 is an implied binary clause.
// However, it may have been deduced using a lemma that has been deleted.