GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/strings/inference_manager.cpp Lines: 164 186 88.2 %
Date: 2021-03-23 Branches: 358 800 44.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inference_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer, Mudathir Mohamed
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 Implementation of the inference manager for the theory of strings.
13
 **/
14
15
#include "theory/strings/inference_manager.h"
16
17
#include "options/strings_options.h"
18
#include "theory/ext_theory.h"
19
#include "theory/rewriter.h"
20
#include "theory/strings/theory_strings_utils.h"
21
#include "theory/strings/word.h"
22
23
using namespace std;
24
using namespace CVC4::context;
25
using namespace CVC4::kind;
26
27
namespace CVC4 {
28
namespace theory {
29
namespace strings {
30
31
8997
InferenceManager::InferenceManager(Theory& t,
32
                                   SolverState& s,
33
                                   TermRegistry& tr,
34
                                   ExtTheory& e,
35
                                   SequencesStatistics& statistics,
36
8997
                                   ProofNodeManager* pnm)
37
    : InferenceManagerBuffered(t, s, pnm, "theory::strings", false),
38
      d_state(s),
39
      d_termReg(tr),
40
      d_extt(e),
41
      d_statistics(statistics),
42
962
      d_ipc(pnm ? new InferProofCons(d_state.getSatContext(), pnm, d_statistics)
43
9959
                : nullptr)
44
{
45
8997
  NodeManager* nm = NodeManager::currentNM();
46
8997
  d_zero = nm->mkConst(Rational(0));
47
8997
  d_one = nm->mkConst(Rational(1));
48
8997
  d_true = nm->mkConst(true);
49
8997
  d_false = nm->mkConst(false);
50
8997
}
51
52
25158
void InferenceManager::doPending()
53
{
54
25158
  doPendingFacts();
55
25158
  if (d_state.isInConflict())
56
  {
57
    // just clear the pending vectors, nothing else to do
58
1597
    clearPendingLemmas();
59
1597
    clearPendingPhaseRequirements();
60
1597
    return;
61
  }
62
23561
  doPendingLemmas();
63
23561
  doPendingPhaseRequirements();
64
}
65
66
16400
bool InferenceManager::sendInternalInference(std::vector<Node>& exp,
67
                                             Node conc,
68
                                             InferenceId infer)
69
{
70
32800
  if (conc.getKind() == AND
71
32800
      || (conc.getKind() == NOT && conc[0].getKind() == OR))
72
  {
73
2986
    Node conj = conc.getKind() == AND ? conc : conc[0];
74
1493
    bool pol = conc.getKind() == AND;
75
1493
    bool ret = true;
76
5139
    for (const Node& cc : conj)
77
    {
78
3646
      bool retc = sendInternalInference(exp, pol ? cc : cc.negate(), infer);
79
3646
      ret = ret && retc;
80
    }
81
1493
    return ret;
82
  }
83
14907
  bool pol = conc.getKind() != NOT;
84
29814
  Node lit = pol ? conc : conc[0];
85
14907
  if (lit.getKind() == EQUAL)
86
  {
87
8920
    for (unsigned i = 0; i < 2; i++)
88
    {
89
6040
      if (!lit[i].isConst() && !d_state.hasTerm(lit[i]))
90
      {
91
        // introduces a new non-constant term, do not infer
92
140
        return false;
93
      }
94
    }
95
    // does it already hold?
96
10098
    if (pol ? d_state.areEqual(lit[0], lit[1])
97
7218
            : d_state.areDisequal(lit[0], lit[1]))
98
    {
99
2654
      return true;
100
    }
101
  }
102
11887
  else if (lit.isConst())
103
  {
104
4
    if (lit.getConst<bool>())
105
    {
106
      Assert(pol);
107
      // trivially holds
108
      return true;
109
    }
110
  }
111
11883
  else if (!d_state.hasTerm(lit))
112
  {
113
    // introduces a new non-constant term, do not infer
114
9971
    return false;
115
  }
116
1912
  else if (d_state.areEqual(lit, pol ? d_true : d_false))
117
  {
118
    // already holds
119
1906
    return true;
120
  }
121
236
  sendInference(exp, conc, infer);
122
236
  return true;
123
}
124
125
26785
bool InferenceManager::sendInference(const std::vector<Node>& exp,
126
                                     const std::vector<Node>& noExplain,
127
                                     Node eq,
128
                                     InferenceId infer,
129
                                     bool isRev,
130
                                     bool asLemma)
131
{
132
26785
  if (eq.isNull())
133
  {
134
32
    eq = d_false;
135
  }
136
26753
  else if (Rewriter::rewrite(eq) == d_true)
137
  {
138
    // if trivial, return
139
    return false;
140
  }
141
  // wrap in infer info and send below
142
53570
  InferInfo ii(infer);
143
26785
  ii.d_idRev = isRev;
144
26785
  ii.d_conc = eq;
145
26785
  ii.d_premises = exp;
146
26785
  ii.d_noExplain = noExplain;
147
26785
  sendInference(ii, asLemma);
148
26785
  return true;
149
}
150
151
24665
bool InferenceManager::sendInference(const std::vector<Node>& exp,
152
                                     Node eq,
153
                                     InferenceId infer,
154
                                     bool isRev,
155
                                     bool asLemma)
156
{
157
49330
  std::vector<Node> noExplain;
158
49330
  return sendInference(exp, noExplain, eq, infer, isRev, asLemma);
159
}
160
161
28910
void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
162
{
163
28910
  Assert(!ii.isTrivial());
164
  // set that this inference manager will be processing this inference
165
28910
  ii.d_sim = this;
166
57820
  Trace("strings-infer-debug")
167
28910
      << "sendInference: " << ii << ", asLemma = " << asLemma << std::endl;
168
  // check if we should send a conflict, lemma or a fact
169
28910
  if (ii.isConflict())
170
  {
171
743
    Trace("strings-infer-debug") << "...as conflict" << std::endl;
172
1486
    Trace("strings-lemma") << "Strings::Conflict: " << ii.d_premises << " by "
173
743
                           << ii.getId() << std::endl;
174
743
    Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_premises << " by " << ii.getId() << std::endl;
175
743
    ++(d_statistics.d_conflictsInfer);
176
    // process the conflict immediately
177
743
    processConflict(ii);
178
743
    return;
179
  }
180
43480
  else if (asLemma || options::stringInferAsLemmas() || !ii.isFact())
181
  {
182
14148
    Trace("strings-infer-debug") << "...as lemma" << std::endl;
183
14148
    addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(ii)));
184
14148
    return;
185
  }
186
14019
  if (options::stringInferSym())
187
  {
188
27648
    std::vector<Node> unproc;
189
56612
    for (const Node& ac : ii.d_premises)
190
    {
191
42593
      d_termReg.removeProxyEqs(ac, unproc);
192
    }
193
14019
    if (unproc.empty())
194
    {
195
780
      Node eqs = ii.d_conc;
196
      // keep the same id for now, since we are transforming the form of the
197
      // inference, not the root reason.
198
780
      InferInfo iiSubsLem(ii.getId());
199
390
      iiSubsLem.d_sim = this;
200
390
      iiSubsLem.d_conc = eqs;
201
390
      if (Trace.isOn("strings-lemma-debug"))
202
      {
203
        Trace("strings-lemma-debug")
204
            << "Strings::Infer " << iiSubsLem << std::endl;
205
        Trace("strings-lemma-debug")
206
            << "Strings::Infer Alternate : " << eqs << std::endl;
207
      }
208
390
      Trace("strings-infer-debug") << "...as symbolic lemma" << std::endl;
209
390
      addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSubsLem)));
210
390
      return;
211
    }
