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 : : * set reduction.
14 : : */
15 : :
16 : : #include "theory/sets/set_reduction.h"
17 : :
18 : : #include "expr/bound_var_manager.h"
19 : : #include "expr/emptyset.h"
20 : : #include "expr/skolem_manager.h"
21 : : #include "theory/datatypes//project_op.h"
22 : : #include "theory/quantifiers/fmf/bounded_integers.h"
23 : : #include "util/rational.h"
24 : :
25 : : using namespace cvc5::internal;
26 : : using namespace cvc5::internal::kind;
27 : :
28 : : namespace cvc5::internal {
29 : : namespace theory {
30 : : namespace sets {
31 : :
32 : 0 : SetReduction::SetReduction() {}
33 : :
34 : 0 : SetReduction::~SetReduction() {}
35 : :
36 : : /**
37 : : * A bound variable corresponding to the universally quantified integer
38 : : * variable used to range over (may be distinct) elements in a set, used
39 : : * for axiomatizing the behavior of some term.
40 : : * If there are multiple quantifiers, this variable should be the first one.
41 : : */
42 : : struct FirstIndexVarAttributeId
43 : : {
44 : : };
45 : : typedef expr::Attribute<FirstIndexVarAttributeId, Node> FirstIndexVarAttribute;
46 : :
47 : : /**
48 : : * A bound variable corresponding to the universally quantified integer
49 : : * variable used to range over (may be distinct) elements in a set, used
50 : : * for axiomatizing the behavior of some term.
51 : : * This variable should be the second of multiple quantifiers.
52 : : */
53 : : struct SecondIndexVarAttributeId
54 : : {
55 : : };
56 : : typedef expr::Attribute<SecondIndexVarAttributeId, Node>
57 : : SecondIndexVarAttribute;
58 : :
59 : 6 : Node SetReduction::reduceFoldOperator(Node node, std::vector<Node>& asserts)
60 : : {
61 [ - + ][ - + ]: 6 : Assert(node.getKind() == Kind::SET_FOLD);
[ - - ]
62 : 6 : NodeManager* nm = NodeManager::currentNM();
63 : 6 : SkolemManager* sm = nm->getSkolemManager();
64 : 12 : Node f = node[0];
65 : 12 : Node t = node[1];
66 : 12 : Node A = node[2];
67 : 12 : Node zero = nm->mkConstInt(Rational(0));
68 : 12 : Node one = nm->mkConstInt(Rational(1));
69 : : // skolem functions
70 : 12 : Node n = sm->mkSkolemFunction(SkolemId::SETS_FOLD_CARD, A);
71 : 12 : Node uf = sm->mkSkolemFunction(SkolemId::SETS_FOLD_ELEMENTS, A);
72 : 12 : Node unionNode = sm->mkSkolemFunction(SkolemId::SETS_FOLD_UNION, A);
73 : 36 : Node combine = sm->mkSkolemFunction(SkolemId::SETS_FOLD_COMBINE, {f, t, A});
74 : :
75 : 6 : BoundVarManager* bvm = nm->getBoundVarManager();
76 : : Node i =
77 : 18 : bvm->mkBoundVar<FirstIndexVarAttribute>(node, "i", nm->integerType());
78 : 12 : Node iList = nm->mkNode(Kind::BOUND_VAR_LIST, i);
79 : 18 : Node iMinusOne = nm->mkNode(Kind::SUB, i, one);
80 : 18 : Node uf_i = nm->mkNode(Kind::APPLY_UF, uf, i);
81 : 18 : Node combine_0 = nm->mkNode(Kind::APPLY_UF, combine, zero);
82 : 18 : Node combine_iMinusOne = nm->mkNode(Kind::APPLY_UF, combine, iMinusOne);
83 : 18 : Node combine_i = nm->mkNode(Kind::APPLY_UF, combine, i);
84 : 12 : Node combine_n = nm->mkNode(Kind::APPLY_UF, combine, n);
85 : 18 : Node union_0 = nm->mkNode(Kind::APPLY_UF, unionNode, zero);
86 : 18 : Node union_iMinusOne = nm->mkNode(Kind::APPLY_UF, unionNode, iMinusOne);
87 : 18 : Node union_i = nm->mkNode(Kind::APPLY_UF, unionNode, i);
88 : 18 : Node union_n = nm->mkNode(Kind::APPLY_UF, unionNode, n);
89 : 12 : Node combine_0_equal = combine_0.eqNode(t);
90 : : Node combine_i_equal =
91 : 18 : combine_i.eqNode(nm->mkNode(Kind::APPLY_UF, f, uf_i, combine_iMinusOne));
92 : 18 : Node union_0_equal = union_0.eqNode(nm->mkConst(EmptySet(A.getType())));
93 : 12 : Node singleton = nm->mkNode(Kind::SET_SINGLETON, uf_i);
94 : :
95 : : Node union_i_equal =
96 : 18 : union_i.eqNode(nm->mkNode(Kind::SET_UNION, singleton, union_iMinusOne));
97 : : Node interval_i = nm->mkNode(
98 : 18 : Kind::AND, nm->mkNode(Kind::GEQ, i, one), nm->mkNode(Kind::LEQ, i, n));
99 : :
100 : : Node body_i =
101 : : nm->mkNode(Kind::IMPLIES,
102 : : interval_i,
103 : 18 : nm->mkNode(Kind::AND, combine_i_equal, union_i_equal));
104 : : Node forAll_i =
105 : 18 : quantifiers::BoundedIntegers::mkBoundedForall(nm, iList, body_i);
106 : 18 : Node nonNegative = nm->mkNode(Kind::GEQ, n, zero);
107 : 12 : Node union_n_equal = A.eqNode(union_n);
108 : 6 : asserts.push_back(forAll_i);
109 : 6 : asserts.push_back(combine_0_equal);
110 : 6 : asserts.push_back(union_0_equal);
111 : 6 : asserts.push_back(union_n_equal);
112 : 6 : asserts.push_back(nonNegative);
113 : 12 : return combine_n;
114 : : }
115 : :
116 : 2 : Node SetReduction::reduceAggregateOperator(Node node)
117 : : {
118 [ - + ][ - + ]: 2 : Assert(node.getKind() == Kind::RELATION_AGGREGATE);
[ - - ]
119 : 2 : NodeManager* nm = NodeManager::currentNM();
120 : 2 : BoundVarManager* bvm = nm->getBoundVarManager();
121 : 4 : Node function = node[0];
122 : 6 : TypeNode elementType = function.getType().getArgTypes()[0];
123 : 4 : Node initialValue = node[1];
124 : 4 : Node A = node[2];
125 : :
126 : 4 : ProjectOp op = node.getOperator().getConst<ProjectOp>();
127 : 4 : Node groupOp = nm->mkConst(Kind::RELATION_GROUP_OP, op);
128 : 8 : Node group = nm->mkNode(Kind::RELATION_GROUP, {groupOp, A});
129 : :
130 : : Node set = bvm->mkBoundVar<FirstIndexVarAttribute>(
131 : 6 : group, "set", nm->mkSetType(elementType));
132 : 4 : Node foldList = nm->mkNode(Kind::BOUND_VAR_LIST, set);
133 : 6 : Node foldBody = nm->mkNode(Kind::SET_FOLD, function, initialValue, set);
134 : :
135 : 6 : Node fold = nm->mkNode(Kind::LAMBDA, foldList, foldBody);
136 : 4 : Node map = nm->mkNode(Kind::SET_MAP, fold, group);
137 : 4 : return map;
138 : : }
139 : :
140 : 14 : Node SetReduction::reduceProjectOperator(Node n)
141 : : {
142 [ - + ][ - + ]: 14 : Assert(n.getKind() == Kind::RELATION_PROJECT);
[ - - ]
143 : 14 : NodeManager* nm = NodeManager::currentNM();
144 : 28 : Node A = n[0];
145 : 28 : TypeNode elementType = A.getType().getSetElementType();
146 : 28 : ProjectOp projectOp = n.getOperator().getConst<ProjectOp>();
147 : 28 : Node op = nm->mkConst(Kind::TUPLE_PROJECT_OP, projectOp);
148 : 42 : Node t = nm->mkBoundVar("t", elementType);
149 : 42 : Node projection = nm->mkNode(Kind::TUPLE_PROJECT, op, t);
150 : : Node lambda =
151 : 42 : nm->mkNode(Kind::LAMBDA, nm->mkNode(Kind::BOUND_VAR_LIST, t), projection);
152 : 28 : Node setMap = nm->mkNode(Kind::SET_MAP, lambda, A);
153 : 28 : return setMap;
154 : : }
155 : :
156 : : } // namespace sets
157 : : } // namespace theory
158 : : } // namespace cvc5::internal
|
