1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Mudathir Mohamed, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of bags state object. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/bags/solver_state.h" |
17 |
|
|
18 |
|
#include "expr/attribute.h" |
19 |
|
#include "expr/bound_var_manager.h" |
20 |
|
#include "expr/skolem_manager.h" |
21 |
|
#include "theory/uf/equality_engine.h" |
22 |
|
|
23 |
|
using namespace std; |
24 |
|
using namespace cvc5::kind; |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
namespace theory { |
28 |
|
namespace bags { |
29 |
|
|
30 |
9853 |
SolverState::SolverState(context::Context* c, |
31 |
|
context::UserContext* u, |
32 |
9853 |
Valuation val) |
33 |
9853 |
: TheoryState(c, u, val) |
34 |
|
{ |
35 |
9853 |
d_true = NodeManager::currentNM()->mkConst(true); |
36 |
9853 |
d_false = NodeManager::currentNM()->mkConst(false); |
37 |
9853 |
d_nm = NodeManager::currentNM(); |
38 |
9853 |
} |
39 |
|
|
40 |
1072 |
void SolverState::registerBag(TNode n) |
41 |
|
{ |
42 |
1072 |
Assert(n.getType().isBag()); |
43 |
1072 |
d_bags.insert(n); |
44 |
1072 |
} |
45 |
|
|
46 |
3139 |
void SolverState::registerCountTerm(TNode n) |
47 |
|
{ |
48 |
3139 |
Assert(n.getKind() == BAG_COUNT); |
49 |
6278 |
Node element = getRepresentative(n[0]); |
50 |
6278 |
Node bag = getRepresentative(n[1]); |
51 |
3139 |
d_bagElements[bag].insert(element); |
52 |
3139 |
} |
53 |
|
|
54 |
30110 |
const std::set<Node>& SolverState::getBags() { return d_bags; } |
55 |
|
|
56 |
3019 |
const std::set<Node>& SolverState::getElements(Node B) |
57 |
|
{ |
58 |
6038 |
Node bag = getRepresentative(B); |
59 |
6038 |
return d_bagElements[bag]; |
60 |
|
} |
61 |
|
|
62 |
15055 |
const std::set<Node>& SolverState::getDisequalBagTerms() { return d_deq; } |
63 |
|
|
64 |
15055 |
void SolverState::reset() |
65 |
|
{ |
66 |
15055 |
d_bagElements.clear(); |
67 |
15055 |
d_bags.clear(); |
68 |
15055 |
d_deq.clear(); |
69 |
15055 |
} |
70 |
|
|
71 |
15055 |
void SolverState::initialize() |
72 |
|
{ |
73 |
15055 |
reset(); |
74 |
15055 |
collectBagsAndCountTerms(); |
75 |
15055 |
collectDisequalBagTerms(); |
76 |
15055 |
} |
77 |
|
|
78 |
15055 |
void SolverState::collectBagsAndCountTerms() |
79 |
|
{ |
80 |
15055 |
eq::EqClassesIterator repIt = eq::EqClassesIterator(d_ee); |
81 |
85953 |
while (!repIt.isFinished()) |
82 |
|
{ |
83 |
70898 |
Node eqc = (*repIt); |
84 |
35449 |
Trace("bags-eqc") << "Eqc [ " << eqc << " ] = { "; |
85 |
|
|
86 |
35449 |
if (eqc.getType().isBag()) |
87 |
|
{ |
88 |
1072 |
registerBag(eqc); |
89 |
|
} |
90 |
|
|
91 |
35449 |
eq::EqClassIterator it = eq::EqClassIterator(eqc, d_ee); |
92 |
137043 |
while (!it.isFinished()) |
93 |
|
{ |
94 |
101594 |
Node n = (*it); |
95 |
50797 |
Trace("bags-eqc") << (*it) << " "; |
96 |
50797 |
Kind k = n.getKind(); |
97 |
50797 |
if (k == MK_BAG) |
98 |
|
{ |
99 |
|
// for terms (bag x c) we need to store x by registering the count term |
100 |
|
// (bag.count x (bag x c)) |
101 |
512 |
Node count = d_nm->mkNode(BAG_COUNT, n[0], n); |
102 |
256 |
registerCountTerm(count); |
103 |
512 |
Trace("SolverState::collectBagsAndCountTerms") |
104 |
256 |
<< "registered " << count << endl; |
105 |
|
} |
106 |
50797 |
if (k == BAG_COUNT) |
107 |
|
{ |
108 |
|
// this takes care of all count terms in each equivalent class |
109 |
2883 |
registerCountTerm(n); |
110 |
5766 |
Trace("SolverState::collectBagsAndCountTerms") |
111 |
2883 |
<< "registered " << n << endl; |
112 |
|
} |
113 |
50797 |
++it; |
114 |
|
} |
115 |
35449 |
Trace("bags-eqc") << " } " << std::endl; |
116 |
35449 |
++repIt; |
117 |
|
} |
118 |
|
|
119 |
15055 |
Trace("bags-eqc") << "bag representatives: " << d_bags << endl; |
120 |
15055 |
Trace("bags-eqc") << "bag elements: " << d_bagElements << endl; |
121 |
15055 |
} |
122 |
|
|
123 |
15055 |
void SolverState::collectDisequalBagTerms() |
124 |
|
{ |
125 |
15055 |
eq::EqClassIterator it = eq::EqClassIterator(d_false, d_ee); |
126 |
48385 |
while (!it.isFinished()) |
127 |
|
{ |
128 |
33330 |
Node n = (*it); |
129 |
16665 |
if (n.getKind() == EQUAL && n[0].getType().isBag()) |
130 |
|
{ |
131 |
344 |
Trace("bags-eqc") << "Disequal terms: " << n << std::endl; |
132 |
344 |
d_deq.insert(n); |
133 |
|
} |
134 |
16665 |
++it; |
135 |
|
} |
136 |
15055 |
} |
137 |
|
|
138 |
|
} // namespace bags |
139 |
|
} // namespace theory |
140 |
29322 |
} // namespace cvc5 |