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/context.h"
  21 #include "expr/proof_node_manager.h"
  22 #include "theory/substitutions.h"
  23 #include "theory/trust_node.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 /**
  29  * A layer on top of SubstitutionMap that tracks proofs.
  30  */
  31 class TrustSubstitutionMap
  32 {
  33  public:
  34   TrustSubstitutionMap(context::Context* c, ProofNodeManager* pnm);
  35   /** Gets a reference to the underlying substitution map */
  36   SubstitutionMap& get();
  37   /**
  38    * Add substitution x -> t, where pg can provide a closed proof of (= x t)
  39    * in the remainder of this user context.
  40    */
  41   void addSubstitution(TNode x, TNode t, ProofGenerator* pg = nullptr);
  42   /**
  43    * Add substitution x -> t, which was derived from the proven field of
  44    * trust node tn. In other words, (= x t) is the solved form of
  45    * tn.getProven(). This method is a helper function for methods (e.g.
  46    * ppAssert) that put literals into solved form. It should be the case
  47    * that (= x t) and tn.getProven() can be shown equivalent by rewriting.
  48    *
  49    * This ensures that we add a substitution with a proof
  50    * based on transforming the tn.getProven() to (= x t) if tn has a
  51    * non-null proof generator; otherwise if tn has no proof generator
  52    * we simply add the substitution.
  53    */
  54   void addSubstitutionSolved(TNode x, TNode t, TrustNode tn);
  55   /**
  56    * Apply substitutions in this class to node n. Returns a trust node
  57    * proving n = n*sigma, where the proof generator is provided by this class
  58    * (when proofs are enabled).
  59    */
  60   TrustNode apply(Node n, bool doRewrite = true);
  61
  62  private:
  63   /** Are proofs enabled? */
  64   bool isProofEnabled() const;
  65   /** The substitution map */
  66   SubstitutionMap d_subs;
  67 };
  68
  69 }  // namespace theory
  70 }  // namespace CVC4
  71
  72 #endif /* CVC4__THEORY__TRUST_SUBSTITUTIONS_H */