From 16478b415b2603175b91a9ecd0a28b845c66e9ea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 May 2020 13:46:25 -0700 Subject: [PATCH] disable order and tangent lemmas on reals Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_basics_lemmas.cpp | 24 ++++-------------------- src/math/lp/nla_basics_lemmas.h | 2 -- src/math/lp/nla_core.cpp | 24 +++++++++++++++++++++--- src/math/lp/nla_core.h | 3 +++ src/math/lp/nla_order_lemmas.cpp | 2 ++ src/smt/theory_lra.cpp | 1 + 6 files changed, 31 insertions(+), 25 deletions(-) diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index dea499fbf..ea6bf2539 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -359,7 +359,7 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factoriz // x != 0 or y = 0 => |xy| >= |y| void basics::proportion_lemma_model_based(const monic& rm, const factorization& factorization) { - if (factorization_has_real(factorization)) // todo: handle the situaiton when all factors are greater than 1, + if (c().has_real(factorization)) // todo: handle the situaiton when all factors are greater than 1, return; // or smaller than 1 rational rmv = abs(var_val(rm)); if (rmv.is_zero()) { @@ -379,7 +379,7 @@ void basics::proportion_lemma_model_based(const monic& rm, const factorization& bool basics::proportion_lemma_derived(const monic& rm, const factorization& factorization) { // NSB review: why return false? return false; - if (factorization_has_real(factorization)) + if (c().has_real(factorization)) return false; rational rmv = abs(var_val(rm)); if (rmv.is_zero()) { @@ -415,7 +415,7 @@ NSB review: */ void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) { - SASSERT(!mon_has_real(m)); + SASSERT(!c().has_real(m)); new_lemma lemma(c(), "generate_pl_on_mon"); unsigned mon_var = m.var(); rational mv = val(mon_var); @@ -445,7 +445,7 @@ void basics::generate_pl_on_mon(const monic& m, unsigned factor_index) { sign_m*m < 0 or f_i = 0 or \/_{j != i} sign_m*m >= sign_j*f_j */ void basics::generate_pl(const monic& m, const factorization& fc, int factor_index) { - SASSERT(!factorization_has_real(fc)); + SASSERT(!c().has_real(fc)); TRACE("nla_solver", tout << "factor_index = " << factor_index << ", m = " << pp_mon(c(), m); tout << ", fc = " << c().pp(fc); @@ -486,22 +486,6 @@ bool basics::is_separated_from_zero(const factorization& f) const { return true; } -bool basics::factorization_has_real(const factorization& f) const { - for (const factor& fc: f) { - lpvar j = var(fc); - if (!c().var_is_int(j)) - return true; - } - return false; -} - -bool basics::mon_has_real(const monic& m) const { - for (lpvar j : m.vars()) - if (!c().var_is_int(j)) - return true; - return false; -} - // here we use the fact xy = 0 -> x = 0 or y = 0 diff --git a/src/math/lp/nla_basics_lemmas.h b/src/math/lp/nla_basics_lemmas.h index d4ff23ef4..7a18fa0ed 100644 --- a/src/math/lp/nla_basics_lemmas.h +++ b/src/math/lp/nla_basics_lemmas.h @@ -92,7 +92,5 @@ struct basics: common { // -> |fc[factor_index]| <= |rm| void generate_pl(const monic& rm, const factorization& fc, int factor_index); bool is_separated_from_zero(const factorization&) const; - bool factorization_has_real(const factorization&) const; - bool mon_has_real(const monic& m) const; }; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index a5cbfb8f5..4fda82f87 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1061,6 +1061,8 @@ bool core::find_bfc_to_refine(const monic* & m, factorization & bf){ lpvar i = m_to_refine[(k + r) % sz]; m = &m_emons[i]; SASSERT (!check_monic(*m)); + if (has_real(m)) + continue; if (m->size() == 2) { bf.set_mon(m); bf.push_back(factor(m->vars()[0], factor_type::VAR)); @@ -1320,9 +1322,7 @@ void core::update_to_refine_of_var(lpvar j) { } bool core::var_is_big(lpvar j) const { - if (var_is_int(j)) - return false; - return val(j).is_big(); + return !var_is_int(j) && val(j).is_big(); } bool core::has_big_num(const monic& m) const { @@ -1334,6 +1334,24 @@ bool core::has_big_num(const monic& m) const { return false; } +bool core::has_real(const factorization& f) const { + for (const factor& fc: f) { + lpvar j = var(fc); + if (!var_is_int(j)) + return true; + } + return false; +} + +bool core::has_real(const monic& m) const { + for (lpvar j : m.vars()) + if (!var_is_int(j)) + return true; + return false; +} + + + bool core::patch_blocker(lpvar u, const monic& m) const { SASSERT(m_to_refine.contains(m.var())); if (var_is_used_in_a_correct_monic(u)) { diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index a0985c376..7707ba023 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -451,6 +451,9 @@ public: bool patch_blocker(lpvar u, const monic& m) const; bool has_big_num(const monic&) const; bool var_is_big(lpvar) const; + bool has_real(const factorization&) const; + bool has_real(const monic& m) const; + }; // end of core struct pp_mon { diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 4b44c8459..92333454f 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -41,6 +41,8 @@ void order::order_lemma_on_monic(const monic& m) { TRACE("nla_solver_details", tout << "m = " << pp_mon(c(), m);); + if (c().has_real(m)) + return; for (auto ac : factorization_factory_imp(m, _())) { if (ac.size() != 2) continue; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 14f28f34e..bd0afe80f 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -435,6 +435,7 @@ class theory_lra::imp { void found_unsupported(expr* n) { ctx().push_trail(value_trail(m_not_handled)); + TRACE("arith", tout << "unsupported " << mk_pp(n, m) << "\n";); m_not_handled = n; }