From 6616a75283b3ac381bdec0eee1ca92d4b6e141ea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Oct 2022 20:06:28 -0700 Subject: [PATCH] porting more Signed-off-by: Nikolaj Bjorner --- src/sat/sat_config.cpp | 1 + src/sat/sat_config.h | 1 + src/sat/sat_params.pyg | 17 ++++++++-------- src/sat/smt/xor_matrix_finder.cpp | 34 +++++++++++++++++++------------ src/sat/smt/xor_matrix_finder.h | 13 ++++++++++++ 5 files changed, 45 insertions(+), 21 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 73fdea20f..1c54d6f97 100644 --- a/src/sat/sat_config.cpp +++ b/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(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index fca046d73..f8ea7b6dc 100644 --- a/src/sat/sat_config.h +++ b/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); diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 26a18f273..d02513f06 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -128,7 +128,7 @@ def_module_params('sat', # Xor parameters ('xor.enable', BOOL, False, 'enable xor solver plugin in combination with pure SAT solving'), - # Pull in other xor parameters as they are determined to be relevant + # Pull in other xor parameters as they are determined to be relevant # ('xor.max_to_find', UINT, 'tbd'), # ('xor.max_to_find_slow', UINT, 'tbd'), # ('xor.max_xor_matrix, UINT64, 'tbd'), @@ -136,12 +136,13 @@ def_module_params('sat', # ('xor.var_per_cut', UINT, 'tbd'), # ('xor.force_preserve_xors', BOOL, 'tbd'), ('xor.gauss.max_matrix_columns', UINT, UINT_MAX, 'tbd'), - ('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.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'), - # ('xor.gauss.min_xor_clauses', UINT, 2, 'tbd'), - # ('xor.gauss.max_xor_clauses, UINT, 500000, 'tbd') + # ('xor.gauss.min_usefulness_cutoff', DOUBLE, 0, 'tbd'), + # ('xor.gauss.do_matrix_find', BOOL, True, 'tbd'), + # ('xor.gauss.min_xor_clauses', UINT, 2, 'tbd'), + # ('xor.gauss.max_xor_clauses, UINT, 500000, 'tbd') )) diff --git a/src/sat/smt/xor_matrix_finder.cpp b/src/sat/smt/xor_matrix_finder.cpp index a2883faeb..bf43dbb0c 100644 --- a/src/sat/smt/xor_matrix_finder.cpp +++ b/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) - //Belongs to none, abort + if (m_table[v] == l_undef) // Belongs to none, abort return false; - if (comp_num == -1) - //Belongs to this one + if (comp_num == -1) // Belongs to this one comp_num = m_table[v]; - else if (comp_num != m_table[v]) - //Another var in this XOR belongs to another component + else if (comp_num != m_table[v]) // 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(); @@ -117,7 +128,7 @@ namespace xr { } for (constraint* x : m_xor.m_constraints) { - //take 1st variable to check which matrix it's in. + // take 1st variable to check which matrix it's in. const uint32_t matrix = m_table[(*x)[0]]; SASSERT(matrix < m_matrix_no); @@ -174,11 +185,8 @@ namespace xr { } } -#if 0 - if (m_sat.get_config().force_use_all_matrixes) { - use_matrix = true; - } -#endif + if (m_sat.get_config().m_xor_gauss_force_use_all_matrices) + use_matrix = true; #if 0 if (use_matrix) { diff --git a/src/sat/smt/xor_matrix_finder.h b/src/sat/smt/xor_matrix_finder.h index bbec3424c..b060dfc52 100644 --- a/src/sat/smt/xor_matrix_finder.h +++ b/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"