GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/proof_manager.cpp Lines: 63 90 70.0 %
Date: 2021-03-23 Branches: 94 326 28.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, 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 The proof manager of the SMT engine
13
 **/
14
15
#include "smt/proof_manager.h"
16
17
#include "expr/proof_checker.h"
18
#include "expr/proof_node_algorithm.h"
19
#include "expr/proof_node_manager.h"
20
#include "options/base_options.h"
21
#include "options/proof_options.h"
22
#include "proof/dot/dot_printer.h"
23
#include "smt/assertions.h"
24
#include "smt/defined_function.h"
25
#include "smt/preprocess_proof_generator.h"
26
#include "smt/proof_post_processor.h"
27
28
namespace CVC4 {
29
namespace smt {
30
31
962
PfManager::PfManager(context::UserContext* u, SmtEngine* smte)
32
1924
    : d_pchecker(new ProofChecker(options::proofPedantic())),
33
962
      d_pnm(new ProofNodeManager(d_pchecker.get())),
34
      d_pppg(new PreprocessProofGenerator(
35
1924
          d_pnm.get(), u, "smt::PreprocessProofGenerator")),
36
962
      d_pfpp(new ProofPostproccess(d_pnm.get(), smte, d_pppg.get())),
37
5772
      d_finalProof(nullptr)
38
{
39
  // add rules to eliminate here
40
3848
  if (options::proofGranularityMode() != options::ProofGranularityMode::OFF)
41
  {
42
962
    d_pfpp->setEliminateRule(PfRule::MACRO_SR_EQ_INTRO);
43
962
    d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_INTRO);
44
962
    d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_ELIM);
45
962
    d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_TRANSFORM);
46
962
    d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION);
47
1924
    if (options::proofGranularityMode()
48
962
        != options::ProofGranularityMode::REWRITE)
49
    {
50
962
      d_pfpp->setEliminateRule(PfRule::SUBS);
51
962
      d_pfpp->setEliminateRule(PfRule::REWRITE);
52
1924
      if (options::proofGranularityMode()
53
962
          != options::ProofGranularityMode::THEORY_REWRITE)
54
      {
55
        // this eliminates theory rewriting steps with finer-grained DSL rules
56
        d_pfpp->setEliminateRule(PfRule::THEORY_REWRITE);
57
      }
58
    }
59
  }
60
962
  d_false = NodeManager::currentNM()->mkConst(false);
61
962
}
62
63
962
PfManager::~PfManager() {}
64
65
1146
void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn,
66
                              Assertions& as,
67
                              DefinedFunctionMap& df)
68
{
69
  // Note this assumes that setFinalProof is only called once per unsat
70
  // response. This method would need to cache its result otherwise.
71
1146
  Trace("smt-proof") << "SmtEngine::setFinalProof(): get proof body...\n";
72
73
1146
  if (Trace.isOn("smt-proof-debug"))
74
  {
75
    Trace("smt-proof-debug")
76
        << "SmtEngine::setFinalProof(): Proof node for false:\n";
77
    Trace("smt-proof-debug") << *pfn.get() << std::endl;
78
    Trace("smt-proof-debug") << "=====" << std::endl;
79
  }
80
81
2292
  std::vector<Node> assertions;
82
1146
  getAssertions(as, df, assertions);
83
84
1146
  if (Trace.isOn("smt-proof"))
85
  {
86
    Trace("smt-proof") << "SmtEngine::setFinalProof(): get free assumptions..."
87
                       << std::endl;
88
    std::vector<Node> fassumps;
89
    expr::getFreeAssumptions(pfn.get(), fassumps);
90
    Trace("smt-proof")
91
        << "SmtEngine::setFinalProof(): initial free assumptions are:\n";
92
    for (const Node& a : fassumps)
93
    {
94
      Trace("smt-proof") << "- " << a << std::endl;
95
    }
96
97
    Trace("smt-proof") << "SmtEngine::setFinalProof(): assertions are:\n";
98
    for (const Node& n : assertions)
99
    {
100
      Trace("smt-proof") << "- " << n << std::endl;
101
    }
102
    Trace("smt-proof") << "=====" << std::endl;
103
  }
104
105
1146
  Trace("smt-proof") << "SmtEngine::setFinalProof(): postprocess...\n";
106
1146
  Assert(d_pfpp != nullptr);
107
1146
  d_pfpp->process(pfn);
108
109
1146
  Trace("smt-proof") << "SmtEngine::setFinalProof(): make scope...\n";
110
111
  // Now make the final scope, which ensures that the only open leaves
112
  // of the proof are the assertions.
113
1146
  d_finalProof = d_pnm->mkScope(pfn, assertions);
114
1146
  Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n";
115
1146
}
116
117
void PfManager::printProof(std::ostream& out,
118
                           std::shared_ptr<ProofNode> pfn,
119
                           Assertions& as,
120
                           DefinedFunctionMap& df)
