USE_GAUSS is now default

.clang-format

@@ -9,12 +9,12 @@ AlignEscapedNewlinesLeft: true
 AlignOperands:   true
 AlignTrailingComments: true
 AllowAllParametersOfDeclarationOnNextLine: true
-AllowShortBlocksOnASingleLine: false
-AllowShortCaseLabelsOnASingleLine: false
-AllowShortFunctionsOnASingleLine: false
-AllowShortIfStatementsOnASingleLine: false
-AllowShortLoopsOnASingleLine: false
-AllowShortIfStatementsOnASingleLine: false
+AllowShortBlocksOnASingleLine: true
+AllowShortCaseLabelsOnASingleLine: true
+AllowShortFunctionsOnASingleLine: true
+AllowShortIfStatementsOnASingleLine: true
+AllowShortLoopsOnASingleLine: true
+AllowShortIfStatementsOnASingleLine: true
 AlwaysBreakAfterDefinitionReturnType: None
 AlwaysBreakAfterReturnType: None
 AlwaysBreakBeforeMultilineStrings: true
@@ -23,11 +23,11 @@ BinPackArguments: true
 BinPackParameters: true
 BreakBeforeBraces: Custom
 BraceWrapping:
-  AfterClass:      true
-  AfterStruct:     true
+  AfterClass:      false
+  AfterStruct:     false
   AfterControlStatement: false
   AfterEnum:       false
-  AfterFunction:   true
+  AfterFunction:   false
   AfterNamespace:  false
   AfterObjCDeclaration: false
   AfterStruct:     false

src/clauseallocator.cpp

@@ -34,9 +34,7 @@ THE SOFTWARE.
 #include "searcher.h"
 #include "time_mem.h"
 #include "sqlstats.h"
-#ifdef USE_GAUSS
 #include "gaussian.h"
-#endif
 
 #ifdef USE_VALGRIND
 #include "valgrind/valgrind.h"

src/cnf.cpp

