Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Haniel Barbosa, Andrew Reynolds, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * The module for processing proof nodes in the prop engine.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__PROP__PROOF_POST_PROCESSOR_H
      19                 :            : #define CVC5__PROP__PROOF_POST_PROCESSOR_H
      20                 :            : 
      21                 :            : #include <map>
      22                 :            : #include <unordered_set>
      23                 :            : 
      24                 :            : #include "context/cdhashset.h"
      25                 :            : #include "proof/proof_generator.h"
      26                 :            : #include "proof/proof_node_updater.h"
      27                 :            : #include "smt/env_obj.h"
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      30                 :            : namespace prop {
      31                 :            : 
      32                 :            : /**
      33                 :            :  * A callback class used by PropEngine for post-processing proof nodes by
      34                 :            :  * connecting proofs of resolution, whose leaves are clausified preprocessed
      35                 :            :  * assertions and lemmas, with the CNF transformation of these formulas, while
      36                 :            :  * expanding the generators of lemmas.
      37                 :            :  */
      38                 :            : class ProofPostprocessCallback : protected EnvObj,
      39                 :            :                                  public ProofNodeUpdaterCallback
      40                 :            : {
      41                 :            :  public:
      42                 :            :   ProofPostprocessCallback(Env& env, ProofGenerator* pg);
      43                 :      20613 :   ~ProofPostprocessCallback() {}
      44                 :            :   /**
      45                 :            :    * Initialize, called once for each new ProofNode to process. This initializes
      46                 :            :    * static information to be used by successive calls to update. For this
      47                 :            :    * callback it resets d_assumpToProof.
      48                 :            :    */
      49                 :            :   void initializeUpdate();
      50                 :            :   /** Should proof pn be updated?
      51                 :            :    *
      52                 :            :    * For this callback a proof node is updatable if it's an assumption for which
      53                 :            :    * the proof cnf straem has a proof. However if the proof node is blocked
      54                 :            :    * (which is the case for proof nodes introduced into the proof cnf stream's
      55                 :            :    * proof via expansion of its generators) then traversal is the proof node is
      56                 :            :    * cancelled, i.e., continueUpdate is set to false.
      57                 :            :    */
      58                 :            :   bool shouldUpdate(std::shared_ptr<ProofNode> pn,
      59                 :            :                     const std::vector<Node>& fa,
      60                 :            :                     bool& continueUpdate) override;
      61                 :            :   /** Update the proof rule application.
      62                 :            :    *
      63                 :            :    * Replaces assumptions by their proof in proof cnf stream. Note that in doing
      64                 :            :    * this the proof node is blocked, so that future post-processing does not
      65                 :            :    * traverse it.
      66                 :            :    *
      67                 :            :    * This method uses the cache in d_assumpToProof to avoid recomputing proofs
      68                 :            :    * for the same assumption (in the same scope).
      69                 :            :    */
      70                 :            :   bool update(Node res,
      71                 :            :               ProofRule id,
      72                 :            :               const std::vector<Node>& children,
      73                 :            :               const std::vector<Node>& args,
      74                 :            :               CDProof* cdp,
      75                 :            :               bool& continueUpdate) override;
      76                 :            : 
      77                 :            :  private:
      78                 :            :   /**
      79                 :            :    * Blocks a proof, so that it is not further updated by a post processor of
      80                 :            :    * this class's proof. */
      81                 :            :   void addBlocked(std::shared_ptr<ProofNode> pfn);
      82                 :            : 
      83                 :            :   /**
      84                 :            :    * Whether a given proof is blocked for further updates.  An example of a
      85                 :            :    * blocked proof node is one integrated into this class via an external proof
      86                 :            :    * generator. */
      87                 :            :   bool isBlocked(std::shared_ptr<ProofNode> pfn);
      88                 :            :   /** The cnf stream proof generator */
      89                 :            :   ProofGenerator* d_pg;
      90                 :            :   /** Blocked proofs.
      91                 :            :    *
      92                 :            :    * These are proof nodes added to this class by external generators. */
      93                 :            :   context::CDHashSet<std::shared_ptr<ProofNode>, ProofNodeHashFunction>
      94                 :            :       d_blocked;
      95                 :            :   //---------------------------------reset at the begining of each update
      96                 :            :   /** Mapping assumptions to their proof from cnf transformation */
      97                 :            :   std::map<Node, std::shared_ptr<ProofNode> > d_assumpToProof;
      98                 :            :   //---------------------------------end reset at the begining of each update
      99                 :            : };
     100                 :            : 
     101                 :            : /**
     102                 :            :  * The proof postprocessor module. This postprocesses the refutation proof
     103                 :            :  * produced by the SAT solver. Its main task is to connect the refutation's
     104                 :            :  * assumptions to the CNF transformation proof in ProofGenerator.
     105                 :            :  */
     106                 :            : class ProofPostprocess : protected EnvObj
     107                 :            : {
     108                 :            :  public:
     109                 :            :   ProofPostprocess(Env& env, ProofGenerator* pg);
     110                 :            :   ~ProofPostprocess();
     111                 :            :   /** post-process
     112                 :            :    *
     113                 :            :    * The post-processing is done via a proof node updater run on pf with this
     114                 :            :    * class's callback d_cb.
     115                 :            :    */
     116                 :            :   void process(std::shared_ptr<ProofNode> pf);
     117                 :            : 
     118                 :            :  private:
     119                 :            :   /** The post process callback */
     120                 :            :   ProofPostprocessCallback d_cb;
     121                 :            : };
     122                 :            : 
     123                 :            : }  // namespace prop
     124                 :            : }  // namespace cvc5::internal
     125                 :            : 
     126                 :            : #endif