Add new probes for arithmetic. Check for LIA and LRA (and activate qe if applicable). Modify echo tactic to send results to the regular stream.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/ast/rewriter/arith_rewriter.cpp

@@ -981,14 +981,6 @@ br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) {
         result = m_util.mk_numeral(a, false);
         return BR_DONE;
     }
-#if 0
-    // The following rewriting rule is not correct.
-    // It is used only for making experiments.
-    if (m_util.is_to_int(arg)) {
-        result = to_app(arg)->get_arg(0);
-        return BR_DONE;
-    }
-#endif
     // push to_real over OP_ADD, OP_MUL
     if (m_push_to_real) {
         if (m_util.is_add(arg) || m_util.is_mul(arg)) {

src/cmd_context/echo_tactic.cpp

@@ -34,9 +34,9 @@ public:
                             expr_dependency_ref & core) {
         #pragma omp critical (echo_tactic)
         {
-            m_ctx.diagnostic_stream() << m_msg;
+            m_ctx.regular_stream() << m_msg;
             if (m_newline)
-                m_ctx.diagnostic_stream() << std::endl;
+                m_ctx.regular_stream() << std::endl;
         }
         skip_tactic::operator()(in, result, mc, pc, core);
     }

src/tactic/arith/probe_arith.cpp

@@ -313,23 +313,28 @@ struct is_non_nira_functor {
     bool          m_int;
     bool          m_real;
     bool          m_quant;
+    bool          m_linear;
 
-    is_non_nira_functor(ast_manager & _m, bool _int, bool _real, bool _quant):m(_m), u(m), m_int(_int), m_real(_real), m_quant(_quant) {}
+    is_non_nira_functor(ast_manager & _m, bool _int, bool _real, bool _quant, bool linear):m(_m), u(m), m_int(_int), m_real(_real), m_quant(_quant), m_linear(linear) {}
+
+    void throw_found() {
+        throw found();
+    }
 
     void operator()(var * x) {
         if (!m_quant)
-            throw found();
+            throw_found();
         sort * s = x->get_sort();
         if (m_int && u.is_int(s))
             return;
         if (m_real && u.is_real(s))
             return;
-        throw found();
+        throw_found();
     }
     
     void operator()(quantifier *) { 
         if (!m_quant)
-            throw found(); 
+            throw_found(); 
     }
     
     bool compatible_sort(app * n) const {
@@ -344,35 +349,92 @@ struct is_non_nira_functor {
 
     void operator()(app * n) {
         if (!compatible_sort(n))
-            throw found();
+            throw_found();
         family_id fid = n->get_family_id();
         if (fid == m.get_basic_family_id())
             return; 
-        if (fid == u.get_family_id())
+        if (fid == u.get_family_id()) {
+            switch (n->get_decl_kind()) {
+            case OP_LE:  case OP_GE: case OP_LT: case OP_GT:
+            case OP_ADD: case OP_UMINUS: case OP_SUB: case OP_ABS: 
+            case OP_NUM:
+                return;
+            case OP_MUL:
+                if (m_linear) {
+                    if (n->get_num_args() != 2)
+                        throw_found();
+                    if (!u.is_numeral(n->get_arg(0)))
+                        throw_found();
+                }
+                return;
+            case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
+                if (m_linear && !u.is_numeral(n->get_arg(1)))
+                    throw_found();
+                return;
+            case OP_IS_INT:
+                if (m_real)
+                    throw_found();
+                return;
+            case OP_TO_INT:
+            case OP_TO_REAL:
+                return;
+            case OP_POWER:
+                if (m_linear)
+                    throw_found();
+                return;
+            case OP_IRRATIONAL_ALGEBRAIC_NUM:
+                if (m_linear || !m_real)
+                    throw_found();
+                return;
+            default:
+                throw_found();
+            }
             return;
+        }
+
         if (is_uninterp_const(n))
             return;
-        throw found();
+        throw_found();
     }
 };
 
 static bool is_qfnia(goal const & g) {
-    is_non_nira_functor p(g.m(), true, false, false);
+    is_non_nira_functor p(g.m(), true, false, false, false);
     return !test(g, p);
 }
 
 static bool is_qfnra(goal const & g) {
-    is_non_nira_functor p(g.m(), false, true, false);
+    is_non_nira_functor p(g.m(), false, true, false, false);
     return !test(g, p);
 }
 
 static bool is_nia(goal const & g) {
-    is_non_nira_functor p(g.m(), true, false, true);
+    is_non_nira_functor p(g.m(), true, false, true, false);
     return !test(g, p);
 }
 
 static bool is_nra(goal const & g) {
-    is_non_nira_functor p(g.m(), false, true, true);
+    is_non_nira_functor p(g.m(), false, true, true, false);
+    return !test(g, p);
+}
+
+static bool is_nira(goal const & g) {
+    is_non_nira_functor p(g.m(), true, true, true, false);
+    return !test(g, p);
+}
+
+static bool is_lra(goal const & g) {
+    is_non_nira_functor p(g.m(), false, true, true, true);
+    return !test(g, p);
+}
+
+static bool is_lia(goal const & g) {
+    is_non_nira_functor p(g.m(), true, false, true, true);
+    return !test(g, p);
+}
+
+static bool is_lira(goal const & g) {
+    is_non_nira_functor p(g.m(), true, true, true, true);
     return !test(g, p);
 }
 
@@ -404,6 +466,34 @@ public:
     }
 };
 
+class is_nira_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return is_nira(g);
+    }
+};
+
+class is_lia_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return is_lia(g);
+    }
+};
+
+class is_lra_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return is_lra(g);
+    }
+};
+
+class is_lira_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return is_lira(g);
+    }
+};
+
 probe * mk_is_qfnia_probe() {
     return alloc(is_qfnia_probe);
 }