212
13629
    if (Trace.isOn("strings-lemma-debug"))
213
    {
214
      for (const Node& u : unproc)
215
      {
216
        Trace("strings-lemma-debug")
217
            << "  non-trivial explanation : " << u << std::endl;
218
      }
219
    }
220
  }
221
13629
  Trace("strings-infer-debug") << "...as fact" << std::endl;
222
  // add to pending to be processed as a fact
223
13629
  addPendingFact(std::unique_ptr<InferInfo>(new InferInfo(ii)));
224
}
225
226
431
bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq)
227
{
228
862
  Node eq = a.eqNode(b);
229
431
  eq = Rewriter::rewrite(eq);
230
431
  if (eq.isConst())
231
  {
232
    return false;
233
  }
234
431
  NodeManager* nm = NodeManager::currentNM();
235
862
  InferInfo iiSplit(infer);
236
431
  iiSplit.d_sim = this;
237
431
  iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
238
431
  eq = Rewriter::rewrite(eq);
239
431
  addPendingPhaseRequirement(eq, preq);
240
431
  addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSplit)));
241
431
  return true;
242
}
243
244
6
void InferenceManager::setIncomplete() { d_out.setIncomplete(); }
245
246
461443
void InferenceManager::addToExplanation(Node a,
247
                                        Node b,
248
                                        std::vector<Node>& exp) const
