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                 :            :  * SAT Solver.
      11                 :            :  *
      12                 :            :  * Implementation of the cryptominisat for cvc5 (bit-vectors).
      13                 :            :  */
      14                 :            : 
      15                 :            : #include "prop/cryptominisat.h"
      16                 :            : 
      17                 :            : #ifdef CVC5_USE_CRYPTOMINISAT
      18                 :            : 
      19                 :            : #include <cryptominisat5/cryptominisat.h>
      20                 :            : 
      21                 :            : #include "util/resource_manager.h"
      22                 :            : #include "util/statistics_registry.h"
      23                 :            : 
      24                 :            : namespace cvc5::internal {
      25                 :            : namespace prop {
      26                 :            : 
      27                 :            : using CMSatVar = unsigned;
      28                 :            : 
      29                 :            : // helper functions
      30                 :            : namespace {
      31                 :            : 
      32                 :       6853 : CMSat::Lit toInternalLit(SatLiteral lit)
      33                 :            : {
      34         [ -  + ]:       6853 :   if (lit == undefSatLiteral)
      35                 :            :   {
      36                 :          0 :     return CMSat::lit_Undef;
      37                 :            :   }
      38                 :       6853 :   return CMSat::Lit(lit.getSatVariable(), lit.isNegated());
      39                 :            : }
      40                 :            : 
      41                 :          8 : SatLiteral toSatLiteral(CMSat::Lit lit)
      42                 :            : {
      43         [ -  + ]:          8 :   if (lit == CMSat::lit_Undef)
      44                 :            :   {
      45                 :          0 :     return undefSatLiteral;
      46                 :            :   }
      47                 :          8 :   return SatLiteral(lit.var(), lit.sign());
      48                 :            : }
      49                 :            : 
      50                 :        157 : SatValue toSatLiteralValue(CMSat::lbool res)
      51                 :            : {
      52         [ +  + ]:        157 :   if (res == CMSat::l_True) return SAT_VALUE_TRUE;
      53         [ -  + ]:        105 :   if (res == CMSat::l_Undef) return SAT_VALUE_UNKNOWN;
      54 [ -  + ][ -  + ]:        105 :   Assert(res == CMSat::l_False);
                 [ -  - ]
      55                 :        105 :   return SAT_VALUE_FALSE;
      56                 :            : }
      57                 :            : 
      58                 :       2700 : void toInternalClause(const SatClause& clause,
      59                 :            :                       std::vector<CMSat::Lit>& internal_clause)
      60                 :            : {
      61         [ +  + ]:       9530 :   for (const SatLiteral i : clause)
      62                 :            :   {
      63                 :       6830 :     internal_clause.push_back(toInternalLit(i));
      64                 :            :   }
      65 [ -  + ][ -  + ]:       2700 :   Assert(clause.size() == internal_clause.size());
                 [ -  - ]
      66                 :       2700 : }
      67                 :            : 
      68                 :            : }  // namespace
      69                 :            : 
      70                 :         10 : CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry& registry,
      71                 :         10 :                                          const std::string& name)
      72                 :         10 :     : d_solver(new CMSat::SATSolver()),
      73                 :         10 :       d_numVariables(0),
      74                 :         10 :       d_okay(true),
      75                 :         10 :       d_statistics(registry, name),
      76                 :         10 :       d_resmgr(nullptr)
      77                 :            : {
      78                 :         10 : }
      79                 :            : 
      80                 :         10 : void CryptoMinisatSolver::initialize()
      81                 :            : {
      82                 :         10 :   d_true = newVar(false, true);
      83                 :         10 :   d_false = newVar(false, true);
      84                 :            : 
      85                 :         10 :   std::vector<CMSat::Lit> clause(1);
      86                 :         10 :   clause[0] = CMSat::Lit(d_true, false);
      87                 :         10 :   d_solver->add_clause(clause);
      88                 :            : 
      89                 :         10 :   clause[0] = CMSat::Lit(d_false, true);
      90                 :         10 :   d_solver->add_clause(clause);
      91                 :         10 : }
      92                 :            : 
      93                 :         20 : CryptoMinisatSolver::~CryptoMinisatSolver() {}
      94                 :            : 
      95                 :          0 : void CryptoMinisatSolver::setTimeLimit(ResourceManager* resmgr)
      96                 :            : {
      97                 :          0 :   d_resmgr = resmgr;
      98                 :          0 : }
      99                 :            : 
     100                 :         13 : void CryptoMinisatSolver::setMaxTime()
     101                 :            : {
     102         [ -  + ]:         13 :   if (d_resmgr)
     103                 :            :   {
     104                 :            :     // Set time limit to remaining number of seconds.
     105                 :          0 :     d_solver->set_max_time(d_resmgr->getRemainingTime() / 1000.0);
     106                 :            :   }
     107                 :         13 : }
     108                 :            : 
     109                 :          0 : ClauseId CryptoMinisatSolver::addXorClause(const SatClause& clause,
     110                 :            :                                            bool rhs,
     111                 :            :                                            CVC5_UNUSED bool removable)
     112                 :            : {
     113         [ -  - ]:          0 :   Trace("sat::cryptominisat")
     114                 :          0 :       << "Add xor clause " << clause << " = " << rhs << "\n";
     115                 :            : 
     116         [ -  - ]:          0 :   if (!d_okay)
     117                 :            :   {
     118         [ -  - ]:          0 :     Trace("sat::cryptominisat") << "Solver unsat: not adding clause.\n";
     119                 :          0 :     return ClauseIdError;
     120                 :            :   }
     121                 :            : 
     122                 :          0 :   ++(d_statistics.d_xorClausesAdded);
     123                 :            : 
     124                 :            :   // ensure all sat literals have positive polarity by pushing
     125                 :            :   // the negation on the result
     126                 :          0 :   std::vector<CMSatVar> xor_clause;
     127         [ -  - ]:          0 :   for (unsigned i = 0; i < clause.size(); ++i)
     128                 :            :   {
     129                 :          0 :     xor_clause.push_back(toInternalLit(clause[i]).var());
     130                 :          0 :     rhs ^= clause[i].isNegated();
     131                 :            :   }
     132                 :          0 :   const bool res = d_solver->add_xor_clause(xor_clause, rhs);
     133                 :          0 :   d_okay &= res;
     134                 :          0 :   return ClauseIdError;
     135                 :          0 : }
     136                 :            : 
     137                 :       2700 : ClauseId CryptoMinisatSolver::addClause(const SatClause& clause,
     138                 :            :                                         CVC5_UNUSED bool removable)
     139                 :            : {
     140         [ +  - ]:       2700 :   Trace("sat::cryptominisat") << "Add clause " << clause << "\n";
     141                 :            : 
     142         [ -  + ]:       2700 :   if (!d_okay)
     143                 :            :   {
     144         [ -  - ]:          0 :     Trace("sat::cryptominisat") << "Solver unsat: not adding clause.\n";
     145                 :          0 :     return ClauseIdError;
     146                 :            :   }
     147                 :            : 
     148                 :       2700 :   ++(d_statistics.d_clausesAdded);
     149                 :            : 
     150                 :       2700 :   std::vector<CMSat::Lit> internal_clause;
     151                 :       2700 :   toInternalClause(clause, internal_clause);
     152                 :       2700 :   const bool nowOkay = d_solver->add_clause(internal_clause);
     153                 :       2700 :   d_okay &= nowOkay;
     154                 :       2700 :   return ClauseIdError;
     155                 :       2700 : }
     156                 :            : 
     157                 :          0 : bool CryptoMinisatSolver::ok() const { return d_okay; }
     158                 :            : 
     159                 :       1029 : SatVariable CryptoMinisatSolver::newVar(CVC5_UNUSED bool isTheoryAtom,
     160                 :            :                                         CVC5_UNUSED bool canErase)
     161                 :            : {
     162                 :       1029 :   d_solver->new_var();
     163                 :       1029 :   ++d_numVariables;
     164 [ -  + ][ -  + ]:       1029 :   Assert(d_numVariables == d_solver->nVars());
                 [ -  - ]
     165                 :       1029 :   return d_numVariables - 1;
     166                 :            : }
     167                 :            : 
     168                 :          0 : SatVariable CryptoMinisatSolver::trueVar() { return d_true; }
     169                 :            : 
     170                 :          0 : SatVariable CryptoMinisatSolver::falseVar() { return d_false; }
     171                 :            : 
     172                 :          0 : void CryptoMinisatSolver::interrupt() { d_solver->interrupt_asap(); }
     173                 :            : 
     174                 :          0 : SatValue CryptoMinisatSolver::solve()
     175                 :            : {
     176                 :          0 :   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
     177                 :          0 :   ++d_statistics.d_statCallsToSolve;
     178                 :          0 :   setMaxTime();
     179                 :          0 :   return toSatLiteralValue(d_solver->solve());
     180                 :          0 : }
     181                 :            : 
     182                 :          0 : SatValue CryptoMinisatSolver::solve(CVC5_UNUSED long unsigned int& resource)
     183                 :            : {
     184                 :            :   // CMSat::SalverConf conf = d_solver->getConf();
     185                 :          0 :   Unreachable() << "Not sure how to set different limits for calls to solve in "
     186                 :          0 :                    "Cryptominisat";
     187                 :            :   return solve();
     188                 :            : }
     189                 :            : 
     190                 :         13 : SatValue CryptoMinisatSolver::solve(const std::vector<SatLiteral>& assumptions)
     191                 :            : {
     192                 :         13 :   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
     193                 :         13 :   std::vector<CMSat::Lit> assumpts;
     194         [ +  + ]:         36 :   for (const SatLiteral& lit : assumptions)
     195                 :            :   {
     196                 :         23 :     assumpts.push_back(toInternalLit(lit));
     197                 :            :   }
     198                 :         13 :   ++d_statistics.d_statCallsToSolve;
     199                 :         13 :   setMaxTime();
     200                 :         26 :   return toSatLiteralValue(d_solver->solve(&assumpts));
     201                 :         13 : }
     202                 :            : 
     203                 :          4 : void CryptoMinisatSolver::getUnsatAssumptions(
     204                 :            :     std::vector<SatLiteral>& assumptions)
     205                 :            : {
     206         [ +  + ]:         12 :   for (const CMSat::Lit& lit : d_solver->get_conflict())
     207                 :            :   {
     208                 :          8 :     assumptions.push_back(toSatLiteral(~lit));
     209                 :            :   }
     210                 :          4 : }
     211                 :            : 
     212                 :        144 : SatValue CryptoMinisatSolver::value(SatLiteral l)
     213                 :            : {
     214                 :        144 :   const std::vector<CMSat::lbool> model = d_solver->get_model();
     215                 :        144 :   CMSatVar var = l.getSatVariable();
     216 [ -  + ][ -  + ]:        144 :   Assert(var < model.size());
                 [ -  - ]
     217                 :        144 :   CMSat::lbool value = model[var];
     218                 :        288 :   return toSatLiteralValue(value);
     219                 :        144 : }
     220                 :            : 
     221                 :        144 : SatValue CryptoMinisatSolver::modelValue(SatLiteral l) { return value(l); }
     222                 :            : 
     223                 :            : // Satistics for CryptoMinisatSolver
     224                 :            : 
     225                 :         10 : CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry& registry,
     226                 :         10 :                                             const std::string& prefix)
     227                 :            :     : d_statCallsToSolve(
     228                 :         10 :           registry.registerInt(prefix + "cryptominisat::calls_to_solve")),
     229                 :            :       d_xorClausesAdded(
     230                 :         10 :           registry.registerInt(prefix + "cryptominisat::xor_clauses")),
     231                 :         10 :       d_clausesAdded(registry.registerInt(prefix + "cryptominisat::clauses")),
     232                 :         10 :       d_solveTime(registry.registerTimer(prefix + "cryptominisat::solve_time"))
     233                 :            : {
     234                 :         10 : }
     235                 :            : 
     236                 :            : }  // namespace prop
     237                 :            : }  // namespace cvc5::internal
     238                 :            : #endif