GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/theory_proxy.cpp Lines: 102 108 94.4 %
Date: 2021-03-23 Branches: 139 318 43.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_proxy.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, Dejan Jovanovic
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
#include "prop/theory_proxy.h"
18
19
#include "context/context.h"
20
#include "decision/decision_engine.h"
21
#include "options/decision_options.h"
22
#include "options/smt_options.h"
23
#include "proof/cnf_proof.h"
24
#include "prop/cnf_stream.h"
25
#include "prop/prop_engine.h"
26
#include "smt/smt_statistics_registry.h"
27
#include "theory/rewriter.h"
28
#include "theory/theory_engine.h"
29
#include "util/statistics_registry.h"
30
31
namespace CVC4 {
32
namespace prop {
33
34
9029
TheoryProxy::TheoryProxy(PropEngine* propEngine,
35
                         TheoryEngine* theoryEngine,
36
                         DecisionEngine* decisionEngine,
37
                         context::Context* context,
38
                         context::UserContext* userContext,
39
9029
                         ProofNodeManager* pnm)
40
    : d_propEngine(propEngine),
41
      d_cnfStream(nullptr),
42
      d_decisionEngine(decisionEngine),
43
      d_theoryEngine(theoryEngine),
44
      d_queue(context),
45
      d_tpp(*theoryEngine, userContext, pnm),
46
9029
      d_skdm(new SkolemDefManager(context, userContext))
47
{
48
9029
}
49
50
18052
TheoryProxy::~TheoryProxy() {
51
  /* nothing to do for now */
52
18052
}
53
54
9029
void TheoryProxy::finishInit(CnfStream* cnfStream) { d_cnfStream = cnfStream; }
55
56
10350
void TheoryProxy::notifyPreprocessedAssertions(
57
    const std::vector<Node>& assertions)
58
{
59
10350
  d_theoryEngine->notifyPreprocessedAssertions(assertions);
60
120914
  for (const Node& assertion : assertions)
61
  {
62
110564
    d_decisionEngine->addAssertion(assertion);
63
  }
64
10350
}
65
66
362748
void TheoryProxy::notifyAssertion(Node lem, TNode skolem)
67
{
68
362748
  if (skolem.isNull())
69
  {
70
333165
    d_decisionEngine->addAssertion(lem);
71
  }
72
  else
73
  {
74
29583
    d_skdm->notifySkolemDefinition(skolem, lem);
75
29583
    d_decisionEngine->addSkolemDefinition(lem, skolem);
76
  }
77
362748
}
78
79
301856
void TheoryProxy::variableNotify(SatVariable var) {
80
301856
  d_theoryEngine->preRegister(getNode(SatLiteral(var)));
81
301856
}
82
83
15708805
void TheoryProxy::theoryCheck(theory::Theory::Effort effort) {
84
27787389
  while (!d_queue.empty()) {
85
24157168
    TNode assertion = d_queue.front();
86
12078584
    d_queue.pop();
87
12078584
    d_theoryEngine->assertFact(assertion);
88
  }
89
3630221
  d_theoryEngine->check(effort);
90
3630204
}
91
92
3630204
void TheoryProxy::theoryPropagate(std::vector<SatLiteral>& output) {
93
  // Get the propagated literals
94
7260408
  std::vector<TNode> outputNodes;
95
3630204
  d_theoryEngine->getPropagatedLiterals(outputNodes);
96
11805775
  for (unsigned i = 0, i_end = outputNodes.size(); i < i_end; ++ i) {
97
8175571
    Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i] << std::endl;
98
8175571
    output.push_back(d_cnfStream->getLiteral(outputNodes[i]));
99
  }
100
3630204
}
101
102
135138
void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
103
270276
  TNode lNode = d_cnfStream->getNode(l);
104
135138
  Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
105
106
270276
  theory::TrustNode tte = d_theoryEngine->getExplanation(lNode);
107
270276
  Node theoryExplanation = tte.getNode();
108
135138
  if (CVC4::options::produceProofs())
109
  {
110
19676
    d_propEngine->getProofCnfStream()->convertPropagation(tte);
111
  }
112
115462
  else if (options::unsatCores())
113
  {
114
39850
    ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
115
  }
116
270276
  Debug("prop-explain") << "explainPropagation() => " << theoryExplanation
117
135138
                        << std::endl;
118
135138
  explanation.push_back(l);
119
135138
  if (theoryExplanation.getKind() == kind::AND)
120
  {
121
1076952
    for (const Node& n : theoryExplanation)
122
    {
123
948646
      explanation.push_back(~d_cnfStream->getLiteral(n));
124
    }
125
  }
126
  else
127
  {
128
6832
    explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
129
  }
130
135138
  if (Trace.isOn("sat-proof"))
131
  {
132
    std::stringstream ss;
133
    ss << "TheoryProxy::explainPropagation: clause for lit is ";
134
    for (unsigned i = 0, size = explanation.size(); i < size; ++i)
135
    {
136
      ss << explanation[i] << " [" << d_cnfStream->getNode(explanation[i])
137
         << "] ";
138
    }
139
    Trace("sat-proof") << ss.str() << "\n";
140
  }
141
135138
}
142
143
15885240
void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {
144
31770480
  Node literalNode = d_cnfStream->getNode(l);
145
15885240
  Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl;
146
15885240
  Assert(!literalNode.isNull());
147
15885240
  d_queue.push(literalNode);
148
15885240
}
149
150
2565385
SatLiteral TheoryProxy::getNextTheoryDecisionRequest() {
151
5130766
  TNode n = d_theoryEngine->getNextDecisionRequest();
152
5130762
  return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n);
