GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/tconv_seq_proof_generator.cpp Lines: 55 78 70.5 %
Date: 2021-03-22 Branches: 70 304 23.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file tconv_seq_proof_generator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 Term conversion sequence proof generator utility
13
 **/
14
15
#include "expr/tconv_seq_proof_generator.h"
16
17
#include <sstream>
18
19
#include "expr/proof_node_manager.h"
20
21
namespace CVC4 {
22
23
966
TConvSeqProofGenerator::TConvSeqProofGenerator(
24
    ProofNodeManager* pnm,
25
    const std::vector<ProofGenerator*>& ts,
26
    context::Context* c,
27
966
    std::string name)
28
966
    : d_pnm(pnm), d_converted(c), d_name(name)
29
{
30
966
  d_tconvs.insert(d_tconvs.end(), ts.begin(), ts.end());
31
966
  AlwaysAssert(!d_tconvs.empty())
32
      << "TConvSeqProofGenerator::TConvSeqProofGenerator: expecting non-empty "
33
         "sequence";
34
966
}
35
36
1932
TConvSeqProofGenerator::~TConvSeqProofGenerator() {}
37
38
1806
void TConvSeqProofGenerator::registerConvertedTerm(Node t, Node s, size_t index)
39
{
40
1806
  if (t == s)
41
  {
42
    // no need
43
    return;
44
  }
45
3612
  std::pair<Node, size_t> key = std::pair<Node, size_t>(t, index);
46
1806
  d_converted[key] = s;
47
}
48
49
220
std::shared_ptr<ProofNode> TConvSeqProofGenerator::getProofFor(Node f)
50
{
51
440
  Trace("tconv-seq-pf-gen")
52
440
      << "TConvSeqProofGenerator::getProofFor: " << identify() << ": " << f
53
220
      << std::endl;
54
220
  return getSubsequenceProofFor(f, 0, d_tconvs.size() - 1);
55
}
56
57
220
std::shared_ptr<ProofNode> TConvSeqProofGenerator::getSubsequenceProofFor(
58
    Node f, size_t start, size_t end)
59
{
60
220
  Assert(end < d_tconvs.size());
61
220
  if (f.getKind() != kind::EQUAL)
62
  {
63
    std::stringstream serr;
64
    serr << "TConvSeqProofGenerator::getProofFor: " << identify()
65
         << ": fail, non-equality " << f;
66
    Unhandled() << serr.str();
67
    Trace("tconv-seq-pf-gen") << serr.str() << std::endl;
68
    return nullptr;
69
  }
70
  // start with the left hand side of the equality
71
440
  Node curr = f[0];
72
  // proofs forming transitivity chain
73
440
  std::vector<std::shared_ptr<ProofNode>> transChildren;
74
440
  std::pair<Node, size_t> currKey;
75
220
  NodeIndexNodeMap::iterator itc;
76
  // convert the term in sequence
77
660
  for (size_t i = start; i <= end; i++)
78
  {
79
440
    currKey = std::pair<Node, size_t>(curr, i);
80
440
    itc = d_converted.find(currKey);
81
    // if we provided a conversion at this index via registerConvertedTerm
82
440
    if (itc != d_converted.end())
83
    {
84
880
      Node next = (*itc).second;
85
440
      Trace("tconv-seq-pf-gen") << "...convert to " << next << std::endl;
86
880
      Node eq = curr.eqNode(next);
87
880
      std::shared_ptr<ProofNode> pf = d_tconvs[i]->getProofFor(eq);
88
440
      transChildren.push_back(pf);
89
440
      curr = next;
90
    }
91
  }
92
  // should end up with the right hand side of the equality
93
220
  if (curr != f[1])
94
  {
95
    // unexpected
96
    std::stringstream serr;
97
    serr << "TConvSeqProofGenerator::getProofFor: " << identify()
98
         << ": failed, mismatch (see -t tconv-seq-pf-gen-debug for details)"
99
         << std::endl;
100
    serr << "                    source: " << f[0] << std::endl;
101
    serr << "expected after conversions: " << f[1] << std::endl;
102
    serr << "  actual after conversions: " << curr << std::endl;
103
104
    if (Trace.isOn("tconv-seq-pf-gen-debug"))
105
    {
106
      Trace("tconv-pf-gen-debug")
107
          << "Printing conversion steps..." << std::endl;
108
      serr << "Conversions: " << std::endl;
109
      for (NodeIndexNodeMap::const_iterator it = d_converted.begin();
110
           it != d_converted.end();
111
           ++it)
112
      {
113
        serr << "(" << (*it).first.first << ", " << (*it).first.second
114
             << ") -> " << (*it).second << std::endl;
115
      }
116
    }
117
    Unhandled() << serr.str();
118
    return nullptr;
119
  }
120
  // otherwise, make transitivity
121
220
  return d_pnm->mkTrans(transChildren, f);
122
}
123
124
32282
theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence(
125
    const std::vector<Node>& cterms)
126
{
127
32282
  Assert(cterms.size() == d_tconvs.size() + 1);
128
32282
  if (cterms[0] == cterms[cterms.size() - 1])
129
  {
130
    return theory::TrustNode::null();
131
  }
132
32282
  bool useThis = false;
133
32282
  ProofGenerator* pg = nullptr;
134
95943
  for (size_t i = 0, nconvs = d_tconvs.size(); i < nconvs; i++)
135
  {
136
64564
    if (cterms[i] == cterms[i + 1])
137
    {
138
31379
      continue;
139
    }
140
33185
    else if (pg == nullptr)
141
    {
142
      // Maybe the i^th generator can explain it alone, which must be the case
143
      // if there is only one position in the sequence where the term changes.
144
      // We may overwrite pg with this class if another step is encountered in
145
      // this loop.
146
32282
      pg = d_tconvs[i];
147
    }
148
    else
149
    {
150
      // need more than a single generator, use this class
151
903
      useThis = true;
152
903
      break;
153
    }
154
  }
155
32282
  if (useThis)
156
  {
157
903
    pg = this;
158
    // if more than two steps, we must register each conversion step
159
2709
    for (size_t i = 0, nconvs = d_tconvs.size(); i < nconvs; i++)
160
    {
161
1806
      registerConvertedTerm(cterms[i], cterms[i + 1], i);
162
    }
163
  }
164
32282
  Assert(pg != nullptr);
165
  return theory::TrustNode::mkTrustRewrite(
166
32282
      cterms[0], cterms[cterms.size() - 1], pg);
167
}
168
169
1240
std::string TConvSeqProofGenerator::identify() const { return d_name; }
170
171
26676
}  // namespace CVC4