From e39107c6829c0962a84f377b8762c09fb5615deb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 10 Jul 2018 21:26:51 -0700
Subject: [PATCH] turn lemma-id into an attribute on the cotext
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/smt_context.cpp | 1 +
src/smt/smt_context.h | 5 ++--
src/smt/smt_context_pp.cpp | 30 ++++++++---------------
src/smt/theory_lra.cpp | 50 ++++++++++++++++++--------------------
4 files changed, 37 insertions(+), 49 deletions(-)
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index be4e8321f..44147c668 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -51,6 +51,7 @@ namespace smt {
m_relevancy_propagator(mk_relevancy_propagator(*this)),
m_random(p.m_random_seed),
m_flushing(false),
+ m_lemma_id(0),
m_progress_callback(nullptr),
m_next_progress_sample(0),
m_fingerprints(m, m_region),
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 77b4ca79c..2ac5695b3 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -88,6 +88,7 @@ namespace smt {
scoped_ptr<relevancy_propagator> m_relevancy_propagator;
random_gen m_random;
bool m_flushing; // (debug support) true when flushing
+ mutable unsigned m_lemma_id;
progress_callback * m_progress_callback;
unsigned m_next_progress_sample;
@@ -1318,12 +1319,12 @@ namespace smt {
void display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, symbol const& logic = symbol::null) const;
- void display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, symbol const& logic = symbol::null) const;
+ unsigned display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent = false_literal, symbol const& logic = symbol::null) const;
void display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs,
literal consequent = false_literal, symbol const& logic = symbol::null) const;
- void display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
+ unsigned display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
unsigned num_antecedent_eqs, enode_pair const * antecedent_eqs,
literal consequent = false_literal, symbol const& logic = symbol::null) const;
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 623141038..8a75dc48c 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -422,21 +422,15 @@ namespace smt {
out << "(check-sat)\n";
}
- static unsigned g_lemma_id = 0;
-
#define BUFFER_SZ 128
- void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const {
- char buffer[BUFFER_SZ];
-#ifdef _WINDOWS
- sprintf_s(buffer, BUFFER_SZ, "lemma_%d.smt2", g_lemma_id);
-#else
- sprintf(buffer, "lemma_%d.smt2", g_lemma_id);
-#endif
- std::ofstream out(buffer);
+ unsigned context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const {
+ std::stringstream strm;
+ strm << "lemma_" << (++m_lemma_id) << ".smt2";
+ std::ofstream out(strm.str());
display_lemma_as_smt_problem(out, num_antecedents, antecedents, consequent, logic);
out.close();
- g_lemma_id++;
+ return m_lemma_id;
}
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
@@ -468,19 +462,15 @@ namespace smt {
out << "(check-sat)\n";
}
- void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
+ unsigned context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
literal consequent, symbol const& logic) const {
- char buffer[BUFFER_SZ];
-#ifdef _WINDOWS
- sprintf_s(buffer, BUFFER_SZ, "lemma_%d.smt2", g_lemma_id);
-#else
- sprintf(buffer, "lemma_%d.smt2", g_lemma_id);
-#endif
- std::ofstream out(buffer);
+ std::stringstream strm;
+ strm << "lemma_" << (++m_lemma_id) << ".smt2";
+ std::ofstream out(strm.str());
display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
out.close();
- g_lemma_id++;
+ return m_lemma_id;
}
/**
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 5f6a48306..3bdd2d784 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1381,6 +1381,11 @@ public:
}
}
}
+ if (!coeffs.empty() && coeffs.begin()->m_value.is_neg()) {
+ offset.neg();
+ lower_bound = !lower_bound;
+ for (auto& kv : coeffs) kv.m_value.neg();
+ }
app_ref atom(m);
app_ref t = coeffs2app(coeffs, rational::zero(), is_int);
@@ -1391,17 +1396,8 @@ public:
atom = a.mk_le(t, a.mk_numeral(offset, is_int));
}
-
-#if 0
- expr_ref atom1(m);
- proof_ref atomp(m);
- ctx().get_rewriter()(atom, atom1, atomp);
- if (!m.is_false(atom1) && !m.is_true(atom1)) {
- atom = to_app(atom1);
- }
-#endif
TRACE("arith", tout << t << ": " << atom << "\n";
- m_solver->print_term(term, tout << "bound atom: "); tout << (lower_bound?" <= ":" >= ") << k << "\n";);
+ m_solver->print_term(term, tout << "bound atom: "); tout << (lower_bound?" >= ":" <= ") << k << "\n";);
ctx().internalize(atom, true);
ctx().mark_as_relevant(atom.get());
return atom;
@@ -1430,7 +1426,7 @@ public:
return l_false;
}
case lp::lia_move::cut: {
- TRACE("arith", tout << "cutn";);
+ TRACE("arith", tout << "cut\n";);
++m_stats.m_gomory_cuts;
// m_explanation implies term <= k
app_ref b = mk_bound(term, k, !upper);
@@ -1529,10 +1525,7 @@ public:
}
}
else {
- enode_vector::const_iterator it = r->begin_parents();
- enode_vector::const_iterator end = r->end_parents();
- for (; it != end; ++it) {
- enode * parent = *it;
+ for (enode * parent : r->get_const_parents()) {
if (is_underspecified(parent->get_owner())) {
return true;
}
@@ -1804,12 +1797,11 @@ public:
lp_api::bound* lo_inf = end, *lo_sup = end;
lp_api::bound* hi_inf = end, *hi_sup = end;
- for (unsigned i = 0; i < bounds.size(); ++i) {
- lp_api::bound& other = *bounds[i];
- if (&other == &b) continue;
- if (b.get_bv() == other.get_bv()) continue;
- lp_api::bound_kind kind2 = other.get_bound_kind();
- rational const& k2 = other.get_value();
+ for (lp_api::bound* other : bounds) {
+ if (other == &b) continue;
+ if (b.get_bv() == other->get_bv()) continue;
+ lp_api::bound_kind kind2 = other->get_bound_kind();
+ rational const& k2 = other->get_value();
if (k1 == k2 && kind1 == kind2) {
// the bounds are equivalent.
continue;
@@ -1819,20 +1811,20 @@ public:
if (kind2 == lp_api::lower_t) {
if (k2 < k1) {
if (lo_inf == end || k2 > lo_inf->get_value()) {
- lo_inf = &other;
+ lo_inf = other;
}
}
else if (lo_sup == end || k2 < lo_sup->get_value()) {
- lo_sup = &other;
+ lo_sup = other;
}
}
else if (k2 < k1) {
if (hi_inf == end || k2 > hi_inf->get_value()) {
- hi_inf = &other;
+ hi_inf = other;
}
}
else if (hi_sup == end || k2 < hi_sup->get_value()) {
- hi_sup = &other;
+ hi_sup = other;
}
}
if (lo_inf != end) mk_bound_axiom(b, *lo_inf);
@@ -2718,7 +2710,9 @@ public:
void dump_conflict() {
if (dump_lemmas()) {
- ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
+ unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
+ (void)id;
+ //SASSERT(id != 55);
}
}
@@ -2736,7 +2730,9 @@ public:
void dump_assign(literal lit) {
if (dump_lemmas()) {
- ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
+ unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
+ (void)id;
+ // SASSERT(id != 71);
}
}