GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bags/theory_bags_type_enumerator.cpp Lines: 1 32 3.1 %
Date: 2021-03-23 Branches: 2 106 1.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bags_type_enumerator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mudathir Mohamed
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 bag enumerator implementation
13
 **/
14
15
#include "theory/bags/theory_bags_type_enumerator.h"
16
17
#include "expr/emptybag.h"
18
#include "theory/rewriter.h"
19
#include "theory_bags_type_enumerator.h"
20
21
namespace CVC4 {
22
namespace theory {
23
namespace bags {
24
25
BagEnumerator::BagEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
26
    : TypeEnumeratorBase<BagEnumerator>(type),
27
      d_nodeManager(NodeManager::currentNM()),
28
      d_elementTypeEnumerator(type.getBagElementType(), tep)
29
{
30
  d_currentBag = d_nodeManager->mkConst(EmptyBag(type));
31
  d_element = *d_elementTypeEnumerator;
32
}
33
34
BagEnumerator::BagEnumerator(const BagEnumerator& enumerator)
35
    : TypeEnumeratorBase<BagEnumerator>(enumerator.getType()),
36
      d_nodeManager(enumerator.d_nodeManager),
37
      d_elementTypeEnumerator(enumerator.d_elementTypeEnumerator),
38
      d_currentBag(enumerator.d_currentBag),
39
      d_element(enumerator.d_element)
40
{
41
}
42
43
BagEnumerator::~BagEnumerator() {}
44
45
Node BagEnumerator::operator*()
46
{
47
  Trace("bag-type-enum") << "BagEnumerator::operator* d_currentBag = "
48
                         << d_currentBag << std::endl;
49
50
  return d_currentBag;
51
}
52
53
BagEnumerator& BagEnumerator::operator++()
54
{
55
  // increase the multiplicity by one
56
  Node one = d_nodeManager->mkConst(Rational(1));
57
  TypeNode elementType = d_elementTypeEnumerator.getType();
58
  Node singleton = d_nodeManager->mkBag(elementType, d_element, one);
59
  if (d_currentBag.getKind() == kind::EMPTYBAG)
60
  {
61
    d_currentBag = singleton;
62
  }
63
  else
64
  {
65
    d_currentBag =
66
        d_nodeManager->mkNode(kind::UNION_DISJOINT, singleton, d_currentBag);
67
  }
68
69
  d_currentBag = Rewriter::rewrite(d_currentBag);
70
71
  Assert(d_currentBag.isConst());
72
73
  Trace("bag-type-enum") << "BagEnumerator::operator++ d_currentBag = "
74
                         << d_currentBag << std::endl;
75
  return *this;
76
}
77
78
bool BagEnumerator::isFinished()
79
{
80
  // bags sequence is infinite and it never ends
81
  return false;
82
}
83
84
}  // namespace bags
85
}  // namespace theory
86
26685
}  // namespace CVC4