Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Implementation of Configuration class, which provides compile-time
      11                 :            :  * configuration information about the cvc5 library.
      12                 :            :  */
      13                 :            : #include "base/configuration.h"
      14                 :            : 
      15                 :            : #include <algorithm>
      16                 :            : #include <sstream>
      17                 :            : #include <string>
      18                 :            : 
      19                 :            : #include "base/Trace_tags.h"
      20                 :            : #include "base/configuration_private.h"
      21                 :            : #include "base/cvc5config.h"
      22                 :            : 
      23                 :            : using namespace std;
      24                 :            : 
      25                 :            : namespace cvc5::internal {
      26                 :            : 
      27                 :        253 : string Configuration::getName() { return CVC5_PACKAGE_NAME; }
      28                 :            : 
      29                 :       4260 : bool Configuration::isSafeBuild() { return IS_SAFE_BUILD; }
      30                 :            : 
      31                 :       4260 : bool Configuration::isStableBuild() { return IS_STABLE_BUILD; }
      32                 :            : 
      33                 :    2287799 : bool Configuration::isDebugBuild() { return IS_DEBUG_BUILD; }
      34                 :            : 
      35                 :       4305 : bool Configuration::isTracingBuild() { return IS_TRACING_BUILD; }
      36                 :            : 
      37                 :    2002528 : bool Configuration::isMuzzledBuild() { return IS_MUZZLED_BUILD; }
      38                 :            : 
      39                 :   31962796 : bool Configuration::isAssertionBuild() { return IS_ASSERTIONS_BUILD; }
      40                 :            : 
      41                 :       4261 : bool Configuration::isCoverageBuild() { return IS_COVERAGE_BUILD; }
      42                 :            : 
      43                 :       4261 : bool Configuration::isProfilingBuild() { return IS_PROFILING_BUILD; }
      44                 :            : 
      45                 :       4260 : bool Configuration::isAsanBuild() { return IS_ASAN_BUILD; }
      46                 :            : 
      47                 :       4260 : bool Configuration::isUbsanBuild() { return IS_UBSAN_BUILD; }
      48                 :            : 
      49                 :       4260 : bool Configuration::isTsanBuild() { return IS_TSAN_BUILD; }
      50                 :            : 
      51                 :       4260 : bool Configuration::isCompetitionBuild() { return IS_COMPETITION_BUILD; }
      52                 :            : 
      53                 :         89 : bool Configuration::isStaticBuild() { return CVC5_STATIC_BUILD; }
      54                 :            : 
      55                 :       4261 : string Configuration::getPackageName() { return CVC5_PACKAGE_NAME; }
      56                 :            : 
      57                 :       4280 : string Configuration::getVersionString() { return CVC5_FULL_VERSION; }
      58                 :            : 
      59                 :         89 : std::string Configuration::copyright()
      60                 :            : {
      61                 :         89 :   std::stringstream ss;
      62                 :            :   ss << "Copyright (c) 2009-2026 by the authors and their institutional\n"
      63                 :         89 :      << "affiliations listed at https://cvc5.github.io/people.html\n\n";
      64                 :            : 
      65         [ +  - ]:         89 :   if (licenseIsGpl())
      66                 :            :   {
      67                 :            :     ss << "This build of cvc5 uses GPLed libraries, and is thus covered by\n"
      68                 :            :        << "the GNU General Public License (GPL) version 3.  Versions of cvc5\n"
      69                 :            :        << "are available that are covered by the (modified) BSD license. If\n"
      70                 :            :        << "you want to license cvc5 under this license, please configure cvc5\n"
      71                 :         89 :        << "with the \"--no-gpl\" option before building from sources.\n\n";
      72                 :            :   }
      73                 :            :   else
      74                 :            :   {
      75                 :            :     ss << "cvc5 is open-source and is covered by the BSD license (modified)."
      76                 :          0 :        << "\n\n";
      77                 :            :   }
      78                 :            : 
      79                 :            :   ss << "THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES.\n"
      80                 :         89 :      << "USE AT YOUR OWN RISK.\n\n";
      81                 :            : 
      82                 :            :   ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n"
      83                 :         89 :      << "third party libraries.\n\n";
      84                 :            : 
      85                 :            :   ss << "  CaDiCaL - Simplified Satisfiability Solver\n"
      86                 :            :      << "  See https://github.com/arminbiere/cadical for copyright "
      87                 :         89 :      << "information.\n\n";
      88                 :            : 
      89         [ -  - ]:         89 :   if (isBuiltWithCryptominisat() || isBuiltWithKissat()
      90 [ -  + ][ -  - ]:         89 :       || isBuiltWithEditline())
                 [ +  - ]
      91                 :            :   {
      92         [ +  - ]:         89 :     if (isBuiltWithCryptominisat())
      93                 :            :     {
      94                 :            :       ss << "  CryptoMiniSat - An Advanced SAT Solver\n"
      95                 :            :          << "  See https://github.com/msoos/cryptominisat for copyright "
      96                 :         89 :          << "information.\n\n";
      97                 :            :     }
      98         [ -  + ]:         89 :     if (isBuiltWithKissat())
      99                 :            :     {
     100                 :            :       ss << "  Kissat - Simplified Satisfiability Solver\n"
     101                 :            :          << "  See https://fmv.jku.at/kissat for copyright "
     102                 :          0 :          << "information.\n\n";
     103                 :            :     }
     104         [ -  + ]:         89 :     if (isBuiltWithEditline())
     105                 :            :     {
     106                 :            :       ss << "  Editline Library\n"
     107                 :            :          << "  See https://thrysoee.dk/editline\n"
     108                 :          0 :          << "  for copyright information.\n\n";
     109                 :            :     }
     110                 :            :   }
     111                 :            : 
     112                 :            :   ss << "  SymFPU - The Symbolic Floating Point Unit\n"
     113                 :            :      << "  See https://github.com/martin-cs/symfpu/tree/main for copyright "
     114                 :         89 :      << "information.\n\n";
     115                 :            : 
     116 [ +  - ][ +  - ]:         89 :   if (isBuiltWithGmp() || isBuiltWithPoly())
                 [ +  - ]
     117                 :            :   {
     118                 :            :     ss << "This version of cvc5 is linked against the following third party\n"
     119                 :            :        << "libraries covered by the LGPLv3 license.\n"
     120                 :         89 :        << "See licenses/lgpl-3.0.txt for more information.\n\n";
     121         [ -  + ]:         89 :     if (isBuiltWithGmp())
     122                 :            :     {
     123                 :            :       ss << "  GMP - Gnu Multi Precision Arithmetic Library\n"
     124                 :          0 :          << "  See http://gmplib.org for copyright information.\n\n";
     125                 :            :     }
     126         [ +  - ]:         89 :     if (isBuiltWithPoly())
     127                 :            :     {
     128                 :            :       ss << "  LibPoly polynomial library\n"
     129                 :            :          << "  See https://github.com/SRI-CSL/libpoly for copyright and\n"
     130                 :         89 :          << "  licensing information.\n\n";
     131                 :            :     }
     132         [ -  + ]:         89 :     if (isStaticBuild())
     133                 :            :     {
     134                 :            :       ss << "cvc5 is statically linked against these libraries. To recompile\n"
     135                 :            :             "this version of cvc5 with different versions of these libraries\n"
     136                 :            :             "follow the instructions on "
     137                 :          0 :             "https://github.com/cvc5/cvc5/blob/main/INSTALL.md\n\n";
     138                 :            :     }
     139                 :            :   }
     140                 :            : 
     141                 :         89 :   if (isBuiltWithCln() || isBuiltWithGlpk() || isBuiltWithCoCoA())
     142                 :            :   {
     143                 :            :     ss << "This version of cvc5 is linked against the following third party\n"
     144                 :            :        << "libraries covered by the GPLv3 license.\n"
     145                 :         89 :        << "See licenses/gpl-3.0.txt for more information.\n\n";
     146         [ +  - ]:         89 :     if (isBuiltWithCln())
     147                 :            :     {
     148                 :            :       ss << "  CLN - Class Library for Numbers\n"
     149                 :         89 :          << "  See http://www.ginac.de/CLN for copyright information.\n\n";
     150                 :            :     }
     151         [ +  - ]:         89 :     if (isBuiltWithGlpk())
     152                 :            :     {
     153                 :            :       ss << "  glpk-cut-log - a modified version of GPLK, "
     154                 :            :          << "the GNU Linear Programming Kit\n"
     155                 :            :          << "  See http://github.com/timothy-king/glpk-cut-log for copyright"
     156                 :         89 :          << " information\n\n";
     157                 :            :     }
     158         [ +  - ]:         89 :     if (isBuiltWithCoCoA())
     159                 :            :     {
     160                 :            :       ss << "  CoCoALib - a computer algebra library\n"
     161                 :            :          << "  See https://cocoa.dima.unige.it/cocoa/cocoalib/index.shtml for "
     162                 :            :             "copyright"
     163                 :         89 :          << " information\n\n";
     164                 :            :     }
     165                 :            :   }
     166                 :            : 
     167                 :            :   ss << "See the file COPYING (distributed with the source code, and with\n"
     168                 :            :      << "all binaries) for the full cvc5 copyright, licensing, and (lack of)\n"
     169                 :         89 :      << "warranty information.\n";
     170                 :        178 :   return ss.str();
     171                 :         89 : }
     172                 :            : 
     173                 :          6 : std::string Configuration::about()
     174                 :            : {
     175                 :          6 :   std::stringstream ss;
     176                 :          6 :   ss << "cvc5 " << getVersionString();
     177         [ +  - ]:          6 :   if (isGitBuild())
     178                 :            :   {
     179                 :          6 :     ss << " [" << getGitInfo() << "]";
     180                 :            :   }
     181                 :          6 :   ss << std::endl;
     182                 :          6 :   ss << "compiled with " << getCompiler() << " on " << getCompiledDateTime();
     183                 :         12 :   return ss.str();
     184                 :          6 : }
     185                 :            : 
     186                 :          5 : std::string Configuration::aboutAndCopyright()
     187                 :            : {
     188                 :          5 :   std::stringstream ss;
     189                 :          5 :   ss << about();
     190                 :          5 :   ss << std::endl << std::endl;
     191                 :          5 :   ss << copyright();
     192                 :         10 :   return ss.str();
     193                 :          5 : }
     194                 :            : 
     195                 :         89 : bool Configuration::licenseIsGpl() { return IS_GPL_BUILD; }
     196                 :            : 
     197                 :       4438 : bool Configuration::isBuiltWithGmp() { return IS_GMP_BUILD; }
     198                 :            : 
     199                 :       4438 : bool Configuration::isBuiltWithCln() { return IS_CLN_BUILD; }
     200                 :            : 
     201                 :       4349 : bool Configuration::isBuiltWithGlpk() { return IS_GLPK_BUILD; }
     202                 :            : 
     203                 :       4550 : bool Configuration::isBuiltWithCryptominisat()
     204                 :            : {
     205                 :       4550 :   return IS_CRYPTOMINISAT_BUILD;
     206                 :            : }
     207                 :            : 
     208                 :       4439 : bool Configuration::isBuiltWithKissat() { return IS_KISSAT_BUILD; }
     209                 :            : 
     210                 :       4349 : bool Configuration::isBuiltWithEditline() { return IS_EDITLINE_BUILD; }
     211                 :            : 
     212                 :       4440 : bool Configuration::isBuiltWithPoly() { return IS_POLY_BUILD; }
     213                 :            : 
     214                 :       4349 : bool Configuration::isBuiltWithCoCoA() { return IS_COCOA_BUILD; }
     215                 :            : 
     216                 :       4260 : bool Configuration::isBuiltWithPortfolio() { return IS_PORTFOLIO_BUILD; }
     217                 :            : 
     218                 :         52 : const std::vector<std::string>& Configuration::getTraceTags()
     219                 :            : {
     220                 :         52 :   return Trace_tags;
     221                 :            : }
     222                 :            : 
     223                 :          0 : bool Configuration::isTraceTag(const std::string& tag)
     224                 :            : {
     225                 :          0 :   return std::find(Trace_tags.begin(), Trace_tags.end(), tag)
     226                 :          0 :          != Trace_tags.end();
     227                 :            : }
     228                 :            : 
     229                 :       4266 : bool Configuration::isGitBuild() { return GIT_BUILD; }
     230                 :            : 
     231                 :       4266 : std::string Configuration::getGitInfo() { return CVC5_GIT_INFO; }
     232                 :            : 
     233                 :          6 : std::string Configuration::getCompiler()
     234                 :            : {
     235                 :          6 :   stringstream ss;
     236                 :            : #ifdef __GNUC__
     237                 :          6 :   ss << "GCC";
     238                 :            : #else  /* __GNUC__ */
     239                 :            :   ss << "unknown compiler";
     240                 :            : #endif /* __GNUC__ */
     241                 :            : #ifdef __VERSION__
     242                 :          6 :   ss << " version " << __VERSION__;
     243                 :            : #else  /* __VERSION__ */
     244                 :            :   ss << ", unknown version";
     245                 :            : #endif /* __VERSION__ */
     246                 :         12 :   return ss.str();
     247                 :          6 : }
     248                 :            : 
     249                 :          6 : std::string Configuration::getCompiledDateTime()
     250                 :            : {
     251                 :          6 :   return __DATE__ " " __TIME__;
     252                 :            : }
     253                 :            : 
     254                 :            : }  // namespace cvc5::internal