mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-07-11 08:53:00 -07:00
commit f09f1a7524
4 changed files with 37 additions and 49 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_context.cpp
View file

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

5
src/smt/smt_context.h
View file

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

30
src/smt/smt_context_pp.cpp
View file

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

50
src/smt/theory_lra.cpp
View file

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