@@ -419,3 +509,19 @@ probe * mk_is_nia_probe() {
 probe * mk_is_nra_probe() {
     return alloc(is_nra_probe);
 }
+
+probe * mk_is_nira_probe() {
+    return alloc(is_nira_probe);
+}
+
+probe * mk_is_lia_probe() {
+    return alloc(is_lia_probe);
+}
+
+probe * mk_is_lra_probe() {
+    return alloc(is_lra_probe);
+}
+
+probe * mk_is_lira_probe() {
+    return alloc(is_lira_probe);
+}

src/tactic/arith/probe_arith.h

@@ -49,11 +49,19 @@ probe * mk_is_qfnia_probe();
 probe * mk_is_qfnra_probe();
 probe * mk_is_nia_probe();
 probe * mk_is_nra_probe();
+probe * mk_is_nira_probe();
+probe * mk_is_lia_probe();
+probe * mk_is_lra_probe();
+probe * mk_is_lira_probe();
 
 /*
   ADD_PROBE("is-qfnia", "true if the goal is in QF_NIA (quantifier-free nonlinear integer arithmetic).", "mk_is_qfnia_probe()")
   ADD_PROBE("is-qfnra", "true if the goal is in QF_NRA (quantifier-free nonlinear real arithmetic).", "mk_is_qfnra_probe()")
   ADD_PROBE("is-nia", "true if the goal is in NIA (nonlinear integer arithmetic, formula may have quantifiers).", "mk_is_nia_probe()")
   ADD_PROBE("is-nra", "true if the goal is in NRA (nonlinear real arithmetic, formula may have quantifiers).", "mk_is_nra_probe()")
+  ADD_PROBE("is-nira", "true if the goal is in NIRA (nonlinear integer and real arithmetic, formula may have quantifiers).", "mk_is_nira_probe()")
+  ADD_PROBE("is-lia", "true if the goal is in LIA (linear integer arithmetic, formula may have quantifiers).", "mk_is_lia_probe()")
+  ADD_PROBE("is-lra", "true if the goal is in LRA (linear real arithmetic, formula may have quantifiers).", "mk_is_lra_probe()")
+  ADD_PROBE("is-lira", "true if the goal is in LIRA (linear integer and real arithmetic, formula may have quantifiers).", "mk_is_lira_probe()")
 */
 #endif

src/tactic/portfolio/default_tactic.cpp

@@ -26,22 +26,18 @@ Notes:
 #include"qfnra_tactic.h"
 #include"nra_tactic.h"
 #include"probe_arith.h"
+#include"quant_tactics.h"
 
 tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
     tactic * st = using_params(and_then(mk_simplify_tactic(m),
-                                        cond(mk_is_qfbv_probe(),
-                                             mk_qfbv_tactic(m),
-                                             cond(mk_is_qflia_probe(),
-                                                  mk_qflia_tactic(m),
-                                                  cond(mk_is_qflra_probe(),
-                                                       mk_qflra_tactic(m),
-                                                       cond(mk_is_qfnra_probe(),
-                                                            mk_qfnra_tactic(m),
-                                                            cond(mk_is_qfnia_probe(),
-                                                                 mk_qfnia_tactic(m),
-                                                                 cond(mk_is_nra_probe(),
-                                                                      mk_nra_tactic(m),
-                                                                      mk_smt_tactic()))))))),
+                                        cond(mk_is_qfbv_probe(),  mk_qfbv_tactic(m),
+                                        cond(mk_is_qflia_probe(), mk_qflia_tactic(m),
+                                        cond(mk_is_qflra_probe(), mk_qflra_tactic(m),
+                                        cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m),
+                                        cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m),
+                                        cond(mk_is_nra_probe(),   mk_nra_tactic(m),
+                                        cond(mk_is_lira_probe(),  mk_lira_tactic(m, p),
+                                             mk_smt_tactic())))))))),
                                p);
     return st;
 }

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -72,6 +72,8 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
         return mk_uflra_tactic(m, p);
     else if (logic=="LRA")
         return mk_lra_tactic(m, p);
+    else if (logic=="LIA")
+        return mk_lia_tactic(m, p);
     else if (logic=="UFBV")
         return mk_ufbv_tactic(m, p);
     else if (logic=="BV")

src/tactic/smtlogics/quant_tactics.cpp

@@ -104,3 +104,10 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
     return st;
 }
 
+tactic * mk_lia_tactic(ast_manager & m, params_ref const & p) {
+    return mk_lra_tactic(m, p);
+}
+
+tactic * mk_lira_tactic(ast_manager & m, params_ref const & p) {
+    return mk_lra_tactic(m, p);
+}

src/tactic/smtlogics/quant_tactics.h

@@ -29,5 +29,7 @@ tactic * mk_auflia_tactic(ast_manager & m, params_ref const & p);
 tactic * mk_auflira_tactic(ast_manager & m, params_ref const & p);
 tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p);
 tactic * mk_lra_tactic(ast_manager & m, params_ref const & p);
+tactic * mk_lia_tactic(ast_manager & m, params_ref const & p);
+tactic * mk_lira_tactic(ast_manager & m, params_ref const & p);
 
 #endif