Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Mudathir Mohamed
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 : : * Sets theory.
14 : : */
15 : :
16 : : #include "theory/sets/theory_sets.h"
17 : :
18 : : #include "options/sets_options.h"
19 : : #include "theory/sets/set_reduction.h"
20 : : #include "theory/sets/theory_sets_private.h"
21 : : #include "theory/sets/theory_sets_rewriter.h"
22 : : #include "theory/theory_model.h"
23 : : #include "theory/trust_substitutions.h"
24 : :
25 : : using namespace cvc5::internal::kind;
26 : :
27 : : namespace cvc5::internal {
28 : : namespace theory {
29 : : namespace sets {
30 : :
31 : 50287 : TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation)
32 : : : Theory(THEORY_SETS, env, out, valuation),
33 : : d_skCache(env.getNodeManager(), env.getRewriter()),
34 : 50287 : d_state(env, valuation, d_skCache),
35 : : d_rewriter(
36 : 150861 : nodeManager(), options().sets.setsCardExp, options().sets.relsExp),
37 : 50287 : d_im(env, *this, &d_rewriter, d_state),
38 : : d_cpacb(*this),
39 : : d_internal(
40 : 50287 : new TheorySetsPrivate(env, *this, d_state, d_im, d_skCache, d_cpacb)),
41 : : d_checker(nodeManager()),
42 : 100574 : d_notify(*d_internal.get(), d_im)
43 : : {
44 : : // use the official theory state and inference manager objects
45 : 50287 : d_theoryState = &d_state;
46 : 50287 : d_inferManager = &d_im;
47 : 50287 : }
48 : :
49 : 99884 : TheorySets::~TheorySets()
50 : : {
51 : 99884 : }
52 : :
53 : 50287 : TheoryRewriter* TheorySets::getTheoryRewriter() { return &d_rewriter; }
54 : :
55 : 18817 : ProofRuleChecker* TheorySets::getProofChecker() { return &d_checker; }
56 : :
57 : 50287 : bool TheorySets::needsEqualityEngine(EeSetupInfo& esi)
58 : : {
59 : 50287 : esi.d_notify = &d_notify;
60 : 50287 : esi.d_name = "theory::sets::ee";
61 : 50287 : esi.d_notifyNewClass = true;
62 : 50287 : esi.d_notifyMerge = true;
63 : 50287 : esi.d_notifyDisequal = true;
64 : 50287 : return true;
65 : : }
66 : :
67 : 50287 : void TheorySets::finishInit()
68 : : {
69 [ - + ][ - + ]: 50287 : Assert(d_equalityEngine != nullptr);
[ - - ]
70 : :
71 : 50287 : d_valuation.setUnevaluatedKind(Kind::SET_COMPREHENSION);
72 : : // choice is used to eliminate witness
73 : 50287 : d_valuation.setUnevaluatedKind(Kind::WITNESS);
74 : : // Universe set is not evaluated. This is moreover important for ensuring that
75 : : // we do not eliminate terms whose value involves the universe set.
76 : 50287 : d_valuation.setUnevaluatedKind(Kind::SET_UNIVERSE);
77 : :
78 : : // functions we are doing congruence over
79 : 50287 : d_equalityEngine->addFunctionKind(Kind::SET_SINGLETON);
80 : 50287 : d_equalityEngine->addFunctionKind(Kind::SET_UNION);
81 : 50287 : d_equalityEngine->addFunctionKind(Kind::SET_INTER);
82 : 50287 : d_equalityEngine->addFunctionKind(Kind::SET_MINUS);
83 : 50287 : d_equalityEngine->addFunctionKind(Kind::SET_MEMBER);
84 : 50287 : d_equalityEngine->addFunctionKind(Kind::SET_SUBSET);
85 : : // relation operators
86 : 50287 : d_equalityEngine->addFunctionKind(Kind::RELATION_PRODUCT);
87 : 50287 : d_equalityEngine->addFunctionKind(Kind::RELATION_JOIN);
88 : 50287 : d_equalityEngine->addFunctionKind(Kind::RELATION_TABLE_JOIN);
89 : 50287 : d_equalityEngine->addFunctionKind(Kind::RELATION_TRANSPOSE);
90 : 50287 : d_equalityEngine->addFunctionKind(Kind::RELATION_TCLOSURE);
91 : 50287 : d_equalityEngine->addFunctionKind(Kind::RELATION_JOIN_IMAGE);
92 : 50287 : d_equalityEngine->addFunctionKind(Kind::RELATION_IDEN);
93 : 50287 : d_equalityEngine->addFunctionKind(Kind::APPLY_CONSTRUCTOR);
94 : : // we do congruence over cardinality
95 : 50287 : d_equalityEngine->addFunctionKind(Kind::SET_CARD);
96 : :
97 : : // finish initialization internally
98 : 50287 : d_internal->finishInit();
99 : :
100 : : // memberships are not relevant for model building
101 : 50287 : d_valuation.setIrrelevantKind(Kind::SET_MEMBER);
102 : 50287 : }
103 : :
104 : 241804 : void TheorySets::postCheck(Effort level) { d_internal->postCheck(level); }
105 : :
106 : 472867 : void TheorySets::notifyFact(TNode atom,
107 : : bool polarity,
108 : : TNode fact,
109 : : bool isInternal)
110 : : {
111 : 472867 : d_internal->notifyFact(atom, polarity, fact);
112 : 472867 : }
113 : :
114 : 13687 : bool TheorySets::collectModelValues(TheoryModel* m,
115 : : const std::set<Node>& termSet)
116 : : {
117 : 13687 : return d_internal->collectModelValues(m, termSet);
118 : : }
119 : :
120 : 26873 : void TheorySets::computeCareGraph() {
121 : 26873 : d_internal->computeCareGraph();
122 : 26873 : }
123 : :
124 : 6949 : TrustNode TheorySets::explain(TNode node)
125 : : {
126 : 6949 : return d_im.explainLit(node);
127 : : }
128 : :
129 : 0 : Node TheorySets::getCandidateModelValue(TNode node) { return Node::null(); }
130 : :
131 : 137073 : void TheorySets::preRegisterTerm(TNode node)
132 : : {
133 : 137073 : d_internal->preRegisterTerm(node);
134 : 137073 : }
135 : :
136 : 67158 : TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
137 : : {
138 : 67158 : Kind nk = n.getKind();
139 [ + + ][ + - ]: 67158 : if (nk == Kind::SET_UNIVERSE || nk == Kind::SET_COMPLEMENT
140 [ + + ][ + + ]: 66720 : || nk == Kind::RELATION_JOIN_IMAGE || nk == Kind::SET_COMPREHENSION)
141 : : {
142 [ - + ]: 621 : if (!options().sets.setsExp)
143 : : {
144 : 0 : std::stringstream ss;
145 : : ss << "Extended set operators are not supported in default mode, try "
146 : 0 : "--sets-exp.";
147 : 0 : throw LogicException(ss.str());
148 : : }
149 : : }
150 [ + + ]: 67158 : if (nk == Kind::SET_COMPREHENSION)
151 : : {
152 : : // set comprehension is an implicit quantifier, require it in the logic
153 [ - + ]: 120 : if (!logicInfo().isQuantified())
154 : : {
155 : 0 : std::stringstream ss;
156 : 0 : ss << "Set comprehensions require quantifiers in the background logic.";
157 : 0 : throw LogicException(ss.str());
158 : : }
159 : : }
160 [ + - ][ + + ]: 67158 : if (nk == Kind::RELATION_AGGREGATE || nk == Kind::RELATION_PROJECT
161 [ + + ][ + + ]: 67153 : || nk == Kind::SET_MAP || nk == Kind::SET_FOLD)
162 : : {
163 : : // requires higher order
164 [ + + ]: 72 : if (!logicInfo().isHigherOrder())
165 : : {
166 : 2 : std::stringstream ss;
167 : 1 : ss << "Term of kind " << nk
168 : : << " are only supported with "
169 : 1 : "higher-order logic. Try adding the logic prefix HO_.";
170 : 1 : throw LogicException(ss.str());
171 : : }
172 : : }
173 [ + + ]: 67157 : if (nk == Kind::SET_FOLD)
174 : : {
175 : 12 : std::vector<Node> asserts;
176 : 12 : Node ret = SetReduction::reduceFoldOperator(n, asserts);
177 : 6 : NodeManager* nm = nodeManager();
178 : 6 : Node andNode = nm->mkNode(Kind::AND, asserts);
179 : 6 : d_im.lemma(andNode, InferenceId::SETS_FOLD);
180 : 6 : return TrustNode::mkTrustRewrite(n, ret, nullptr);
181 : : }
182 [ - + ]: 67151 : if (nk == Kind::RELATION_AGGREGATE)
183 : : {
184 : 0 : Node ret = SetReduction::reduceAggregateOperator(n);
185 : 0 : return TrustNode::mkTrustRewrite(n, ret, nullptr);
186 : : }
187 [ + + ]: 67151 : if (nk == Kind::RELATION_PROJECT)
188 : : {
189 : 4 : Node ret = SetReduction::reduceProjectOperator(n);
190 : 4 : return TrustNode::mkTrustRewrite(n, ret, nullptr);
191 : : }
192 : 67147 : return d_internal->ppRewrite(n, lems);
193 : : }
194 : :
195 : 6058 : bool TheorySets::ppAssert(TrustNode tin, TrustSubstitutionMap& outSubstitutions)
196 : : {
197 : 6058 : TNode in = tin.getNode();
198 [ + - ]: 6058 : Trace("sets-proc") << "ppAssert : " << in << std::endl;
199 : 6058 : bool status = false;
200 : :
201 : : // this is based off of Theory::ppAssert
202 [ + + ]: 6058 : if (in.getKind() == Kind::EQUAL)
203 : : {
204 : 1769 : if (in[0].isVar() && d_valuation.isLegalElimination(in[0], in[1]))
205 : : {
206 : : // We cannot solve for sets if setsExp is enabled, since universe set
207 : : // may appear when this option is enabled, and solving for such a set
208 : : // impacts the semantics of universe set, see
209 : : // regress0/sets/pre-proc-univ.smt2
210 : 965 : if (!in[0].getType().isSet() || !options().sets.setsExp)
211 : : {
212 : 832 : outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
213 : 832 : status = true;
214 : : }
215 : : }
216 : 804 : else if (in[1].isVar() && d_valuation.isLegalElimination(in[1], in[0]))
217 : : {
218 : 15 : if (!in[0].getType().isSet() || !options().sets.setsExp)
219 : : {
220 : 0 : outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
221 : 0 : status = true;
222 : : }
223 : : }
224 : : }
225 : 12116 : return status;
226 : : }
227 : :
228 : 49720 : void TheorySets::presolve() {
229 : 49720 : d_internal->presolve();
230 : 49720 : }
231 : :
232 : 0 : bool TheorySets::isEntailed( Node n, bool pol ) {
233 : 0 : return d_internal->isEntailed( n, pol );
234 : : }
235 : :
236 : 16447 : void TheorySets::processCarePairArgs(TNode a, TNode b)
237 : : {
238 : : // Usually when (= (f x) (f y)), we don't care whether (= x y) is true or
239 : : // not for the shared variables x, y in the care graph.
240 : : // However, this does not apply to the membership operator since the
241 : : // equality or disequality between members affects the number of elements
242 : : // in a set. Therefore we need to split on (= x y) for kind SET_MEMBER.
243 : : // Example:
244 : : // Suppose (set.member x S) = (set.member y S) = true and there are
245 : : // no other members in S. We would get S = {x} if (= x y) is true.
246 : : // Otherwise we would get S = {x, y}.
247 : 16447 : if (a.getKind() != Kind::SET_MEMBER && d_state.areEqual(a, b))
248 : : {
249 : 0 : return;
250 : : }
251 : : // otherwise, we add pairs for each of their arguments
252 : 16447 : addCarePairArgs(a, b);
253 : :
254 : 16447 : d_internal->processCarePairArgs(a, b);
255 : : }
256 : :
257 : : /**************************** eq::NotifyClass *****************************/
258 : :
259 : 118181 : void TheorySets::NotifyClass::eqNotifyNewClass(TNode t)
260 : : {
261 [ + - ]: 236362 : Trace("sets-eq") << "[sets-eq] eqNotifyNewClass:"
262 : 118181 : << " t = " << t << std::endl;
263 : 118181 : d_theory.eqNotifyNewClass(t);
264 : 118181 : }
265 : :
266 : 464675 : void TheorySets::NotifyClass::eqNotifyMerge(TNode t1, TNode t2)
267 : : {
268 [ + - ]: 929350 : Trace("sets-eq") << "[sets-eq] eqNotifyMerge:"
269 : 464675 : << " t1 = " << t1 << " t2 = " << t2 << std::endl;
270 : 464675 : d_theory.eqNotifyMerge(t1, t2);
271 : 464675 : }
272 : :
273 : 73002 : void TheorySets::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
274 : : {
275 [ + - ]: 146004 : Trace("sets-eq") << "[sets-eq] eqNotifyDisequal:"
276 : 0 : << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason
277 : 73002 : << std::endl;
278 : 73002 : d_theory.eqNotifyDisequal(t1, t2, reason);
279 : 73002 : }
280 : :
281 : : } // namespace sets
282 : : } // namespace theory
283 : : } // namespace cvc5::internal
|
