Spacer Global Guidance

src/ast/substitution/substitution.h

@@ -152,7 +152,7 @@ class substitution {
         return find(to_var(v.get_expr()), v.get_offset(), r);
     }
 
-    void get_binding(unsigned binding_num, var_offset& var, expr_offset& r) {
+    void get_binding(unsigned binding_num, var_offset& var, expr_offset& r) const {
         var = m_vars[binding_num];
         VERIFY(m_subst.find(var.first, var.second, r));
     }

src/math/simplex/simplex.cpp

@@ -41,6 +41,10 @@ namespace simplex {
         sparse_matrix_ops::kernel(M, K);
     }
 
+    void kernel_ffe(sparse_matrix<mpq_ext> &M, vector<vector<rational>> &K) {
+      sparse_matrix_ops::kernel_ffe(M, K);
+    }
+
     void ensure_rational_solution(simplex<mpq_ext>& S) {
         rational delta(1);
         for (unsigned i = 0; i < S.get_num_vars(); ++i) {

src/math/simplex/simplex.h

@@ -203,5 +203,6 @@ namespace simplex {
     void ensure_rational_solution(simplex<mpq_ext>& s);
 
     void kernel(sparse_matrix<mpq_ext>& s, vector<vector<rational>>& K);
+    void kernel_ffe(sparse_matrix<mpq_ext> &s, vector<vector<rational>> &K);
 };
 

src/math/simplex/sparse_matrix.h

@@ -168,6 +168,7 @@ namespace simplex {
         void add_var(row r, numeral const& n, var_t var);
         void add(row r, numeral const& n, row src);
         void mul(row r, numeral const& n);
+        void div(row r, numeral const& n);
         void neg(row r);
         void del(row r);
 

src/math/simplex/sparse_matrix_def.h

@@ -432,6 +432,25 @@ namespace simplex {
         }                       
     }
 
+    /**
+       \brief Set row <- n/row
+    */
+    template <typename Ext>
+    void sparse_matrix<Ext>::div(row r, numeral const &n) {
+      SASSERT(!m.is_zero(n));
+      if (m.is_one(n)) {
+        // no op
+      } else if (m.is_minus_one(n)) {
+        neg(r);
+      } else {
+        row_iterator it = row_begin(r);
+        row_iterator end = row_end(r);
+        for (; it != end; ++it) {
+          m.div(it->m_coeff, n, it->m_coeff);
+        }
+      }
+    }
+
     /**
        \brief Delete row.
     */    

src/math/simplex/sparse_matrix_ops.h

@@ -43,7 +43,7 @@ class sparse_matrix_ops {
             for (auto [row, row_entry] : M.get_rows(k)) {
                 if (c[row.id()] != 0) continue;
                 auto &m_jk = row_entry->m_coeff;
-                if (mpq_manager<false>::is_zero(m_jk)) continue;
+                if (m.is_zero(m_jk)) continue;
 
                 // D = rational(-1) / m_jk;
                 m.set(D, m_jk);
@@ -68,9 +68,10 @@ class sparse_matrix_ops {
             K.push_back(vector<rational>());
             for (unsigned i = 0; i < n_vars; ++i) {
                 if (d[i] > 0) {
-                    auto r = sparse_matrix<mpq_ext>::row(d[i] - 1);
+                    auto r = typename sparse_matrix<Ext>::row(d[i] - 1);
                     K.back().push_back(rational(M.get_coeff(r, k)));
-                } else if (i == k)
+                }
+                else if (i == k)
                     K.back().push_back(rational(1));
                 else
                     K.back().push_back(rational(0));
@@ -81,5 +82,157 @@ class sparse_matrix_ops {
     static void kernel(sparse_matrix<mpq_ext> &M, vector<vector<rational>> &K) {
         kernel<mpq_ext>(M, K);
     }
+
+    /// \brief Kernel computation using fraction-free-elimination
+    ///
+    template <typename Ext>
+    static void kernel_ffe(sparse_matrix<Ext> &M, vector<vector<rational>> &K) {
+        using scoped_numeral = typename Ext::scoped_numeral;
+
+        /// Based on 	George Nakos, Peter R. Turner, Robert M. Williams:
+        /// Fraction-free algorithms for linear and polynomial equations. SIGSAM
+        /// Bull. 31(3): 11-19 (1997)
+        vector<unsigned> d, c;
+        unsigned n_vars = M.num_vars(), n_rows = M.num_rows();
+        c.resize(n_rows, 0u);
+        d.resize(n_vars, 0u);
+
+        auto &m = M.get_manager();
+        scoped_numeral m_ik(m);
+        scoped_numeral m_jk(m);
+        scoped_numeral last_pv(m);
+
+        m.set(last_pv, 1);
+
+        for (unsigned k = 0; k < n_vars; ++k) {
+            d[k] = 0;
+            for (auto [row, row_entry] : M.get_rows(k)) {
+                if (c[row.id()] != 0) continue;
+                auto &m_jk_ref = row_entry->m_coeff;
+                if (m.is_zero(m_jk_ref))
+                    // XXX: should not happen, the matrix is sparse
+                    continue;
+
+                // this a pivot column
+                m.set(m_jk, m_jk_ref);
+
+                // ensure that pivot is negative
+                if (m.is_pos(m_jk_ref)) { M.neg(row); }
+                else { m.neg(m_jk); }
+                // m_jk is abs(M[j]][k])
+
+                for (auto row_i : M.get_rows()) {
+                    if (row_i.id() == row.id()) continue;
+
+                    m.set(m_ik, M.get_coeff(row_i, k));
+                    // row_i *= m_jk
+                    M.mul(row_i, m_jk);
+                    if (!m.is_zero(m_ik)) {
+                        // row_i += m_ik * row
+                        M.add(row_i, m_ik, row);
+                    }
+                    M.div(row_i, last_pv);
+                }
+                c[row.id()] = k + 1;
+                d[k] = row.id() + 1;
+                m.set(last_pv, m_jk);
+                break;
+            }
+        }
+
+        for (unsigned k = 0; k < n_vars; ++k) {
+            if (d[k] != 0) continue;
+            K.push_back(vector<rational>());
+            for (unsigned i = 0; i < n_vars; ++i) {
+                if (d[i] > 0) {
+                    auto r = typename sparse_matrix<Ext>::row(d[i] - 1);
+                    K.back().push_back(rational(M.get_coeff(r, k)));
+                }
+                else if (i == k)
+                    K.back().push_back(rational(last_pv));
+                else
+                    K.back().push_back(rational(0));
+            }
+        }
+    }
+
+    static void kernel_ffe(sparse_matrix<mpq_ext> &M,
+                           vector<vector<rational>> &K) {
+        kernel_ffe<mpq_ext>(M, K);
+    }
+
+
+    template <typename Ext>
+    static void kernel_ffe(sparse_matrix<Ext> &M, sparse_matrix<Ext> &K,
+                           vector<unsigned> &basics) {
+        using scoped_numeral = typename Ext::scoped_numeral;
+
+        /// Based on 	George Nakos, Peter R. Turner, Robert M. Williams:
+        /// Fraction-free algorithms for linear and polynomial equations. SIGSAM
+        /// Bull. 31(3): 11-19 (1997)
+        vector<unsigned> d, c;
+        unsigned n_vars = M.num_vars(), n_rows = M.num_rows();
+        c.resize(n_rows, 0u);
+        d.resize(n_vars, 0u);
+
+        auto &m = M.get_manager();
+        scoped_numeral m_ik(m);
+        scoped_numeral m_jk(m);
+        scoped_numeral last_pv(m);
+
+        m.set(last_pv, 1);
+
+        for (unsigned k = 0; k < n_vars; ++k) {
+            d[k] = 0;
+            for (auto [row, row_entry] : M.get_rows(k)) {
+                if (c[row.id()] != 0) continue;
+                auto &m_jk_ref = row_entry->m_coeff;
+                if (m.is_zero(m_jk_ref))
+                    // XXX: should not happen, the matrix is sparse
+                    continue;
+
+                // this a pivot column
+                m.set(m_jk, m_jk_ref);
+
+                // ensure that pivot is negative
+                if (m.is_pos(m_jk_ref)) { M.neg(row); }
+                else { m.neg(m_jk); }
+                // m_jk is abs(M[j]][k])
+
+                for (auto row_i : M.get_rows()) {
+                    if (row_i.id() == row.id()) continue;
+
+                    m.set(m_ik, M.get_coeff(row_i, k));
+                    // row_i *= m_jk
+                    M.mul(row_i, m_jk);
+                    if (!m.is_zero(m_ik)) {
+                        // row_i += m_ik * row
+                        M.add(row_i, m_ik, row);
+                    }
+                    M.div(row_i, last_pv);
+                }
+                c[row.id()] = k + 1;
+                d[k] = row.id() + 1;
+                m.set(last_pv, m_jk);
+                break;
+            }
+        }
+
+        K.ensure_var(n_vars - 1);
+        for (unsigned k = 0; k < n_vars; ++k) {
+            if (d[k] != 0) continue;
+            auto row = K.mk_row();
+            basics.push_back(k);
+            for (unsigned i = 0; i < n_vars; ++i) {
+                if (d[i] > 0) {
+                    auto r = typename sparse_matrix<Ext>::row(d[i] - 1);
+                    K.add_var(row, M.get_coeff(r, k), i);
+                }
+                else if (i == k)
+                  K.add_var(row, last_pv, i);
+            }
+        }
+    }
+
 };
 } // namespace simplex

src/muz/base/fp_params.pyg

@@ -169,7 +169,6 @@ def_module_params('fp',
                           ('spacer.p3.share_lemmas', BOOL, False, 'Share frame lemmas'),
                           ('spacer.p3.share_invariants', BOOL, False, "Share invariants lemmas"),
                           ('spacer.min_level', UINT, 0, 'Minimal level to explore'),
-                          ('spacer.print_json', SYMBOL, '', 'Print pobs tree in JSON format to a given file'),
                           ('spacer.trace_file', SYMBOL, '', 'Log file for progress events'),
                           ('spacer.ctp', BOOL, True, 'Enable counterexample-to-pushing'),
                           ('spacer.use_inc_clause', BOOL, True, 'Use incremental clause to represent trans'),
@@ -181,4 +180,10 @@ def_module_params('fp',
                           ('spacer.use_lim_num_gen', BOOL, False, 'Enable limit numbers generalizer to get smaller numbers'),
                           ('spacer.logic', SYMBOL, '', 'SMT-LIB logic to configure internal SMT solvers'),
                           ('spacer.arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
+                          ('spacer.global', BOOL, False, 'Enable global guidance'),
+                          ('spacer.gg.concretize', BOOL, True, 'Enable global guidance concretize'),
+                          ('spacer.gg.conjecture', BOOL, True, 'Enable global guidance conjecture'),
+                          ('spacer.gg.subsume', BOOL, True, 'Enable global guidance subsume'),
+                          ('spacer.use_iuc', BOOL, True, 'Enable Interpolating Unsat Core(IUC) for lemma generalization'),
+                          ('spacer.expand_bnd', BOOL, False, 'Enable expand-bound lemma generalization'),
                           ))

src/muz/spacer/.clang-format

@@ -0,0 +1,8 @@
+---
+BasedOnStyle: LLVM
+AllowShortFunctionsOnASingleLine: All
+IndentWidth: '4'
+AllowShortBlocksOnASingleLine: true
+AllowShortIfStatementsOnASingleLine: true
+AllowShortLoopsOnASingleLine: true
+...

src/muz/spacer/CMakeLists.txt

@@ -10,6 +10,7 @@ z3_add_component(spacer
   spacer_prop_solver.cpp
   spacer_sym_mux.cpp
   spacer_util.cpp
+  spacer_cluster_util.cpp
   spacer_iuc_solver.cpp
   spacer_legacy_mbp.cpp
   spacer_proof_utils.cpp
@@ -22,12 +23,19 @@ z3_add_component(spacer
   spacer_sem_matcher.cpp
   spacer_quant_generalizer.cpp
   spacer_arith_generalizers.cpp
+  spacer_global_generalizer.cpp
+  spacer_ind_lemma_generalizer.cpp
+  spacer_expand_bnd_generalizer.cpp
+  spacer_cluster.cpp
   spacer_callback.cpp
-  spacer_json.cpp
   spacer_iuc_proof.cpp
   spacer_mbc.cpp
   spacer_pdr.cpp
   spacer_sat_answer.cpp
+  spacer_concretize.cpp
+  spacer_convex_closure.cpp
+  spacer_conjecture.cpp
+  spacer_arith_kernel.cpp
   COMPONENT_DEPENDENCIES
   arith_tactics
   core_tactics

src/muz/spacer/spacer_antiunify.cpp

@@ -155,6 +155,7 @@ void anti_unifier::operator()(expr *e1, expr *e2, expr_ref &res,
             m_pinned.push_back(u);
             m_cache.insert(n1, n2, u);
         }
+        m_todo.pop_back();
     }
 
     expr *r;