GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/proof/proof_manager.cpp Lines: 80 109 73.4 %
Date: 2021-03-22 Branches: 162 484 33.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Morgan Deters, Andres Noetzli
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
 ** [[ Add lengthier description here ]]
13
14
 ** \todo document this file
15
16
**/
17
18
#include "proof/proof_manager.h"
19
20
#include "base/check.h"
21
#include "context/context.h"
22
#include "expr/node_visitor.h"
23
#include "options/bv_options.h"
24
#include "options/smt_options.h"
25
#include "proof/clause_id.h"
26
#include "proof/cnf_proof.h"
27
#include "proof/sat_proof_implementation.h"
28
#include "smt/smt_engine.h"
29
#include "smt/smt_engine_scope.h"
30
#include "smt/smt_statistics_registry.h"
31
#include "theory/arrays/theory_arrays.h"
32
#include "theory/output_channel.h"
33
#include "theory/term_registration_visitor.h"
34
#include "theory/uf/equality_engine.h"
35
#include "theory/uf/theory_uf.h"
36
#include "theory/valuation.h"
37
#include "util/hash.h"
38
39
namespace CVC4 {
40
41
9619
ProofManager::ProofManager(context::Context* context)
42
    : d_context(context),
43
      d_satProof(nullptr),
44
      d_cnfProof(nullptr),
45
      d_inputCoreFormulas(context),
46
      d_outputCoreFormulas(context),
47
      d_nextId(0),
48
9619
      d_deps(context)
49
{
50
9619
}
51
52
9598
ProofManager::~ProofManager() {}
53
54
10230834
ProofManager* ProofManager::currentPM() {
55
10230834
  return smt::currentProofManager();
56
}
57
58
4045846
CoreSatProof* ProofManager::getSatProof()
59
{
60
4045846
  Assert(currentPM()->d_satProof);
61
4045846
  return currentPM()->d_satProof.get();
62
}
63
64
768489
CnfProof* ProofManager::getCnfProof()
65
{
66
768489
  Assert(currentPM()->d_cnfProof);
67
768489
  return currentPM()->d_cnfProof.get();
68
}
69
70
1826
void ProofManager::initSatProof(Minisat::Solver* solver)
71
{
72
  // Destroy old instance before initializing new one to avoid issues with
73
  // registering stats
74
1826
  d_satProof.reset();
75
1826
  d_satProof.reset(new CoreSatProof(solver, d_context, ""));
76
1826
}
77
78
1826
void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
79
                                context::Context* ctx)
80
{
81
1826
  Assert(d_satProof != nullptr);
82
83
1826
  d_cnfProof.reset(new CnfProof(cnfStream, ctx, ""));
84
85
  // true and false have to be setup in a special way
86
3652
  Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
87
3652
  Node false_node = NodeManager::currentNM()->mkConst<bool>(false).notNode();
88
89
1826
  d_cnfProof->pushCurrentAssertion(true_node);
90
1826
  d_cnfProof->registerConvertedClause(d_satProof->getTrueUnit());
91
1826
  d_cnfProof->popCurrentAssertion();
92
93
1826
  d_cnfProof->pushCurrentAssertion(false_node);
94
1826
  d_cnfProof->registerConvertedClause(d_satProof->getFalseUnit());
95
1826
  d_cnfProof->popCurrentAssertion();
96
1826
}
97
98
78271
void ProofManager::traceDeps(TNode n, CDNodeSet* coreAssertions)
99
{
100
78271
  Debug("cores") << "trace deps " << n << std::endl;
101
234937
  if ((n.isConst() && n == NodeManager::currentNM()->mkConst<bool>(true)) ||
102
162614
      (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst<bool>(false))) {
103
142
    return;
104
  }
105
78129
  if (d_inputCoreFormulas.find(n) != d_inputCoreFormulas.end())
106
  {
107
    // originating formula was in core set
108
27838
    Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl;
109
27838
    coreAssertions->insert(n);
110
  } else {
111
50291
    Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl;
112
50291
    if(d_deps.find(n) == d_deps.end()) {
113
      InternalError()
114
          << "Cannot trace dependence information back to input assertion:\n`"
115
          << n << "'";
116
    }
117
50291
    Assert(d_deps.find(n) != d_deps.end());
118
100582
    std::vector<Node> deps = (*d_deps.find(n)).second;
119
120
100642
    for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) {
121
50351
      Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl;
122
50351
      if( !(*i).isNull() ){
123
50351
        traceDeps(*i, coreAssertions);
124
      }
125
    }
126
  }
