GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/icp/contraction_origins.cpp Lines: 1 43 2.3 %
Date: 2021-03-22 Branches: 2 136 1.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file contraction_origins.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
13
 **/
14
15
#include "theory/arith/nl/icp/contraction_origins.h"
16
17
namespace CVC4 {
18
namespace theory {
19
namespace arith {
20
namespace nl {
21
namespace icp {
22
23
void ContractionOriginManager::getOrigins(ContractionOrigin const* const origin,
24
                                          std::set<Node>& res) const
25
{
26
  if (!origin->candidate.isNull())
27
  {
28
    res.insert(origin->candidate);
29
  }
30
  for (const auto& co : origin->origins)
31
  {
32
    getOrigins(co, res);
33
  }
34
}
35
36
const std::map<Node, ContractionOriginManager::ContractionOrigin*>&
37
ContractionOriginManager::currentOrigins() const
38
{
39
  return d_currentOrigins;
40
}
41
42
void ContractionOriginManager::add(const Node& targetVariable,
43
                                   const Node& candidate,
44
                                   const std::vector<Node>& originVariables,
45
                                   bool addTarget)
46
{
47
  Trace("nl-icp") << "Adding contraction for " << targetVariable << std::endl;
48
  std::vector<ContractionOrigin*> origins;
49
  if (addTarget)
50
  {
51
    auto it = d_currentOrigins.find(targetVariable);
52
    if (it != d_currentOrigins.end())
53
    {
54
      origins.emplace_back(it->second);
55
    }
56
  }
57
  for (const auto& v : originVariables)
58
  {
59
    auto it = d_currentOrigins.find(v);
60
    if (it != d_currentOrigins.end())
61
    {
62
      origins.emplace_back(it->second);
63
    }
64
  }
65
  d_allocations.emplace_back(
66
      new ContractionOrigin{candidate, std::move(origins)});
67
  d_currentOrigins[targetVariable] = d_allocations.back().get();
68
}
69
70
std::vector<Node> ContractionOriginManager::getOrigins(
71
    const Node& variable) const
72
{
73
  Trace("nl-icp") << "Obtaining origins for " << variable << std::endl;
74
  std::set<Node> origins;
75
  Assert(d_currentOrigins.find(variable) != d_currentOrigins.end())
76
      << "Using variable as origin that is unknown yet.";
77
  getOrigins(d_currentOrigins.at(variable), origins);
78
  Assert(!origins.empty()) << "There should be at least one origin";
79
  return std::vector<Node>(origins.begin(), origins.end());
80
}
81
82
bool ContractionOriginManager::isInOrigins(const Node& variable,
83
                                           const Node& c) const
84
{
85
  std::set<Node> origins;
86
  Assert(d_currentOrigins.find(variable) != d_currentOrigins.end())
87
      << "Using variable as origin that is unknown yet.";
88
  getOrigins(d_currentOrigins.at(variable), origins);
89
  return origins.find(c) != origins.end();
90
}
91
92
void print(std::ostream& os,
93
           const std::string& indent,
94
           const ContractionOriginManager::ContractionOrigin* co)
95
{
96
  os << indent << co->candidate << std::endl;
97
  for (const auto& o : co->origins)
98
  {
99
    print(os, indent + "\t", o);
100
  }
101
}
102
103
inline std::ostream& operator<<(std::ostream& os,
104
                                const ContractionOriginManager& com)
105
{
106
  os << "ContractionOrigins:" << std::endl;
107
  const auto& origins = com.currentOrigins();
108
  for (const auto& vars : origins)
109
  {
110
    os << vars.first << ":" << std::endl;
111
    print(os, "\t", vars.second);
112
  }
113
  return os;
114
}
115
116
}  // namespace icp
117
}  // namespace nl
118
}  // namespace arith
119
}  // namespace theory
120
26676
}  // namespace CVC4