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-2025 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::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 : 34 : Node A = n[0];
89 : 34 : TypeNode setType = A.getType();
90 : 34 : TypeNode partitionType = n.getType();
91 : :
92 [ - + ]: 17 : if (A.getKind() == Kind::SET_EMPTY)
93 : : {
94 : : // return a nonempty partition
95 : 0 : return NodeManager::mkNode(Kind::SET_SINGLETON, A);
96 : : }
97 : :
98 : : std::vector<uint32_t> indices =
99 : 34 : n.getOperator().getConst<ProjectOp>().getIndices();
100 : :
101 : 34 : std::set<Node> elements = NormalForm::getElementsFromNormalConstant(A);
102 [ + - ]: 17 : Trace("sets-group") << "elements: " << elements << std::endl;
103 : : // a simple map from elements to equivalent classes with this invariant:
104 : : // each key element must appear exactly once in one of the values.
105 : 34 : std::map<Node, std::set<Node>> sets;
106 : 34 : std::set<Node> emptyClass;
107 [ + + ]: 127 : for (const Node& element : elements)
108 : : {
109 : : // initially each singleton element is an equivalence class
110 : 220 : sets[element] = {element};
111 : : }
112 [ + + ]: 127 : for (std::set<Node>::iterator i = elements.begin(); i != elements.end(); ++i)
113 : : {
114 : 110 : Node iElement = *i;
115 [ + + ]: 110 : if (sets[iElement].empty())
116 : : {
117 : : // skip this element since its equivalent class has already been processed
118 : 63 : continue;
119 : : }
120 : 47 : std::set<Node>::iterator j = i;
121 : 47 : ++j;
122 [ + + ]: 230 : while (j != elements.end())
123 : : {
124 : 366 : Node jElement = *j;
125 [ + + ]: 183 : if (TupleUtils::sameProjection(indices, iElement, jElement))
126 : : {
127 : : // add element j to the equivalent class
128 : 63 : sets[iElement].insert(jElement);
129 : : // mark the equivalent class of j as processed
130 : 63 : sets[jElement] = emptyClass;
131 : : }
132 : 183 : ++j;
133 : : }
134 : : }
135 : :
136 : : // construct the partition parts
137 : 34 : std::set<Node> parts;
138 [ + + ]: 127 : for (std::pair<Node, std::set<Node>> pair : sets)
139 : : {
140 : 110 : const std::set<Node>& eqc = pair.second;
141 [ + + ]: 110 : if (eqc.empty())
142 : : {
143 : 63 : continue;
144 : : }
145 : 94 : Node part = NormalForm::elementsToSet(eqc, setType);
146 : 47 : parts.insert(part);
147 : : }
148 : 34 : Node ret = NormalForm::elementsToSet(parts, partitionType);
149 [ + - ]: 17 : Trace("sets-group") << "ret: " << ret << std::endl;
150 : 17 : return ret;
151 : : }
152 : :
153 : 2 : Node RelsUtils::evaluateRelationAggregate(TNode n)
154 : : {
155 [ - + ][ - + ]: 2 : Assert(n.getKind() == Kind::RELATION_AGGREGATE);
[ - - ]
156 : 2 : if (!(n[1].isConst() && n[2].isConst()))
157 : : {
158 : : // we can't proceed further.
159 : 0 : return n;
160 : : }
161 : :
162 : 4 : Node reduction = SetReduction::reduceAggregateOperator(n);
163 : 2 : return reduction;
164 : : }
165 : :
166 : : } // namespace sets
167 : : } // namespace theory
168 : : } // namespace cvc5::internal
|