127
}
128
129
908
void ProofManager::traceUnsatCore() {
130
908
  Assert(options::unsatCores());
131
908
  d_satProof->refreshProof();
132
1816
  IdToSatClause used_lemmas;
133
1816
  IdToSatClause used_inputs;
134
908
  d_satProof->collectClausesUsed(used_inputs,
135
                                 used_lemmas);
136
137
  // At this point, there should be no assertions without a clause id
138
908
  Assert(d_cnfProof->isAssertionStackEmpty());
139
140
908
  IdToSatClause::const_iterator it = used_inputs.begin();
141
56748
  for(; it != used_inputs.end(); ++it) {
142
55840
    Node node = d_cnfProof->getAssertionForClause(it->first);
143
144
27920
    Debug("cores") << "core input assertion " << node << "\n";
145
    // trace dependences back to actual assertions
146
    // (this adds them to the unsat core)
147
27920
    traceDeps(node, &d_outputCoreFormulas);
148
  }
149
908
}
150
151
bool ProofManager::unsatCoreAvailable() const {
152
  return d_satProof->derivedEmptyClause();
153
}
154
155
908
std::vector<Node> ProofManager::extractUnsatCore()
156
{
157
908
  std::vector<Node> result;
158
908
  output_core_iterator it = begin_unsat_core();
159
908
  output_core_iterator end = end_unsat_core();
160
6214
  while ( it != end ) {
161
2653
    result.push_back(*it);
162
2653
    ++it;
163
  }
164
908
  return result;
165
}
166
167
void ProofManager::constructSatProof()
168
{
169
  if (!d_satProof->proofConstructed())
170
  {
171
    d_satProof->constructProof();
172
  }
173
}
174
175
void ProofManager::getLemmasInUnsatCore(std::vector<Node>& lemmas)
176
{
177
  Assert(options::unsatCores())
178
      << "Cannot compute unsat core when proofs are off";
179
  Assert(unsatCoreAvailable())
180
      << "Cannot get unsat core at this time. Mabye the input is SAT?";
181
  constructSatProof();
182
  IdToSatClause used_lemmas;
183
  IdToSatClause used_inputs;
184
  d_satProof->collectClausesUsed(used_inputs, used_lemmas);
185
  Debug("pf::lemmasUnsatCore") << "Retrieving all lemmas in unsat core\n";
186
  IdToSatClause::const_iterator it;
187
  for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it)
188
  {
189
    Node lemma = d_cnfProof->getAssertionForClause(it->first);
190
    Debug("pf::lemmasUnsatCore") << "Retrieved lemma " << lemma << "\n";
191
    lemmas.push_back(lemma);
192
  }
193
}
194
195
15512
void ProofManager::addCoreAssertion(Node formula)
196
{
197
15512
  Debug("cores") << "assert: " << formula << std::endl;
198
15512
  d_deps[formula];  // empty vector of deps
199
15512
  d_inputCoreFormulas.insert(formula);
200
15512
}
201
202
18793
void ProofManager::addDependence(TNode n, TNode dep) {
203
18793
  if(dep != n) {
204
18793
    Debug("cores") << "dep: " << n << " : " << dep << std::endl;
205
18793
    if( !dep.isNull() && d_deps.find(dep) == d_deps.end()) {
206
2
      Debug("cores") << "WHERE DID " << dep << " come from ??" << std::endl;
207
    }
208
37586
    std::vector<Node> deps = d_deps[n].get();
209
18793
    deps.push_back(dep);
210
18793
    d_deps[n].set(deps);
211
  }
212
18793
}
213
214
void ProofManager::addUnsatCore(Node formula)
215
{
216
  Assert(d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end());
217
  d_outputCoreFormulas.insert(formula);
218
}
219
220
26676
} /* CVC4  namespace */