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 |
9459 |
SolverState::SolverState(context::Context* c, |
31 |
|
context::UserContext* u, |
32 |
9459 |
Valuation val) |
33 |
9459 |
: TheoryState(c, u, val) |
34 |
|
{ |
35 |
9459 |
d_true = NodeManager::currentNM()->mkConst(true); |
36 |
9459 |
d_false = NodeManager::currentNM()->mkConst(false); |
37 |
9459 |
d_nm = NodeManager::currentNM(); |
38 |
9459 |
} |
39 |
|
|
40 |
990 |
void SolverState::registerBag(TNode n) |
41 |
|
{ |
42 |
990 |
Assert(n.getType().isBag()); |
43 |
990 |
d_bags.insert(n); |
44 |
990 |
} |
45 |
|
|
46 |
2743 |
void SolverState::registerCountTerm(TNode n) |
47 |
|
{ |
48 |
2743 |
Assert(n.getKind() == BAG_COUNT); |
49 |
5486 |
Node element = getRepresentative(n[0]); |
50 |
5486 |
Node bag = getRepresentative(n[1]); |
51 |
2743 |
d_bagElements[bag].insert(element); |
52 |
2743 |
} |
53 |
|
|
54 |
23984 |
const std::set<Node>& SolverState::getBags() { return d_bags; } |
55 |
|
|
56 |
2839 |
const std::set<Node>& SolverState::getElements(Node B) |
57 |
|
{ |
58 |
5678 |
Node bag = getRepresentative(B); |
59 |
5678 |
return d_bagElements[bag]; |
60 |
|
} |
61 |
|
|
62 |
11992 |
const std::set<Node>& SolverState::getDisequalBagTerms() { return d_deq; } |
63 |
|
|
64 |
11992 |
void SolverState::reset() |
65 |
|
{ |
66 |
11992 |
d_bagElements.clear(); |
67 |
11992 |
d_bags.clear(); |
68 |
11992 |
d_deq.clear(); |
69 |
11992 |
} |
70 |
|
|
71 |
11992 |
void SolverState::initialize() |
72 |
|
{ |
73 |
11992 |
reset(); |
74 |
11992 |
collectBagsAndCountTerms(); |
75 |
11992 |
collectDisequalBagTerms(); |
76 |
11992 |
} |
77 |
|
|
78 |
11992 |
void SolverState::collectBagsAndCountTerms() |
79 |
|
{ |
80 |
11992 |
eq::EqClassesIterator repIt = eq::EqClassesIterator(d_ee); |
81 |
64866 |
while (!repIt.isFinished()) |
82 |
|
{ |
83 |
52874 |
Node eqc = (*repIt); |
84 |
26437 |
Trace("bags-eqc") << "Eqc [ " << eqc << " ] = { "; |
85 |
|
|
86 |
26437 |
if (eqc.getType().isBag()) |
87 |
|
{ |
88 |
990 |
registerBag(eqc); |
89 |
|
} |
90 |
|
|
91 |
26437 |
eq::EqClassIterator it = eq::EqClassIterator(eqc, d_ee); |
92 |
86035 |
while (!it.isFinished()) |
93 |
|
{ |
94 |
59598 |
Node n = (*it); |
95 |
29799 |
Trace("bags-eqc") << (*it) << " "; |
96 |
29799 |
Kind k = n.getKind(); |
97 |
29799 |
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 |
504 |
Node count = d_nm->mkNode(BAG_COUNT, n[0], n); |
102 |
252 |
registerCountTerm(count); |
103 |
504 |
Trace("SolverState::collectBagsAndCountTerms") |
104 |
252 |
<< "registered " << count << endl; |
105 |
|
} |
106 |
29799 |
if (k == BAG_COUNT) |
107 |
|
{ |
108 |
|
// this takes care of all count terms in each equivalent class |
109 |
2491 |
registerCountTerm(n); |
110 |
4982 |
Trace("SolverState::collectBagsAndCountTerms") |
111 |
2491 |
<< "registered " << n << endl; |
112 |
|
} |
113 |
29799 |
++it; |
114 |
|
} |
115 |
26437 |
Trace("bags-eqc") << " } " << std::endl; |
116 |
26437 |
++repIt; |
117 |
|
} |
118 |
|
|
119 |
11992 |
Trace("bags-eqc") << "bag representatives: " << d_bags << endl; |
120 |
11992 |
Trace("bags-eqc") << "bag elements: " << d_bagElements << endl; |
121 |
11992 |
} |
122 |
|
|
123 |
11992 |
void SolverState::collectDisequalBagTerms() |
124 |
|
{ |
125 |
11992 |
eq::EqClassIterator it = eq::EqClassIterator(d_false, d_ee); |
126 |
37412 |
while (!it.isFinished()) |
127 |
|
{ |
128 |
25420 |
Node n = (*it); |
129 |
12710 |
if (n.getKind() == EQUAL && n[0].getType().isBag()) |
130 |
|
{ |
131 |
270 |
Trace("bags-eqc") << "Disequal terms: " << n << std::endl; |
132 |
270 |
d_deq.insert(n); |
133 |
|
} |
134 |
12710 |
++it; |
135 |
|
} |
136 |
11992 |
} |
137 |
|
|
138 |
|
} // namespace bags |
139 |
|
} // namespace theory |
140 |
28191 |
} // namespace cvc5 |