GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/proof/lazy_tree_proof_generator.cpp Lines: 48 65 73.8 %
Date: 2021-11-07 Branches: 32 140 22.9 %

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