1 /********************* */
2 /*! \file theory_sets_private.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Mudathir Mohamed, Kshitij Bansal
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Sets theory implementation.
14 ** Sets theory implementation.
17 #include "theory/sets/theory_sets_private.h"
21 #include "expr/emptyset.h"
22 #include "expr/node_algorithm.h"
23 #include "options/sets_options.h"
24 #include "smt/smt_statistics_registry.h"
25 #include "theory/sets/normal_form.h"
26 #include "theory/sets/theory_sets.h"
27 #include "theory/theory_model.h"
28 #include "util/result.h"
31 using namespace CVC4::kind
;
37 TheorySetsPrivate::TheorySetsPrivate(TheorySets
& external
,
41 : d_deq(state
.getSatContext()),
42 d_termProcessed(state
.getUserContext()),
43 d_full_check_incomplete(false),
48 d_treg(state
, im
, skc
),
49 d_rels(new TheorySetsRels(state
, im
, skc
, d_treg
)),
50 d_cardSolver(new CardinalityExtension(state
, im
, d_treg
)),
51 d_rels_enabled(false),
54 d_true
= NodeManager::currentNM()->mkConst(true);
55 d_false
= NodeManager::currentNM()->mkConst(false);
56 d_zero
= NodeManager::currentNM()->mkConst(Rational(0));
59 TheorySetsPrivate::~TheorySetsPrivate()
61 for (std::pair
<const Node
, EqcInfo
*>& current_pair
: d_eqc_info
)
63 delete current_pair
.second
;
67 void TheorySetsPrivate::finishInit()
69 d_equalityEngine
= d_external
.getEqualityEngine();
70 Assert(d_equalityEngine
!= nullptr);
73 void TheorySetsPrivate::eqNotifyNewClass(TNode t
)
75 if (t
.getKind() == kind::SINGLETON
|| t
.getKind() == kind::EMPTYSET
)
77 EqcInfo
* e
= getOrMakeEqcInfo(t
, true);
82 void TheorySetsPrivate::eqNotifyMerge(TNode t1
, TNode t2
)
84 if (!d_state
.isInConflict())
86 Trace("sets-prop-debug")
87 << "Merge " << t1
<< " and " << t2
<< "..." << std::endl
;
89 EqcInfo
* e2
= getOrMakeEqcInfo(t2
);
93 EqcInfo
* e1
= getOrMakeEqcInfo(t1
);
94 Trace("sets-prop-debug") << "Merging singletons..." << std::endl
;
98 if (!s1
.isNull() && !s2
.isNull())
100 if (s1
.getKind() == s2
.getKind())
102 Trace("sets-prop") << "Propagate eq inference : " << s1
103 << " == " << s2
<< std::endl
;
104 // infer equality between elements of singleton
105 Node exp
= s1
.eqNode(s2
);
106 Node eq
= s1
[0].eqNode(s2
[0]);
107 d_im
.assertInternalFact(eq
, true, InferenceId::SETS_SINGLETON_EQ
, exp
);
111 // singleton equal to emptyset, conflict
113 << "Propagate conflict : " << s1
<< " == " << s2
<< std::endl
;
114 d_im
.conflictEqConstantMerge(s1
, s2
);
122 e1
= getOrMakeEqcInfo(t1
, true);
123 e1
->d_singleton
.set(e2
->d_singleton
);
126 // merge membership list
127 Trace("sets-prop-debug") << "Copying membership list..." << std::endl
;
128 // if s1 has a singleton or empty set and s2 does not, we may have new
129 // inferences to process.
130 Node checkSingleton
= s2
.isNull() ? s1
: Node::null();
131 std::vector
<Node
> facts
;
132 // merge the membership list in the state, which may produce facts or
133 // conflicts to propagate
134 if (!d_state
.merge(t1
, t2
, facts
, checkSingleton
))
137 Assert(facts
.size() == 1);
138 Trace("sets-prop") << "Propagate eq-mem conflict : " << facts
[0]
140 d_im
.conflict(facts
[0], InferenceId::SETS_EQ_MEM_CONFLICT
);
143 for (const Node
& f
: facts
)
145 Assert(f
.getKind() == kind::IMPLIES
);
146 Trace("sets-prop") << "Propagate eq-mem eq inference : " << f
[0] << " => "
147 << f
[1] << std::endl
;
148 d_im
.assertInternalFact(f
[1], true, InferenceId::SETS_EQ_MEM
, f
[0]);
153 void TheorySetsPrivate::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
)
155 if (t1
.getType().isSet())
157 Node eq
= t1
.eqNode(t2
);
158 if (d_deq
.find(eq
) == d_deq
.end())
165 TheorySetsPrivate::EqcInfo::EqcInfo(context::Context
* c
) : d_singleton(c
) {}
167 TheorySetsPrivate::EqcInfo
* TheorySetsPrivate::getOrMakeEqcInfo(TNode n
,
170 std::map
<Node
, EqcInfo
*>::iterator eqc_i
= d_eqc_info
.find(n
);
171 if (eqc_i
== d_eqc_info
.end())
176 ei
= new EqcInfo(d_external
.getSatContext());
183 return eqc_i
->second
;
187 bool TheorySetsPrivate::areCareDisequal(Node a
, Node b
)
189 if (d_equalityEngine
->isTriggerTerm(a
, THEORY_SETS
)
190 && d_equalityEngine
->isTriggerTerm(b
, THEORY_SETS
))
193 d_equalityEngine
->getTriggerTermRepresentative(a
, THEORY_SETS
);
195 d_equalityEngine
->getTriggerTermRepresentative(b
, THEORY_SETS
);
196 EqualityStatus eqStatus
=
197 d_external
.d_valuation
.getEqualityStatus(a_shared
, b_shared
);
198 if (eqStatus
== EQUALITY_FALSE_AND_PROPAGATED
|| eqStatus
== EQUALITY_FALSE
199 || eqStatus
== EQUALITY_FALSE_IN_MODEL
)
207 void TheorySetsPrivate::fullEffortReset()
209 Assert(d_equalityEngine
->consistent());
210 d_full_check_incomplete
= false;
211 d_most_common_type
.clear();
212 d_most_common_type_term
.clear();
213 d_card_enabled
= false;
214 d_rels_enabled
= false;
215 // reset the state object
217 // reset the inference manager
219 d_im
.clearPendingLemmas();
220 // reset the cardinality solver
221 d_cardSolver
->reset();
224 void TheorySetsPrivate::fullEffortCheck()
226 Trace("sets") << "----- Full effort check ------" << std::endl
;
229 Assert(!d_im
.hasPendingLemma() || d_im
.hasSent());
231 Trace("sets") << "...iterate full effort check..." << std::endl
;
234 Trace("sets-eqc") << "Equality Engine:" << std::endl
;
235 std::map
<TypeNode
, unsigned> eqcTypeCount
;
236 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(d_equalityEngine
);
237 while (!eqcs_i
.isFinished())
239 Node eqc
= (*eqcs_i
);
241 TypeNode tn
= eqc
.getType();
242 d_state
.registerEqc(tn
, eqc
);
244 // common type node and term
250 tnc
= tn
.getSetElementType();
253 Trace("sets-eqc") << "[" << eqc
<< "] : ";
254 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, d_equalityEngine
);
255 while (!eqc_i
.isFinished())
260 Trace("sets-eqc") << n
<< " (" << n
.isConst() << ") ";
262 TypeNode tnn
= n
.getType();
266 TypeNode tnnel
= tnn
.getSetElementType();
267 tnc
= TypeNode::mostCommonTypeNode(tnc
, tnnel
);
268 Assert(!tnc
.isNull());
269 // update the common type term
275 // register it with the state
276 d_state
.registerTerm(eqc
, tnn
, n
);
277 Kind nk
= n
.getKind();
278 if (nk
== kind::SINGLETON
)
280 // ensure the proxy has been introduced
283 else if (nk
== kind::CARD
)
285 d_card_enabled
= true;
286 // register it with the cardinality solver
287 d_cardSolver
->registerTerm(n
);
288 // if we do not handle the kind, set incomplete
289 Kind nk0
= n
[0].getKind();
290 // some kinds of cardinality we cannot handle
291 if (d_rels
->isRelationKind(nk0
))
293 d_full_check_incomplete
= true;
294 Trace("sets-incomplete")
295 << "Sets : incomplete because of " << n
<< "." << std::endl
;
296 // TODO (#1124): The issue can be divided into 4 parts
297 // 1- Supporting the universe cardinality for finite types with
298 // finite cardinality (done)
299 // 2- Supporting the universe cardinality for uninterpreted sorts
300 // with finite-model-find (pending) See the implementation of
301 // CardinalityExtension::checkCardinalityExtended
302 // 3- Supporting the universe cardinality for non-finite types
304 // 4- Supporting cardinality for relations (hard)
307 else if (d_rels
->isRelationKind(nk
))
309 d_rels_enabled
= true;
315 Assert(tnct
.getType().getSetElementType() == tnc
);
316 d_most_common_type
[eqc
] = tnc
;
317 d_most_common_type_term
[eqc
] = tnct
;
319 Trace("sets-eqc") << std::endl
;
323 Trace("sets-eqc") << "...finished equality engine." << std::endl
;
325 if (Trace
.isOn("sets-state"))
327 Trace("sets-state") << "Equivalence class counters:" << std::endl
;
328 for (std::pair
<const TypeNode
, unsigned>& ec
: eqcTypeCount
)
331 << " " << ec
.first
<< " -> " << ec
.second
<< std::endl
;
335 // We may have sent lemmas while registering the terms in the loop above,
336 // e.g. the cardinality solver.
341 if (Trace
.isOn("sets-mem"))
343 const std::vector
<Node
>& sec
= d_state
.getSetsEqClasses();
344 for (const Node
& s
: sec
)
346 Trace("sets-mem") << "Eqc " << s
<< " : ";
347 const std::map
<Node
, Node
>& smem
= d_state
.getMembers(s
);
350 Trace("sets-mem") << "Memberships : ";
351 for (const std::pair
<const Node
, Node
>& it2
: smem
)
353 Trace("sets-mem") << it2
.first
<< " ";
356 Node ss
= d_state
.getSingletonEqClass(s
);
359 Trace("sets-mem") << " : Singleton : " << ss
;
361 Trace("sets-mem") << std::endl
;
364 d_im
.doPendingLemmas();
369 // check downwards closure
370 checkDownwardsClosure();
371 d_im
.doPendingLemmas();
376 // check upwards closure
377 checkUpwardsClosure();
378 d_im
.doPendingLemmas();
383 // check disequalities
384 checkDisequalities();
385 d_im
.doPendingLemmas();
390 // check reduce comprehensions
391 checkReduceComprehensions();
393 d_im
.doPendingLemmas();
400 // call the check method of the cardinality solver
401 d_cardSolver
->check();
409 // call the check method of the relations solver
410 d_rels
->check(Theory::EFFORT_FULL
);
412 } while (!d_im
.hasSentLemma() && !d_state
.isInConflict()
413 && d_im
.hasSentFact());
414 Assert(!d_im
.hasPendingLemma() || d_im
.hasSent());
415 Trace("sets") << "----- End full effort check, conflict="
416 << d_state
.isInConflict() << ", lemma=" << d_im
.hasSentLemma()
420 void TheorySetsPrivate::checkDownwardsClosure()
422 Trace("sets") << "TheorySetsPrivate: check downwards closure..." << std::endl
;
424 const std::vector
<Node
>& sec
= d_state
.getSetsEqClasses();
425 for (const Node
& s
: sec
)
427 const std::vector
<Node
>& nvsets
= d_state
.getNonVariableSets(s
);
430 const std::map
<Node
, Node
>& smem
= d_state
.getMembers(s
);
431 for (const Node
& nv
: nvsets
)
433 if (!d_state
.isCongruent(nv
))
435 for (const std::pair
<const Node
, Node
>& it2
: smem
)
437 Node mem
= it2
.second
;
439 Assert(d_equalityEngine
->areEqual(mem
[1], eq_set
));
440 if (mem
[1] != eq_set
)
442 Trace("sets-debug") << "Downwards closure based on " << mem
443 << ", eq_set = " << eq_set
<< std::endl
;
444 if (!options::setsProxyLemmas())
446 Node nmem
= NodeManager::currentNM()->mkNode(
447 kind::MEMBER
, mem
[0], eq_set
);
448 nmem
= Rewriter::rewrite(nmem
);
449 std::vector
<Node
> exp
;
451 exp
.push_back(mem
[1].eqNode(eq_set
));
452 d_im
.assertInference(nmem
, InferenceId::SETS_DOWN_CLOSURE
, exp
);
453 if (d_state
.isInConflict())
461 Node k
= d_treg
.getProxy(eq_set
);
463 NodeManager::currentNM()->mkNode(kind::MEMBER
, mem
[0], k
);
464 Node nmem
= NodeManager::currentNM()->mkNode(
465 kind::MEMBER
, mem
[0], eq_set
);
466 nmem
= Rewriter::rewrite(nmem
);
467 std::vector
<Node
> exp
;
468 if (d_state
.areEqual(mem
, pmem
))
474 nmem
= NodeManager::currentNM()->mkNode(
475 kind::OR
, pmem
.negate(), nmem
);
477 d_im
.assertInference(nmem
, InferenceId::SETS_DOWN_CLOSURE
, exp
);
487 void TheorySetsPrivate::checkUpwardsClosure()
490 NodeManager
* nm
= NodeManager::currentNM();
491 const std::map
<Kind
, std::map
<Node
, std::map
<Node
, Node
> > >& boi
=
492 d_state
.getBinaryOpIndex();
493 for (const std::pair
<const Kind
, std::map
<Node
, std::map
<Node
, Node
> > >&
497 Trace("sets") << "TheorySetsPrivate: check upwards closure " << k
<< "..."
499 for (const std::pair
<const Node
, std::map
<Node
, Node
> >& it
: itb
.second
)
502 // see if there are members in first argument r1
503 const std::map
<Node
, Node
>& r1mem
= d_state
.getMembers(r1
);
504 if (!r1mem
.empty() || k
== kind::UNION
)
506 for (const std::pair
<const Node
, Node
>& it2
: it
.second
)
509 Node term
= it2
.second
;
510 // see if there are members in second argument
511 const std::map
<Node
, Node
>& r2mem
= d_state
.getMembers(r2
);
512 const std::map
<Node
, Node
>& r2nmem
= d_state
.getNegativeMembers(r2
);
513 if (!r2mem
.empty() || k
!= kind::INTERSECTION
)
516 << "Checking " << term
<< ", members = " << (!r1mem
.empty())
517 << ", " << (!r2mem
.empty()) << std::endl
;
518 // for all members of r1
521 for (const std::pair
<const Node
, Node
>& itm1m
: r1mem
)
523 Node xr
= itm1m
.first
;
524 Node x
= itm1m
.second
[0];
525 Trace("sets-debug") << "checking membership " << xr
<< " "
526 << itm1m
.second
<< std::endl
;
527 std::vector
<Node
> exp
;
528 exp
.push_back(itm1m
.second
);
529 d_state
.addEqualityToExp(term
[0], itm1m
.second
[1], exp
);
532 if (k
== kind::UNION
)
536 else if (k
== kind::INTERSECTION
)
538 // conclude x is in term
539 // if also existing in members of r2
540 std::map
<Node
, Node
>::const_iterator itm
= r2mem
.find(xr
);
541 if (itm
!= r2mem
.end())
543 exp
.push_back(itm
->second
);
544 d_state
.addEqualityToExp(term
[1], itm
->second
[1], exp
);
545 d_state
.addEqualityToExp(x
, itm
->second
[0], exp
);
550 // if not, check whether it is definitely not a member, if
552 if (r2nmem
.find(xr
) == r2nmem
.end())
554 exp
.push_back(nm
->mkNode(kind::MEMBER
, x
, term
[1]));
562 Assert(k
== kind::SETMINUS
);
563 std::map
<Node
, Node
>::const_iterator itm
= r2mem
.find(xr
);
564 if (itm
== r2mem
.end())
566 // must add lemma for set minus since non-membership in this
567 // case is not explained
569 nm
->mkNode(kind::MEMBER
, x
, term
[1]).negate());
576 Node rr
= d_equalityEngine
->getRepresentative(term
);
577 if (!d_state
.isMember(x
, rr
))
579 Node kk
= d_treg
.getProxy(term
);
580 Node fact
= nm
->mkNode(kind::MEMBER
, x
, kk
);
581 d_im
.assertInference(
582 fact
, InferenceId::SETS_UP_CLOSURE
, exp
, inferType
);
583 if (d_state
.isInConflict())
589 Trace("sets-debug") << "done checking membership " << xr
<< " "
590 << itm1m
.second
<< std::endl
;
593 if (k
== kind::UNION
)
597 // for all members of r2
598 for (const std::pair
<const Node
, Node
>& itm2m
: r2mem
)
600 Node x
= itm2m
.second
[0];
601 Node rr
= d_equalityEngine
->getRepresentative(term
);
602 if (!d_state
.isMember(x
, rr
))
604 std::vector
<Node
> exp
;
605 exp
.push_back(itm2m
.second
);
606 d_state
.addEqualityToExp(term
[1], itm2m
.second
[1], exp
);
607 Node r
= d_treg
.getProxy(term
);
608 Node fact
= nm
->mkNode(kind::MEMBER
, x
, r
);
609 d_im
.assertInference(fact
, InferenceId::SETS_UP_CLOSURE_2
, exp
);
610 if (d_state
.isInConflict())
625 if (options::setsExt())
628 Trace("sets-debug") << "Check universe sets..." << std::endl
;
629 // all elements must be in universal set
630 const std::vector
<Node
>& sec
= d_state
.getSetsEqClasses();
631 for (const Node
& s
: sec
)
633 // if equivalence class contains a variable
634 Node v
= d_state
.getVariableSet(s
);
637 // the variable in the equivalence class
638 std::map
<TypeNode
, Node
> univ_set
;
639 const std::map
<Node
, Node
>& smems
= d_state
.getMembers(s
);
640 for (const std::pair
<const Node
, Node
>& it2
: smems
)
642 Node e
= it2
.second
[0];
643 TypeNode tn
= NodeManager::currentNM()->mkSetType(e
.getType());
645 std::map
<TypeNode
, Node
>::iterator itu
= univ_set
.find(tn
);
646 if (itu
== univ_set
.end())
648 Node ueqc
= d_state
.getUnivSetEqClass(tn
);
649 // if the universe does not yet exist, or is not in this
653 u
= d_treg
.getUnivSet(tn
);
663 Assert(it2
.second
.getKind() == kind::MEMBER
);
664 std::vector
<Node
> exp
;
665 exp
.push_back(it2
.second
);
666 if (v
!= it2
.second
[1])
668 exp
.push_back(v
.eqNode(it2
.second
[1]));
670 Node fact
= nm
->mkNode(kind::MEMBER
, it2
.second
[0], u
);
671 d_im
.assertInference(fact
, InferenceId::SETS_UP_UNIV
, exp
);
672 if (d_state
.isInConflict())
684 void TheorySetsPrivate::checkDisequalities()
687 Trace("sets") << "TheorySetsPrivate: check disequalities..." << std::endl
;
688 NodeManager
* nm
= NodeManager::currentNM();
689 for (NodeBoolMap::const_iterator it
= d_deq
.begin(); it
!= d_deq
.end(); ++it
)
696 Node deq
= (*it
).first
;
697 // check if it is already satisfied
698 Assert(d_equalityEngine
->hasTerm(deq
[0])
699 && d_equalityEngine
->hasTerm(deq
[1]));
700 Node r1
= d_equalityEngine
->getRepresentative(deq
[0]);
701 Node r2
= d_equalityEngine
->getRepresentative(deq
[1]);
702 bool is_sat
= d_state
.isSetDisequalityEntailed(r1
, r2
);
703 Trace("sets-debug") << "Check disequality " << deq
704 << ", is_sat = " << is_sat
<< std::endl
;
705 // will process regardless of sat/processed/unprocessed
713 if (d_termProcessed
.find(deq
) != d_termProcessed
.end())
715 // already added lemma
718 d_termProcessed
.insert(deq
);
719 d_termProcessed
.insert(deq
[1].eqNode(deq
[0]));
720 Trace("sets") << "Process Disequality : " << deq
.negate() << std::endl
;
721 TypeNode elementType
= deq
[0].getType().getSetElementType();
722 Node x
= d_skCache
.mkTypedSkolemCached(
723 elementType
, deq
[0], deq
[1], SkolemCache::SK_DISEQUAL
, "sde");
724 Node mem1
= nm
->mkNode(MEMBER
, x
, deq
[0]);
725 Node mem2
= nm
->mkNode(MEMBER
, x
, deq
[1]);
726 Node lem
= nm
->mkNode(OR
, deq
, nm
->mkNode(EQUAL
, mem1
, mem2
).negate());
727 lem
= Rewriter::rewrite(lem
);
728 d_im
.assertInference(lem
, InferenceId::SETS_DEQ
, d_true
, 1);
729 d_im
.doPendingLemmas();
737 void TheorySetsPrivate::checkReduceComprehensions()
739 NodeManager
* nm
= NodeManager::currentNM();
740 const std::vector
<Node
>& comps
= d_state
.getComprehensionSets();
741 for (const Node
& n
: comps
)
743 if (d_termProcessed
.find(n
) != d_termProcessed
.end())
745 // already reduced it
748 d_termProcessed
.insert(n
);
749 Node v
= nm
->mkBoundVar(n
[2].getType());
750 Node body
= nm
->mkNode(AND
, n
[1], v
.eqNode(n
[2]));
751 // must do substitution
752 std::vector
<Node
> vars
;
753 std::vector
<Node
> subs
;
754 for (const Node
& cv
: n
[0])
757 Node cvs
= nm
->mkBoundVar(cv
.getType());
760 body
= body
.substitute(vars
.begin(), vars
.end(), subs
.begin(), subs
.end());
761 Node bvl
= nm
->mkNode(BOUND_VAR_LIST
, subs
);
762 body
= nm
->mkNode(EXISTS
, bvl
, body
);
763 Node mem
= nm
->mkNode(MEMBER
, v
, n
);
765 nm
->mkNode(FORALL
, nm
->mkNode(BOUND_VAR_LIST
, v
), body
.eqNode(mem
));
766 Trace("sets-comprehension")
767 << "Comprehension reduction: " << lem
<< std::endl
;
768 d_im
.lemma(lem
, InferenceId::SETS_COMPREHENSION
);
772 //--------------------------------- standard check
774 void TheorySetsPrivate::postCheck(Theory::Effort level
)
776 Trace("sets-check") << "Sets finished assertions effort " << level
778 // invoke full effort check, relations check
779 if (!d_state
.isInConflict())
781 if (level
== Theory::EFFORT_FULL
)
783 if (!d_external
.d_valuation
.needCheck())
786 if (!d_state
.isInConflict() && !d_im
.hasSentLemma()
787 && d_full_check_incomplete
)
789 d_im
.setIncomplete();
794 Trace("sets-check") << "Sets finish Check effort " << level
<< std::endl
;
797 void TheorySetsPrivate::notifyFact(TNode atom
, bool polarity
, TNode fact
)
799 if (d_state
.isInConflict())
803 if (atom
.getKind() == kind::MEMBER
&& polarity
)
805 // check if set has a value, if so, we can propagate
806 Node r
= d_equalityEngine
->getRepresentative(atom
[1]);
807 EqcInfo
* e
= getOrMakeEqcInfo(r
, true);
810 Node s
= e
->d_singleton
;
813 Node pexp
= NodeManager::currentNM()->mkNode(
814 kind::AND
, atom
, atom
[1].eqNode(s
));
815 if (s
.getKind() == kind::SINGLETON
)
819 Trace("sets-prop") << "Propagate mem-eq : " << pexp
<< std::endl
;
820 Node eq
= s
[0].eqNode(atom
[0]);
821 // triggers an internal inference
822 d_im
.assertInternalFact(eq
, true, InferenceId::SETS_MEM_EQ
, pexp
);
828 << "Propagate mem-eq conflict : " << pexp
<< std::endl
;
829 d_im
.conflict(pexp
, InferenceId::SETS_MEM_EQ_CONFLICT
);
833 // add to membership list
834 d_state
.addMember(r
, atom
);
837 //--------------------------------- end standard check
839 /************************ Sharing ************************/
840 /************************ Sharing ************************/
841 /************************ Sharing ************************/
843 void TheorySetsPrivate::addCarePairs(TNodeTrie
* t1
,
853 Node f1
= t1
->getData();
854 Node f2
= t2
->getData();
856 // Usually when (= (f x) (f y)), we don't care whether (= x y) is true or
857 // not for the shared variables x, y in the care graph.
858 // However, this does not apply to the membership operator since the
859 // equality or disequality between members affects the number of elements
860 // in a set. Therefore we need to split on (= x y) for kind MEMBER.
862 // Suppose (= (member x S) member( y, S)) is true and there are
863 // no other members in S. We would get S = {x} if (= x y) is true.
864 // Otherwise we would get S = {x, y}.
865 if (f1
.getKind() == MEMBER
|| !d_state
.areEqual(f1
, f2
))
867 Trace("sets-cg") << "Check " << f1
<< " and " << f2
<< std::endl
;
868 vector
<pair
<TNode
, TNode
> > currentPairs
;
869 for (unsigned k
= 0; k
< f1
.getNumChildren(); ++k
)
873 Assert(d_equalityEngine
->hasTerm(x
));
874 Assert(d_equalityEngine
->hasTerm(y
));
875 Assert(!d_state
.areDisequal(x
, y
));
876 Assert(!areCareDisequal(x
, y
));
877 if (!d_equalityEngine
->areEqual(x
, y
))
880 << "Arg #" << k
<< " is " << x
<< " " << y
<< std::endl
;
881 if (d_equalityEngine
->isTriggerTerm(x
, THEORY_SETS
)
882 && d_equalityEngine
->isTriggerTerm(y
, THEORY_SETS
))
884 TNode x_shared
= d_equalityEngine
->getTriggerTermRepresentative(
886 TNode y_shared
= d_equalityEngine
->getTriggerTermRepresentative(
888 currentPairs
.push_back(make_pair(x_shared
, y_shared
));
890 else if (isCareArg(f1
, k
) && isCareArg(f2
, k
))
892 // splitting on sets (necessary for handling set of sets properly)
893 if (x
.getType().isSet())
895 Assert(y
.getType().isSet());
896 if (!d_state
.areDisequal(x
, y
))
898 Trace("sets-cg-lemma")
899 << "Should split on : " << x
<< "==" << y
<< std::endl
;
900 d_im
.split(x
.eqNode(y
), InferenceId::UNKNOWN
);
906 for (unsigned c
= 0; c
< currentPairs
.size(); ++c
)
908 Trace("sets-cg-pair") << "Pair : " << currentPairs
[c
].first
<< " "
909 << currentPairs
[c
].second
<< std::endl
;
910 d_external
.addCarePair(currentPairs
[c
].first
, currentPairs
[c
].second
);
920 if (depth
< (arity
- 1))
922 // add care pairs internal to each child
923 for (std::pair
<const TNode
, TNodeTrie
>& t
: t1
->d_data
)
925 addCarePairs(&t
.second
, NULL
, arity
, depth
+ 1, n_pairs
);
928 // add care pairs based on each pair of non-disequal arguments
929 for (std::map
<TNode
, TNodeTrie
>::iterator it
= t1
->d_data
.begin();
930 it
!= t1
->d_data
.end();
933 std::map
<TNode
, TNodeTrie
>::iterator it2
= it
;
935 for (; it2
!= t1
->d_data
.end(); ++it2
)
937 if (!d_equalityEngine
->areDisequal(it
->first
, it2
->first
, false))
939 if (!areCareDisequal(it
->first
, it2
->first
))
942 &it
->second
, &it2
->second
, arity
, depth
+ 1, n_pairs
);
950 // add care pairs based on product of indices, non-disequal arguments
951 for (std::pair
<const TNode
, TNodeTrie
>& tt1
: t1
->d_data
)
953 for (std::pair
<const TNode
, TNodeTrie
>& tt2
: t2
->d_data
)
955 if (!d_equalityEngine
->areDisequal(tt1
.first
, tt2
.first
, false))
957 if (!areCareDisequal(tt1
.first
, tt2
.first
))
959 addCarePairs(&tt1
.second
, &tt2
.second
, arity
, depth
+ 1, n_pairs
);
968 void TheorySetsPrivate::computeCareGraph()
970 const std::map
<Kind
, std::vector
<Node
> >& ol
= d_state
.getOperatorList();
971 for (const std::pair
<const Kind
, std::vector
<Node
> >& it
: ol
)
974 if (k
== kind::SINGLETON
|| k
== kind::MEMBER
)
976 unsigned n_pairs
= 0;
977 Trace("sets-cg-summary") << "Compute graph for sets, op=" << k
<< "..."
978 << it
.second
.size() << std::endl
;
979 Trace("sets-cg") << "Build index for " << k
<< "..." << std::endl
;
980 std::map
<TypeNode
, TNodeTrie
> index
;
983 for (TNode f1
: it
.second
)
985 Trace("sets-cg-debug") << "...build for " << f1
<< std::endl
;
986 Assert(d_equalityEngine
->hasTerm(f1
));
987 // break into index based on operator, and type of first argument (since
988 // some operators are parametric)
989 TypeNode tn
= f1
[0].getType();
990 std::vector
<TNode
> reps
;
991 bool hasCareArg
= false;
992 for (unsigned j
= 0; j
< f1
.getNumChildren(); j
++)
994 reps
.push_back(d_equalityEngine
->getRepresentative(f1
[j
]));
995 if (isCareArg(f1
, j
))
1002 Trace("sets-cg-debug") << "......adding." << std::endl
;
1003 index
[tn
].addTerm(f1
, reps
);
1004 arity
= reps
.size();
1008 Trace("sets-cg-debug") << "......skip." << std::endl
;
1014 for (std::pair
<const TypeNode
, TNodeTrie
>& tt
: index
)
1016 Trace("sets-cg") << "Process index " << tt
.first
<< "..."
1018 addCarePairs(&tt
.second
, nullptr, arity
, 0, n_pairs
);
1021 Trace("sets-cg-summary") << "...done, # pairs = " << n_pairs
<< std::endl
;
1026 bool TheorySetsPrivate::isCareArg(Node n
, unsigned a
)
1028 if (d_equalityEngine
->isTriggerTerm(n
[a
], THEORY_SETS
))
1032 else if ((n
.getKind() == kind::MEMBER
|| n
.getKind() == kind::SINGLETON
)
1033 && a
== 0 && n
[0].getType().isSet())
1043 /******************** Model generation ********************/
1044 /******************** Model generation ********************/
1045 /******************** Model generation ********************/
1049 * This function is a helper function to print sets as
1050 * Set A = { a0, a1, a2, }
1052 * (union (singleton a0) (union (singleton a1) (singleton a2)))
1054 void traceSetElementsRecursively(stringstream
& stream
, const Node
& set
)
1056 Assert(set
.getType().isSet());
1057 if (set
.getKind() == SINGLETON
)
1059 stream
<< set
[0] << ", ";
1061 if (set
.getKind() == UNION
)
1063 traceSetElementsRecursively(stream
, set
[0]);
1064 traceSetElementsRecursively(stream
, set
[1]);
1068 std::string
traceElements(const Node
& set
)
1070 std::stringstream stream
;
1071 traceSetElementsRecursively(stream
, set
);
1072 return stream
.str();
1077 bool TheorySetsPrivate::collectModelValues(TheoryModel
* m
,
1078 const std::set
<Node
>& termSet
)
1080 Trace("sets-model") << "Set collect model values" << std::endl
;
1082 NodeManager
* nm
= NodeManager::currentNM();
1083 std::map
<Node
, Node
> mvals
;
1084 // If cardinality is enabled, we need to use the ordered equivalence class
1085 // list computed by the cardinality solver, where sets equivalence classes
1086 // are assigned model values based on their position in the cardinality
1088 const std::vector
<Node
>& sec
= d_card_enabled
1089 ? d_cardSolver
->getOrderedSetsEqClasses()
1090 : d_state
.getSetsEqClasses();
1091 Valuation
& val
= getValuation();
1092 for (int i
= (int)(sec
.size() - 1); i
>= 0; i
--)
1095 if (termSet
.find(eqc
) == termSet
.end())
1097 Trace("sets-model") << "* Do not assign value for " << eqc
1098 << " since is not relevant." << std::endl
;
1102 std::vector
<Node
> els
;
1103 bool is_base
= !d_card_enabled
|| d_cardSolver
->isModelValueBasic(eqc
);
1107 << "Collect elements of base eqc " << eqc
<< std::endl
;
1108 // members that must be in eqc
1109 const std::map
<Node
, Node
>& emems
= d_state
.getMembers(eqc
);
1112 TypeNode elementType
= eqc
.getType().getSetElementType();
1113 for (const std::pair
<const Node
, Node
>& itmm
: emems
)
1116 << "m->getRepresentative(" << itmm
.first
1117 << ")= " << m
->getRepresentative(itmm
.first
) << std::endl
;
1118 Node t
= nm
->mkSingleton(elementType
, itmm
.first
);
1125 // make the slack elements for the equivalence class based on set
1127 d_cardSolver
->mkModelValueElementsFor(val
, eqc
, els
, mvals
, m
);
1130 Node rep
= NormalForm::mkBop(kind::UNION
, els
, eqc
.getType());
1131 rep
= Rewriter::rewrite(rep
);
1132 Trace("sets-model") << "* Assign representative of " << eqc
<< " to "
1133 << rep
<< std::endl
;
1135 if (!m
->assertEquality(eqc
, rep
, true))
1139 m
->assertSkeleton(rep
);
1141 // we add the element terms (singletons) as representatives to tell the
1142 // model builder to evaluate them along with their union (rep).
1143 // This is needed to account for cases when members and rep are not enough
1144 // for the model builder to evaluate set terms.
1146 // eqc(rep) = [(union (singleton skolem) (singleton 0))]
1147 // eqc(skolem) = [0]
1148 // The model builder would fail to evaluate rep as (singleton 0)
1149 // if (singleton skolem) is not registered as a representative in the
1151 for (const Node
& el
: els
)
1153 m
->assertSkeleton(el
);
1156 Trace("sets-model") << "Set " << eqc
<< " = { " << traceElements(rep
)
1157 << " }" << std::endl
;
1161 // handle slack elements constraints for finite types
1164 const std::map
<TypeNode
, std::vector
<TNode
> >& slackElements
=
1165 d_cardSolver
->getFiniteTypeSlackElements();
1166 for (const auto& pair
: slackElements
)
1168 const std::vector
<Node
>& members
=
1169 d_cardSolver
->getFiniteTypeMembers(pair
.first
);
1170 m
->setAssignmentExclusionSetGroup(pair
.second
, members
);
1171 Trace("sets-model") << "ExclusionSet: Group " << pair
.second
1172 << " is excluded from set" << members
<< std::endl
;
1178 /********************** Helper functions ***************************/
1179 /********************** Helper functions ***************************/
1180 /********************** Helper functions ***************************/
1182 Node
mkAnd(const std::vector
<TNode
>& conjunctions
)
1184 Assert(conjunctions
.size() > 0);
1186 std::set
<TNode
> all
;
1187 for (unsigned i
= 0; i
< conjunctions
.size(); ++i
)
1189 TNode t
= conjunctions
[i
];
1190 if (t
.getKind() == kind::AND
)
1192 for (TNode::iterator child_it
= t
.begin(); child_it
!= t
.end();
1195 Assert((*child_it
).getKind() != kind::AND
);
1196 all
.insert(*child_it
);
1205 Assert(all
.size() > 0);
1206 if (all
.size() == 1)
1208 // All the same, or just one
1209 return conjunctions
[0];
1212 NodeBuilder
<> conjunction(kind::AND
);
1213 std::set
<TNode
>::const_iterator it
= all
.begin();
1214 std::set
<TNode
>::const_iterator it_end
= all
.end();
1215 while (it
!= it_end
)
1223 Valuation
& TheorySetsPrivate::getValuation() { return d_external
.d_valuation
; }
1225 Node
TheorySetsPrivate::explain(TNode literal
)
1227 Debug("sets") << "TheorySetsPrivate::explain(" << literal
<< ")" << std::endl
;
1229 bool polarity
= literal
.getKind() != kind::NOT
;
1230 TNode atom
= polarity
? literal
: literal
[0];
1231 std::vector
<TNode
> assumptions
;
1233 if (atom
.getKind() == kind::EQUAL
)
1235 d_equalityEngine
->explainEquality(atom
[0], atom
[1], polarity
, assumptions
);
1237 else if (atom
.getKind() == kind::MEMBER
)
1239 d_equalityEngine
->explainPredicate(atom
, polarity
, assumptions
);
1243 Debug("sets") << "unhandled: " << literal
<< "; (" << atom
<< ", "
1244 << polarity
<< "); kind" << atom
.getKind() << std::endl
;
1248 return mkAnd(assumptions
);
1251 void TheorySetsPrivate::preRegisterTerm(TNode node
)
1253 Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node
<< ")"
1255 switch (node
.getKind())
1260 // add trigger predicate for equality and membership
1261 d_equalityEngine
->addTriggerPredicate(node
);
1264 default: d_equalityEngine
->addTerm(node
); break;
1268 TrustNode
TheorySetsPrivate::expandDefinition(Node node
)
1270 Debug("sets-proc") << "expandDefinition : " << node
<< std::endl
;
1272 if (node
.getKind()==kind::CHOOSE
)
1274 return expandChooseOperator(node
);
1276 return TrustNode::null();
1279 TrustNode
TheorySetsPrivate::ppRewrite(Node node
)
1281 Debug("sets-proc") << "ppRewrite : " << node
<< std::endl
;
1283 switch (node
.getKind())
1285 case kind::CHOOSE
: return expandChooseOperator(node
);
1286 case kind::IS_SINGLETON
: return expandIsSingletonOperator(node
);
1287 default: return TrustNode::null();
1291 TrustNode
TheorySetsPrivate::expandChooseOperator(const Node
& node
)
1293 Assert(node
.getKind() == CHOOSE
);
1295 // we call the rewriter here to handle the pattern (choose (singleton x))
1296 // because the rewriter is called after expansion
1297 Node rewritten
= Rewriter::rewrite(node
);
1298 if (rewritten
.getKind() != CHOOSE
)
1300 return TrustNode::mkTrustRewrite(node
, rewritten
, nullptr);
1303 // (choose A) is expanded as
1304 // (witness ((x elementType))
1306 // (= A (as emptyset setType))
1307 // (= x chooseUf(A))
1308 // (and (member x A) (= x chooseUf(A)))
1310 NodeManager
* nm
= NodeManager::currentNM();
1311 Node set
= rewritten
[0];
1312 TypeNode setType
= set
.getType();
1313 Node chooseSkolem
= getChooseFunction(setType
);
1314 Node apply
= NodeManager::currentNM()->mkNode(APPLY_UF
, chooseSkolem
, set
);
1316 Node witnessVariable
= nm
->mkBoundVar(setType
.getSetElementType());
1318 Node equal
= witnessVariable
.eqNode(apply
);
1319 Node emptySet
= nm
->mkConst(EmptySet(setType
));
1320 Node isEmpty
= set
.eqNode(emptySet
);
1321 Node member
= nm
->mkNode(MEMBER
, witnessVariable
, set
);
1322 Node memberAndEqual
= member
.andNode(equal
);
1323 Node ite
= nm
->mkNode(ITE
, isEmpty
, equal
, memberAndEqual
);
1324 Node witnessVariables
= nm
->mkNode(BOUND_VAR_LIST
, witnessVariable
);
1325 Node witness
= nm
->mkNode(WITNESS
, witnessVariables
, ite
);
1326 return TrustNode::mkTrustRewrite(node
, witness
, nullptr);
1329 TrustNode
TheorySetsPrivate::expandIsSingletonOperator(const Node
& node
)
1331 Assert(node
.getKind() == IS_SINGLETON
);
1333 // we call the rewriter here to handle the pattern
1334 // (is_singleton (singleton x)) because the rewriter is called after expansion
1335 Node rewritten
= Rewriter::rewrite(node
);
1336 if (rewritten
.getKind() != IS_SINGLETON
)
1338 return TrustNode::mkTrustRewrite(node
, rewritten
, nullptr);
1341 // (is_singleton A) is expanded as
1342 // (exists ((x: T)) (= A (singleton x)))
1343 // where T is the sort of elements of A
1345 NodeManager
* nm
= NodeManager::currentNM();
1346 Node set
= rewritten
[0];
1348 std::map
<Node
, Node
>::iterator it
= d_isSingletonNodes
.find(rewritten
);
1350 if (it
!= d_isSingletonNodes
.end())
1352 return TrustNode::mkTrustRewrite(rewritten
, it
->second
, nullptr);
1355 TypeNode setType
= set
.getType();
1356 Node boundVar
= nm
->mkBoundVar(setType
.getSetElementType());
1357 Node singleton
= nm
->mkSingleton(setType
.getSetElementType(), boundVar
);
1358 Node equal
= set
.eqNode(singleton
);
1359 std::vector
<Node
> variables
= {boundVar
};
1360 Node boundVars
= nm
->mkNode(BOUND_VAR_LIST
, variables
);
1361 Node exists
= nm
->mkNode(kind::EXISTS
, boundVars
, equal
);
1362 d_isSingletonNodes
[rewritten
] = exists
;
1364 return TrustNode::mkTrustRewrite(node
, exists
, nullptr);
1367 Node
TheorySetsPrivate::getChooseFunction(const TypeNode
& setType
)
1369 std::map
<TypeNode
, Node
>::iterator it
= d_chooseFunctions
.find(setType
);
1370 if (it
!= d_chooseFunctions
.end())
1375 NodeManager
* nm
= NodeManager::currentNM();
1376 TypeNode chooseUf
= nm
->mkFunctionType(setType
, setType
.getSetElementType());
1377 stringstream stream
;
1378 stream
<< "chooseUf" << setType
.getId();
1379 string name
= stream
.str();
1380 Node chooseSkolem
= nm
->mkSkolem(
1381 name
, chooseUf
, "choose function", NodeManager::SKOLEM_EXACT_NAME
);
1382 d_chooseFunctions
[setType
] = chooseSkolem
;
1383 return chooseSkolem
;
1386 void TheorySetsPrivate::presolve() { d_state
.reset(); }
1389 } // namespace theory