Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Gereon Kremer
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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 abstract proof generator class.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__PROOF__PROOF_GENERATOR_H
      19                 :            : #define CVC5__PROOF__PROOF_GENERATOR_H
      20                 :            : 
      21                 :            : #include "expr/node.h"
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : 
      25                 :            : class CDProof;
      26                 :            : class ProofNode;
      27                 :            : 
      28                 :            : /** An overwrite policy for CDProof */
      29                 :            : enum class CDPOverwrite : uint32_t
      30                 :            : {
      31                 :            :   // always overwrite an existing step.
      32                 :            :   ALWAYS,
      33                 :            :   // overwrite ASSUME with non-ASSUME steps.
      34                 :            :   ASSUME_ONLY,
      35                 :            :   // never overwrite an existing step.
      36                 :            :   NEVER,
      37                 :            : };
      38                 :            : /** Writes a overwrite policy name to a stream. */
      39                 :            : std::ostream& operator<<(std::ostream& out, CDPOverwrite opol);
      40                 :            : 
      41                 :            : /**
      42                 :            :  * An abstract proof generator class.
      43                 :            :  *
      44                 :            :  * A proof generator is intended to be used as a utility e.g. in theory
      45                 :            :  * solvers for constructing and storing proofs internally. A theory may have
      46                 :            :  * multiple instances of ProofGenerator objects, e.g. if it has more than one
      47                 :            :  * way of justifying lemmas or conflicts.
      48                 :            :  *
      49                 :            :  * A proof generator has two main interfaces for generating proofs:
      50                 :            :  * (1) getProofFor, and (2) addProofTo. The latter is optional.
      51                 :            :  *
      52                 :            :  * The addProofTo method can be used as an optimization for avoiding
      53                 :            :  * the construction of the ProofNode for a given fact.
      54                 :            :  *
      55                 :            :  * If no implementation of addProofTo is provided, then addProofTo(f, pf)
      56                 :            :  * calls getProofFor(f) and links the topmost ProofNode of the returned proof
      57                 :            :  * into pf. Note this top-most ProofNode can be avoided in the addProofTo
      58                 :            :  * method.
      59                 :            :  */
      60                 :            : class ProofGenerator
      61                 :            : {
      62                 :            :  public:
      63                 :            :   ProofGenerator();
      64                 :            :   virtual ~ProofGenerator();
      65                 :            :   /** Get the proof for formula f
      66                 :            :    *
      67                 :            :    * This forces the proof generator to construct a proof for formula f and
      68                 :            :    * return it. If this is an "eager" proof generator, this function is expected
      69                 :            :    * to be implemented as a map lookup. If this is a "lazy" proof generator,
      70                 :            :    * this function is expected to invoke a proof producing procedure of the
      71                 :            :    * generator.
      72                 :            :    *
      73                 :            :    * It should be the case that hasProofFor(f) is true.
      74                 :            :    *
      75                 :            :    * @param f The fact to get the proof for.
      76                 :            :    * @return The proof for f.
      77                 :            :    */
      78                 :            :   virtual std::shared_ptr<ProofNode> getProofFor(Node f);
      79                 :            :   /**
      80                 :            :    * Add the proof for formula f to proof pf. The proof of f is overwritten in
      81                 :            :    * pf based on the policy opolicy.
      82                 :            :    *
      83                 :            :    * @param f The fact to get the proof for.
      84                 :            :    * @param pf The CDProof object to add the proof to.
      85                 :            :    * @param opolicy The overwrite policy for adding to pf.
      86                 :            :    * @param doCopy Whether to do a deep copy of the proof steps into pf.
      87                 :            :    * @return True if this call was sucessful.
      88                 :            :    */
      89                 :            :   virtual bool addProofTo(Node f,
      90                 :            :                           CDProof* pf,
      91                 :            :                           CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY,
      92                 :            :                           bool doCopy = false);
      93                 :            :   /**
      94                 :            :    * Can we give the proof for formula f? This is used for debugging. This
      95                 :            :    * returns false if the generator cannot provide a proof of formula f.
      96                 :            :    *
      97                 :            :    * Also notice that this function does not require the proof for f to be
      98                 :            :    * constructed at the time of this call. Thus, if this is a "lazy" proof
      99                 :            :    * generator, it is expected that this call is implemented as a map lookup
     100                 :            :    * into the bookkeeping maintained by the generator only.
     101                 :            :    *
     102                 :            :    * Notice the default return value is true. In other words, a proof generator
     103                 :            :    * may choose to override this function to verify the construction, although
     104                 :            :    * we do not insist this is the case.
     105                 :            :    */
     106                 :    5105640 :   virtual bool hasProofFor(Node f) { return true; }
     107                 :            :   /** Identify this generator (for debugging, etc..) */
     108                 :            :   virtual std::string identify() const = 0;
     109                 :            : };
     110                 :            : 
     111                 :            : }  // namespace cvc5::internal
     112                 :            : 
     113                 :            : #endif /* CVC5__PROOF__PROOF_GENERATOR_H */