src/theory/trust_substitutions.h

   1 /*********************                                                        */
   2 /*! \file trust_substitutions.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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.\endverbatim
  11  **
  12  ** \brief Trust substitutions
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__TRUST_SUBSTITUTIONS_H
  18 #define CVC4__THEORY__TRUST_SUBSTITUTIONS_H
  19
  20 #include "context/cdlist.h"
  21 #include "context/context.h"
  22 #include "expr/lazy_proof.h"
  23 #include "expr/lazy_proof_set.h"
  24 #include "expr/proof_node_manager.h"
  25 #include "expr/term_conversion_proof_generator.h"
  26 #include "theory/eager_proof_generator.h"
  27 #include "theory/substitutions.h"
  28 #include "theory/theory_proof_step_buffer.h"
  29 #include "theory/trust_node.h"
  30
  31 namespace CVC4 {
  32 namespace theory {
  33
  34 /**
  35  * A layer on top of SubstitutionMap that tracks proofs.
  36  */
  37 class TrustSubstitutionMap
  38 {
  39  public:
  40   TrustSubstitutionMap(context::Context* c,
  41                        ProofNodeManager* pnm,
  42                        std::string name = "TrustSubstitutionMap",
  43                        PfRule trustId = PfRule::TRUST_SUBS_MAP,
  44                        MethodId ids = MethodId::SB_DEFAULT);
  45   /** Gets a reference to the underlying substitution map */
  46   SubstitutionMap& get();
  47   /**
  48    * Add substitution x -> t, where pg can provide a closed proof of (= x t)
  49    * in the remainder of this user context.
  50    */
  51   void addSubstitution(TNode x, TNode t, ProofGenerator* pg = nullptr);
  52   /**
  53    * Add substitution x -> t from a single proof step with rule id, no children
  54    * and arguments args.
  55    */
  56   void addSubstitution(TNode x,
  57                        TNode t,
  58                        PfRule id,
  59                        const std::vector<Node>& args);
  60   /**
  61    * Add substitution x -> t, which was derived from the proven field of
  62    * trust node tn. In other words, (= x t) is the solved form of
  63    * tn.getProven(). This method is a helper function for methods (e.g.
  64    * ppAssert) that put literals into solved form. It should be the case
  65    * that (= x t) and tn.getProven() can be shown equivalent by rewriting.
  66    *
  67    * This ensures that we add a substitution with a proof
  68    * based on transforming the tn.getProven() to (= x t) if tn has a
  69    * non-null proof generator; otherwise if tn has no proof generator
  70    * we simply add the substitution.
  71    */
  72   void addSubstitutionSolved(TNode x, TNode t, TrustNode tn);
  73   /**
  74    * Add substitutions from trust substitution map t. This adds all
  75    * substitutions from the map t and carries over its information about proofs.
  76    */
  77   void addSubstitutions(TrustSubstitutionMap& t);
  78   /**
  79    * Apply substitutions in this class to node n. Returns a trust node
  80    * proving n = n*sigma, where the proof generator is provided by this class
  81    * (when proofs are enabled).
  82    */
  83   TrustNode apply(Node n, bool doRewrite = true);
  84
  85  private:
  86   /** Are proofs enabled? */
  87   bool isProofEnabled() const;
  88   /**
  89    * Get current substitution. This returns a node of the form:
  90    *   (and (= x1 t1) ... (= xn tn))
  91    * where (x1, t1) ... (xn, tn) have been registered via addSubstitution above.
  92    * Moreover, it ensures that d_subsPg has a proof of the returned value.
  93    */
  94   Node getCurrentSubstitution();
  95   /** The substitution map */
  96   SubstitutionMap d_subs;
  97   /** The proof node manager */
  98   ProofNodeManager* d_pnm;
  99   /** A context-dependent list of trust nodes */
 100   context::CDList<TrustNode> d_tsubs;
 101   /** Theory proof step buffer */
 102   std::unique_ptr<TheoryProofStepBuffer> d_tspb;
 103   /** A lazy proof for substitution steps */
 104   std::unique_ptr<LazyCDProof> d_subsPg;
 105   /** A lazy proof for apply steps */
 106   std::unique_ptr<LazyCDProof> d_applyPg;
 107   /**
 108    * A context-dependent list of LazyCDProof, allocated for internal steps.
 109    */
 110   LazyCDProofSet d_helperPf;
 111   /**
 112    * The formula corresponding to the current substitution. This is of the form
 113    *   (and (= x1 t1) ... (= xn tn))
 114    * when the substitution map contains { x1 -> t1, ... xn -> tn }. This field
 115    * is updated on demand. When this class applies a substitution to a node,
 116    * this formula is computed and recorded as the premise of a
 117    * MACRO_SR_EQ_INTRO step.
 118    */
 119   context::CDO<Node> d_currentSubs;
 120   /** Name for debugging */
 121   std::string d_name;
 122   /**
 123    * The placeholder trusted PfRule identifier for calls to addSubstitution
 124    * that are not given proof generators.
 125    */
 126   PfRule d_trustId;
 127   /** The method id for which form of substitution to apply */
 128   MethodId d_ids;
 129 };
 130
 131 }  // namespace theory
 132 }  // namespace CVC4
 133
 134 #endif /* CVC4__THEORY__TRUST_SUBSTITUTIONS_H */