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-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 : : * 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 : 49283 : TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation)
32 : : : Theory(THEORY_SETS, env, out, valuation),
33 : : d_skCache(env.getNodeManager(), env.getRewriter()),
34 : 49283 : d_state(env, valuation, d_skCache),
35 : : d_rewriter(nodeManager()),
36 : 49283 : d_im(env, *this, &d_rewriter, d_state),
37 : : d_cpacb(*this),
38 : : d_internal(
39 : 49283 : new TheorySetsPrivate(env, *this, d_state, d_im, d_skCache, d_cpacb)),
40 : : d_checker(nodeManager()),
41 : 98566 : d_notify(*d_internal.get(), d_im)
42 : : {
43 : : // use the official theory state and inference manager objects
44 : 49283 : d_theoryState = &d_state;
45 : 49283 : d_inferManager = &d_im;
46 : 49283 : }
47 : :
48 : 98054 : TheorySets::~TheorySets()
49 : : {
50 : 98054 : }
51 : :
52 : 49283 : TheoryRewriter* TheorySets::getTheoryRewriter() { return &d_rewriter; }
53 : :
54 : 18636 : ProofRuleChecker* TheorySets::getProofChecker() { return &d_checker; }
55 : :
56 : 49283 : bool TheorySets::needsEqualityEngine(EeSetupInfo& esi)
57 : : {
58 : 49283 : esi.d_notify = &d_notify;
59 : 49283 : esi.d_name = "theory::sets::ee";
60 : 49283 : esi.d_notifyNewClass = true;
61 : 49283 : esi.d_notifyMerge = true;
62 : 49283 : esi.d_notifyDisequal = true;
63 : 49283 : return true;
64 : : }
65 : :
66 : 49283 : void TheorySets::finishInit()
67 : : {
68 [ - + ][ - + ]: 49283 : Assert(d_equalityEngine != nullptr);
[ - - ]
69 : :
70 : 49283 : d_valuation.setUnevaluatedKind(Kind::SET_COMPREHENSION);
71 : : // choice is used to eliminate witness
72 : 49283 : d_valuation.setUnevaluatedKind(Kind::WITNESS);
73 : : // Universe set is not evaluated. This is moreover important for ensuring that
74 : : // we do not eliminate terms whose value involves the universe set.
75 : 49283 : d_valuation.setUnevaluatedKind(Kind::SET_UNIVERSE);
76 : :
77 : : // functions we are doing congruence over
78 : 49283 : d_equalityEngine->addFunctionKind(Kind::SET_SINGLETON);
79 : 49283 : d_equalityEngine->addFunctionKind(Kind::SET_UNION);
80 : 49283 : d_equalityEngine->addFunctionKind(Kind::SET_INTER);
81 : 49283 : d_equalityEngine->addFunctionKind(Kind::SET_MINUS);
82 : 49283 : d_equalityEngine->addFunctionKind(Kind::SET_MEMBER);
83 : 49283 : d_equalityEngine->addFunctionKind(Kind::SET_SUBSET);
84 : : // relation operators
85 : 49283 : d_equalityEngine->addFunctionKind(Kind::RELATION_PRODUCT);
86 : 49283 : d_equalityEngine->addFunctionKind(Kind::RELATION_JOIN);
87 : 49283 : d_equalityEngine->addFunctionKind(Kind::RELATION_TABLE_JOIN);
88 : 49283 : d_equalityEngine->addFunctionKind(Kind::RELATION_TRANSPOSE);
89 : 49283 : d_equalityEngine->addFunctionKind(Kind::RELATION_TCLOSURE);
90 : 49283 : d_equalityEngine->addFunctionKind(Kind::RELATION_JOIN_IMAGE);
91 : 49283 : d_equalityEngine->addFunctionKind(Kind::RELATION_IDEN);
92 : 49283 : d_equalityEngine->addFunctionKind(Kind::APPLY_CONSTRUCTOR);
93 : : // we do congruence over cardinality
94 : 49283 : d_equalityEngine->addFunctionKind(Kind::SET_CARD);
95 : :
96 : : // finish initialization internally
97 : 49283 : d_internal->finishInit();
98 : :
99 : : // memberships are not relevant for model building
100 : 49283 : d_valuation.setIrrelevantKind(Kind::SET_MEMBER);
101 : 49283 : }
102 : :
103 : 264052 : void TheorySets::postCheck(Effort level) { d_internal->postCheck(level); }
104 : :
105 : 550017 : void TheorySets::notifyFact(TNode atom,
106 : : bool polarity,
107 : : TNode fact,
108 : : bool isInternal)
109 : : {
110 : 550017 : d_internal->notifyFact(atom, polarity, fact);
111 : 550017 : }
112 : :
113 : 16448 : bool TheorySets::collectModelValues(TheoryModel* m,
114 : : const std::set<Node>& termSet)
115 : : {
116 : 16448 : return d_internal->collectModelValues(m, termSet);
117 : : }
118 : :
119 : 25834 : void TheorySets::computeCareGraph() {
120 : 25834 : d_internal->computeCareGraph();
121 : 25834 : }
122 : :
123 : 7320 : TrustNode TheorySets::explain(TNode node)
124 : : {
125 : 7320 : return d_im.explainLit(node);
126 : : }
127 : :
128 : 0 : Node TheorySets::getCandidateModelValue(TNode node) { return Node::null(); }
129 : :
130 : 149801 : void TheorySets::preRegisterTerm(TNode node)
131 : : {
132 : 149801 : d_internal->preRegisterTerm(node);
133 : 149801 : }
134 : :
135 : 72902 : TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
136 : : {
137 : 72902 : Kind nk = n.getKind();
138 [ + + ][ + - ]: 72902 : if (nk == Kind::SET_UNIVERSE || nk == Kind::SET_COMPLEMENT
139 [ + + ][ + + ]: 72427 : || nk == Kind::RELATION_JOIN_IMAGE || nk == Kind::SET_COMPREHENSION)
140 : : {
141 [ - + ]: 680 : if (!options().sets.setsExp)
142 : : {
143 : 0 : std::stringstream ss;
144 : : ss << "Extended set operators are not supported in default mode, try "
145 : 0 : "--sets-exp.";
146 : 0 : throw LogicException(ss.str());
147 : : }
148 : : }
149 [ + + ]: 72902 : if (nk == Kind::SET_COMPREHENSION)
150 : : {
151 : : // set comprehension is an implicit quantifier, require it in the logic
152 [ - + ]: 136 : if (!logicInfo().isQuantified())
153 : : {
154 : 0 : std::stringstream ss;
155 : 0 : ss << "Set comprehensions require quantifiers in the background logic.";
156 : 0 : throw LogicException(ss.str());
157 : : }
158 : : }
159 [ + - ][ + + ]: 72902 : if (nk == Kind::RELATION_AGGREGATE || nk == Kind::RELATION_PROJECT
160 [ + + ][ + + ]: 72897 : || nk == Kind::SET_MAP || nk == Kind::SET_FOLD)
161 : : {
162 : : // requires higher order
163 [ + + ]: 75 : if (!logicInfo().isHigherOrder())
164 : : {
165 : 2 : std::stringstream ss;
166 : 1 : ss << "Term of kind " << nk
167 : : << " are only supported with "
168 : 1 : "higher-order logic. Try adding the logic prefix HO_.";
169 : 1 : throw LogicException(ss.str());
170 : : }
171 : : }
172 [ + + ]: 72901 : if (nk == Kind::SET_FOLD)
173 : : {
174 : 12 : std::vector<Node> asserts;
175 : 12 : Node ret = SetReduction::reduceFoldOperator(n, asserts);
176 : 6 : NodeManager* nm = nodeManager();
177 : 6 : Node andNode = nm->mkNode(Kind::AND, asserts);
178 : 6 : d_im.lemma(andNode, InferenceId::SETS_FOLD);
179 : 6 : return TrustNode::mkTrustRewrite(n, ret, nullptr);
180 : : }
181 [ - + ]: 72895 : if (nk == Kind::RELATION_AGGREGATE)
182 : : {
183 : 0 : Node ret = SetReduction::reduceAggregateOperator(n);
184 : 0 : return TrustNode::mkTrustRewrite(n, ret, nullptr);
185 : : }
186 [ + + ]: 72895 : if (nk == Kind::RELATION_PROJECT)
187 : : {
188 : 4 : Node ret = SetReduction::reduceProjectOperator(n);
189 : 4 : return TrustNode::mkTrustRewrite(n, ret, nullptr);
190 : : }
191 : 72891 : return d_internal->ppRewrite(n, lems);
192 : : }
193 : :
194 : 6848 : Theory::PPAssertStatus TheorySets::ppAssert(
195 : : TrustNode tin, TrustSubstitutionMap& outSubstitutions)
196 : : {
197 : 6848 : TNode in = tin.getNode();
198 [ + - ]: 6848 : Trace("sets-proc") << "ppAssert : " << in << std::endl;
199 : 6848 : Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
200 : :
201 : : // this is based off of Theory::ppAssert
202 [ + + ]: 6848 : if (in.getKind() == Kind::EQUAL)
203 : : {
204 : 1976 : if (in[0].isVar() && 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 : 1081 : if (!in[0].getType().isSet() || !options().sets.setsExp)
211 : : {
212 : 936 : outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
213 : 936 : status = Theory::PP_ASSERT_STATUS_SOLVED;
214 : : }
215 : : }
216 : 895 : else if (in[1].isVar() && isLegalElimination(in[1], in[0]))
217 : : {
218 : 17 : if (!in[0].getType().isSet() || !options().sets.setsExp)
219 : : {
220 : 0 : outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
221 : 0 : status = Theory::PP_ASSERT_STATUS_SOLVED;
222 : : }
223 : : }
224 : : }
225 : 13696 : return status;
226 : : }
227 : :
228 : 49317 : void TheorySets::presolve() {
229 : 49317 : d_internal->presolve();
230 : 49317 : }
231 : :
232 : 0 : bool TheorySets::isEntailed( Node n, bool pol ) {
233 : 0 : return d_internal->isEntailed( n, pol );
234 : : }
235 : :
236 : 17160 : 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 : 17160 : 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 : 17160 : addCarePairArgs(a, b);
253 : :
254 : 17160 : d_internal->processCarePairArgs(a, b);
255 : : }
256 : :
257 : : /**************************** eq::NotifyClass *****************************/
258 : :
259 : 128222 : void TheorySets::NotifyClass::eqNotifyNewClass(TNode t)
260 : : {
261 [ + - ]: 256444 : Trace("sets-eq") << "[sets-eq] eqNotifyNewClass:"
262 : 128222 : << " t = " << t << std::endl;
263 : 128222 : d_theory.eqNotifyNewClass(t);
264 : 128222 : }
265 : :
266 : 542319 : void TheorySets::NotifyClass::eqNotifyMerge(TNode t1, TNode t2)
267 : : {
268 [ + - ]: 1084640 : Trace("sets-eq") << "[sets-eq] eqNotifyMerge:"
269 : 542319 : << " t1 = " << t1 << " t2 = " << t2 << std::endl;
270 : 542319 : d_theory.eqNotifyMerge(t1, t2);
271 : 542319 : }
272 : :
273 : 100969 : void TheorySets::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
274 : : {
275 [ + - ]: 201938 : Trace("sets-eq") << "[sets-eq] eqNotifyDisequal:"
276 : 0 : << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason
277 : 100969 : << std::endl;
278 : 100969 : d_theory.eqNotifyDisequal(t1, t2, reason);
279 : 100969 : }
280 : :
281 : : } // namespace sets
282 : : } // namespace theory
283 : : } // namespace cvc5::internal
|
