GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/trust_substitutions.cpp Lines: 95 103 92.2 %
Date: 2021-03-22 Branches: 228 466 48.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file trust_substitutions.cpp
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 "theory/trust_substitutions.h"
16
17
#include "theory/rewriter.h"
18
19
namespace CVC4 {
20
namespace theory {
21
22
28079
TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c,
23
                                           ProofNodeManager* pnm,
24
                                           std::string name,
25
                                           PfRule trustId,
26
28079
                                           MethodId ids)
27
    : d_ctx(c),
28
      d_subs(c),
29
      d_pnm(pnm),
30
      d_tsubs(c),
31
4192
      d_tspb(pnm ? new TheoryProofStepBuffer(pnm->getChecker()) : nullptr),
32
      d_subsPg(
33
4192
          pnm ? new LazyCDProof(pnm, nullptr, c, "TrustSubstitutionMap::subsPg")
34
              : nullptr),
35
      d_applyPg(pnm ? new LazyCDProof(
36
4192
                          pnm, nullptr, c, "TrustSubstitutionMap::applyPg")
37
                    : nullptr),
38
      d_helperPf(pnm, c),
39
      d_currentSubs(c),
40
      d_name(name),
41
      d_trustId(trustId),
42
40655
      d_ids(ids)
43
{
44
28079
}
45
46
53996
void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg)
47
{
48
107992
  Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: add " << x
49
53996
                      << " -> " << t << std::endl;
50
53996
  d_subs.addSubstitution(x, t);
51
53996
  if (isProofEnabled())
52
  {
53
13848
    TrustNode tnl = TrustNode::mkTrustRewrite(x, t, pg);
54
6924
    d_tsubs.push_back(tnl);
55
    // current substitution node is no longer valid.
56
6924
    d_currentSubs = Node::null();
57
    // add to lazy proof
58
6924
    d_subsPg->addLazyStep(tnl.getProven(), pg, d_trustId);
59
  }
60
53996
}
61
62
void TrustSubstitutionMap::addSubstitution(TNode x,
63
                                           TNode t,
64
                                           PfRule id,
65
                                           const std::vector<Node>& args)
66
{
67
  if (!isProofEnabled())
68
  {
69
    addSubstitution(x, t, nullptr);
70
    return;
71
  }
72
  LazyCDProof* stepPg = d_helperPf.allocateProof(nullptr, d_ctx);
73
  Node eq = x.eqNode(t);
74
  stepPg->addStep(eq, id, {}, args);
75
  addSubstitution(x, t, stepPg);
76
}
77
78
51031
ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x,
79
                                                            TNode t,
80
                                                            TrustNode tn)
