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                 :            :  * Wrapper for CaDiCaL SAT Solver.
      11                 :            :  *
      12                 :            :  * Implementation of the CaDiCaL SAT solver for cvc5 (bit-vectors).
      13                 :            :  */
      14                 :            : 
      15                 :            : #include "prop/cadical/cadical.h"
      16                 :            : 
      17                 :            : #include <cadical/cadical.hpp>
      18                 :            : #include <cstdint>
      19                 :            : #include <memory>
      20                 :            : 
      21                 :            : #include "base/check.h"
      22                 :            : #include "options/base_options.h"
      23                 :            : #include "options/main_options.h"
      24                 :            : #include "options/proof_options.h"
      25                 :            : #include "prop/cadical/cdclt_propagator.h"
      26                 :            : #include "prop/cadical/proof_tracer.h"
      27                 :            : #include "prop/cadical/util.h"
      28                 :            : #include "prop/sat_solver_types.h"
      29                 :            : #include "prop/theory_proxy.h"
      30                 :            : #include "theory/shared_terms_database.h"
      31                 :            : #include "util/resource_manager.h"
      32                 :            : #include "util/statistics_registry.h"
      33                 :            : #include "util/string.h"
      34                 :            : 
      35                 :            : namespace cvc5::internal::prop {
      36                 :            : using namespace cadical;
      37                 :            : 
      38                 :            : /* -------------------------------------------------------------------------- */
      39                 :            : 
      40                 :            : class ClauseLearner : public CaDiCaL::Learner
      41                 :            : {
      42                 :            :  public:
      43                 :          1 :   ClauseLearner(TheoryProxy& proxy, int32_t clause_size)
      44                 :          1 :       : d_proxy(proxy), d_max_clause_size(clause_size)
      45                 :            :   {
      46                 :          1 :   }
      47                 :          2 :   ~ClauseLearner() override {}
      48                 :            : 
      49                 :          1 :   bool learning(int size) override
      50                 :            :   {
      51 [ -  + ][ -  - ]:          1 :     return d_max_clause_size == 0 || size <= d_max_clause_size;
      52                 :            :   }
      53                 :            : 
      54                 :          2 :   void learn(int lit) override
      55                 :            :   {
      56         [ +  + ]:          2 :     if (lit)
      57                 :            :     {
      58                 :          1 :       SatLiteral slit = toSatLiteral(lit);
      59                 :          1 :       d_clause.push_back(slit);
      60                 :            :     }
      61                 :            :     else
      62                 :            :     {
      63                 :          1 :       d_proxy.notifySatClause(d_clause);
      64                 :          1 :       d_clause.clear();
      65                 :            :     }
      66                 :          2 :   }
      67                 :            : 
      68                 :            :  private:
      69                 :            :   TheoryProxy& d_proxy;
      70                 :            :   /** Intermediate literals buffer. */
      71                 :            :   std::vector<SatLiteral> d_clause;
      72                 :            :   /** Maximum size of clauses to get notified about. */
      73                 :            :   int32_t d_max_clause_size;
      74                 :            : };
      75                 :            : 
      76                 :      20009 : CadicalSolver::CadicalSolver(Env& env,
      77                 :            :                              StatisticsRegistry& registry,
      78                 :      20009 :                              const std::string& name)
      79                 :            :     : EnvObj(env),
      80                 :      20009 :       d_solver(new CaDiCaL::Solver()),
      81                 :      20009 :       d_context(context()),
      82                 :            :       // Note: CaDiCaL variables start with index 1 rather than 0 since negated
      83                 :            :       //       literals are represented as the negation of the index.
      84                 :      20009 :       d_nextVarIdx(1),
      85                 :      20009 :       d_inSatMode(false),
      86                 :      60027 :       d_statistics(registry, name)
      87                 :            : {
      88                 :      20009 : }
      89                 :            : 
      90                 :      20009 : void CadicalSolver::initialize()
      91                 :            : {
      92                 :      20009 :   d_solver->set("quiet", 1);  // CaDiCaL is verbose by default
      93                 :            : 
      94                 :            :   // walk and lucky phase do not use the external propagator, disable for now
      95         [ +  + ]:      20009 :   if (d_propagator)
      96                 :            :   {
      97                 :         72 :     d_solver->set("walk", 0);
      98                 :         72 :     d_solver->set("lucky", 0);
      99                 :            :     // ilb currently does not play well with user propagators
     100                 :         72 :     d_solver->set("ilb", 0);
     101                 :         72 :     d_solver->set("ilbassumptions", 0);
     102         [ +  - ]:         72 :     d_solver->connect_fixed_listener(d_propagator.get());
     103                 :         72 :     d_solver->connect_external_propagator(d_propagator.get());
     104                 :            :   }
     105                 :            : 
     106                 :      20009 :   d_true = newVar(false, true);
     107                 :      20009 :   d_false = newVar(false, true);
     108                 :      20009 :   d_solver->clause(toCadicalVar(d_true));
     109                 :      20009 :   d_solver->clause(-toCadicalVar(d_false));
     110                 :      20009 : }
     111                 :            : 
     112                 :      39992 : CadicalSolver::~CadicalSolver()
     113                 :            : {
     114         [ +  + ]:      19996 :   if (d_proof_tracer != nullptr)
     115                 :            :   {
     116                 :         20 :     d_solver->disconnect_proof_tracer(d_proof_tracer.get());
     117                 :            :   }
     118                 :      39992 : }
     119                 :            : 
     120                 :            : /**
     121                 :            :  * Terminator class that notifies CaDiCaL to terminate when the resource limit
     122                 :            :  * is reached (used for resource limits specified via --rlimit or --tlimit).
     123                 :            :  */
     124                 :            : class ResourceLimitTerminator : public CaDiCaL::Terminator
     125                 :            : {
     126                 :            :  public:
     127                 :      20009 :   ResourceLimitTerminator(ResourceManager& resmgr) : d_resmgr(resmgr) {}
     128                 :            : 
     129                 :     788766 :   bool terminate() override
     130                 :            :   {
     131                 :     788766 :     d_resmgr.spendResource(Resource::BvSatStep);
     132                 :     788766 :     return d_resmgr.out();
     133                 :            :   }
     134                 :            : 
     135                 :            :  private:
     136                 :            :   ResourceManager& d_resmgr;
     137                 :            : };
     138                 :            : 
     139                 :      20009 : void CadicalSolver::setResourceLimit(ResourceManager* resmgr)
     140                 :            : {
     141                 :      20009 :   d_terminator.reset(new ResourceLimitTerminator(*resmgr));
     142                 :      20009 :   d_solver->connect_terminator(d_terminator.get());
     143                 :      20009 : }
     144                 :            : 
     145                 :      61302 : SatValue CadicalSolver::_solve(const std::vector<SatLiteral>& assumptions)
     146                 :            : {
     147         [ +  + ]:      61302 :   if (d_propagator)
     148                 :            :   {
     149         [ +  - ]:        101 :     Trace("cadical::propagator") << "solve start" << std::endl;
     150                 :        101 :     d_propagator->renotify_fixed();
     151                 :            :   }
     152                 :      61302 :   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
     153                 :      61302 :   d_assumptions.clear();
     154         [ +  + ]:      61302 :   if (d_propagator)
     155                 :            :   {
     156                 :            :     // Assume activation literals for all active user levels.
     157         [ +  + ]:        133 :     for (const auto& lit : d_propagator->activation_literals())
     158                 :            :     {
     159         [ +  - ]:         64 :       Trace("cadical::propagator")
     160                 :         32 :           << "assume activation lit: " << ~lit << std::endl;
     161                 :         32 :       d_solver->assume(toCadicalLit(~lit));
     162                 :            :     }
     163                 :            :   }
     164                 :            :   SatValue res;
     165         [ +  + ]:    7877881 :   for (const SatLiteral& lit : assumptions)
     166                 :            :   {
     167         [ +  + ]:    7816579 :     if (d_propagator)
     168                 :            :     {
     169         [ +  - ]:        246 :       Trace("cadical::propagator") << "assume: " << lit << std::endl;
     170                 :            :     }
     171                 :    7816579 :     d_solver->assume(toCadicalLit(lit));
     172                 :    7816579 :     d_assumptions.push_back(lit);
     173                 :            :   }
     174         [ +  + ]:      61302 :   if (d_propagator)
     175                 :            :   {
     176                 :        101 :     d_propagator->in_search(true);
     177                 :            :   }
     178                 :      61302 :   res = toSatValue(d_solver->solve());
     179         [ +  + ]:      61302 :   if (d_propagator)
     180                 :            :   {
     181 [ +  + ][ +  - ]:        101 :     Assert(res != SAT_VALUE_TRUE || d_propagator->done());
         [ -  + ][ -  + ]
                 [ -  - ]
     182         [ +  - ]:        101 :     Trace("cadical::propagator") << "solve done: " << res << std::endl;
     183                 :        101 :     d_propagator->in_search(false);
     184                 :            :   }
     185                 :      61302 :   ++d_statistics.d_numSatCalls;
     186                 :      61302 :   d_inSatMode = (res == SAT_VALUE_TRUE);
     187                 :      61302 :   return res;
     188                 :      61302 : }
     189                 :            : 
     190                 :            : /* SatSolver Interface ------------------------------------------------------ */
     191                 :            : 
     192                 :   10560029 : ClauseId CadicalSolver::addClause(const SatClause& clause, bool removable)
     193                 :            : {
     194                 :   10560029 :   if (d_propagator && TraceIsOn("cadical::propagator"))
     195                 :            :   {
     196         [ -  - ]:          0 :     Trace("cadical::propagator") << "addClause (" << removable << "):";
     197                 :          0 :     SatLiteral alit = d_propagator->current_activation_lit();
     198         [ -  - ]:          0 :     if (alit != undefSatLiteral)
     199                 :            :     {
     200         [ -  - ]:          0 :       Trace("cadical::propagator") << " " << alit;
     201                 :            :     }
     202         [ -  - ]:          0 :     for (const SatLiteral& lit : clause)
     203                 :            :     {
     204         [ -  - ]:          0 :       Trace("cadical::propagator") << " " << lit;
     205                 :            :     }
     206         [ -  - ]:          0 :     Trace("cadical::propagator") << " 0" << std::endl;
     207                 :            :   }
     208         [ +  + ]:   10560029 :   if (d_propagator)
     209                 :            :   {
     210                 :       2590 :     d_propagator->add_clause(clause);
     211                 :            :   }
     212                 :            :   else
     213                 :            :   {
     214         [ +  + ]:   39651426 :     for (const SatLiteral& lit : clause)
     215                 :            :     {
     216                 :   29093987 :       d_solver->add(toCadicalLit(lit));
     217                 :            :     }
     218                 :   10557439 :     d_solver->add(0);
     219                 :            :   }
     220                 :   10560029 :   ++d_statistics.d_numClauses;
     221                 :   10560029 :   return ClauseIdError;
     222                 :            : }
     223                 :            : 
     224                 :    2364142 : SatVariable CadicalSolver::newVar(bool isTheoryAtom, CVC5_UNUSED bool canErase)
     225                 :            : {
     226                 :    2364142 :   ++d_statistics.d_numVariables;
     227         [ +  + ]:    2364142 :   if (d_propagator)
     228                 :            :   {
     229                 :       2067 :     d_propagator->add_new_var(d_nextVarIdx, isTheoryAtom);
     230                 :            :   }
     231                 :    2364142 :   return d_nextVarIdx++;
     232                 :            : }
     233                 :            : 
     234                 :        177 : SatVariable CadicalSolver::trueVar() { return d_true; }
     235                 :            : 
     236                 :        262 : SatVariable CadicalSolver::falseVar() { return d_false; }
     237                 :            : 
     238                 :         66 : SatValue CadicalSolver::solve() { return _solve({}); }
     239                 :            : 
     240                 :          0 : SatValue CadicalSolver::solve(long unsigned int&)
     241                 :            : {
     242                 :          0 :   Unimplemented() << "Setting limits for CaDiCaL not supported yet";
     243                 :            :   return SatValue::SAT_VALUE_UNKNOWN;
     244                 :            : };
     245                 :            : 
     246                 :      61236 : SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions)
     247                 :            : {
     248                 :      61236 :   return _solve(assumptions);
     249                 :            : }
     250                 :            : 
     251                 :          0 : bool CadicalSolver::setPropagateOnly()
     252                 :            : {
     253                 :          0 :   d_solver->limit("decisions", 0); /* Gets reset after next solve() call. */
     254                 :          0 :   return true;
     255                 :            : }
     256                 :            : 
     257                 :      19753 : void CadicalSolver::getUnsatAssumptions(std::vector<SatLiteral>& assumptions)
     258                 :            : {
     259         [ +  + ]:    7639090 :   for (const SatLiteral& lit : d_assumptions)
     260                 :            :   {
     261         [ +  + ]:    7619337 :     if (d_solver->failed(toCadicalLit(lit)))
     262                 :            :     {
     263                 :     151633 :       assumptions.push_back(lit);
     264                 :            :     }
     265                 :            :   }
     266                 :      19753 : }
     267                 :            : 
     268                 :          0 : void CadicalSolver::interrupt() { d_solver->terminate(); }
     269                 :            : 
     270                 :     130309 : SatValue CadicalSolver::value(SatLiteral l) { return d_propagator->value(l); }
     271                 :            : 
     272                 :     213427 : SatValue CadicalSolver::modelValue(SatLiteral l)
     273                 :            : {
     274 [ -  + ][ -  + ]:     213427 :   Assert(d_inSatMode);
                 [ -  - ]
     275                 :     213427 :   auto val = d_solver->val(toCadicalVar(l.getSatVariable()));
     276         [ +  + ]:     213427 :   return toSatValueLit(l.isNegated() ? -val : val);
     277                 :            : }
     278                 :            : 
     279                 :          0 : bool CadicalSolver::ok() const { return d_inSatMode; }
     280                 :            : 
     281                 :      20009 : CadicalSolver::Statistics::Statistics(StatisticsRegistry& registry,
     282                 :      20009 :                                       const std::string& prefix)
     283                 :      20009 :     : d_numSatCalls(registry.registerInt(prefix + "cadical::calls_to_solve")),
     284                 :      20009 :       d_numVariables(registry.registerInt(prefix + "cadical::variables")),
     285                 :      20009 :       d_numClauses(registry.registerInt(prefix + "cadical::clauses")),
     286                 :      20009 :       d_solveTime(registry.registerTimer(prefix + "cadical::solve_time"))
     287                 :            : {
     288                 :      20009 : }
     289                 :            : 
     290                 :            : /* CDCLTSatSolver Interface ------------------------------------------------- */
     291                 :            : 
     292                 :         72 : void CadicalSolver::initialize(TheoryProxy* theoryProxy)
     293                 :            : {
     294                 :         72 :   d_proxy = theoryProxy;
     295                 :         72 :   d_propagator.reset(new CadicalPropagator(
     296                 :         72 :       theoryProxy, d_context, *d_solver, statisticsRegistry()));
     297         [ +  + ]:         72 :   if (!d_env.getPlugins().empty())
     298                 :            :   {
     299                 :          1 :     d_clause_learner.reset(new ClauseLearner(*theoryProxy, 0));
     300                 :          1 :     d_solver->connect_learner(d_clause_learner.get());
     301                 :            :   }
     302                 :            : 
     303         [ +  + ]:         72 :   if (d_env.isSatProofProducing())
     304                 :            :   {
     305                 :         20 :     d_proof_tracer.reset(new ProofTracer(*d_propagator));
     306                 :         20 :     d_solver->connect_proof_tracer(d_proof_tracer.get(), true);
     307                 :            :   }
     308                 :            : 
     309                 :         72 :   initialize();
     310                 :         72 : }
     311                 :            : 
     312                 :         46 : void CadicalSolver::attachProofManager(CVC5_UNUSED PropPfManager* ppm)
     313                 :            : {
     314                 :            :   // not implemented yet
     315                 :         46 : }
     316                 :            : 
     317                 :         32 : void CadicalSolver::push()
     318                 :            : {
     319                 :         32 :   d_context->push();  // SAT context for cvc5
     320                 :            :   // Push new user level
     321                 :         32 :   d_propagator->user_push();
     322                 :            :   // Set new activation literal for pushed user level
     323                 :            :   // Note: This happens after the push to ensure that the activation literal's
     324                 :            :   // introduction level is the current user level.
     325                 :         32 :   SatVariable alit = newVar(false, true);
     326                 :         32 :   d_propagator->set_activation_lit(alit);
     327                 :         32 : }
     328                 :            : 
     329                 :         72 : uint32_t CadicalSolver::getAssertionLevel() const
     330                 :            : {
     331 [ -  + ][ -  + ]:         72 :   Assert(d_propagator);
                 [ -  - ]
     332                 :         72 :   return d_propagator->current_user_level();
     333                 :            : }
     334                 :            : 
     335                 :         32 : void CadicalSolver::pop()
     336                 :            : {
     337                 :         32 :   d_context->pop();  // SAT context for cvc5
     338                 :         32 :   d_propagator->user_pop();
     339                 :            :   // CaDiCaL issues notify_backtrack(0) when done, we don't have to call this
     340                 :            :   // explicitly here
     341                 :         32 : }
     342                 :            : 
     343                 :        101 : void CadicalSolver::resetTrail()
     344                 :            : {
     345                 :            :   // Reset SAT context to decision level 0
     346                 :        101 :   d_propagator->notify_backtrack(0);
     347                 :        101 : }
     348                 :            : 
     349                 :         61 : void CadicalSolver::preferPhase(SatLiteral lit)
     350                 :            : {
     351         [ +  - ]:         61 :   Trace("cadical::propagator") << "phase: " << lit << std::endl;
     352                 :         61 :   d_propagator->phase(lit);
     353                 :         61 : }
     354                 :            : 
     355                 :          5 : bool CadicalSolver::isDecision(SatVariable var) const
     356                 :            : {
     357                 :          5 :   return d_solver->is_decision(toCadicalVar(var));
     358                 :            : }
     359                 :            : 
     360                 :          0 : bool CadicalSolver::isFixed(SatVariable var) const
     361                 :            : {
     362         [ -  - ]:          0 :   if (d_propagator)
     363                 :            :   {
     364                 :          0 :     return d_propagator->is_fixed(var);
     365                 :            :   }
     366                 :          0 :   return d_solver->fixed(toCadicalVar(var));
     367                 :            : }
     368                 :            : 
     369                 :          0 : std::vector<SatLiteral> CadicalSolver::getDecisions() const
     370                 :            : {
     371                 :          0 :   std::vector<SatLiteral> decisions;
     372         [ -  - ]:          0 :   for (SatLiteral lit : d_propagator->get_decisions())
     373                 :            :   {
     374         [ -  - ]:          0 :     if (lit != undefSatLiteral)
     375                 :            :     {
     376                 :          0 :       decisions.push_back(lit);
     377                 :            :     }
     378                 :            :   }
     379                 :          0 :   return decisions;
     380                 :          0 : }
     381                 :            : 
     382                 :          0 : std::vector<Node> CadicalSolver::getOrderHeap() const { return {}; }
     383                 :            : 
     384                 :         20 : std::shared_ptr<ProofNode> CadicalSolver::getProof()
     385                 :            : {
     386         [ +  - ]:         20 :   if (d_proof_tracer)
     387                 :            :   {
     388                 :         20 :     ProofNodeManager* pnm = d_env.getProofNodeManager();
     389                 :         20 :     NodeManager* nm = d_env.getNodeManager();
     390                 :         20 :     return d_proof_tracer->get_chain_resolution_proof(pnm, nm, d_proxy);
     391                 :            :   }
     392                 :          0 :   return nullptr;
     393                 :            : }
     394                 :            : 
     395                 :            : /* -------------------------------------------------------------------------- */
     396                 :            : }  // namespace cvc5::internal::prop