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                 :            :  * CaDiCaL proof tracer.
      11                 :            :  *
      12                 :            :  * Implementation of a CaDiCaL proof tracer.
      13                 :            :  */
      14                 :            : 
      15                 :            : #include "prop/cadical/proof_tracer.h"
      16                 :            : 
      17                 :            : #include <unordered_set>
      18                 :            : 
      19                 :            : #include "proof/proof_node.h"
      20                 :            : #include "prop/cadical/cadical.h"
      21                 :            : #include "prop/cadical/cdclt_propagator.h"
      22                 :            : 
      23                 :            : namespace cvc5::internal::prop::cadical {
      24                 :            : 
      25                 :          0 : ProofTracer::ProofTracer(const CadicalPropagator& propagator)
      26                 :          0 :     : d_propagator(propagator)
      27                 :            : {
      28                 :          0 :   d_antecedents.emplace_back();  // clauses start with id 1
      29                 :          0 : }
      30                 :            : 
      31                 :          0 : void ProofTracer::add_original_clause(uint64_t clause_id,
      32                 :            :                                       CVC5_UNUSED bool redundant,
      33                 :            :                                       const std::vector<int>& clause,
      34                 :            :                                       CVC5_UNUSED bool restored)
      35                 :            : {
      36                 :          0 :   Assert(d_antecedents.size() == clause_id);
      37                 :          0 :   d_antecedents.emplace_back();  // no antecedents
      38                 :            :   ClauseType ctype =
      39         [ -  - ]:          0 :       d_propagator.in_search() ? ClauseType::THEORY : ClauseType::INPUT;
      40                 :          0 :   d_orig_clauses.try_emplace(clause_id, clause, ctype);
      41                 :            : 
      42         [ -  - ]:          0 :   if (TraceIsOn("cadical::prooftracer"))
      43                 :            :   {
      44         [ -  - ]:          0 :     Trace("cadical::prooftracer")
      45         [ -  - ]:          0 :         << (ctype == ProofTracer::ClauseType::INPUT ? "i: " : "t: ");
      46         [ -  - ]:          0 :     for (const auto lit : clause)
      47                 :            :     {
      48         [ -  - ]:          0 :       Trace("cadical::prooftracer") << lit << " ";
      49                 :            :     }
      50         [ -  - ]:          0 :     Trace("cadical::prooftracer") << "0" << std::endl;
      51                 :            :   }
      52                 :          0 : }
      53                 :            : 
      54                 :          0 : void ProofTracer::add_derived_clause(uint64_t clause_id,
      55                 :            :                                      bool redundant,
      56                 :            :                                      const std::vector<int>& clause,
      57                 :            :                                      const std::vector<uint64_t>& antecedents)
      58                 :            : {
      59                 :          0 :   Assert(d_antecedents.size() == clause_id);
      60                 :            :   (void)clause;
      61                 :            :   (void)redundant;
      62                 :            :   // Only store antecedents for a derived clause, no need to store the
      63                 :            :   // literals.
      64                 :          0 :   d_antecedents.emplace_back(antecedents);
      65                 :          0 : }
      66                 :            : 
      67                 :          0 : void ProofTracer::add_assumption_clause(
      68                 :            :     uint64_t clause_id,
      69                 :            :     const std::vector<int>& clause,
      70                 :            :     const std::vector<uint64_t>& antecedents)
      71                 :            : {
      72                 :          0 :   Assert(d_antecedents.size() == clause_id);
      73                 :            :   // Assumption clauses are the negation of the core of failed/unsat
      74                 :            :   // assumptions.
      75                 :          0 :   d_antecedents.emplace_back(antecedents);
      76                 :            :   // Assumptions are original clauses.
      77                 :          0 :   d_orig_clauses.try_emplace(clause_id, clause, ClauseType::ASSUMPTION);
      78                 :            : 
      79         [ -  - ]:          0 :   if (TraceIsOn("cadical::prooftracer"))
      80                 :            :   {
      81         [ -  - ]:          0 :     Trace("cadical::prooftracer") << "a: ~(";
      82         [ -  - ]:          0 :     for (const auto lit : clause)
      83                 :            :     {
      84         [ -  - ]:          0 :       Trace("cadical::prooftracer") << lit << " ";
      85                 :            :     }
      86         [ -  - ]:          0 :     Trace("cadical::prooftracer") << "0)" << std::endl;
      87                 :            :   }
      88                 :          0 : }
      89                 :            : 
      90                 :          0 : void ProofTracer::conclude_unsat(CVC5_UNUSED CaDiCaL::ConclusionType type,
      91                 :            :                                  const std::vector<uint64_t>& clause_ids)
      92                 :            : {
      93                 :            :   // Store final clause ids that concluded unsat.
      94                 :          0 :   d_final_clauses = clause_ids;
      95                 :          0 : }
      96                 :            : 
      97                 :          0 : void ProofTracer::compute_unsat_core(std::vector<SatClause>& unsat_core,
      98                 :            :                                      bool include_theory_lemmas) const
      99                 :            : {
     100                 :          0 :   std::vector<uint64_t> core;
     101                 :          0 :   std::vector<uint64_t> visit{d_final_clauses};
     102                 :          0 :   std::vector<bool> visited(d_antecedents.size() + 1, false);
     103                 :            : 
     104                 :            :   // Trace back from final clause ids (empty clause) to original clauses.
     105         [ -  - ]:          0 :   while (!visit.empty())
     106                 :            :   {
     107                 :          0 :     const uint64_t clause_id = visit.back();
     108                 :          0 :     visit.pop_back();
     109                 :            : 
     110         [ -  - ]:          0 :     if (!visited[clause_id])
     111                 :            :     {
     112                 :          0 :       visited[clause_id] = true;
     113         [ -  - ]:          0 :       if (d_orig_clauses.find(clause_id) != d_orig_clauses.end())
     114                 :            :       {
     115                 :          0 :         core.push_back(clause_id);
     116                 :            :       }
     117                 :          0 :       Assert(clause_id < d_antecedents.size());
     118                 :          0 :       const auto& antecedents = d_antecedents[clause_id];
     119                 :          0 :       visit.insert(visit.end(), antecedents.begin(), antecedents.end());
     120                 :            :     }
     121                 :            :   }
     122                 :            : 
     123                 :            :   // Get activation literals, required for filtering below.
     124                 :          0 :   std::unordered_set<int64_t> alits;
     125         [ -  - ]:          0 :   for (const auto& lit : d_propagator.activation_literals())
     126                 :            :   {
     127         [ -  - ]:          0 :     Trace("cadical::prooftracer")
     128                 :          0 :         << "act. lit: " << lit.getSatVariable() << std::endl;
     129                 :          0 :     alits.insert(lit.getSatVariable());
     130                 :            :   }
     131                 :            : 
     132         [ -  - ]:          0 :   Trace("cadical::prooftracer") << "unsat core:" << std::endl;
     133                 :            : 
     134                 :            :   // Get the core in terms of SatClause/SatLiteral, filters out activation
     135                 :            :   // literals.
     136         [ -  - ]:          0 :   for (const uint64_t cid : core)
     137                 :            :   {
     138                 :          0 :     const auto& [clause, ctype] = d_orig_clauses.at(cid);
     139                 :            : 
     140                 :            :     // Skip theory lemmas if not requested.
     141 [ -  - ][ -  - ]:          0 :     if (!include_theory_lemmas && ctype == ProofTracer::ClauseType::THEORY)
     142                 :            :     {
     143                 :          0 :       continue;
     144                 :            :     }
     145                 :            : 
     146                 :            :     // Filter out activation literals
     147                 :          0 :     std::vector<int64_t> cl;
     148         [ -  - ]:          0 :     for (const auto& lit : clause)
     149                 :            :     {
     150         [ -  - ]:          0 :       if (alits.find(std::abs(lit)) == alits.end())
     151                 :            :       {
     152                 :          0 :         cl.push_back(lit);
     153                 :            :       }
     154                 :            :     }
     155                 :            : 
     156         [ -  - ]:          0 :     if (cl.empty())
     157                 :            :     {
     158                 :          0 :       continue;
     159                 :            :     }
     160                 :            : 
     161         [ -  - ]:          0 :     if (TraceIsOn("cadical::prooftracer"))
     162                 :            :     {
     163                 :          0 :       char ct = ' ';
     164 [ -  - ][ -  - ]:          0 :       switch (ctype)
     165                 :            :       {
     166                 :          0 :         case ProofTracer::ClauseType::ASSUMPTION: ct = 'a'; break;
     167                 :          0 :         case ProofTracer::ClauseType::INPUT: ct = 'i'; break;
     168                 :          0 :         case ProofTracer::ClauseType::THEORY: ct = 't'; break;
     169                 :            :       }
     170         [ -  - ]:          0 :       Trace("cadical::prooftracer") << ct << ": ";
     171                 :            :     }
     172                 :            : 
     173                 :            :     // Assumption clauses are the negation of a core of failed/unsat
     174                 :            :     // assumptions. Add each assumption as a unit clause.
     175         [ -  - ]:          0 :     if (ctype == ProofTracer::ClauseType::ASSUMPTION)
     176                 :            :     {
     177         [ -  - ]:          0 :       for (const auto lit : cl)
     178                 :            :       {
     179                 :          0 :         auto& sat_clause = unsat_core.emplace_back();
     180                 :          0 :         sat_clause.emplace_back(toSatLiteral(-lit));
     181         [ -  - ]:          0 :         Trace("cadical::prooftracer") << -lit << " 0" << std::endl;
     182                 :            :       }
     183                 :            :     }
     184                 :            :     else
     185                 :            :     {
     186                 :          0 :       auto& sat_clause = unsat_core.emplace_back();
     187         [ -  - ]:          0 :       for (const auto& lit : cl)
     188                 :            :       {
     189         [ -  - ]:          0 :         Trace("cadical::prooftracer") << lit << " ";
     190                 :          0 :         sat_clause.emplace_back(toSatLiteral(lit));
     191                 :            :       }
     192         [ -  - ]:          0 :       Trace("cadical::prooftracer") << "0" << std::endl;
     193                 :            :     }
     194         [ -  - ]:          0 :   }
     195                 :          0 : }
     196                 :            : 
     197                 :            : }  // namespace cvc5::internal::prop::cadical