Fixing version printig

Fixing another typo

Better version printing

Not using walksat anymore

More universial printing of SHA1

Also CadiBack

Author: msoos

src/GitSHA1.cpp.in

@@ -58,8 +58,7 @@ const char* CMSat::get_compilation_env()
     "BREAKID_LIBRARIES = @BREAKID_LIBRARIES@ | "
     "BREAKID-VER = @BREAKID_VERSION_MAJOR@.@BREAKID_VERSION_MINOR@ | "
     "BOSPHORUS_LIBRARIES = @BOSPHORUS_LIBRARIES@ | "
-    "BOSPH-VER = @BOSPHORUS_VERSION_MAJOR@.@BOSPHORUS_VERSION_MINOR@ | "
-    ""
+    "BOSPH-VER = @BOSPHORUS_VERSION_MAJOR@.@BOSPHORUS_VERSION_MINOR@"
     ;
     return compilation_env;
 }

src/cryptominisat.cpp

@@ -1077,35 +1077,23 @@ DLL_PUBLIC const char* SATSolver::get_compilation_env()
     return Solver::get_compilation_env();
 }
 
-DLL_PUBLIC std::string SATSolver::get_text_version_info(const char* prefix)
+DLL_PUBLIC std::string SATSolver::get_thanks_info(const char* prefix)
 {
     std::stringstream ss;
-    ss << prefix << "CryptoMiniSat version " << get_version() << endl;
-    ss << prefix << "CMS Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file" << endl;
-    ss << prefix << "CMS SHA revision " << get_version_sha1() << endl;
-    ss << prefix << "Using VMTF and picosat code by Armin Biere from CaDiCaL" << endl;
-    ss << prefix << "Using WalkSAT by Henry Kautz, see Kautz and Selman Pushing the envelope: planning, propositional logic, and stochastic search, AAAI'96," << endl;
+    ss << prefix << "Using VMTF, picosat, CaDiCaL, and CadiBack code by Armin Biere" << endl;
     #ifdef USE_BREAKID
     ss << prefix << "Using BreakID by Devriendt, Bogaerts, Bruynooghe and Denecker" << endl;
     ss << prefix << "Using Bliss graph automorphism library (under LGPL) by Tommi Junttila" << endl;
     ss << prefix << "CMS is GPL licensed due to Bliss being linked. Build without Bliss to get MIT version" << endl;
     #else
     ss << prefix << "CMS is MIT licensed" << endl;
     #endif
-
     ss << prefix << "Using code from 'When Boolean Satisfiability Meets Gauss-E. in a Simplex Way'" << endl;
     ss << prefix << "      by C.-S. Han and J.-H. Roland Jiang in CAV 2012. Fixes by M. Soos" << endl;
     ss << prefix << "Using CCAnr from 'CCAnr: A Conf. Checking Based Local Search Solver [...]'" << endl;
     ss << prefix << "      by Shaowei Cai, Chuan Luo, and Kaile Su, SAT 2015" << endl;
-    ss << prefix << "Using Oracle code from 'Integrating Tree Decompositions [...]" << endl;
-    ss << prefix << "      by Tuukaa Korhonen and Matti Jarvisalo, CP 2021" << endl;
-    ss << prefix << "CMS compilation env " << get_compilation_env() << endl;
-    #ifdef __GNUC__
-    ss << prefix << "CMS compiled with gcc version " << __VERSION__ << endl;
-    #else
-    ss << prefix << "CMS compiled with non-gcc compiler" << endl;
-    #endif
-
+    ss << prefix << "Using Oracle code from 'Integrating Tree Decompositions [...]'" << endl;
+    ss << prefix << "      by Tuukka Korhonen and Matti Jarvisalo, CP 2021";
     return ss.str();
 }
 

src/cryptominisat.h

@@ -192,7 +192,7 @@ namespace CMSat {
         static const char* get_version(); //get solver version in string format
         static const char* get_version_sha1(); //get SHA1 version string of the solver
         static const char* get_compilation_env(); //get compilation environment string
-        static std::string get_text_version_info(const char* prefix = "c ");  //get printable version and copyright text
+        static std::string get_thanks_info(const char* prefix = "c ");  //get printable version and copyright text
 
 
         ////////////////////////////

src/main.cpp

@@ -1360,7 +1360,10 @@ void Main::ban_found_solution() {
 
 void Main::printVersionInfo()
 {
-    cout << solver->get_text_version_info();
+    cout << "c " << "CMS SHA1: " << solver->get_version_sha1() << endl;
+    cout << "c " << "CryptoMiniSat version " << solver->get_version() << endl;
+    cout << "c " << "CMS compilation env " << solver->get_compilation_env();
+    cout << "c " << solver->get_thanks_info("c ") << endl;
 }
 
 int Main::correctReturnValue(const lbool ret) const