porting more

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

src/sat/sat_config.cpp

@@ -264,6 +264,7 @@ namespace sat {
         m_xor_gauss_min_matrix_rows = p.xor_gauss_min_matrix_rows();
         m_xor_gauss_max_matrix_columns = p.xor_gauss_max_matrix_columns();
         m_xor_gauss_max_num_matrices = p.xor_gauss_max_num_matrices();
+        m_xor_gauss_force_use_all_matrices = p.xor_gauss_force_use_all_matrices();
         
         sat_simplifier_params ssp(_p);
         m_elim_vars = ssp.elim_vars();

src/sat/sat_config.h

@@ -207,6 +207,7 @@ namespace sat {
         unsigned           m_xor_gauss_min_matrix_rows;
         unsigned           m_xor_gauss_max_matrix_columns;
         unsigned           m_xor_gauss_max_num_matrices;
+        bool               m_xor_gauss_force_use_all_matrices;
         
 
         config(params_ref const & p);

src/sat/sat_params.pyg

@@ -139,6 +139,7 @@ def_module_params('sat',
                           ('xor.gauss.max_matrix_rows', UINT,  UINT_MAX, 'The maximum matrix size -- no. of rows'),
                           ('xor.gauss.min_matrix_rows', UINT,  0, 'The minimum matrix size -- no. of rows'),
                           ('xor.gauss.max_num_matrices', UINT,  UINT_MAX, 'Maximum number of matrices'),
+                          ('xor.gauss.force_use_all_matrices', BOOL, True, 'tbd'),
                           # ('xor.gauss.autodisable', BOOL, False, 'tbd'),
                           # ('xor.gauss.min_usefulness_cutoff', DOUBLE, 0, 'tbd'),
                           # ('xor.gauss.do_matrix_find', BOOL, True, 'tbd'),

src/sat/smt/xor_matrix_finder.cpp

@@ -1,3 +1,17 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    xor_matrix_finder.cpp
+
+Abstract:
+
+   Based on CMS (crypto minisat by Mate Soos).
+
+--*/
+
+
 #include "sat/smt/xor_matrix_finder.h"
 #include "sat/smt/xor_solver.h"
 
@@ -9,14 +23,11 @@ namespace xr {
     inline bool xor_matrix_finder::belong_same_matrix(const constraint& x) {
         uint32_t comp_num = -1;
         for (sat::bool_var v : x) {
-            if (m_table[v] == l_undef) 
+            if (m_table[v] == l_undef) // Belongs to none, abort
-                //Belongs to none, abort
                 return false;            
-            if (comp_num == -1) 
+            if (comp_num == -1) // Belongs to this one                
-                //Belongs to this one
                 comp_num = m_table[v];            
-            else if (comp_num != m_table[v]) 
+            else if (comp_num != m_table[v]) // Another var in this XOR belongs to another component                
-                //Another var in this XOR belongs to another component
                 return false;            
         }
         return true;
@@ -26,7 +37,7 @@ namespace xr {
 
         SASSERT(!m_sat.inconsistent());
 #if 0
-        SASSERT(m_solver->gmatrices.empty());
+        SASSERT(m_xor.gmatrices.empty());
         can_detach = true;
     
         m_table.clear();
@@ -174,11 +185,8 @@ namespace xr {
                 }
             }
     
-#if 0
+            if (m_sat.get_config().m_xor_gauss_force_use_all_matrices) 
-            if (m_sat.get_config().force_use_all_matrixes) {
                 use_matrix = true;            
-            }
-#endif
     
 #if 0
             if (use_matrix) {

src/sat/smt/xor_matrix_finder.h

@@ -1,3 +1,16 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    xor_matrix_finder.h
+
+Abstract:
+
+   Based on CMS (crypto minisat by Mate Soos).
+
+--*/
+
 #pragma once
 
 #include "util/debug.h"