GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bags/solver_state.cpp Lines: 69 69 100.0 %
Date: 2021-03-22 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
8995
SolverState::SolverState(context::Context* c,
30
                         context::UserContext* u,
31
8995
                         Valuation val)
32
8995
    : TheoryState(c, u, val)
33
{
34
8995
  d_true = NodeManager::currentNM()->mkConst(true);
35
8995
  d_false = NodeManager::currentNM()->mkConst(false);
36
8995
  d_nm = NodeManager::currentNM();
37
8995
}
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
22494
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
11247
const std::set<Node>& SolverState::getDisequalBagTerms() { return d_deq; }
62
63
11247
void SolverState::reset()
64
{
65
11247
  d_bagElements.clear();
66
11247
  d_bags.clear();
67
11247
  d_deq.clear();
68
11247
}
69
70
11247
void SolverState::initialize()
71
{
72
11247
  reset();
73
11247
  collectBagsAndCountTerms();
74
11247
  collectDisequalBagTerms();
75
11247
}
76
77
11247
void SolverState::collectBagsAndCountTerms()
78
{
79
11247
  eq::EqClassesIterator repIt = eq::EqClassesIterator(d_ee);
80
60109
  while (!repIt.isFinished())
81
  {
82
48862
    Node eqc = (*repIt);
83
24431
    Trace("bags-eqc") << "Eqc [ " << eqc << " ] = { ";
84
85
24431
    if (eqc.getType().isBag())
86
    {
87
815
      registerBag(eqc);
88
    }
89
90
24431
    eq::EqClassIterator it = eq::EqClassIterator(eqc, d_ee);
91
79521
    while (!it.isFinished())
92
    {
93
55090
      Node n = (*it);
94
27545
      Trace("bags-eqc") << (*it) << " ";
95
27545
      Kind k = n.getKind();
96
27545
      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
27545
      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
27545
      ++it;
113
    }
114
24431
    Trace("bags-eqc") << " } " << std::endl;
115
24431
    ++repIt;
116
  }
117
118
11247
  Trace("bags-eqc") << "bag representatives: " << d_bags << endl;
119
11247
  Trace("bags-eqc") << "bag elements: " << d_bagElements << endl;
120
11247
}
121
122
11247
void SolverState::collectDisequalBagTerms()
123
{
124
11247
  eq::EqClassIterator it = eq::EqClassIterator(d_false, d_ee);
125
35235
  while (!it.isFinished())
126
  {
127
23988
    Node n = (*it);
128
11994
    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
11994
    ++it;
134
  }
135
11247
}
136
137
}  // namespace bags
138
}  // namespace theory
139
26676
}  // namespace CVC4