@@ -148,9 +148,7 @@ void CNF::enlarge_nonminimial_datastructs(size_t n)
 void CNF::enlarge_minimal_datastructs(size_t n)
 {
     watches.insert(2*n);
-    #ifdef USE_GAUSS
     gwatches.insert(2*n);
-    #endif
     seen.insert(seen.end(), 2*n, 0);
     seen2.insert(seen2.end(), 2*n, 0);
     permDiff.insert(permDiff.end(), 2*n, 0);
@@ -164,12 +162,7 @@ void CNF::save_on_var_memory()
 
     watches.resize(nVars()*2);
     watches.consolidate();
-
-    #ifdef USE_GAUSS
     gwatches.resize(nVars()*2);
-    //TODO
-    //gwatches.consolidate();
-    #endif
 
     for(auto& l: longRedCls) {
         l.shrink_to_fit();

src/cnf.h

@@ -122,9 +122,7 @@ class CNF
     bool ok = true; //If FALSE, state of CNF is UNSAT
 
     watch_array watches;
-    #ifdef USE_GAUSS
     vec<vec<GaussWatched>> gwatches;
-    #endif
     uint32_t num_sls_called = 0;
     vector<VarData> varData;
     branch branch_strategy = branch::vsids;

src/cryptominisat.cpp

@@ -612,10 +612,6 @@ DLL_PUBLIC void SATSolver::set_no_simplify()
 
 DLL_PUBLIC void SATSolver::set_allow_otf_gauss()
 {
-    #ifndef USE_GAUSS
-    std::cerr << "ERROR: CryptoMiniSat was not compiled with GAUSS" << endl;
-    exit(-1);
-    #else
     for (size_t i = 0; i < data->solvers.size(); ++i) {
         Solver& s = *data->solvers[i];
         //s.conf.reconfigure_at = 0;
@@ -628,7 +624,6 @@ DLL_PUBLIC void SATSolver::set_allow_otf_gauss()
         s.conf.xor_detach_reattach = true;
         s.conf.allow_elim_xor_vars = false;
     }
-    #endif
 }
 
 DLL_PUBLIC void SATSolver::set_no_simplify_at_startup()
@@ -1091,10 +1086,8 @@ DLL_PUBLIC std::string SATSolver::get_text_version_info()
     ss << "c Using Bliss graph automorphism library (under LGPL) by Tommi Junttila" << endl;
     #endif
 
-    #ifdef USE_GAUSS
     ss << "c Using code from 'When Boolean Satisfiability Meets Gauss-E. in a Simplex Way'" << endl;
     ss << "c       by C.-S. Han and J.-H. Roland Jiang in CAV 2012. Fixes by M. Soos" << endl;
-    #endif
     ss << "c Using CCAnr from 'CCAnr: A Conf. Checking Based Local Search Solver [...]'" << endl;
     ss << "c       by Shaowei Cai, Chuan Luo, and Kaile Su, SAT 2015" << endl;
     ss << "c CMS compilation env " << get_compilation_env() << endl;

src/distillerlongwithimpl.cpp

@@ -339,9 +339,7 @@ bool DistillerLongWithImpl::sub_str_all_cl_with_watch(
     size_t i = 0;
     size_t j = i;
     ClOffset offset;
-    #ifdef USE_GAUSS
     Clause* cl;
-    #endif
     const size_t end = clauses.size();
     for (
         ; i < end
@@ -361,14 +359,12 @@ bool DistillerLongWithImpl::sub_str_all_cl_with_watch(
             goto copy;
         }
 
-        #ifdef USE_GAUSS
         cl = solver->cl_alloc.ptr(offset);
         if (cl->used_in_xor() &&
             solver->conf.force_preserve_xors)
         {
             goto copy;
         }
-        #endif
 
         if (sub_str_cl_with_watch(offset, alsoStrengthen)) {
             solver->detachClause(offset);

src/hyperengine.cpp

@@ -439,9 +439,7 @@ Lit HyperEngine::analyzeFail(const PropBy propBy)
             break;
         }
 
-#ifdef USE_GAUSS
         case xor_t:
-#endif
         case null_clause_t:
             assert(false);
             break;

src/main.cpp

@@ -848,7 +848,6 @@ void Main::add_supported_options()
      ;
 #endif
 
-#ifdef USE_GAUSS
     po::options_description gaussOptions("Gauss options");
     gaussOptions.add_options()
      ("maxmatrixrows", po::value(&conf.gaussconf.max_matrix_rows)->default_value(conf.gaussconf.max_matrix_rows)
@@ -873,8 +872,6 @@ void Main::add_supported_options()
     ("gaussusefulcutoff", po::value(&conf.gaussconf.min_usefulness_cutoff)->default_value(conf.gaussconf.min_usefulness_cutoff)
         , "Turn off Gauss if less than this many usefulenss ratio is recorded")
     ;
-#endif //USE_GAUSS
-
     help_options_complicated
     .add(generalOptions)
     .add(polar_options)
@@ -910,9 +907,7 @@ void Main::add_supported_options()
     .add(mem_save_opts)
     .add(xorOptions)
     .add(gateOptions)
-    #ifdef USE_GAUSS
     .add(gaussOptions)
-    #endif
     .add(distillOptions)
     .add(miscOptions)
     ;

src/occsimplifier.cpp

@@ -1856,10 +1856,8 @@ bool OccSimplifier::simplify(const bool _startup, const std::string& schedule)
     #endif
 
     assert(solver->detached_xor_repr_cls.empty());
-    #ifdef USE_GAUSS
     assert(solver->gmatrices.empty());
     assert(solver->gqueuedata.empty());
-    #endif
 
     startup = _startup;
     if (!setup()) {

src/propby.h

@@ -73,15 +73,13 @@ class PropBy
             #endif*/
         }
 
-#ifdef USE_GAUSS
         //XOR
         PropBy(const uint32_t matrix_num, const uint32_t row_num):
             data1(matrix_num)
             , type(xor_t)
             , data2(row_num)
         {
         }
-#endif
 
         //BNN prop
         PropBy(uint32_t bnn_idx, void*):

src/propengine.cpp

@@ -36,9 +36,7 @@ THE SOFTWARE.
 #include "varupdatehelper.h"
 #include "watchalgos.h"
 #include "sqlstats.h"
-#ifdef USE_GAUSS
 #include "gaussian.h"
-#endif
 
 using namespace CMSat;
 using std::cout;
@@ -159,9 +157,6 @@ void PropEngine::detach_modified_clause(
     removeWCl(watches[lit2], offset);
 }
 
-
-
-#ifdef USE_GAUSS
 PropBy PropEngine::gauss_jordan_elim(const Lit p, const uint32_t currLevel)
 {
     VERBOSE_PRINT("Gauss searcher::gauss_jordan_elim called, declevel: " << decisionLevel());
@@ -269,7 +264,6 @@ PropBy PropEngine::gauss_jordan_elim(const Lit p, const uint32_t currLevel)
     }
     return PropBy();
 }
-#endif //USE_GAUSS
 
 lbool PropEngine::bnn_prop(
     const uint32_t bnn_idx, uint32_t level, Lit l, BNNPropType prop_t)

src/propengine.h

@@ -259,11 +259,9 @@ class PropEngine: public CNF
     //Clause activities
     double max_cl_act = 0.0;
 
-    #ifdef USE_GAUSS
     enum class gauss_ret {g_cont, g_nothing, g_false};
     vector<EGaussian*> gmatrices;
     vector<GaussQData> gqueuedata;
-    #endif
 
 protected:
     friend class DataSync;
@@ -397,9 +395,7 @@ class PropEngine: public CNF
     );
     void sql_dump_vardata_picktime(uint32_t v, PropBy from);
 
-    #ifdef USE_GAUSS
     PropBy gauss_jordan_elim(const Lit p, const uint32_t currLevel);
-    #endif
 };
 
 inline void PropEngine::new_decision_level()

src/reducedb.h

@@ -32,7 +32,6 @@ namespace CMSat {
 
 class Solver;
 class ClPredictors;
-class ClusteringImp;
 
 struct val_and_pos {
     float val;