153
}
154
155
2510962
SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) {
156
2510962
  Assert(d_decisionEngine != NULL);
157
2510962
  Assert(stopSearch != true);
158
2510962
  SatLiteral ret = d_decisionEngine->getNext(stopSearch);
159
2510962
  if(stopSearch) {
160
39181
    Trace("decision") << "  ***  Decision Engine stopped search *** " << std::endl;
161
  }
162
2510962
  return options::decisionStopOnly() ? undefSatLiteral : ret;
163
}
164
165
23858
bool TheoryProxy::theoryNeedCheck() const {
166
23858
  return d_theoryEngine->needCheck();
167
}
168
169
301856
TNode TheoryProxy::getNode(SatLiteral lit) {
170
301856
  return d_cnfStream->getNode(lit);
171
}
172
173
2312
void TheoryProxy::notifyRestart() {
174
2312
  d_propEngine->spendResource(ResourceManager::Resource::RestartStep);
175
2312
  d_theoryEngine->notifyRestart();
176
2312
}
177
178
2839859
void TheoryProxy::spendResource(ResourceManager::Resource r)
179
{
180
2839859
  d_theoryEngine->spendResource(r);
181
2839859
}
182
183
5844453
bool TheoryProxy::isDecisionRelevant(SatVariable var) { return true; }
184
185
64835
bool TheoryProxy::isDecisionEngineDone() {
186
64835
  return d_decisionEngine->isDone();
187
}
188
189
1858660
SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
190
1858660
  return SAT_VALUE_UNKNOWN;
191
}
192
193
966
CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; }
194
195
461320
theory::TrustNode TheoryProxy::preprocessLemma(
196
    theory::TrustNode trn,
197
    std::vector<theory::TrustNode>& newLemmas,
198
    std::vector<Node>& newSkolems)
199
{
200
461320
  return d_tpp.preprocessLemma(trn, newLemmas, newSkolems);
201
}
202
203
278121
theory::TrustNode TheoryProxy::preprocess(
204
    TNode node,
205
    std::vector<theory::TrustNode>& newLemmas,
206
    std::vector<Node>& newSkolems)
207
{
208
278121
  return d_tpp.preprocess(node, newLemmas, newSkolems);
209
}
210
211
2
theory::TrustNode TheoryProxy::removeItes(
212
    TNode node,
213
    std::vector<theory::TrustNode>& newLemmas,
214
    std::vector<Node>& newSkolems)
215
{
216
2
  RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
217
2
  return rtf.run(node, newLemmas, newSkolems, true);
218
}
219
220
2694
void TheoryProxy::getSkolems(TNode node,
221
                             std::vector<Node>& skAsserts,
222
                             std::vector<Node>& sks)
223
{
224
5388
  std::unordered_set<Node, NodeHashFunction> skolems;
225
2694
  d_skdm->getSkolems(node, skolems);
226
4733
  for (const Node& k : skolems)
227
  {
228
2039
    sks.push_back(k);
229
2039
    skAsserts.push_back(d_skdm->getDefinitionForSkolem(k));
230
  }
231
2694
}
232
233
537600
void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
234
235
}/* CVC4::prop namespace */
236
26685
}/* CVC4 namespace */