121
{
122
  Trace("smt-proof") << "PfManager::printProof: start" << std::endl;
123
  std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as, df);
124
  // TODO (proj #37) according to the proof format, post process the proof node
125
  // TODO (proj #37) according to the proof format, print the proof node
126
127
  if (options::proofFormatMode() == options::ProofFormatMode::DOT)
128
  {
129
    proof::DotPrinter::print(out, fp.get());
130
  }
131
  else
132
  {
133
    out << "(proof\n";
134
    out << *fp;
135
    out << "\n)\n";
136
  }
137
}
138
1142
void PfManager::checkProof(std::shared_ptr<ProofNode> pfn,
139
                           Assertions& as,
140
                           DefinedFunctionMap& df)
141
{
142
1142
  Trace("smt-proof") << "PfManager::checkProof: start" << std::endl;
143
2284
  std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as, df);
144
2284
  Trace("smt-proof-debug") << "PfManager::checkProof: returned " << *fp.get()
145
1142
                           << std::endl;
146
1142
}
147
148
ProofChecker* PfManager::getProofChecker() const { return d_pchecker.get(); }
149
150
962
ProofNodeManager* PfManager::getProofNodeManager() const { return d_pnm.get(); }
151
152
962
smt::PreprocessProofGenerator* PfManager::getPreprocessProofGenerator() const
153
{
154
962
  return d_pppg.get();
155
}
156
157
1146
std::shared_ptr<ProofNode> PfManager::getFinalProof(
158
    std::shared_ptr<ProofNode> pfn, Assertions& as, DefinedFunctionMap& df)
159
{
160
1146
  setFinalProof(pfn, as, df);
161
1146
  Assert(d_finalProof);
162
1146
  return d_finalProof;
163
}
164
165
1146
void PfManager::getAssertions(Assertions& as,
166
                              DefinedFunctionMap& df,
167
                              std::vector<Node>& assertions)
168
{
169
1146
  context::CDList<Node>* al = as.getAssertionList();
170
1146
  Assert(al != nullptr);
171
14717
  for (context::CDList<Node>::const_iterator i = al->begin(); i != al->end();
172
       ++i)
173
  {
174
13571
    assertions.push_back(*i);
175
  }
176
1146
  NodeManager* nm = NodeManager::currentNM();
177
1606
  for (const std::pair<const Node, const smt::DefinedFunction>& dfn : df)
178
  {
179
920
    Node def = dfn.second.getFormula();
180
460
    const std::vector<Node>& formals = dfn.second.getFormals();
181
460
    if (!formals.empty())
182
    {
183
500
      Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, formals);
184
250
      def = nm->mkNode(kind::LAMBDA, bvl, def);
185
    }
186
    // assume the (possibly higher order) equality
187
920
    Node eq = dfn.first.eqNode(def);
188
460
    assertions.push_back(eq);
189
  }
190
1146
}
191
192
}  // namespace smt
193
30533
}  // namespace CVC4