disable order and tangent lemmas on reals

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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

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

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)) {

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 {

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;

src/smt/theory_lra.cpp

@@ -435,6 +435,7 @@ class theory_lra::imp {
 
     void found_unsupported(expr* n) {
         ctx().push_trail(value_trail<context, expr*>(m_not_handled));
+        TRACE("arith", tout << "unsupported " << mk_pp(n, m) << "\n";);
         m_not_handled = n;    
     }