From 20d6543538e993a596b77175a22476e7372d77e5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 4 Feb 2018 12:56:21 -0800 Subject: [PATCH 1/2] set uninitialized fields. Maybe related to #1468 Signed-off-by: Nikolaj Bjorner --- src/interp/iz3interp.cpp | 4 ++++ src/interp/iz3translate.cpp | 33 +++++++++++++++++---------------- src/interp/iz3translate.h | 3 ++- src/sat/sat_clause.cpp | 2 ++ src/sat/sat_solver.cpp | 5 +---- 5 files changed, 26 insertions(+), 21 deletions(-) diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index c1c4588cc..6f918bccb 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -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"); diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index ce2249a88..b108ba047 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -983,6 +983,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 +994,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 +1102,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 +1114,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 +1238,7 @@ public: if(pr(rew) == PR_REWRITE){ return clause; // just hope the rewrite does nothing! } - throw unsupported(); + throw unsupported(rew); } @@ -1311,7 +1312,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 +1338,7 @@ public: prs.push_back(con); return clone(proof,prs); default: - throw unsupported(); + throw unsupported(proof); } } @@ -1837,7 +1838,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 +1909,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 +1947,7 @@ public: get_broken_gcd_test_coeffs(proof,farkas_coeffs); if(farkas_coeffs.size() != nprems){ pfgoto(proof); - throw unsupported(); + throw unsupported(proof); } std::vector my_prems; my_prems.resize(2); std::vector my_prem_cons; my_prem_cons.resize(2); @@ -1969,7 +1970,7 @@ public: if(args.size() > 0) res = GomoryCutRule2Farkas(proof, conc(proof), args); else - throw unsupported(); + throw unsupported(proof); break; } case EqPropagateKind: { @@ -1988,7 +1989,7 @@ public: break; } default: - throw unsupported(); + throw unsupported(proof); } break; case ArrayTheory: {// nothing fancy for this @@ -2000,7 +2001,7 @@ public: break; } default: - throw unsupported(); + throw unsupported(proof); } break; } @@ -2024,7 +2025,7 @@ public: if(is_local(con)) res = args[0]; else - throw unsupported(); + throw unsupported(con); break; } case PR_COMMUTATIVITY: { @@ -2048,7 +2049,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); } } diff --git a/src/interp/iz3translate.h b/src/interp/iz3translate.h index 8ecafbd3a..d80c3b3fe 100755 --- a/src/interp/iz3translate.h +++ b/src/interp/iz3translate.h @@ -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, diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index c5829ae4e..76a1ee8c3 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -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()); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 03c17aaf0..91bff7406 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -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. From bf04c38a639556ef17ef7afc5eea1cd769626b51 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 4 Feb 2018 13:06:14 -0800 Subject: [PATCH 2/2] add logging for #1470 Signed-off-by: Nikolaj Bjorner --- src/interp/iz3translate.cpp | 35 +++++++++++++++++++---------------- 1 file changed, 19 insertions(+), 16 deletions(-) diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index b108ba047..4831e7eaf 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -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: @@ -994,10 +997,10 @@ public: else if(arg(lhs,0) == make_int(rational(-1))) lb = true; else - throw unsupported(lhs); + throw_unsupported(lhs); return arg(lhs,1); default: - throw unsupported(lhs); + throw_unsupported(lhs); } } @@ -1102,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(x); // 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(y); // can this ever happen? + throw_unsupported(y); // can this ever happen? return make_int(ratio); // better be integer! } @@ -1114,7 +1117,7 @@ public: get_assign_bounds_coeffs(proof,farkas_coeffs); int nargs = num_args(con); if(nargs != (int)(farkas_coeffs.size())) - throw unsupported(proof); // 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)); @@ -1238,7 +1241,7 @@ public: if(pr(rew) == PR_REWRITE){ return clause; // just hope the rewrite does nothing! } - throw unsupported(rew); + throw_unsupported(rew); } @@ -1312,7 +1315,7 @@ public: ast commute_equality_iff(const ast &con){ if(op(con) != Iff || op(arg(con,0)) != Equal) - throw unsupported(con); + throw_unsupported(con); return make(Iff,commute_equality(arg(con,0)),commute_equality(arg(con,1))); } @@ -1338,7 +1341,7 @@ public: prs.push_back(con); return clone(proof,prs); default: - throw unsupported(proof); + throw_unsupported(proof); } } @@ -1838,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(proof); + throw_unsupported(proof); switch(dk){ case PR_TRANSITIVITY: { @@ -1909,7 +1912,7 @@ public: int nargs = num_args(con); if(farkas_coeffs.size() != (unsigned)nargs){ pfgoto(proof); - throw unsupported(proof); + throw_unsupported(proof); } for(int i = 0; i < nargs; i++){ ast lit = mk_not(arg(con,i)); @@ -1947,7 +1950,7 @@ public: get_broken_gcd_test_coeffs(proof,farkas_coeffs); if(farkas_coeffs.size() != nprems){ pfgoto(proof); - throw unsupported(proof); + throw_unsupported(proof); } std::vector my_prems; my_prems.resize(2); std::vector my_prem_cons; my_prem_cons.resize(2); @@ -1970,7 +1973,7 @@ public: if(args.size() > 0) res = GomoryCutRule2Farkas(proof, conc(proof), args); else - throw unsupported(proof); + throw_unsupported(proof); break; } case EqPropagateKind: { @@ -1989,7 +1992,7 @@ public: break; } default: - throw unsupported(proof); + throw_unsupported(proof); } break; case ArrayTheory: {// nothing fancy for this @@ -2001,7 +2004,7 @@ public: break; } default: - throw unsupported(proof); + throw_unsupported(proof); } break; } @@ -2025,7 +2028,7 @@ public: if(is_local(con)) res = args[0]; else - throw unsupported(con); + throw_unsupported(con); break; } case PR_COMMUTATIVITY: { @@ -2049,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(proof); + throw_unsupported(proof); } }