GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/theory_proxy.cpp Lines: 92 98 93.9 %
Date: 2021-03-22 Branches: 126 296 42.6 %

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
9027
TheoryProxy::TheoryProxy(PropEngine* propEngine,
35
                         TheoryEngine* theoryEngine,
36
                         DecisionEngine* decisionEngine,
37
                         context::Context* context,
38
                         context::UserContext* userContext,
39
9027
                         ProofNodeManager* pnm)
40
    : d_propEngine(propEngine),
41
      d_cnfStream(nullptr),
42
      d_decisionEngine(decisionEngine),
43
      d_theoryEngine(theoryEngine),
44
      d_queue(context),
45
9027
      d_tpp(*theoryEngine, userContext, pnm)
46
{
47
9027
}
48
49
18048
TheoryProxy::~TheoryProxy() {
50
  /* nothing to do for now */
51
18048
}
52
53
9027
void TheoryProxy::finishInit(CnfStream* cnfStream) { d_cnfStream = cnfStream; }
54
55
301724
void TheoryProxy::variableNotify(SatVariable var) {
56
301724
  d_theoryEngine->preRegister(getNode(SatLiteral(var)));
57
301724
}
58
59
15708293
void TheoryProxy::theoryCheck(theory::Theory::Effort effort) {
60
27786519
  while (!d_queue.empty()) {
61
24156452
    TNode assertion = d_queue.front();
62
12078226
    d_queue.pop();
63
12078226
    d_theoryEngine->assertFact(assertion);
64
  }
65
3630067
  d_theoryEngine->check(effort);
66
3630050
}
67
68
3630050
void TheoryProxy::theoryPropagate(std::vector<SatLiteral>& output) {
69
  // Get the propagated literals
70
7260100
  std::vector<TNode> outputNodes;
71
3630050
  d_theoryEngine->getPropagatedLiterals(outputNodes);
72
11805430
  for (unsigned i = 0, i_end = outputNodes.size(); i < i_end; ++ i) {
73
8175380
    Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i] << std::endl;
74
8175380
    output.push_back(d_cnfStream->getLiteral(outputNodes[i]));
75
  }
76
3630050
}
77
78
135138
void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
79
270276
  TNode lNode = d_cnfStream->getNode(l);
80
135138
  Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
81
82
270276
  theory::TrustNode tte = d_theoryEngine->getExplanation(lNode);
83
270276
  Node theoryExplanation = tte.getNode();
84
135138
  if (CVC4::options::produceProofs())
85
  {
86
19676
    d_propEngine->getProofCnfStream()->convertPropagation(tte);
87
  }
88
115462
  else if (options::unsatCores())
89
  {
90
39850
    ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
91
  }
92
270276
  Debug("prop-explain") << "explainPropagation() => " << theoryExplanation
93
135138
                        << std::endl;
94
135138
  explanation.push_back(l);
95
135138
  if (theoryExplanation.getKind() == kind::AND)
96
  {
97
1076952
    for (const Node& n : theoryExplanation)
98
    {
99
948646
      explanation.push_back(~d_cnfStream->getLiteral(n));
100
    }
101
  }
102
  else
103
  {
104
6832
    explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
105
  }
106
135138
  if (Trace.isOn("sat-proof"))
107
  {
108
    std::stringstream ss;
109
    ss << "TheoryProxy::explainPropagation: clause for lit is ";
110
    for (unsigned i = 0, size = explanation.size(); i < size; ++i)
111
    {
112
      ss << explanation[i] << " [" << d_cnfStream->getNode(explanation[i])
113
         << "] ";
114
    }
115
    Trace("sat-proof") << ss.str() << "\n";
116
  }
117
135138
}
118
119
15884873
void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {
120
31769746
  Node literalNode = d_cnfStream->getNode(l);
121
15884873
  Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl;
122
15884873
  Assert(!literalNode.isNull());
123
15884873
  d_queue.push(literalNode);
124
15884873
}
125
126
2565306
SatLiteral TheoryProxy::getNextTheoryDecisionRequest() {
127
5130608
  TNode n = d_theoryEngine->getNextDecisionRequest();
128
5130604
  return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n);
129
}
130
131
2510897
SatLiteral TheoryProxy::getNextDecisionEngineRequest(bool &stopSearch) {
132
2510897
  Assert(d_decisionEngine != NULL);
133
2510897
  Assert(stopSearch != true);
134
2510897
  SatLiteral ret = d_decisionEngine->getNext(stopSearch);
135
2510897
  if(stopSearch) {
136
39155
    Trace("decision") << "  ***  Decision Engine stopped search *** " << std::endl;
137
  }
138
2510897
  return options::decisionStopOnly() ? undefSatLiteral : ret;
139
}
140
141
23854
bool TheoryProxy::theoryNeedCheck() const {
142
23854
  return d_theoryEngine->needCheck();
143
}
144
145
301724
TNode TheoryProxy::getNode(SatLiteral lit) {
146
301724
  return d_cnfStream->getNode(lit);
147
}
148
149
2312
void TheoryProxy::notifyRestart() {
150
2312
  d_propEngine->spendResource(ResourceManager::Resource::RestartStep);
151
2312
  d_theoryEngine->notifyRestart();
152
2312
}
153
154
2839709
void TheoryProxy::spendResource(ResourceManager::Resource r)
155
{
156
2839709
  d_theoryEngine->spendResource(r);
157
2839709
}
158
159
5844453
bool TheoryProxy::isDecisionRelevant(SatVariable var) { return true; }
160
161
64809
bool TheoryProxy::isDecisionEngineDone() {
162
64809
  return d_decisionEngine->isDone();
163
}
164
165
1858660
SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
166
1858660
  return SAT_VALUE_UNKNOWN;
167
}
168
169
966
CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; }
170
171
461169
theory::TrustNode TheoryProxy::preprocessLemma(
172
    theory::TrustNode trn,
173
    std::vector<theory::TrustNode>& newLemmas,
174
    std::vector<Node>& newSkolems)
175
{
176
461169
  return d_tpp.preprocessLemma(trn, newLemmas, newSkolems);
177
}
178
179
277854
theory::TrustNode TheoryProxy::preprocess(
180
    TNode node,
181
    std::vector<theory::TrustNode>& newLemmas,
182
    std::vector<Node>& newSkolems)
183
{
184
277854
  return d_tpp.preprocess(node, newLemmas, newSkolems);
185
}
186
187
2
theory::TrustNode TheoryProxy::removeItes(
188
    TNode node,
189
    std::vector<theory::TrustNode>& newLemmas,
190
    std::vector<Node>& newSkolems)
191
{
192
2
  RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
193
2
  return rtf.run(node, newLemmas, newSkolems, true);
194
}
195
196
2471
void TheoryProxy::getSkolems(TNode node,
197
                             std::vector<theory::TrustNode>& skAsserts,
198
                             std::vector<Node>& sks)
199
{
200
2471
  RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
201
4942
  std::unordered_set<Node, NodeHashFunction> skolems;
202
2471
  rtf.getSkolems(node, skolems);
203
4033
  for (const Node& k : skolems)
204
  {
205
1562
    sks.push_back(k);
206
1562
    skAsserts.push_back(rtf.getLemmaForSkolem(k));
207
  }
208
2471
}
209
210
537410
void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
211
212
}/* CVC4::prop namespace */
213
26676
}/* CVC4 namespace */