Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * set reduction.
11 : : */
12 : :
13 : : #include "theory/sets/set_reduction.h"
14 : :
15 : : #include "expr/bound_var_manager.h"
16 : : #include "expr/emptyset.h"
17 : : #include "expr/skolem_manager.h"
18 : : #include "theory/datatypes//project_op.h"
19 : : #include "theory/quantifiers/fmf/bounded_integers.h"
20 : : #include "util/rational.h"
21 : :
22 : : using namespace cvc5::internal;
23 : : using namespace cvc5::internal::kind;
24 : :
25 : : namespace cvc5::internal {
26 : : namespace theory {
27 : : namespace sets {
28 : :
29 : 0 : SetReduction::SetReduction() {}
30 : :
31 : 0 : SetReduction::~SetReduction() {}
32 : :
33 : 6 : Node SetReduction::reduceFoldOperator(Node node, std::vector<Node>& asserts)
34 : : {
35 [ - + ][ - + ]: 6 : Assert(node.getKind() == Kind::SET_FOLD);
[ - - ]
36 : 6 : NodeManager* nm = node.getNodeManager();
37 : 6 : SkolemManager* sm = nm->getSkolemManager();
38 : 6 : Node f = node[0];
39 : 6 : Node t = node[1];
40 : 6 : Node A = node[2];
41 : 6 : Node zero = nm->mkConstInt(Rational(0));
42 : 6 : Node one = nm->mkConstInt(Rational(1));
43 : : // skolem functions
44 : 6 : Node n = sm->mkSkolemFunction(SkolemId::SETS_FOLD_CARD, A);
45 : 6 : Node uf = sm->mkSkolemFunction(SkolemId::SETS_FOLD_ELEMENTS, A);
46 : 6 : Node unionNode = sm->mkSkolemFunction(SkolemId::SETS_FOLD_UNION, A);
47 : 30 : Node combine = sm->mkSkolemFunction(SkolemId::SETS_FOLD_COMBINE, {f, t, A});
48 : :
49 : 6 : BoundVarManager* bvm = nm->getBoundVarManager();
50 : : Node i = bvm->mkBoundVar(
51 : 12 : BoundVarId::SETS_FIRST_INDEX, node, "i", nm->integerType());
52 : 6 : Node iList = nm->mkNode(Kind::BOUND_VAR_LIST, i);
53 : 12 : Node iMinusOne = nm->mkNode(Kind::SUB, i, one);
54 : 12 : Node uf_i = nm->mkNode(Kind::APPLY_UF, uf, i);
55 : 12 : Node combine_0 = nm->mkNode(Kind::APPLY_UF, combine, zero);
56 : 12 : Node combine_iMinusOne = nm->mkNode(Kind::APPLY_UF, combine, iMinusOne);
57 : 12 : Node combine_i = nm->mkNode(Kind::APPLY_UF, combine, i);
58 : 12 : Node combine_n = nm->mkNode(Kind::APPLY_UF, combine, n);
59 : 12 : Node union_0 = nm->mkNode(Kind::APPLY_UF, unionNode, zero);
60 : 12 : Node union_iMinusOne = nm->mkNode(Kind::APPLY_UF, unionNode, iMinusOne);
61 : 12 : Node union_i = nm->mkNode(Kind::APPLY_UF, unionNode, i);
62 : 12 : Node union_n = nm->mkNode(Kind::APPLY_UF, unionNode, n);
63 : 6 : Node combine_0_equal = combine_0.eqNode(t);
64 : : Node combine_i_equal =
65 : 12 : combine_i.eqNode(nm->mkNode(Kind::APPLY_UF, f, uf_i, combine_iMinusOne));
66 : 12 : Node union_0_equal = union_0.eqNode(nm->mkConst(EmptySet(A.getType())));
67 : 6 : Node singleton = nm->mkNode(Kind::SET_SINGLETON, uf_i);
68 : :
69 : : Node union_i_equal =
70 : 12 : union_i.eqNode(nm->mkNode(Kind::SET_UNION, singleton, union_iMinusOne));
71 : 18 : Node interval_i = nm->mkNode(
72 : 12 : Kind::AND, {nm->mkNode(Kind::GEQ, i, one), nm->mkNode(Kind::LEQ, i, n)});
73 : :
74 : : Node body_i =
75 : : nm->mkNode(Kind::IMPLIES,
76 : : interval_i,
77 : 12 : nm->mkNode(Kind::AND, combine_i_equal, union_i_equal));
78 : : Node forAll_i =
79 : 12 : quantifiers::BoundedIntegers::mkBoundedForall(nm, iList, body_i);
80 : 12 : Node nonNegative = nm->mkNode(Kind::GEQ, n, zero);
81 : 6 : Node union_n_equal = A.eqNode(union_n);
82 : 6 : asserts.push_back(forAll_i);
83 : 6 : asserts.push_back(combine_0_equal);
84 : 6 : asserts.push_back(union_0_equal);
85 : 6 : asserts.push_back(union_n_equal);
86 : 6 : asserts.push_back(nonNegative);
87 : 12 : return combine_n;
88 : 6 : }
89 : :
90 : 2 : Node SetReduction::reduceAggregateOperator(Node node)
91 : : {
92 [ - + ][ - + ]: 2 : Assert(node.getKind() == Kind::RELATION_AGGREGATE);
[ - - ]
93 : 2 : NodeManager* nm = node.getNodeManager();
94 : 2 : BoundVarManager* bvm = nm->getBoundVarManager();
95 : 2 : Node function = node[0];
96 : 4 : TypeNode elementType = function.getType().getArgTypes()[0];
97 : 2 : Node initialValue = node[1];
98 : 2 : Node A = node[2];
99 : :
100 : 2 : ProjectOp op = node.getOperator().getConst<ProjectOp>();
101 : 2 : Node groupOp = nm->mkConst(Kind::RELATION_GROUP_OP, op);
102 : 6 : Node group = nm->mkNode(Kind::RELATION_GROUP, {groupOp, A});
103 : :
104 : : Node set = bvm->mkBoundVar(
105 : 4 : BoundVarId::SETS_FIRST_INDEX, group, "set", nm->mkSetType(elementType));
106 : 2 : Node foldList = nm->mkNode(Kind::BOUND_VAR_LIST, set);
107 : 4 : Node foldBody = nm->mkNode(Kind::SET_FOLD, function, initialValue, set);
108 : :
109 : 4 : Node fold = nm->mkNode(Kind::LAMBDA, foldList, foldBody);
110 : 4 : Node map = nm->mkNode(Kind::SET_MAP, fold, group);
111 : 4 : return map;
112 : 2 : }
113 : :
114 : 14 : Node SetReduction::reduceProjectOperator(Node n)
115 : : {
116 [ - + ][ - + ]: 14 : Assert(n.getKind() == Kind::RELATION_PROJECT);
[ - - ]
117 : 14 : NodeManager* nm = n.getNodeManager();
118 : 14 : Node A = n[0];
119 : 14 : TypeNode elementType = A.getType().getSetElementType();
120 : 14 : ProjectOp projectOp = n.getOperator().getConst<ProjectOp>();
121 : 14 : Node op = nm->mkConst(Kind::TUPLE_PROJECT_OP, projectOp);
122 : 28 : Node t = NodeManager::mkBoundVar("t", elementType);
123 : 28 : Node projection = nm->mkNode(Kind::TUPLE_PROJECT, op, t);
124 : : Node lambda =
125 : 28 : nm->mkNode(Kind::LAMBDA, nm->mkNode(Kind::BOUND_VAR_LIST, t), projection);
126 : 28 : Node setMap = nm->mkNode(Kind::SET_MAP, lambda, A);
127 : 28 : return setMap;
128 : 14 : }
129 : :
130 : : } // namespace sets
131 : : } // namespace theory
132 : : } // namespace cvc5::internal
|
