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

Line Exec Source
1
/*********************                                                        */
2
/*! \file preprocess_proof_generator.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 The module for proofs for preprocessing in an SMT engine.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__SMT__PREPROCESS_PROOF_GENERATOR_H
18
#define CVC4__SMT__PREPROCESS_PROOF_GENERATOR_H
19
20
#include "context/cdhashmap.h"
21
#include "expr/lazy_proof.h"
22
#include "expr/proof.h"
23
#include "expr/proof_set.h"
24
#include "expr/proof_generator.h"
25
#include "theory/trust_node.h"
26
27
namespace CVC4 {
28
29
class LazyCDProof;
30
class ProofNodeManager;
31
32
namespace smt {
33
34
/**
35
 * This is a proof generator that manages proofs for a set of formulas that
36
 * may be replaced over time. This set of formulas is implicit; formulas that
37
 * are not notified as assertions to this class are treated as assumptions.
38
 *
39
 * The main use case of this proof generator is for proofs of preprocessing,
40
 * although it can be used in other scenarios where proofs for an evolving set
41
 * of formulas is maintained. In the remainder of the description here, we
42
 * describe its role as a proof generator for proofs of preprocessing.
43
 *
44
 * This class has two main interfaces during solving:
45
 * (1) notifyNewAssert, for assertions that are not part of the input and are
46
 * added to the assertion pipeline by preprocessing passes,
47
 * (2) notifyPreprocessed, which is called when a preprocessing pass rewrites
48
 * an assertion into another.
49
 * Notice that input assertions do not need to be provided to this class.
50
 *
51
 * Its getProofFor method produces a proof for a preprocessed assertion
52
 * whose free assumptions are intended to be input assertions, which are
53
 * implictly all assertions that are not notified to this class.
54
 */
55
class PreprocessProofGenerator : public ProofGenerator
56
{
57
  typedef context::CDHashMap<Node, theory::TrustNode, NodeHashFunction>
58
      NodeTrustNodeMap;
59
60
 public:
61
  /**
62
   * @param pnm The proof node manager
63
   * @param c The context this class depends on
64
   * @param name The name of this generator (for debugging)
65
   * @param ra The proof rule to use when no generator is provided for new
66
   * assertions
67
   * @param rpp The proof rule to use when no generator is provided for
68
   * preprocessing steps.
69
   */
70
  PreprocessProofGenerator(ProofNodeManager* pnm,
71
                           context::Context* c = nullptr,
72
                           std::string name = "PreprocessProofGenerator",
73
                           PfRule ra = PfRule::PREPROCESS_LEMMA,
74
                           PfRule rpp = PfRule::PREPROCESS);
75
3848
  ~PreprocessProofGenerator() {}
76
  /**
77
   * Notify that n is an input (its proof is ASSUME).
78
   */
79
  void notifyInput(Node n);
80
  /**
81
   * Notify that n is a new assertion, where pg can provide a proof of n.
82
   */
83
  void notifyNewAssert(Node n, ProofGenerator* pg);
84
  /**  Notify a new assertion, trust node version. */
85
  void notifyNewTrustedAssert(theory::TrustNode tn);
86
  /**
87
   * Notify that n was replaced by np due to preprocessing, where pg can
88
   * provide a proof of the equality n=np.
89
   */
90
  void notifyPreprocessed(Node n, Node np, ProofGenerator* pg);
91
  /** Notify preprocessed, trust node version */
92
  void notifyTrustedPreprocessed(theory::TrustNode tnp);
93
  /**
94
   * Get proof for f, which returns a proof based on proving an equality based
95
   * on transitivity of preprocessing steps, and then using the original
96
   * assertion with EQ_RESOLVE to obtain the proof of the ending assertion f.
97
   */
98
  std::shared_ptr<ProofNode> getProofFor(Node f) override;
99
  /** Identify */
100
  std::string identify() const override;
101
  /** Get the proof manager */
102
  ProofNodeManager* getManager();
103
  /**
104
   * Allocate a helper proof. This returns a fresh lazy proof object that
105
   * remains alive in the context. This feature is used to construct
106
   * helper proofs for preprocessing, e.g. to support the skeleton of proofs
107
   * that connect AssertionPipeline::conjoin steps.
108
   */
109
  LazyCDProof* allocateHelperProof();
110
111
 private:
112
  /**
113
   * Possibly check pedantic failure for null proof generator provided
114
   * to this class.
115
   */
116
  void checkEagerPedantic(PfRule r);
117
  /** The proof node manager */
118
  ProofNodeManager* d_pnm;
119
  /** A dummy context used by this class if none is provided */
120
  context::Context d_context;
121
  /** The context used here */
122
  context::Context* d_ctx;
123
  /**
124
   * The trust node that was the source of each node constructed during
125
   * preprocessing. For each n, d_src[n] is a trust node whose node is n. This
126
   * can either be:
127
   * (1) A trust node REWRITE proving (n_src = n) for some n_src, or
128
   * (2) A trust node LEMMA proving n.
129
   */
130
  NodeTrustNodeMap d_src;
131
  /** A context-dependent list of LazyCDProof, allocated for conjoin steps */
132
  CDProofSet<LazyCDProof> d_helperProofs;
133
  /**
134
   * A cd proof for input assertions, this is an empty proof that intentionally
135
   * returns (ASSUME f) for all f.
136
   */
137
  CDProof d_inputPf;
138
  /** Name for debugging */
139
  std::string d_name;
140
  /** The trust rule for new assertions with no provided proof generator */
141
  PfRule d_ra;
142
  /** The trust rule for rewrites with no provided proof generator */
143
  PfRule d_rpp;
144
};
145
146
}  // namespace smt
147
}  // namespace CVC4
148
149
#endif