making new arith solver default for LIA (Z3Prover#67)

* log quantifiers only if present Signed-off-by: Nikolaj Bjorner <[email protected]> * merge and fix some warnings Signed-off-by: Nikolaj Bjorner <[email protected]> * set new arith as default for LIA Signed-off-by: Nikolaj Bjorner <[email protected]>
NikolajBjorner · May 30, 2018 · 137e2b4 · 137e2b4
1 parent 5940843
commit 137e2b4
Show file tree

Hide file tree

Showing 8 changed files with 62 additions and 88 deletions.
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
@@ -1838,7 +1838,7 @@ namespace pdr {
                     m_fparams.m_arith_eq2ineq = true;
                 }
                 else {
-                    m_fparams.m_arith_mode = AS_ARITH;
+                    m_fparams.m_arith_mode = AS_OLD_ARITH;
                     m_fparams.m_arith_eq2ineq = false;
                 }
             }

diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h
@@ -25,11 +25,11 @@ Revision History:
 enum arith_solver_id {
     AS_NO_ARITH,              // 0
     AS_DIFF_LOGIC,            // 1
-    AS_ARITH,                 // 2
+    AS_OLD_ARITH,             // 2
     AS_DENSE_DIFF_LOGIC,      // 3
     AS_UTVPI,                 // 4
     AS_OPTINF,                // 5
-    AS_LRA                    // 6
+    AS_NEW_ARITH              // 6
 };
 
 enum bound_prop_mode {
@@ -113,7 +113,7 @@ struct theory_arith_params {
     theory_arith_params(params_ref const & p = params_ref()):
         m_arith_eq2ineq(false),
         m_arith_process_all_eqs(false),
-        m_arith_mode(AS_ARITH),
+        m_arith_mode(AS_NEW_ARITH),
         m_arith_auto_config_simplex(false),
         m_arith_blands_rule_threshold(1000),
         m_arith_propagate_eqs(true),

diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
@@ -732,11 +732,11 @@ namespace smt {
     }
 
     void setup::setup_i_arith() {
-        if (AS_LRA == m_params.m_arith_mode) {
-            setup_r_arith();
+        if (AS_OLD_ARITH == m_params.m_arith_mode) {
+            m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
         }
         else {
-            m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
+            setup_r_arith();
         }
     }
 
@@ -749,7 +749,7 @@ namespace smt {
         case AS_OPTINF:
             m_context.register_plugin(alloc(smt::theory_inf_arith, m_manager, m_params));            
             break;
-        case AS_LRA:
+        case AS_NEW_ARITH:
             setup_r_arith();
             break;
         default:
@@ -813,12 +813,15 @@ namespace smt {
         case AS_OPTINF:
             m_context.register_plugin(alloc(smt::theory_inf_arith, m_manager, m_params));            
             break;
-        case AS_LRA:
-            setup_r_arith();
+        case AS_OLD_ARITH:
+            if (m_params.m_arith_int_only && int_only)
+                m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
+            else
+                m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
             break;
         default:
             if (m_params.m_arith_int_only && int_only)
-                m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
+                setup_i_arith();
             else
                 m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
             break;

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -2533,18 +2533,18 @@ class theory_lra::imp {
     struct scoped_arith_mode {
         smt_params& p;
         scoped_arith_mode(smt_params& p) : p(p) {
-            p.m_arith_mode = AS_ARITH;
+            p.m_arith_mode = AS_OLD_ARITH;
         }
         ~scoped_arith_mode() {
-            p.m_arith_mode = AS_LRA;
+            p.m_arith_mode = AS_NEW_ARITH;
         }
     };
 
     bool validate_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);
         }
-        if (m_arith_params.m_arith_mode != AS_LRA) return true;
+        if (m_arith_params.m_arith_mode != AS_NEW_ARITH) return true;
         scoped_arith_mode _sa(ctx().get_fparams());
         context nctx(m, ctx().get_fparams(), ctx().get_params());
         add_background(nctx);
@@ -2559,7 +2559,7 @@ class theory_lra::imp {
         if (dump_lemmas()) {                
             ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
         }
-        if (m_arith_params.m_arith_mode != AS_LRA) return true;
+        if (m_arith_params.m_arith_mode != AS_NEW_ARITH) return true;
         scoped_arith_mode _sa(ctx().get_fparams());
         context nctx(m, ctx().get_fparams(), ctx().get_params());
         m_core.push_back(~lit);
@@ -2574,7 +2574,7 @@ class theory_lra::imp {
     }
 
     bool validate_eq(enode* x, enode* y) {
-        if (m_arith_params.m_arith_mode == AS_LRA) return true;
+        if (m_arith_params.m_arith_mode == AS_NEW_ARITH) return true;
         context nctx(m, ctx().get_fparams(), ctx().get_params());
         add_background(nctx);
         nctx.assert_expr(m.mk_not(m.mk_eq(x->get_owner(), y->get_owner())));

diff --git a/src/util/lp/hnf.h b/src/util/lp/hnf.h
@@ -20,7 +20,6 @@ Let $e_i$ be a vector of length $m$ with all elements equal to $0$ and
 We find  $e_iH^{-1} = f$ by solving $e_i = fH$ and then $fA$ gives us $t$.
 
 Author:
-    Nikolaj Bjorner (nbjorner)
     Lev Nachmanson (levnach)
 
 Revision History:
@@ -502,9 +501,7 @@ class hnf {
             m_W[k][j] -= u * m_W[k][m_i];
             //  m_W[k][j] = mod_R_balanced(m_W[k][j]);
         }
-    }
-
-
+    }    
 
     bool is_unit_matrix(const M& u) const {
         unsigned m = u.row_count();

diff --git a/src/util/lp/hnf_cutter.h b/src/util/lp/hnf_cutter.h
@@ -11,7 +11,6 @@ Module Name:
 
 Author:
     Lev Nachmanson (levnach)
-    Nikolaj Bjorner (nbjorner)
 
 Revision History:
 
@@ -35,7 +34,7 @@ class hnf_cutter {
     unsigned                   m_column_count;
     lp_settings &              m_settings;
 public:
-    hnf_cutter(lp_settings & settings) : m_settings(settings) {}
+    hnf_cutter(lp_settings & settings) : m_row_count(0), m_column_count(0), m_settings(settings) {}
 
     unsigned row_count() const {
         return m_row_count;
@@ -103,16 +102,8 @@ class hnf_cutter {
         int ret = -1;
         int n = 0;
         for (int i = 0; i < static_cast<int>(b.size()); i++) {
-            if (!is_int(b[i])) {
-                if (n == 0 ) {
-                    lp_assert(ret == -1);
-                    n = 1;
-                    ret = i;
-                } else {
-                    if (m_settings.random_next() % (++n) == 0) {
-                       ret = i;
-                    }
-                }
+            if (!is_int(b[i]) && (m_settings.random_next() % (++n) == 0)) {
+                ret = i;
             }
         }
         return ret;
@@ -182,7 +173,7 @@ class hnf_cutter {
 
         vector<mpq> b = create_b(basis_rows);
         lp_assert(m_A * x0 == b);
-        vector<mpq> bcopy = b;
+        vector<mpq> bcopy = b;  // debug
         find_h_minus_1_b(h.W(), b);
         lp_assert(bcopy == h.W().take_first_n_columns(b.size()) * b);
         int cut_row = find_cut_row_index(b);