Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Mudathir Mohamed, Aina Niemetz, Andrew Reynolds
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * Utility functions for relations.
14 : : */
15 : :
16 : : #include "rels_utils.h"
17 : :
18 : : #include "expr/dtype.h"
19 : : #include "expr/dtype_cons.h"
20 : : #include "theory/datatypes/project_op.h"
21 : : #include "theory/datatypes/tuple_utils.h"
22 : : #include "theory/sets/normal_form.h"
23 : : #include "theory/sets/set_reduction.h"
24 : :
25 : : using namespace cvc5::internal::kind;
26 : : using namespace cvc5::internal::theory::datatypes;
27 : : using namespace cvc5::internal::theory::sets;
28 : :
29 : : namespace cvc5::internal {
30 : : namespace theory {
31 : : namespace sets {
32 : :
33 : 9 : std::set<Node> RelsUtils::computeTC(const std::set<Node>& members, Node rel)
34 : : {
35 : 9 : std::set<Node>::iterator mem_it = members.begin();
36 : 18 : std::map<Node, int> ele_num_map;
37 : 9 : std::set<Node> tc_rel_mem;
38 : :
39 [ + + ]: 29 : while (mem_it != members.end())
40 : : {
41 : 40 : Node fst = TupleUtils::nthElementOfTuple(*mem_it, 0);
42 : 40 : Node snd = TupleUtils::nthElementOfTuple(*mem_it, 1);
43 : 40 : std::set<Node> traversed;
44 : 20 : traversed.insert(fst);
45 : 20 : computeTC(rel, members, fst, snd, traversed, tc_rel_mem);
46 : 20 : mem_it++;
47 : : }
48 : 18 : return tc_rel_mem;
49 : : }
50 : :
51 : 37 : void RelsUtils::computeTC(Node rel,
52 : : const std::set<Node>& members,
53 : : Node a,
54 : : Node b,
55 : : std::set<Node>& traversed,
56 : : std::set<Node>& transitiveClosureMembers)
57 : : {
58 : 37 : transitiveClosureMembers.insert(constructPair(rel, a, b));
59 [ + + ]: 37 : if (traversed.find(b) != traversed.end())
60 : : {
61 : 3 : return;
62 : : }
63 : 34 : traversed.insert(b);
64 : 34 : std::set<Node>::iterator mem_it = members.begin();
65 [ + + ]: 151 : while (mem_it != members.end())
66 : : {
67 : 234 : Node new_fst = TupleUtils::nthElementOfTuple(*mem_it, 0);
68 : 234 : Node new_snd = TupleUtils::nthElementOfTuple(*mem_it, 1);
69 [ + + ]: 117 : if (b == new_fst)
70 : : {
71 : 17 : computeTC(rel, members, a, new_snd, traversed, transitiveClosureMembers);
72 : : }
73 : 117 : mem_it++;
74 : : }
75 : : }
76 : :
77 : 2634 : Node RelsUtils::constructPair(Node rel, Node a, Node b)
78 : : {
79 : 2634 : const DType& dt = rel.getType().getSetElementType().getDType();
80 : : return NodeManager::currentNM()->mkNode(
81 : 2634 : Kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), a, b);
82 : : }
83 : :
84 : 17 : Node RelsUtils::evaluateGroup(TNode n)
85 : : {
86 [ - + ][ - + ]: 17 : Assert(n.getKind() == Kind::RELATION_GROUP);
[ - - ]
87 : :
88 : 17 : NodeManager* nm = NodeManager::currentNM();
89 : :
90 : 34 : Node A = n[0];
91 : 34 : TypeNode setType = A.getType();
92 : 34 : TypeNode partitionType = n.getType();
93 : :
94 [ - + ]: 17 : if (A.getKind() == Kind::SET_EMPTY)
95 : : {
96 : : // return a nonempty partition
97 : 0 : return nm->mkNode(Kind::SET_SINGLETON, A);
98 : : }
99 : :
100 : : std::vector<uint32_t> indices =
101 : 34 : n.getOperator().getConst<ProjectOp>().getIndices();
102 : :
103 : 34 : std::set<Node> elements = NormalForm::getElementsFromNormalConstant(A);
104 [ + - ]: 17 : Trace("sets-group") << "elements: " << elements << std::endl;
105 : : // a simple map from elements to equivalent classes with this invariant:
106 : : // each key element must appear exactly once in one of the values.
107 : 34 : std::map<Node, std::set<Node>> sets;
108 : 34 : std::set<Node> emptyClass;
109 [ + + ]: 127 : for (const Node& element : elements)
110 : : {
111 : : // initially each singleton element is an equivalence class
112 : 220 : sets[element] = {element};
113 : : }
114 [ + + ]: 127 : for (std::set<Node>::iterator i = elements.begin(); i != elements.end(); ++i)
115 : : {
116 : 110 : Node iElement = *i;
117 [ + + ]: 110 : if (sets[iElement].empty())
118 : : {
119 : : // skip this element since its equivalent class has already been processed
120 : 63 : continue;
121 : : }
122 : 47 : std::set<Node>::iterator j = i;
123 : 47 : ++j;
124 [ + + ]: 230 : while (j != elements.end())
125 : : {
126 : 366 : Node jElement = *j;
127 [ + + ]: 183 : if (TupleUtils::sameProjection(indices, iElement, jElement))
128 : : {
129 : : // add element j to the equivalent class
130 : 63 : sets[iElement].insert(jElement);
131 : : // mark the equivalent class of j as processed
132 : 63 : sets[jElement] = emptyClass;
133 : : }
134 : 183 : ++j;
135 : : }
136 : : }
137 : :
138 : : // construct the partition parts
139 : 34 : std::set<Node> parts;
140 [ + + ]: 127 : for (std::pair<Node, std::set<Node>> pair : sets)
141 : : {
142 : 110 : const std::set<Node>& eqc = pair.second;
143 [ + + ]: 110 : if (eqc.empty())
144 : : {
145 : 63 : continue;
146 : : }
147 : 94 : Node part = NormalForm::elementsToSet(eqc, setType);
148 : 47 : parts.insert(part);
149 : : }
150 : 34 : Node ret = NormalForm::elementsToSet(parts, partitionType);
151 [ + - ]: 17 : Trace("sets-group") << "ret: " << ret << std::endl;
152 : 17 : return ret;
153 : : }
154 : :
155 : 2 : Node RelsUtils::evaluateRelationAggregate(TNode n)
156 : : {
157 [ - + ][ - + ]: 2 : Assert(n.getKind() == Kind::RELATION_AGGREGATE);
[ - - ]
158 : 2 : if (!(n[1].isConst() && n[2].isConst()))
159 : : {
160 : : // we can't proceed further.
161 : 0 : return n;
162 : : }
163 : :
164 : 4 : Node reduction = SetReduction::reduceAggregateOperator(n);
165 : 2 : return reduction;
166 : : }
167 : :
168 : : } // namespace sets
169 : : } // namespace theory
170 : : } // namespace cvc5::internal
|
