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                 :            :  * Proof set utility.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__PROOF__PROOF_SET_H
      16                 :            : #define CVC5__PROOF__PROOF_SET_H
      17                 :            : 
      18                 :            : #include <memory>
      19                 :            : 
      20                 :            : #include "context/cdlist.h"
      21                 :            : #include "context/context.h"
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : 
      25                 :            : class Env;
      26                 :            : 
      27                 :            : /**
      28                 :            :  * A (context-dependent) set of proofs, which is used for memory
      29                 :            :  * management purposes.
      30                 :            :  */
      31                 :            : template <typename T>
      32                 :            : class CDProofSet
      33                 :            : {
      34                 :            :  public:
      35                 :      75368 :   CDProofSet(Env& env, context::Context* c, std::string namePrefix = "Proof")
      36                 :      75368 :       : d_env(env), d_proofs(c), d_namePrefix(namePrefix)
      37                 :            :   {
      38                 :      75368 :   }
      39                 :            :   /**
      40                 :            :    * Allocate a new proof.
      41                 :            :    *
      42                 :            :    * This returns a fresh proof object that remains alive in the context given
      43                 :            :    * to this class. Internally, this adds a new proof of type T to a
      44                 :            :    * context-dependent list of proofs and passes the following arguments to the
      45                 :            :    * T constructor:
      46                 :            :    *   pnm, args..., name
      47                 :            :    * where pnm is the proof node manager
      48                 :            :    * provided to this proof set upon construction, args... are the arguments to
      49                 :            :    * allocateProof() and name is the namePrefix with an appended index.
      50                 :            :    */
      51                 :            :   template <typename... Args>
      52                 :      27916 :   T* allocateProof(Args&&... args)
      53                 :            :   {
      54                 :      55832 :     d_proofs.push_back(std::make_shared<T>(
      55                 :            :         d_env,
      56                 :            :         std::forward<Args>(args)...,
      57                 :      27916 :         d_namePrefix + "_" + std::to_string(d_proofs.size())));
      58                 :      27916 :     return d_proofs.back().get();
      59                 :            :   }
      60                 :            : 
      61                 :            :  protected:
      62                 :            :   /** Reference to env */
      63                 :            :   Env& d_env;
      64                 :            :   /** A context-dependent list of lazy proofs. */
      65                 :            :   context::CDList<std::shared_ptr<T>> d_proofs;
      66                 :            :   /** The name prefix of the lazy proofs */
      67                 :            :   std::string d_namePrefix;
      68                 :            : };
      69                 :            : 
      70                 :            : }  // namespace cvc5::internal
      71                 :            : 
      72                 :            : #endif /* CVC5__PROOF__LAZY_PROOF_SET_H */