81
{
82
102062
  Trace("trust-subs") << "TrustSubstitutionMap::addSubstitutionSolved: add "
83
102062
                      << x << " -> " << t << " from " << tn.getProven()
84
51031
                      << std::endl;
85
51031
  if (!isProofEnabled() || tn.getGenerator() == nullptr)
86
  {
87
    // no generator or not proof enabled, nothing to do
88
47072
    addSubstitution(x, t, nullptr);
89
47072
    Trace("trust-subs") << "...no proof" << std::endl;
90
47072
    return nullptr;
91
  }
92
7918
  Node eq = x.eqNode(t);
93
7918
  Node proven = tn.getProven();
94
  // notice that this checks syntactic equality, not CDProof::isSame since
95
  // tn.getGenerator() is not necessarily robust to symmetry.
96
3959
  if (eq == proven)
97
  {
98
    // no rewrite required, just use the generator
99
3001
    addSubstitution(x, t, tn.getGenerator());
100
3001
    Trace("trust-subs") << "...use generator directly" << std::endl;
101
3001
    return tn.getGenerator();
102
  }
103
958
  LazyCDProof* solvePg = d_helperPf.allocateProof(nullptr, d_ctx);
104
  // Try to transform tn.getProven() to (= x t) here, if necessary
105
958
  if (!d_tspb->applyPredTransform(proven, eq, {}))
106
  {
107
    // failed to rewrite
108
12
    addSubstitution(x, t, nullptr);
109
12
    Trace("trust-subs") << "...failed to rewrite" << std::endl;
110
12
    return nullptr;
111
  }
112
946
  Trace("trust-subs") << "...successful rewrite" << std::endl;
113
946
  solvePg->addSteps(*d_tspb.get());
114
946
  d_tspb->clear();
115
  // link the given generator
116
946
  solvePg->addLazyStep(proven, tn.getGenerator());
117
946
  addSubstitution(x, t, solvePg);
118
946
  return solvePg;
119
}
120
121
9374
void TrustSubstitutionMap::addSubstitutions(TrustSubstitutionMap& t)
122
{
123
9374
  if (!isProofEnabled())
124
  {
125
    // just use the basic utility
126
7803
    d_subs.addSubstitutions(t.get());
127
7803
    return;
128
  }
129
  // call addSubstitution above in sequence
130
4536
  for (const TrustNode& tns : t.d_tsubs)
131
  {
132
5930
    Node proven = tns.getProven();
133
2965
    addSubstitution(proven[0], proven[1], tns.getGenerator());
134
  }
135
}
136
137
642338
TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
138
{
139
1284676
  Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n
140
642338
                      << std::endl;
141
1284676
  Node ns = d_subs.apply(n, doRewrite);
142
642336
  Trace("trust-subs") << "...subs " << ns << std::endl;
143
642336
  if (n == ns)
144
  {
145
    // no change
146
535224
    return TrustNode::null();
147
  }
148
107112
  if (!isProofEnabled())
149
  {
150
    // no proofs, use null generator
151
82195
    return TrustNode::mkTrustRewrite(n, ns, nullptr);
152
  }
153
49834
  Node cs = getCurrentSubstitution();
154
49834
  Trace("trust-subs")
155
24917
      << "TrustSubstitutionMap::addSubstitution: current substitution is " << cs
156
24917
      << std::endl;
157
  // Easy case: if n is in the domain of the substitution, maybe it is already
158
  // a proof in the substitution proof generator. This is moreover required
159
  // to avoid cyclic proofs below. For example, if { x -> 5 } is a substitution,
160
  // and we are asked to transform x, resulting in 5, we hence must provide
161
  // a proof of (= x 5) based on the substitution. However, it must be the
162
  // case that (= x 5) is a proven fact of the substitution generator. Hence
163
  // we avoid a proof that looks like:
164
  // ---------- from d_subsPg
165
  // (= x 5)
166
  // ---------- MACRO_SR_EQ_INTRO{x}
167
  // (= x 5)
168
  // by taking the premise proof directly.
169
49834
  Node eq = n.eqNode(ns);
170
24917
  if (d_subsPg->hasStep(eq) || d_subsPg->hasGenerator(eq))
171
  {
172
374
    return TrustNode::mkTrustRewrite(n, ns, d_subsPg.get());
173
  }
174
24543
  Assert(eq != cs);
175
49086
  std::vector<Node> pfChildren;
176
24543
  if (!cs.isConst())
177
  {
178
    // note we will get more proof reuse if we do not special case AND here.
179
14938
    if (cs.getKind() == kind::AND)
180
    {
181
1146280
      for (const Node& csc : cs)
182
      {
183
1133102
        pfChildren.push_back(csc);
184
        // connect substitution generator into apply generator
185
1133102
        d_applyPg->addLazyStep(csc, d_subsPg.get());
186
      }
187
    }
188
    else
189
    {
190
1760
      pfChildren.push_back(cs);
191
      // connect substitution generator into apply generator
192
1760
      d_applyPg->addLazyStep(cs, d_subsPg.get());
193
    }
194
  }
195
24543
  if (!d_tspb->applyEqIntro(n, ns, pfChildren, d_ids))
196
  {
197
    // if we fail for any reason, we must use a trusted step instead
198
1
    d_tspb->addStep(PfRule::TRUST_SUBS_MAP, pfChildren, {eq}, eq);
199
  }
200
  // -------        ------- from external proof generators
201
  // x1 = t1 ...    xn = tn
202
  // ----------------------- AND_INTRO
203
  //   ...
204
  // --------- MACRO_SR_EQ_INTRO (or TRUST_SUBS_MAP if we failed above)
205
  // n == ns
206
  // add it to the apply proof generator.
207
  //
208
  // Notice that we use a single child to MACRO_SR_EQ_INTRO here. This is an
209
  // optimization motivated by the fact that n may be large and reused many
210
  // time. For instance, if this class is being used to track substitutions
211
  // derived during non-clausal simplification during preprocessing, it is
212
  // a fixed (possibly) large substitution applied to many terms. Having
213
  // a single child saves us from creating many proofs with n children, where
214
  // notice this proof is reused.
215
24543
  d_applyPg->addSteps(*d_tspb.get());
216
24543
  d_tspb->clear();
217
24543
  return TrustNode::mkTrustRewrite(n, ns, d_applyPg.get());
218
}
219
220
36437
SubstitutionMap& TrustSubstitutionMap::get() { return d_subs; }
221
222
246430
bool TrustSubstitutionMap::isProofEnabled() const
223
{
224
246430
  return d_subsPg != nullptr;
225
}
226
227
24917
Node TrustSubstitutionMap::getCurrentSubstitution()
228
{
229
24917
  Assert(isProofEnabled());
230
24917
  if (!d_currentSubs.get().isNull())
231
  {
232
21887
    return d_currentSubs;
233
  }
234
6060
  std::vector<Node> csubsChildren;
235
214217
  for (const TrustNode& tns : d_tsubs)
236
  {
237
211187
    csubsChildren.push_back(tns.getProven());
238
  }
239
3030
  std::reverse(csubsChildren.begin(),csubsChildren.end());
240
3030
  d_currentSubs = NodeManager::currentNM()->mkAnd(csubsChildren);
241
3030
  if (d_currentSubs.get().getKind() == kind::AND)
242
  {
243
1774
    d_subsPg->addStep(d_currentSubs, PfRule::AND_INTRO, csubsChildren, {});
244
  }
245
3030
  return d_currentSubs;
246
}
247
248
}  // namespace theory
249
26676
}  // namespace CVC4