GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/lazy_tree_proof_generator.cpp Lines: 1 64 1.6 %
Date: 2021-03-22 Branches: 2 142 1.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file lazy_tree_proof_generator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 Implementation of the lazy tree proof generator class
13
 **/
14
15
#include "theory/lazy_tree_proof_generator.h"
16
17
#include <iostream>
18
19
#include "expr/node.h"
20
#include "expr/proof_generator.h"
21
#include "expr/proof_node.h"
22
#include "expr/proof_node_manager.h"
23
24
namespace CVC4 {
25
namespace theory {
26
27
LazyTreeProofGenerator::LazyTreeProofGenerator(ProofNodeManager* pnm,
28
                                               const std::string& name)
29
    : d_pnm(pnm), d_name(name)
30
{
31
  d_stack.emplace_back(&d_proof);
32
}
33
void LazyTreeProofGenerator::openChild()
34
{
35
  detail::TreeProofNode& pn = getCurrent();
36
  pn.d_children.emplace_back();
37
  d_stack.emplace_back(&pn.d_children.back());
38
}
39
void LazyTreeProofGenerator::closeChild()
40
{
41
  Assert(getCurrent().d_rule != PfRule::UNKNOWN);
42
  d_stack.pop_back();
43
}
44
detail::TreeProofNode& LazyTreeProofGenerator::getCurrent()
45
{
46
  Assert(!d_stack.empty()) << "Proof construction has already been finished.";
47
  return *d_stack.back();
48
}
49
void LazyTreeProofGenerator::setCurrent(PfRule rule,
50
                                        const std::vector<Node>& premise,
51
                                        std::vector<Node> args,
52
                                        Node proven)
53
{
54
  detail::TreeProofNode& pn = getCurrent();
55
  pn.d_rule = rule;
56
  pn.d_premise = premise;
57
  pn.d_args = args;
58
  pn.d_proven = proven;
59
}
60
std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProof() const
61
{
62
  // Check cache
63
  if (d_cached) return d_cached;
64
  Assert(d_stack.empty()) << "Proof construction has not yet been finished.";
65
  std::vector<std::shared_ptr<ProofNode>> scope;
66
  d_cached = getProof(scope, d_proof);
67
  return d_cached;
68
}
69
70
std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProofFor(Node f)
71
{
72
  Assert(hasProofFor(f));
73
  return getProof();
74
}
75
76
bool LazyTreeProofGenerator::hasProofFor(Node f)
77
{
78
  return f == getProof()->getResult();
79
}
80
81
std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProof(
82
    std::vector<std::shared_ptr<ProofNode>>& scope,
83
    const detail::TreeProofNode& pn) const
84
{
85
  // Store scope size to reset scope afterwards
86
  std::size_t before = scope.size();
87
  std::vector<std::shared_ptr<ProofNode>> children;
88
  if (pn.d_rule == PfRule::SCOPE)
89
  {
90
    // Extend scope for all but the root node
91
    if (&pn != &d_proof)
92
    {
93
      for (const auto& a : pn.d_args)
94
      {
95
        scope.emplace_back(d_pnm->mkAssume(a));
96
      }
97
    }
98
  }
99
  else
100
  {
101
    // Initialize the children with the scope
102
    children = scope;
103
  }
104
  for (auto& c : pn.d_children)
105
  {
106
    // Recurse into tree
107
    children.emplace_back(getProof(scope, c));
108
  }
109
  for (const auto& p : pn.d_premise)
110
  {
111
    // Add premises as assumptions
112
    children.emplace_back(d_pnm->mkAssume(p));
113
  }
114
  // Reset scope
115
  scope.resize(before);
116
  return d_pnm->mkNode(pn.d_rule, children, pn.d_args);
117
}
118
119
void LazyTreeProofGenerator::print(std::ostream& os,
120
                                   const std::string& prefix,
121
                                   const detail::TreeProofNode& pn) const
122
{
123
  os << prefix << pn.d_rule << ": ";
124
  container_to_stream(os, pn.d_premise);
125
  os << " ==> " << pn.d_proven << std::endl;
126
  if (!pn.d_args.empty())
127
  {
128
    os << prefix << ":args ";
129
    container_to_stream(os, pn.d_args);
130
    std::cout << std::endl;
131
  }
132
  for (const auto& c : pn.d_children)
133
  {
134
    print(os, prefix + '\t', c);
135
  }
136
}
137
138
std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg)
139
{
140
  ltpg.print(os, "", ltpg.d_proof);
141
  return os;
142
}
143
144
}  // namespace theory
145
26676
}  // namespace CVC4