GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/inference_manager.cpp Lines: 62 62 100.0 %
Date: 2021-03-23 Branches: 133 244 54.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inference_manager.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 Datatypes inference manager
13
 **/
14
15
#include "theory/datatypes/inference_manager.h"
16
17
#include "expr/dtype.h"
18
#include "options/datatypes_options.h"
19
#include "smt/smt_statistics_registry.h"
20
#include "theory/eager_proof_generator.h"
21
#include "theory/rewriter.h"
22
#include "theory/theory.h"
23
#include "theory/theory_state.h"
24
#include "theory/trust_substitutions.h"
25
26
using namespace CVC4::kind;
27
28
namespace CVC4 {
29
namespace theory {
30
namespace datatypes {
31
32
8997
InferenceManager::InferenceManager(Theory& t,
33
                                   TheoryState& state,
34
8997
                                   ProofNodeManager* pnm)
35
    : InferenceManagerBuffered(t, state, pnm, "theory::datatypes"),
36
      d_pnm(pnm),
37
      d_ipc(pnm == nullptr ? nullptr
38
962
                           : new InferProofCons(state.getSatContext(), pnm)),
39
      d_lemPg(pnm == nullptr
40
                  ? nullptr
41
                  : new EagerProofGenerator(
42
9959
                      pnm, state.getUserContext(), "datatypes::lemPg"))
43
{
44
8997
  d_false = NodeManager::currentNM()->mkConst(false);
45
8997
}
46
47
8994
InferenceManager::~InferenceManager()
48
{
49
8994
}
50
51
420957
void InferenceManager::addPendingInference(Node conc,
52
                                           InferenceId id,
53
                                           Node exp,
54
                                           bool forceLemma)
55
{
56
  // if we are forcing the inference to be processed as a lemma, or if the
57
  // inference must be sent as a lemma based on the policy in
58
  // mustCommunicateFact.
59
420957
  if (forceLemma || DatatypesInference::mustCommunicateFact(conc, exp))
60
  {
61
9304
    d_pendingLem.emplace_back(new DatatypesInference(this, conc, exp, id));
62
  }
63
  else
64
  {
65
411653
    d_pendingFact.emplace_back(new DatatypesInference(this, conc, exp, id));
66
  }
67
420957
}
68
69
3462722
void InferenceManager::process()
70
{
71
  // process pending lemmas, used infrequently, only for definitional lemmas
72
3462722
  doPendingLemmas();
73
  // now process the pending facts
74
3462722
  doPendingFacts();
75
3462722
}
76
77
1549
void InferenceManager::sendDtLemma(Node lem, InferenceId id, LemmaProperty p)
78
{
79
1549
  if (isProofEnabled())
80
  {
81
126
    TrustNode trn = processDtLemma(lem, Node::null(), id);
82
63
    trustedLemma(trn, id);
83
63
    return;
84
  }
85
  // otherwise send as a normal lemma directly
86
1486
  lemma(lem, id, p);
87
}
88
89
5354
void InferenceManager::sendDtConflict(const std::vector<Node>& conf, InferenceId id)
90
{
91
5354
  if (isProofEnabled())
92
  {
93
1546
    Node exp = NodeManager::currentNM()->mkAnd(conf);
94
773
    prepareDtInference(d_false, exp, id, d_ipc.get());
95
  }
96
5354
  conflictExp(id, conf, d_ipc.get());
97
5354
}
98
99
442985
bool InferenceManager::isProofEnabled() const { return d_ipc != nullptr; }
100
101
9342
TrustNode InferenceManager::processDtLemma(Node conc, Node exp, InferenceId id)
102
{
103
  // set up a proof constructor
104
18684
  std::shared_ptr<InferProofCons> ipcl;
105
9342
  if (isProofEnabled())
106
  {
107
757
    ipcl = std::make_shared<InferProofCons>(nullptr, d_pnm);
108
  }
109
9342
  conc = prepareDtInference(conc, exp, id, ipcl.get());
110
  // send it as a lemma
111
18684
  Node lem;
112
9342
  if (!exp.isNull() && !exp.isConst())
113
  {
114
9012
    lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, conc);
115
  }
116
  else
117
  {
118
330
    lem = conc;
119
  }
120
9342
  if (isProofEnabled())
121
  {
122
    // store its proof
123
1514
    std::shared_ptr<ProofNode> pbody = ipcl->getProofFor(conc);
124
1514
    std::shared_ptr<ProofNode> pn = pbody;
125
757
    if (!exp.isNull() && !exp.isConst())
126
    {
127
1296
      std::vector<Node> expv;
128
648
      expv.push_back(exp);
129
648
      pn = d_pnm->mkScope(pbody, expv);
130
    }
131
757
    d_lemPg->setProofFor(lem, pn);
132
  }
133
18684
  return TrustNode::mkTrustLemma(lem, d_lemPg.get());
134
}
135
136
407283
Node InferenceManager::processDtFact(Node conc,
137
                                     Node exp,
138
                                     InferenceId id,
139
                                     ProofGenerator*& pg)
140
{
141
407283
  pg = d_ipc.get();
142
407283
  return prepareDtInference(conc, exp, id, d_ipc.get());
143
}
144
145
417398
Node InferenceManager::prepareDtInference(Node conc,
146
                                          Node exp,
147
                                          InferenceId id,
148
                                          InferProofCons* ipc)
149
{
150
834796
  Trace("dt-lemma-debug") << "prepareDtInference : " << conc << " via " << exp
151
417398
                          << " by " << id << std::endl;
152
417398
  if (conc.getKind() == EQUAL && conc[0].getType().isBoolean())
153
  {
154
    // must turn (= conc false) into (not conc)
155
399
    conc = Rewriter::rewrite(conc);
156
  }
157
417398
  if (isProofEnabled())
158
  {
159
14922
    Assert(ipc != nullptr);
160
    // If proofs are enabled, notify the proof constructor.
161
    // Notice that we have to reconstruct a datatypes inference here. This is
162
    // because the inference in the pending vector may be destroyed as we are
163
    // processing this inference, if we triggered to backtrack based on the
164
    // call below, since it is a unique pointer.
165
    std::shared_ptr<DatatypesInference> di =
166
29844
        std::make_shared<DatatypesInference>(this, conc, exp, id);
167
14922
    ipc->notifyFact(di);
168
  }
169
417398
  return conc;
170
}
171
172
}  // namespace datatypes
173
}  // namespace theory
174
26685
}  // namespace CVC4