mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-14 23:05:26 +00:00
Code Activity

relax the literal check in theory_lra

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-02-14 16:06:57 -08:00
parent 762f265616
commit 697fd37d26
2 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/nla_core.cpp
View file

@ -1231,6 +1231,10 @@ rational core::val(const factorization& f) const {
void core::add_empty_lemma() { void core::add_empty_lemma() {
m_lemma_vec->push_back(lemma()); m_lemma_vec->push_back(lemma());
if (lp_settings().stats().m_nla_calls == 5 && m_lemma_vec->size() == 11) {
TRACE("nla_solver", tout << "bad lemma\n";);
}
} }
void core::negate_relation(unsigned j, const rational& a) { void core::negate_relation(unsigned j, const rational& a) {

4
src/smt/theory_lra.cpp
View file

@ -2221,11 +2221,13 @@ public:
switch (r) { switch (r) {
case l_false: { case l_false: {
m_stats.m_nla_lemmas += lv.size(); m_stats.m_nla_lemmas += lv.size();
int i = 0;
for(const nla::lemma & l : lv) { for(const nla::lemma & l : lv) {
m_lemma = l; //todo avoid the copy m_lemma = l; //todo avoid the copy
m_explanation = l.expl(); m_explanation = l.expl();
m_stats.m_nla_explanations += static_cast<unsigned>(l.expl().size()); m_stats.m_nla_explanations += static_cast<unsigned>(l.expl().size());
false_case_of_check_nla(); false_case_of_check_nla();
i++;
} }
break; break;
} }
@ -3371,7 +3373,7 @@ public:
c.neg(); c.neg();
ctx().mark_as_relevant(c); ctx().mark_as_relevant(c);
} }
TRACE("arith", ctx().display_literals_verbose(tout, m_core) << "\n";);
// DEBUG_CODE( // DEBUG_CODE(
// for (literal const& c : m_core) { // for (literal const& c : m_core) {
// if (ctx().get_assignment(c) == l_true) { // if (ctx().get_assignment(c) == l_true) {