GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/trust_substitutions.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file trust_substitutions.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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
28076
class TrustSubstitutionMap
38
{
39
 public:
40
  TrustSubstitutionMap(context::Context* c,
41
                       ProofNodeManager* pnm,
42
                       std::string name = "TrustSubstitutionMap",
43
                       PfRule trustId = PfRule::PREPROCESS_LEMMA,
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 */