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 |
9940 |
SolverState::SolverState(Env& env, Valuation val) : TheoryState(env, val) |
31 |
|
{ |
32 |
9940 |
d_true = NodeManager::currentNM()->mkConst(true); |
33 |
9940 |
d_false = NodeManager::currentNM()->mkConst(false); |
34 |
9940 |
d_nm = NodeManager::currentNM(); |
35 |
9940 |
} |
36 |
|
|
37 |
1072 |
void SolverState::registerBag(TNode n) |
38 |
|
{ |
39 |
1072 |
Assert(n.getType().isBag()); |
40 |
1072 |
d_bags.insert(n); |
41 |
1072 |
} |
42 |
|
|
43 |
3139 |
void SolverState::registerCountTerm(TNode n) |
44 |
|
{ |
45 |
3139 |
Assert(n.getKind() == BAG_COUNT); |
46 |
6278 |
Node element = getRepresentative(n[0]); |
47 |
6278 |
Node bag = getRepresentative(n[1]); |
48 |
3139 |
d_bagElements[bag].insert(element); |
49 |
3139 |
} |
50 |
|
|
51 |
30962 |
const std::set<Node>& SolverState::getBags() { return d_bags; } |
52 |
|
|
53 |
3019 |
const std::set<Node>& SolverState::getElements(Node B) |
54 |
|
{ |
55 |
6038 |
Node bag = getRepresentative(B); |
56 |
6038 |
return d_bagElements[bag]; |
57 |
|
} |
58 |
|
|
59 |
15481 |
const std::set<Node>& SolverState::getDisequalBagTerms() { return d_deq; } |
60 |
|
|
61 |
15481 |
void SolverState::reset() |
62 |
|
{ |
63 |
15481 |
d_bagElements.clear(); |
64 |
15481 |
d_bags.clear(); |
65 |
15481 |
d_deq.clear(); |
66 |
15481 |
} |
67 |
|
|
68 |
15481 |
void SolverState::initialize() |
69 |
|
{ |
70 |
15481 |
reset(); |
71 |
15481 |
collectBagsAndCountTerms(); |
72 |
15481 |
collectDisequalBagTerms(); |
73 |
15481 |
} |
74 |
|
|
75 |
15481 |
void SolverState::collectBagsAndCountTerms() |
76 |
|
{ |
77 |
15481 |
eq::EqClassesIterator repIt = eq::EqClassesIterator(d_ee); |
78 |
85951 |
while (!repIt.isFinished()) |
79 |
|
{ |
80 |
70470 |
Node eqc = (*repIt); |
81 |
35235 |
Trace("bags-eqc") << "Eqc [ " << eqc << " ] = { "; |
82 |
|
|
83 |
35235 |
if (eqc.getType().isBag()) |
84 |
|
{ |
85 |
1072 |
registerBag(eqc); |
86 |
|
} |
87 |
|
|
88 |
35235 |
eq::EqClassIterator it = eq::EqClassIterator(eqc, d_ee); |
89 |
122929 |
while (!it.isFinished()) |
90 |
|
{ |
91 |
87694 |
Node n = (*it); |
92 |
43847 |
Trace("bags-eqc") << (*it) << " "; |
93 |
43847 |
Kind k = n.getKind(); |
94 |
43847 |
if (k == MK_BAG) |
95 |
|
{ |
96 |
|
// for terms (bag x c) we need to store x by registering the count term |
97 |
|
// (bag.count x (bag x c)) |
98 |
512 |
Node count = d_nm->mkNode(BAG_COUNT, n[0], n); |
99 |
256 |
registerCountTerm(count); |
100 |
512 |
Trace("SolverState::collectBagsAndCountTerms") |
101 |
256 |
<< "registered " << count << endl; |
102 |
|
} |
103 |
43847 |
if (k == BAG_COUNT) |
104 |
|
{ |
105 |
|
// this takes care of all count terms in each equivalent class |
106 |
2883 |
registerCountTerm(n); |
107 |
5766 |
Trace("SolverState::collectBagsAndCountTerms") |
108 |
2883 |
<< "registered " << n << endl; |
109 |
|
} |
110 |
43847 |
++it; |
111 |
|
} |
112 |
35235 |
Trace("bags-eqc") << " } " << std::endl; |
113 |
35235 |
++repIt; |
114 |
|
} |
115 |
|
|
116 |
15481 |
Trace("bags-eqc") << "bag representatives: " << d_bags << endl; |
117 |
15481 |
Trace("bags-eqc") << "bag elements: " << d_bagElements << endl; |
118 |
15481 |
} |
119 |
|
|
120 |
15481 |
void SolverState::collectDisequalBagTerms() |
121 |
|
{ |
122 |
15481 |
eq::EqClassIterator it = eq::EqClassIterator(d_false, d_ee); |
123 |
48903 |
while (!it.isFinished()) |
124 |
|
{ |
125 |
33422 |
Node n = (*it); |
126 |
16711 |
if (n.getKind() == EQUAL && n[0].getType().isBag()) |
127 |
|
{ |
128 |
344 |
Trace("bags-eqc") << "Disequal terms: " << n << std::endl; |
129 |
344 |
d_deq.insert(n); |
130 |
|
} |
131 |
16711 |
++it; |
132 |
|
} |
133 |
15481 |
} |
134 |
|
|
135 |
|
} // namespace bags |
136 |
|
} // namespace theory |
137 |
29574 |
} // namespace cvc5 |