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/proof_node_manager.h"
  24 #include "expr/proof_set.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    * @return The proof generator that can prove (= x t).
  73    */
  74   ProofGenerator* addSubstitutionSolved(TNode x, TNode t, TrustNode tn);
  75   /**
  76    * Add substitutions from trust substitution map t. This adds all
  77    * substitutions from the map t and carries over its information about proofs.
  78    */
  79   void addSubstitutions(TrustSubstitutionMap& t);
  80   /**
  81    * Apply substitutions in this class to node n. Returns a trust node
  82    * proving n = n*sigma, where the proof generator is provided by this class
  83    * (when proofs are enabled).
  84    */
  85   TrustNode apply(Node n, bool doRewrite = true);
  86
  87  private:
  88   /** Are proofs enabled? */
  89   bool isProofEnabled() const;
  90   /**
  91    * Get current substitution. This returns a node of the form:
  92    *   (and (= x1 t1) ... (= xn tn))
  93    * where (x1, t1) ... (xn, tn) have been registered via addSubstitution above.
  94    * Moreover, it ensures that d_subsPg has a proof of the returned value.
  95    */
  96   Node getCurrentSubstitution();
  97   /** The context used here */
  98   context::Context* d_ctx;
  99   /** The substitution map */
 100   SubstitutionMap d_subs;
 101   /** The proof node manager */
 102   ProofNodeManager* d_pnm;
 103   /** A context-dependent list of trust nodes */
 104   context::CDList<TrustNode> d_tsubs;
 105   /** Theory proof step buffer */
 106   std::unique_ptr<TheoryProofStepBuffer> d_tspb;
 107   /** A lazy proof for substitution steps */
 108   std::unique_ptr<LazyCDProof> d_subsPg;
 109   /** A lazy proof for apply steps */
 110   std::unique_ptr<LazyCDProof> d_applyPg;
 111   /**
 112    * A context-dependent list of LazyCDProof, allocated for internal steps.
 113    */
 114   CDProofSet<LazyCDProof> d_helperPf;
 115   /**
 116    * The formula corresponding to the current substitution. This is of the form
 117    *   (and (= x1 t1) ... (= xn tn))
 118    * when the substitution map contains { x1 -> t1, ... xn -> tn }. This field
 119    * is updated on demand. When this class applies a substitution to a node,
 120    * this formula is computed and recorded as the premise of a
 121    * MACRO_SR_EQ_INTRO step.
 122    */
 123   context::CDO<Node> d_currentSubs;
 124   /** Name for debugging */
 125   std::string d_name;
 126   /**
 127    * The placeholder trusted PfRule identifier for calls to addSubstitution
 128    * that are not given proof generators.
 129    */
 130   PfRule d_trustId;
 131   /** The method id for which form of substitution to apply */
 132   MethodId d_ids;
 133 };
 134
 135 }  // namespace theory
 136 }  // namespace CVC4
 137
 138 #endif /* CVC4__THEORY__TRUST_SUBSTITUTIONS_H */