249
{
250
461443
  if (a != b)
251
  {
252
442692
    Debug("strings-explain")
253
221346
        << "Add to explanation : " << a << " == " << b << std::endl;
254
221346
    Assert(d_state.areEqual(a, b));
255
221346
    exp.push_back(a.eqNode(b));
256
  }
257
461443
}
258
259
void InferenceManager::addToExplanation(Node lit, std::vector<Node>& exp) const
260
{
261
  if (!lit.isNull())
262
  {
263
    Assert(!lit.isConst());
264
    exp.push_back(lit);
265
  }
266
}
267
268
2462190
bool InferenceManager::hasProcessed() const
269
{
270
2462190
  return d_state.isInConflict() || hasPending();
271
}
272
273
void InferenceManager::markCongruent(Node a, Node b)
274
{
275
  Assert(a.getKind() == b.getKind());
276
  if (d_extt.hasFunctionKind(a.getKind()))
277
  {
278
    d_extt.markCongruent(a, b);
279
  }
280
}
281
282
87
void InferenceManager::markReduced(Node n, bool contextDepend)
283
{
284
87
  d_extt.markReduced(n, contextDepend);
285
87
}
286
287
1028
void InferenceManager::processConflict(const InferInfo& ii)
288
{
289
1028
  Assert(!d_state.isInConflict());
290
  // setup the fact to reproduce the proof in the call below
291
1028
  if (d_ipc != nullptr)
292
  {
293
158
    d_ipc->notifyFact(ii);
294
  }
295
  // make the trust node
296
2056
  TrustNode tconf = mkConflictExp(ii.d_premises, d_ipc.get());
297
1028
  Assert(tconf.getKind() == TrustNodeKind::CONFLICT);
298
2056
  Trace("strings-assert") << "(assert (not " << tconf.getNode()
299
1028
                          << ")) ; conflict " << ii.getId() << std::endl;
300
  // send the trusted conflict
301
1028
  trustedConflict(tconf, ii.getId());
302
1028
}
303
304
13355
void InferenceManager::processFact(InferInfo& ii, ProofGenerator*& pg)
305
{
306
26710
  Trace("strings-assert") << "(assert (=> " << ii.getPremises() << " "
307
13355
                          << ii.d_conc << ")) ; fact " << ii.getId() << std::endl;
308
26710
  Trace("strings-lemma") << "Strings::Fact: " << ii.d_conc << " from "
309
26710
                         << ii.getPremises() << " by " << ii.getId()
310
13355
                         << std::endl;
311
13355
  if (d_ipc != nullptr)
312
  {
313
    // ensure the proof generator is ready to explain this fact in the
314
    // current SAT context
315
637
    d_ipc->notifyFact(ii);
316
637
    pg = d_ipc.get();
317
  }
318
13355
}
319
320
14852
TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p)
321
{
322
14852
  Assert(!ii.isTrivial());
323
14852
  Assert(!ii.isConflict());
324
  // set up the explanation and no-explanation
325
29704
  std::vector<Node> exp;
326
45941
  for (const Node& ec : ii.d_premises)
327
  {
328
31089
    utils::flattenOp(AND, ec, exp);
329
  }
330
29704
  std::vector<Node> noExplain;
331
29704
  if (!options::stringRExplainLemmas())
332
  {
333
    // if we aren't regressing the explanation, we add all literals to
334
    // noExplain and ignore ii.d_ant.
335
    noExplain.insert(noExplain.end(), exp.begin(), exp.end());
336
  }
337
  else
338
  {
339
    // otherwise, the no-explain literals are those provided
340
17331
    for (const Node& ecn : ii.d_noExplain)
341
    {
342
2479
      utils::flattenOp(AND, ecn, noExplain);
343
    }
344
  }
345
  // ensure that the proof generator is ready to explain the final conclusion
346
  // of the lemma (ii.d_conc).
347
14852
  if (d_ipc != nullptr)
348
  {
349
803
    d_ipc->notifyFact(ii);
350
  }
351
14852
  TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipc.get());
352
29704
  Trace("strings-pending") << "Process pending lemma : " << tlem.getNode()
353
14852
                           << std::endl;
354
355
  // Process the side effects of the inference info.
356
  // Register the new skolems from this inference. We register them here
357
  // (lazily), since this is the moment when we have decided to process the
358
  // inference.
359
1048
  for (const std::pair<const LengthStatus, std::vector<Node> >& sks :
360
14852
       ii.d_skolems)
361
  {
362
2096
    for (const Node& n : sks.second)
363
    {
364
1048
      d_termReg.registerTermAtomic(n, sks.first);
365
    }
366
  }
367
14852
  if (ii.getId() == InferenceId::STRINGS_REDUCTION)
368
  {
369
1281
    p |= LemmaProperty::NEEDS_JUSTIFY;
370
  }
371
29704
  Trace("strings-assert") << "(assert " << tlem.getNode() << ") ; lemma "
372
14852
                          << ii.getId() << std::endl;
373
29704
  Trace("strings-lemma") << "Strings::Lemma: " << tlem.getNode() << " by "
374
14852
                         << ii.getId() << std::endl;
375
29704
  return tlem;
376
}
377
378
}  // namespace strings
379
}  // namespace theory
380
26685
}  // namespace CVC4