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 minisat interface for cvc5.
      13                 :            :  */
      14                 :            : 
      15                 :            : #include "prop/minisat/minisat.h"
      16                 :            : 
      17                 :            : #include "options/base_options.h"
      18                 :            : #include "options/decision_options.h"
      19                 :            : #include "options/proof_options.h"
      20                 :            : #include "options/prop_options.h"
      21                 :            : #include "options/smt_options.h"
      22                 :            : #include "proof/clause_id.h"
      23                 :            : #include "prop/minisat/simp/SimpSolver.h"
      24                 :            : #include "util/statistics_stats.h"
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : namespace prop {
      28                 :            : 
      29                 :            : //// DPllMinisatSatSolver
      30                 :            : 
      31                 :      51568 : MinisatSatSolver::MinisatSatSolver(Env& env, StatisticsRegistry& registry)
      32                 :            :     : EnvObj(env),
      33                 :      51568 :       d_minisat(nullptr),
      34                 :     103136 :       d_context(context()),
      35                 :      51568 :       d_assumptions(),
      36                 :     103136 :       d_statistics(registry)
      37                 :            : {
      38                 :      51568 : }
      39                 :            : 
      40                 :     102446 : MinisatSatSolver::~MinisatSatSolver()
      41                 :            : {
      42                 :      51223 :   d_statistics.deinit();
      43         [ +  - ]:      51223 :   delete d_minisat;
      44                 :     102446 : }
      45                 :            : 
      46                 :          0 : SatVariable MinisatSatSolver::toSatVariable(Minisat::Var var)
      47                 :            : {
      48         [ -  - ]:          0 :   if (var == var_Undef)
      49                 :            :   {
      50                 :          0 :     return undefSatVariable;
      51                 :            :   }
      52                 :          0 :   return SatVariable(var);
      53                 :            : }
      54                 :            : 
      55                 :   95435231 : Minisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit)
      56                 :            : {
      57         [ +  + ]:   95435231 :   if (lit == undefSatLiteral)
      58                 :            :   {
      59                 :    4140388 :     return Minisat::lit_Undef;
      60                 :            :   }
      61                 :   91294843 :   return Minisat::mkLit(lit.getSatVariable(), lit.isNegated());
      62                 :            : }
      63                 :            : 
      64                 :  121730297 : SatLiteral MinisatSatSolver::toSatLiteral(Minisat::Lit lit)
      65                 :            : {
      66         [ -  + ]:  121730297 :   if (lit == Minisat::lit_Undef)
      67                 :            :   {
      68                 :          0 :     return undefSatLiteral;
      69                 :            :   }
      70                 :            : 
      71                 :  121730297 :   return SatLiteral(SatVariable(Minisat::var(lit)), Minisat::sign(lit));
      72                 :            : }
      73                 :            : 
      74                 :   50541749 : SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res)
      75                 :            : {
      76         [ +  + ]:   50541749 :   if (res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
      77         [ +  + ]:   27748702 :   if (res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
      78 [ -  + ][ -  + ]:    7324508 :   Assert(res == (Minisat::lbool((uint8_t)1)));
                 [ -  - ]
      79                 :    7324508 :   return SAT_VALUE_FALSE;
      80                 :            : }
      81                 :            : 
      82                 :          0 : Minisat::lbool MinisatSatSolver::toMinisatlbool(SatValue val)
      83                 :            : {
      84         [ -  - ]:          0 :   if (val == SAT_VALUE_TRUE) return Minisat::lbool((uint8_t)0);
      85         [ -  - ]:          0 :   if (val == SAT_VALUE_UNKNOWN) return Minisat::lbool((uint8_t)2);
      86                 :          0 :   Assert(val == SAT_VALUE_FALSE);
      87                 :          0 :   return Minisat::lbool((uint8_t)1);
      88                 :            : }
      89                 :            : 
      90                 :            : /*bool MinisatSatSolver::tobool(SatValue val)
      91                 :            : {
      92                 :            :   if(val == SAT_VALUE_TRUE) return true;
      93                 :            :   Assert(val == SAT_VALUE_FALSE);
      94                 :            :   return false;
      95                 :            :   }*/
      96                 :            : 
      97                 :   17444423 : void MinisatSatSolver::toMinisatClause(
      98                 :            :     const SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause)
      99                 :            : {
     100         [ +  + ]:   52699121 :   for (const SatLiteral i : clause)
     101                 :            :   {
     102                 :   35254698 :     minisat_clause.push(toMinisatLit(i));
     103                 :            :   }
     104 [ -  + ][ -  + ]:   17444423 :   Assert(clause.size() == static_cast<unsigned>(minisat_clause.size()));
                 [ -  - ]
     105                 :   17444423 : }
     106                 :            : 
     107                 :     904297 : void MinisatSatSolver::toSatClause(const Minisat::Clause& clause,
     108                 :            :                                    SatClause& sat_clause)
     109                 :            : {
     110         [ +  + ]:   39553516 :   for (int i = 0; i < clause.size(); ++i)
     111                 :            :   {
     112                 :   38649219 :     sat_clause.push_back(toSatLiteral(clause[i]));
     113                 :            :   }
     114 [ -  + ][ -  + ]:     904297 :   Assert((unsigned)clause.size() == sat_clause.size());
                 [ -  - ]
     115                 :     904297 : }
     116                 :            : 
     117                 :      51568 : void MinisatSatSolver::initialize(TheoryProxy* theoryProxy)
     118                 :            : {
     119         [ +  + ]:      51568 :   if (options().decision.decisionMode != options::DecisionMode::INTERNAL)
     120                 :            :   {
     121                 :      41243 :     verbose(1) << "minisat: Incremental solving is forced on (to avoid "
     122                 :            :                   "variable elimination)"
     123                 :      41243 :                << " unless using internal decision strategy." << std::endl;
     124                 :            :   }
     125                 :            : 
     126                 :            :   // Create the solver
     127                 :      51568 :   d_minisat =
     128                 :            :       new Minisat::SimpSolver(d_env,
     129                 :            :                               theoryProxy,
     130                 :      51568 :                               context(),
     131                 :      51568 :                               options().base.incrementalSolving
     132 [ +  + ][ +  + ]:      51568 :                                   || options().decision.decisionMode
     133                 :      51568 :                                          != options::DecisionMode::INTERNAL);
     134                 :            : 
     135                 :      51568 :   d_statistics.init(d_minisat);
     136                 :      51568 :   initialize();
     137                 :      51568 : }
     138                 :            : 
     139                 :      51568 : void MinisatSatSolver::initialize() {}
     140                 :            : 
     141                 :      19900 : void MinisatSatSolver::attachProofManager(PropPfManager* ppm)
     142                 :            : {
     143                 :      19900 :   d_minisat->attachProofManager(ppm);
     144                 :      19900 : }
     145                 :            : 
     146                 :            : // Like initialize() above, but called just before each search when in
     147                 :            : // incremental mode
     148                 :      50291 : void MinisatSatSolver::setupOptions()
     149                 :            : {
     150                 :            :   // Copy options from cvc5 options structure into minisat, as appropriate
     151                 :            : 
     152                 :            :   // Set up the verbosity
     153         [ +  + ]:      50291 :   d_minisat->verbosity = (options().base.verbosity > 0) ? 1 : -1;
     154                 :            : 
     155                 :            :   // Set up the random decision parameters
     156                 :      50291 :   d_minisat->random_var_freq = options().prop.satRandomFreq;
     157                 :            :   // If 0, we use whatever we like (here, the Minisat default seed)
     158         [ +  + ]:      50291 :   if (options().prop.satRandomSeed != 0)
     159                 :            :   {
     160                 :          2 :     d_minisat->random_seed = double(options().prop.satRandomSeed);
     161                 :            :   }
     162                 :            : 
     163                 :            :   // Give access to all possible options in the sat solver
     164                 :      50291 :   d_minisat->var_decay = options().prop.satVarDecay;
     165                 :      50291 :   d_minisat->clause_decay = options().prop.satClauseDecay;
     166                 :      50291 :   d_minisat->restart_first = options().prop.satRestartFirst;
     167                 :      50291 :   d_minisat->restart_inc = options().prop.satRestartInc;
     168                 :      50291 : }
     169                 :            : 
     170                 :    5943405 : ClauseId MinisatSatSolver::addClause(const SatClause& clause, bool removable)
     171                 :            : {
     172                 :    5943405 :   Minisat::vec<Minisat::Lit> minisat_clause;
     173                 :    5943405 :   toMinisatClause(clause, minisat_clause);
     174                 :    5943405 :   ClauseId clause_id = ClauseIdError;
     175                 :            :   // FIXME: This relies on the invariant that when ok() is false
     176                 :            :   // the SAT solver does not add the clause (which is what Minisat currently
     177                 :            :   // does)
     178         [ +  + ]:    5943405 :   if (!ok())
     179                 :            :   {
     180                 :       7060 :     return ClauseIdUndef;
     181                 :            :   }
     182                 :    5936345 :   d_minisat->addClause(minisat_clause, removable, clause_id);
     183                 :            :   // FIXME: to be deleted when we kill old proof code for unsat cores
     184 [ +  + ][ +  - ]:    5936345 :   Assert(!options().smt.produceUnsatCores || options().smt.produceProofs
         [ -  + ][ -  - ]
         [ -  + ][ -  + ]
                 [ -  - ]
     185                 :            :          || clause_id != ClauseIdError);
     186                 :    5936345 :   return clause_id;
     187                 :    5943405 : }
     188                 :            : 
     189                 :    2152826 : SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool canErase)
     190                 :            : {
     191                 :    2152826 :   return d_minisat->newVar(true, true, isTheoryAtom, canErase);
     192                 :            : }
     193                 :            : 
     194                 :          0 : SatValue MinisatSatSolver::solve(unsigned long& resource)
     195                 :            : {
     196         [ -  - ]:          0 :   Trace("limit") << "SatSolver::solve(): have limit of " << resource
     197                 :          0 :                  << " conflicts" << std::endl;
     198                 :          0 :   setupOptions();
     199         [ -  - ]:          0 :   if (resource == 0)
     200                 :            :   {
     201                 :          0 :     d_minisat->budgetOff();
     202                 :            :   }
     203                 :            :   else
     204                 :            :   {
     205                 :          0 :     d_minisat->setConfBudget(resource);
     206                 :            :   }
     207                 :          0 :   Minisat::vec<Minisat::Lit> empty;
     208                 :          0 :   unsigned long conflictsBefore =
     209                 :          0 :       d_minisat->conflicts + d_minisat->resources_consumed;
     210                 :          0 :   SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
     211                 :          0 :   d_minisat->clearInterrupt();
     212                 :          0 :   resource =
     213                 :          0 :       d_minisat->conflicts + d_minisat->resources_consumed - conflictsBefore;
     214         [ -  - ]:          0 :   Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts"
     215                 :          0 :                  << std::endl;
     216                 :          0 :   return result;
     217                 :          0 : }
     218                 :            : 
     219                 :      41338 : SatValue MinisatSatSolver::solve()
     220                 :            : {
     221                 :      41338 :   setupOptions();
     222                 :      41338 :   d_minisat->budgetOff();
     223                 :      41338 :   SatValue result = toSatLiteralValue(d_minisat->solve());
     224                 :      41322 :   d_minisat->clearInterrupt();
     225                 :      41322 :   return result;
     226                 :            : }
     227                 :            : 
     228                 :       8953 : SatValue MinisatSatSolver::solve(const std::vector<SatLiteral>& assumptions)
     229                 :            : {
     230                 :       8953 :   setupOptions();
     231                 :       8953 :   d_minisat->budgetOff();
     232                 :            : 
     233                 :       8953 :   d_assumptions.clear();
     234                 :       8953 :   Minisat::vec<Minisat::Lit> assumps;
     235                 :            : 
     236         [ +  + ]:     137904 :   for (const SatLiteral& lit : assumptions)
     237                 :            :   {
     238                 :     128951 :     Minisat::Lit mlit = toMinisatLit(lit);
     239                 :     128951 :     assumps.push(mlit);
     240                 :     128951 :     d_assumptions.emplace(lit);
     241                 :            :   }
     242                 :            : 
     243                 :       8953 :   SatValue result = toSatLiteralValue(d_minisat->solve(assumps));
     244                 :       8953 :   d_minisat->clearInterrupt();
     245                 :       8953 :   return result;
     246                 :       8953 : }
     247                 :            : 
     248                 :       3895 : void MinisatSatSolver::getUnsatAssumptions(
     249                 :            :     std::vector<SatLiteral>& unsat_assumptions)
     250                 :            : {
     251         [ +  + ]:      22812 :   for (size_t i = 0, size = d_minisat->d_conflict.size(); i < size; ++i)
     252                 :            :   {
     253                 :      18917 :     Minisat::Lit mlit = d_minisat->d_conflict[i];
     254                 :      18917 :     SatLiteral lit = ~toSatLiteral(mlit);
     255         [ +  - ]:      18917 :     if (d_assumptions.find(lit) != d_assumptions.end())
     256                 :            :     {
     257                 :      18917 :       unsat_assumptions.push_back(lit);
     258                 :            :     }
     259                 :            :   }
     260                 :       3895 : }
     261                 :            : 
     262                 :    5943405 : bool MinisatSatSolver::ok() const { return d_minisat->okay(); }
     263                 :            : 
     264                 :       6121 : void MinisatSatSolver::interrupt() { d_minisat->interrupt(); }
     265                 :            : 
     266                 :   50491474 : SatValue MinisatSatSolver::value(SatLiteral l)
     267                 :            : {
     268                 :   50491474 :   return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
     269                 :            : }
     270                 :            : 
     271                 :          0 : SatValue MinisatSatSolver::modelValue(SatLiteral l)
     272                 :            : {
     273                 :          0 :   return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
     274                 :            : }
     275                 :            : 
     276                 :     168122 : void MinisatSatSolver::preferPhase(SatLiteral lit)
     277                 :            : {
     278 [ -  + ][ -  + ]:     168122 :   Assert(!d_minisat->rnd_pol);
                 [ -  - ]
     279         [ +  - ]:     336244 :   Trace("minisat") << "preferPhase(" << lit << ")"
     280                 :     168122 :                    << " " << lit.getSatVariable() << " " << lit.isNegated()
     281                 :     168122 :                    << std::endl;
     282                 :     168122 :   SatVariable v = lit.getSatVariable();
     283                 :     168122 :   d_minisat->freezePolarity(v, lit.isNegated());
     284                 :     168122 : }
     285                 :            : 
     286                 :     193453 : bool MinisatSatSolver::isDecision(SatVariable decn) const
     287                 :            : {
     288                 :     193453 :   return d_minisat->isDecision(decn);
     289                 :            : }
     290                 :            : 
     291                 :         16 : bool MinisatSatSolver::isFixed(SatVariable var) const
     292                 :            : {
     293         [ +  + ]:         32 :   return d_minisat->intro_level(var) == 0 && d_minisat->user_level(var) == 0
     294 [ +  - ][ +  + ]:         32 :          && d_minisat->level(var) == 0;
     295                 :            : }
     296                 :            : 
     297                 :          0 : std::vector<SatLiteral> MinisatSatSolver::getDecisions() const
     298                 :            : {
     299                 :          0 :   std::vector<SatLiteral> decisions;
     300                 :            :   const Minisat::vec<Minisat::Lit>& miniDecisions =
     301                 :          0 :       d_minisat->getMiniSatAssignmentTrail();
     302         [ -  - ]:          0 :   for (size_t i = 0, ndec = miniDecisions.size(); i < ndec; ++i)
     303                 :            :   {
     304                 :          0 :     auto satLit = toSatLiteral(miniDecisions[i]);
     305         [ -  - ]:          0 :     if (isDecision(satLit.getSatVariable()))
     306                 :            :     {
     307                 :          0 :       decisions.push_back(satLit);
     308                 :            :     }
     309                 :            :   }
     310                 :          0 :   return decisions;
     311                 :          0 : }
     312                 :            : 
     313                 :          0 : std::vector<Node> MinisatSatSolver::getOrderHeap() const
     314                 :            : {
     315                 :          0 :   return d_minisat->getMiniSatOrderHeap();
     316                 :            : }
     317                 :            : 
     318                 :       9413 : std::shared_ptr<ProofNode> MinisatSatSolver::getProof()
     319                 :            : {
     320 [ -  + ][ -  + ]:       9413 :   Assert(d_env.isSatProofProducing());
                 [ -  - ]
     321                 :       9413 :   return d_minisat->getProof();
     322                 :            : }
     323                 :            : 
     324                 :            : /** Incremental interface */
     325                 :            : 
     326                 :      50874 : uint32_t MinisatSatSolver::getAssertionLevel() const
     327                 :            : {
     328                 :      50874 :   return d_minisat->getAssertionLevel();
     329                 :            : }
     330                 :            : 
     331                 :       8192 : void MinisatSatSolver::push() { d_minisat->push(); }
     332                 :            : 
     333                 :       8185 : void MinisatSatSolver::pop() { d_minisat->pop(); }
     334                 :            : 
     335                 :      49450 : void MinisatSatSolver::resetTrail() { d_minisat->resetTrail(); }
     336                 :            : 
     337                 :            : /// Statistics for MinisatSatSolver
     338                 :            : 
     339                 :      51568 : MinisatSatSolver::Statistics::Statistics(StatisticsRegistry& registry)
     340                 :      51568 :     : d_statStarts(registry.registerReference<int64_t>("sat::starts")),
     341                 :      51568 :       d_statDecisions(registry.registerReference<int64_t>("sat::decisions")),
     342                 :      51568 :       d_statRndDecisions(
     343                 :            :           registry.registerReference<int64_t>("sat::rnd_decisions")),
     344                 :      51568 :       d_statPropagations(
     345                 :            :           registry.registerReference<int64_t>("sat::propagations")),
     346                 :      51568 :       d_statConflicts(registry.registerReference<int64_t>("sat::conflicts")),
     347                 :      51568 :       d_statClausesLiterals(
     348                 :            :           registry.registerReference<int64_t>("sat::clauses_literals")),
     349                 :      51568 :       d_statLearntsLiterals(
     350                 :            :           registry.registerReference<int64_t>("sat::learnts_literals")),
     351                 :      51568 :       d_statMaxLiterals(
     352                 :            :           registry.registerReference<int64_t>("sat::max_literals")),
     353                 :      51568 :       d_statTotLiterals(
     354                 :            :           registry.registerReference<int64_t>("sat::tot_literals"))
     355                 :            : {
     356                 :      51568 : }
     357                 :            : 
     358                 :      51568 : void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat)
     359                 :            : {
     360                 :      51568 :   d_statStarts.set(minisat->starts);
     361                 :      51568 :   d_statDecisions.set(minisat->decisions);
     362                 :      51568 :   d_statRndDecisions.set(minisat->rnd_decisions);
     363                 :      51568 :   d_statPropagations.set(minisat->propagations);
     364                 :      51568 :   d_statConflicts.set(minisat->conflicts);
     365                 :      51568 :   d_statClausesLiterals.set(minisat->clauses_literals);
     366                 :      51568 :   d_statLearntsLiterals.set(minisat->learnts_literals);
     367                 :      51568 :   d_statMaxLiterals.set(minisat->max_literals);
     368                 :      51568 :   d_statTotLiterals.set(minisat->tot_literals);
     369                 :      51568 : }
     370                 :      51223 : void MinisatSatSolver::Statistics::deinit()
     371                 :            : {
     372                 :      51223 :   d_statStarts.reset();
     373                 :      51223 :   d_statDecisions.reset();
     374                 :      51223 :   d_statRndDecisions.reset();
     375                 :      51223 :   d_statPropagations.reset();
     376                 :      51223 :   d_statConflicts.reset();
     377                 :      51223 :   d_statClausesLiterals.reset();
     378                 :      51223 :   d_statLearntsLiterals.reset();
     379                 :      51223 :   d_statMaxLiterals.reset();
     380                 :      51223 :   d_statTotLiterals.reset();
     381                 :      51223 : }
     382                 :            : 
     383                 :            : }  // namespace prop
     384                 :            : }  // namespace cvc5::internal
     385                 :            : 
     386                 :            : namespace cvc5::internal {
     387                 :            : template <>
     388                 :          0 : prop::SatLiteral toSatLiteral<cvc5::internal::Minisat::Solver>(
     389                 :            :     Minisat::Solver::TLit lit)
     390                 :            : {
     391                 :          0 :   return prop::MinisatSatSolver::toSatLiteral(lit);
     392                 :            : }
     393                 :            : 
     394                 :            : template <>
     395                 :          0 : void toSatClause<cvc5::internal::Minisat::Solver>(
     396                 :            :     const cvc5::internal::Minisat::Solver::TClause& minisat_cl,
     397                 :            :     prop::SatClause& sat_cl)
     398                 :            : {
     399                 :          0 :   prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl);
     400                 :          0 : }
     401                 :            : 
     402                 :            : }  // namespace cvc5::internal