GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bags/solver_state.cpp Lines: 69 69 100.0 %
Date: 2021-03-23 Branches: 123 254 48.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file solver_state.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mudathir Mohamed, Morgan Deters, Dejan Jovanovic
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 bags state object
13
 **/
14
15
#include "theory/bags/solver_state.h"
16
17
#include "expr/attribute.h"
18
#include "expr/bound_var_manager.h"
19
#include "expr/skolem_manager.h"
20
#include "theory/uf/equality_engine.h"
21
22
using namespace std;
23
using namespace CVC4::kind;
24
25
namespace CVC4 {
26
namespace theory {
27
namespace bags {
28
29
8997
SolverState::SolverState(context::Context* c,
30
                         context::UserContext* u,
31
8997
                         Valuation val)
32
8997
    : TheoryState(c, u, val)
33
{
34
8997
  d_true = NodeManager::currentNM()->mkConst(true);
35
8997
  d_false = NodeManager::currentNM()->mkConst(false);
36
8997
  d_nm = NodeManager::currentNM();
37
8997
}
38
39
815
void SolverState::registerBag(TNode n)
40
{
41
815
  Assert(n.getType().isBag());
42
815
  d_bags.insert(n);
43
815
}
44
45
2278
void SolverState::registerCountTerm(TNode n)
46
{
47
2278
  Assert(n.getKind() == BAG_COUNT);
48
4556
  Node element = getRepresentative(n[0]);
49
4556
  Node bag = getRepresentative(n[1]);
50
2278
  d_bagElements[bag].insert(element);
51
2278
}
52
53
22514
const std::set<Node>& SolverState::getBags() { return d_bags; }
54
55
2411
const std::set<Node>& SolverState::getElements(Node B)
56
{
57
4822
  Node bag = getRepresentative(B);
58
4822
  return d_bagElements[bag];
59
}
60
61
11257
const std::set<Node>& SolverState::getDisequalBagTerms() { return d_deq; }
62
63
11257
void SolverState::reset()
64
{
65
11257
  d_bagElements.clear();
66
11257
  d_bags.clear();
67
11257
  d_deq.clear();
68
11257
}
69
70
11257
void SolverState::initialize()
71
{
72
11257
  reset();
73
11257
  collectBagsAndCountTerms();
74
11257
  collectDisequalBagTerms();
75
11257
}
76
77
11257
void SolverState::collectBagsAndCountTerms()
78
{
79
11257
  eq::EqClassesIterator repIt = eq::EqClassesIterator(d_ee);
80
60159
  while (!repIt.isFinished())
81
  {
82
48902
    Node eqc = (*repIt);
83
24451
    Trace("bags-eqc") << "Eqc [ " << eqc << " ] = { ";
84
85
24451
    if (eqc.getType().isBag())
86
    {
87
815
      registerBag(eqc);
88
    }
89
90
24451
    eq::EqClassIterator it = eq::EqClassIterator(eqc, d_ee);
91
79581
    while (!it.isFinished())
92
    {
93
55130
      Node n = (*it);
94
27565
      Trace("bags-eqc") << (*it) << " ";
95
27565
      Kind k = n.getKind();
96
27565
      if (k == MK_BAG)
97
      {
98
        // for terms (bag x c) we need to store x by registering the count term
99
        // (bag.count x (bag x c))
100
440
        Node count = d_nm->mkNode(BAG_COUNT, n[0], n);
101
220
        registerCountTerm(count);
102
440
        Trace("SolverState::collectBagsAndCountTerms")
103
220
            << "registered " << count << endl;
104
      }
105
27565
      if (k == BAG_COUNT)
106
      {
107
        // this takes care of all count terms in each equivalent class
108
2058
        registerCountTerm(n);
109
4116
        Trace("SolverState::collectBagsAndCountTerms")
110
2058
            << "registered " << n << endl;
111
      }
112
27565
      ++it;
113
    }
114
24451
    Trace("bags-eqc") << " } " << std::endl;
115
24451
    ++repIt;
116
  }
117
118
11257
  Trace("bags-eqc") << "bag representatives: " << d_bags << endl;
119
11257
  Trace("bags-eqc") << "bag elements: " << d_bagElements << endl;
120
11257
}
121
122
11257
void SolverState::collectDisequalBagTerms()
123
{
124
11257
  eq::EqClassIterator it = eq::EqClassIterator(d_false, d_ee);
125
35265
  while (!it.isFinished())
126
  {
127
24008
    Node n = (*it);
128
12004
    if (n.getKind() == EQUAL && n[0].getType().isBag())
129
    {
130
283
      Trace("bags-eqc") << "Disequal terms: " << n << std::endl;
131
283
      d_deq.insert(n);
132
    }
133
12004
    ++it;
134
  }
135
11257
}
136
137
}  // namespace bags
138
}  // namespace theory
139
26685
}  // namespace CVC4