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
,
39 context::UserContext
* u
,
45 d_full_check_incomplete(false),
47 d_state(*this, c
, u
, valuation
),
48 d_im(*this, d_state
, c
, u
),
49 d_rels(new TheorySetsRels(d_state
, d_im
, u
)),
50 d_cardSolver(new CardinalityExtension(d_state
, d_im
, c
, u
)),
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]);
113 // singleton equal to emptyset, conflict
115 << "Propagate conflict : " << s1
<< " == " << s2
<< std::endl
;
124 e1
= getOrMakeEqcInfo(t1
, true);
125 e1
->d_singleton
.set(e2
->d_singleton
);
128 // merge membership list
129 Trace("sets-prop-debug") << "Copying membership list..." << std::endl
;
130 NodeIntMap::iterator mem_i2
= d_members
.find(t2
);
131 if (mem_i2
!= d_members
.end())
133 NodeIntMap::iterator mem_i1
= d_members
.find(t1
);
135 if (mem_i1
!= d_members
.end())
137 n_members
= (*mem_i1
).second
;
139 for (int i
= 0; i
< (*mem_i2
).second
; i
++)
141 Assert(i
< (int)d_members_data
[t2
].size()
142 && d_members_data
[t2
][i
].getKind() == kind::MEMBER
);
143 Node m2
= d_members_data
[t2
][i
];
144 // check if redundant
146 for (int j
= 0; j
< n_members
; j
++)
148 Assert(j
< (int)d_members_data
[t1
].size()
149 && d_members_data
[t1
][j
].getKind() == kind::MEMBER
);
150 if (d_state
.areEqual(m2
[0], d_members_data
[t1
][j
][0]))
158 if (!s1
.isNull() && s2
.isNull())
160 Assert(m2
[1].getType().isComparableTo(s1
.getType()));
161 Assert(d_state
.areEqual(m2
[1], s1
));
162 Node exp
= NodeManager::currentNM()->mkNode(
163 kind::AND
, m2
[1].eqNode(s1
), m2
);
164 if (s1
.getKind() == kind::SINGLETON
)
168 Node eq
= s1
[0].eqNode(m2
[0]);
171 Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp
172 << " => " << eq
<< std::endl
;
180 << "Propagate eq-mem conflict : " << exp
<< std::endl
;
185 if (n_members
< (int)d_members_data
[t1
].size())
187 d_members_data
[t1
][n_members
] = m2
;
191 d_members_data
[t1
].push_back(m2
);
196 d_members
[t1
] = n_members
;
201 void TheorySetsPrivate::eqNotifyDisequal(TNode t1
, TNode t2
, TNode reason
)
203 if (t1
.getType().isSet())
205 Node eq
= t1
.eqNode(t2
);
206 if (d_deq
.find(eq
) == d_deq
.end())
213 TheorySetsPrivate::EqcInfo::EqcInfo(context::Context
* c
) : d_singleton(c
) {}
215 TheorySetsPrivate::EqcInfo
* TheorySetsPrivate::getOrMakeEqcInfo(TNode n
,
218 std::map
<Node
, EqcInfo
*>::iterator eqc_i
= d_eqc_info
.find(n
);
219 if (eqc_i
== d_eqc_info
.end())
224 ei
= new EqcInfo(d_external
.getSatContext());
231 return eqc_i
->second
;
235 bool TheorySetsPrivate::areCareDisequal(Node a
, Node b
)
237 if (d_equalityEngine
->isTriggerTerm(a
, THEORY_SETS
)
238 && d_equalityEngine
->isTriggerTerm(b
, THEORY_SETS
))
241 d_equalityEngine
->getTriggerTermRepresentative(a
, THEORY_SETS
);
243 d_equalityEngine
->getTriggerTermRepresentative(b
, THEORY_SETS
);
244 EqualityStatus eqStatus
=
245 d_external
.d_valuation
.getEqualityStatus(a_shared
, b_shared
);
246 if (eqStatus
== EQUALITY_FALSE_AND_PROPAGATED
|| eqStatus
== EQUALITY_FALSE
247 || eqStatus
== EQUALITY_FALSE_IN_MODEL
)
255 bool TheorySetsPrivate::isMember(Node x
, Node s
)
257 Assert(d_equalityEngine
->hasTerm(s
)
258 && d_equalityEngine
->getRepresentative(s
) == s
);
259 NodeIntMap::iterator mem_i
= d_members
.find(s
);
260 if (mem_i
!= d_members
.end())
262 for (int i
= 0; i
< (*mem_i
).second
; i
++)
264 if (d_state
.areEqual(d_members_data
[s
][i
][0], x
))
273 bool TheorySetsPrivate::assertFact(Node fact
, Node exp
)
275 Trace("sets-assert") << "TheorySets::assertFact : " << fact
276 << ", exp = " << exp
<< std::endl
;
277 bool polarity
= fact
.getKind() != kind::NOT
;
278 TNode atom
= polarity
? fact
: fact
[0];
279 if (!d_state
.isEntailed(atom
, polarity
))
281 if (atom
.getKind() == kind::EQUAL
)
283 d_equalityEngine
->assertEquality(atom
, polarity
, exp
);
287 d_equalityEngine
->assertPredicate(atom
, polarity
, exp
);
289 if (!d_state
.isInConflict())
291 if (atom
.getKind() == kind::MEMBER
&& polarity
)
293 // check if set has a value, if so, we can propagate
294 Node r
= d_equalityEngine
->getRepresentative(atom
[1]);
295 EqcInfo
* e
= getOrMakeEqcInfo(r
, true);
298 Node s
= e
->d_singleton
;
301 Node pexp
= NodeManager::currentNM()->mkNode(
302 kind::AND
, atom
, atom
[1].eqNode(s
));
304 if (s
.getKind() == kind::SINGLETON
)
309 << "Propagate mem-eq : " << pexp
<< std::endl
;
310 Node eq
= s
[0].eqNode(atom
[0]);
312 assertFact(eq
, pexp
);
318 << "Propagate mem-eq conflict : " << pexp
<< std::endl
;
323 // add to membership list
324 NodeIntMap::iterator mem_i
= d_members
.find(r
);
326 if (mem_i
!= d_members
.end())
328 n_members
= (*mem_i
).second
;
330 d_members
[r
] = n_members
+ 1;
331 if (n_members
< (int)d_members_data
[r
].size())
333 d_members_data
[r
][n_members
] = atom
;
337 d_members_data
[r
].push_back(atom
);
349 void TheorySetsPrivate::fullEffortReset()
351 Assert(d_equalityEngine
->consistent());
352 d_full_check_incomplete
= false;
353 d_most_common_type
.clear();
354 d_most_common_type_term
.clear();
355 d_card_enabled
= false;
356 d_rels_enabled
= false;
357 // reset the state object
359 // reset the inference manager
361 // reset the cardinality solver
362 d_cardSolver
->reset();
365 void TheorySetsPrivate::fullEffortCheck()
367 Trace("sets") << "----- Full effort check ------" << std::endl
;
370 Assert(!d_im
.hasPendingLemmas() || d_im
.hasProcessed());
372 Trace("sets") << "...iterate full effort check..." << std::endl
;
375 Trace("sets-eqc") << "Equality Engine:" << std::endl
;
376 std::map
<TypeNode
, unsigned> eqcTypeCount
;
377 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator(d_equalityEngine
);
378 while (!eqcs_i
.isFinished())
380 Node eqc
= (*eqcs_i
);
382 TypeNode tn
= eqc
.getType();
383 d_state
.registerEqc(tn
, eqc
);
385 // common type node and term
391 tnc
= tn
.getSetElementType();
394 Trace("sets-eqc") << "[" << eqc
<< "] : ";
395 eq::EqClassIterator eqc_i
= eq::EqClassIterator(eqc
, d_equalityEngine
);
396 while (!eqc_i
.isFinished())
401 Trace("sets-eqc") << n
<< " ";
403 TypeNode tnn
= n
.getType();
407 TypeNode tnnel
= tnn
.getSetElementType();
408 tnc
= TypeNode::mostCommonTypeNode(tnc
, tnnel
);
409 Assert(!tnc
.isNull());
410 // update the common type term
416 // register it with the state
417 d_state
.registerTerm(eqc
, tnn
, n
);
418 if (n
.getKind() == kind::CARD
)
420 d_card_enabled
= true;
421 // register it with the cardinality solver
422 d_cardSolver
->registerTerm(n
);
423 // if we do not handle the kind, set incomplete
424 Kind nk
= n
[0].getKind();
425 // some kinds of cardinality we cannot handle
426 if (d_rels
->isRelationKind(nk
))
428 d_full_check_incomplete
= true;
429 Trace("sets-incomplete")
430 << "Sets : incomplete because of " << n
<< "." << std::endl
;
431 // TODO (#1124): The issue can be divided into 4 parts
432 // 1- Supporting the universe cardinality for finite types with
433 // finite cardinality (done)
434 // 2- Supporting the universe cardinality for uninterpreted sorts
435 // with finite-model-find (pending) See the implementation of
436 // CardinalityExtension::checkCardinalityExtended
437 // 3- Supporting the universe cardinality for non-finite types
439 // 4- Supporting cardinality for relations (hard)
444 if (d_rels
->isRelationKind(n
.getKind()))
446 d_rels_enabled
= true;
453 Assert(tnct
.getType().getSetElementType() == tnc
);
454 d_most_common_type
[eqc
] = tnc
;
455 d_most_common_type_term
[eqc
] = tnct
;
457 Trace("sets-eqc") << std::endl
;
461 Trace("sets-eqc") << "...finished equality engine." << std::endl
;
463 if (Trace
.isOn("sets-state"))
465 Trace("sets-state") << "Equivalence class counters:" << std::endl
;
466 for (std::pair
<const TypeNode
, unsigned>& ec
: eqcTypeCount
)
469 << " " << ec
.first
<< " -> " << ec
.second
<< std::endl
;
473 // We may have sent lemmas while registering the terms in the loop above,
474 // e.g. the cardinality solver.
475 if (d_im
.hasProcessed())
479 if (Trace
.isOn("sets-mem"))
481 const std::vector
<Node
>& sec
= d_state
.getSetsEqClasses();
482 for (const Node
& s
: sec
)
484 Trace("sets-mem") << "Eqc " << s
<< " : ";
485 const std::map
<Node
, Node
>& smem
= d_state
.getMembers(s
);
488 Trace("sets-mem") << "Memberships : ";
489 for (const std::pair
<const Node
, Node
>& it2
: smem
)
491 Trace("sets-mem") << it2
.first
<< " ";
494 Node ss
= d_state
.getSingletonEqClass(s
);
497 Trace("sets-mem") << " : Singleton : " << ss
;
499 Trace("sets-mem") << std::endl
;
504 d_im
.flushPendingLemmas(true);
505 if (d_im
.hasProcessed())
509 // check downwards closure
510 checkDownwardsClosure();
511 d_im
.flushPendingLemmas();
512 if (d_im
.hasProcessed())
516 // check upwards closure
517 checkUpwardsClosure();
518 d_im
.flushPendingLemmas();
519 if (d_im
.hasProcessed())
523 // check disequalities
524 checkDisequalities();
525 d_im
.flushPendingLemmas();
526 if (d_im
.hasProcessed())
530 // check reduce comprehensions
531 checkReduceComprehensions();
532 d_im
.flushPendingLemmas();
533 if (d_im
.hasProcessed())
539 // call the check method of the cardinality solver
540 d_cardSolver
->check();
541 if (d_im
.hasProcessed())
548 // call the check method of the relations solver
549 d_rels
->check(Theory::EFFORT_FULL
);
551 } while (!d_im
.hasSentLemma() && !d_state
.isInConflict()
552 && d_im
.hasAddedFact());
553 Assert(!d_im
.hasPendingLemmas() || d_im
.hasProcessed());
554 Trace("sets") << "----- End full effort check, conflict="
555 << d_state
.isInConflict() << ", lemma=" << d_im
.hasSentLemma()
559 void TheorySetsPrivate::checkSubtypes()
561 Trace("sets") << "TheorySetsPrivate: check Subtypes..." << std::endl
;
562 const std::vector
<Node
>& sec
= d_state
.getSetsEqClasses();
563 for (const Node
& s
: sec
)
565 TypeNode mct
= d_most_common_type
[s
];
566 Assert(!mct
.isNull());
567 const std::map
<Node
, Node
>& smems
= d_state
.getMembers(s
);
570 for (const std::pair
<const Node
, Node
>& it2
: smems
)
572 Trace("sets") << " check subtype " << it2
.first
<< " " << it2
.second
574 Trace("sets") << " types : " << it2
.first
.getType() << " " << mct
576 if (!it2
.first
.getType().isSubtypeOf(mct
))
578 Node mctt
= d_most_common_type_term
[s
];
579 Assert(!mctt
.isNull());
580 Trace("sets") << " most common type term is " << mctt
<< std::endl
;
581 std::vector
<Node
> exp
;
582 exp
.push_back(it2
.second
);
583 Assert(d_state
.areEqual(mctt
, it2
.second
[1]));
584 exp
.push_back(mctt
.eqNode(it2
.second
[1]));
585 Node tc_k
= d_state
.getTypeConstraintSkolem(it2
.first
, mct
);
588 Node etc
= tc_k
.eqNode(it2
.first
);
589 d_im
.assertInference(etc
, exp
, "subtype-clash");
590 if (d_state
.isInConflict())
599 Trace("sets") << "TheorySetsPrivate: finished." << std::endl
;
602 void TheorySetsPrivate::checkDownwardsClosure()
604 Trace("sets") << "TheorySetsPrivate: check downwards closure..." << std::endl
;
606 const std::vector
<Node
>& sec
= d_state
.getSetsEqClasses();
607 for (const Node
& s
: sec
)
609 const std::vector
<Node
>& nvsets
= d_state
.getNonVariableSets(s
);
612 const std::map
<Node
, Node
>& smem
= d_state
.getMembers(s
);
613 for (const Node
& nv
: nvsets
)
615 if (!d_state
.isCongruent(nv
))
617 for (const std::pair
<const Node
, Node
>& it2
: smem
)
619 Node mem
= it2
.second
;
621 Assert(d_equalityEngine
->areEqual(mem
[1], eq_set
));
622 if (mem
[1] != eq_set
)
624 Trace("sets-debug") << "Downwards closure based on " << mem
625 << ", eq_set = " << eq_set
<< std::endl
;
626 if (!options::setsProxyLemmas())
628 Node nmem
= NodeManager::currentNM()->mkNode(
629 kind::MEMBER
, mem
[0], eq_set
);
630 nmem
= Rewriter::rewrite(nmem
);
631 std::vector
<Node
> exp
;
633 exp
.push_back(mem
[1].eqNode(eq_set
));
634 d_im
.assertInference(nmem
, exp
, "downc");
635 if (d_state
.isInConflict())
643 Node k
= d_state
.getProxy(eq_set
);
645 NodeManager::currentNM()->mkNode(kind::MEMBER
, mem
[0], k
);
646 Node nmem
= NodeManager::currentNM()->mkNode(
647 kind::MEMBER
, mem
[0], eq_set
);
648 nmem
= Rewriter::rewrite(nmem
);
649 std::vector
<Node
> exp
;
650 if (d_state
.areEqual(mem
, pmem
))
656 nmem
= NodeManager::currentNM()->mkNode(
657 kind::OR
, pmem
.negate(), nmem
);
659 d_im
.assertInference(nmem
, exp
, "downc");
669 void TheorySetsPrivate::checkUpwardsClosure()
672 NodeManager
* nm
= NodeManager::currentNM();
673 const std::map
<Kind
, std::map
<Node
, std::map
<Node
, Node
> > >& boi
=
674 d_state
.getBinaryOpIndex();
675 for (const std::pair
<const Kind
, std::map
<Node
, std::map
<Node
, Node
> > >&
679 Trace("sets") << "TheorySetsPrivate: check upwards closure " << k
<< "..."
681 for (const std::pair
<const Node
, std::map
<Node
, Node
> >& it
: itb
.second
)
684 // see if there are members in first argument r1
685 const std::map
<Node
, Node
>& r1mem
= d_state
.getMembers(r1
);
686 if (!r1mem
.empty() || k
== kind::UNION
)
688 for (const std::pair
<const Node
, Node
>& it2
: it
.second
)
691 Node term
= it2
.second
;
692 // see if there are members in second argument
693 const std::map
<Node
, Node
>& r2mem
= d_state
.getMembers(r2
);
694 const std::map
<Node
, Node
>& r2nmem
= d_state
.getNegativeMembers(r2
);
695 if (!r2mem
.empty() || k
!= kind::INTERSECTION
)
698 << "Checking " << term
<< ", members = " << (!r1mem
.empty())
699 << ", " << (!r2mem
.empty()) << std::endl
;
700 // for all members of r1
703 for (const std::pair
<const Node
, Node
>& itm1m
: r1mem
)
705 Node xr
= itm1m
.first
;
706 Node x
= itm1m
.second
[0];
707 Trace("sets-debug") << "checking membership " << xr
<< " "
708 << itm1m
.second
<< std::endl
;
709 std::vector
<Node
> exp
;
710 exp
.push_back(itm1m
.second
);
711 d_state
.addEqualityToExp(term
[0], itm1m
.second
[1], exp
);
714 if (k
== kind::UNION
)
718 else if (k
== kind::INTERSECTION
)
720 // conclude x is in term
721 // if also existing in members of r2
722 std::map
<Node
, Node
>::const_iterator itm
= r2mem
.find(xr
);
723 if (itm
!= r2mem
.end())
725 exp
.push_back(itm
->second
);
726 d_state
.addEqualityToExp(term
[1], itm
->second
[1], exp
);
727 d_state
.addEqualityToExp(x
, itm
->second
[0], exp
);
732 // if not, check whether it is definitely not a member, if
734 if (r2nmem
.find(xr
) == r2nmem
.end())
736 exp
.push_back(nm
->mkNode(kind::MEMBER
, x
, term
[1]));
744 Assert(k
== kind::SETMINUS
);
745 std::map
<Node
, Node
>::const_iterator itm
= r2mem
.find(xr
);
746 if (itm
== r2mem
.end())
748 // must add lemma for set minus since non-membership in this
749 // case is not explained
751 nm
->mkNode(kind::MEMBER
, x
, term
[1]).negate());
758 Node rr
= d_equalityEngine
->getRepresentative(term
);
759 if (!isMember(x
, rr
))
761 Node kk
= d_state
.getProxy(term
);
762 Node fact
= nm
->mkNode(kind::MEMBER
, x
, kk
);
763 d_im
.assertInference(fact
, exp
, "upc", inferType
);
764 if (d_state
.isInConflict())
770 Trace("sets-debug") << "done checking membership " << xr
<< " "
771 << itm1m
.second
<< std::endl
;
774 if (k
== kind::UNION
)
778 // for all members of r2
779 for (const std::pair
<const Node
, Node
>& itm2m
: r2mem
)
781 Node x
= itm2m
.second
[0];
782 Node rr
= d_equalityEngine
->getRepresentative(term
);
783 if (!isMember(x
, rr
))
785 std::vector
<Node
> exp
;
786 exp
.push_back(itm2m
.second
);
787 d_state
.addEqualityToExp(term
[1], itm2m
.second
[1], exp
);
788 Node r
= d_state
.getProxy(term
);
789 Node fact
= nm
->mkNode(kind::MEMBER
, x
, r
);
790 d_im
.assertInference(fact
, exp
, "upc2");
791 if (d_state
.isInConflict())
804 if (!d_im
.hasProcessed())
806 if (options::setsExt())
809 Trace("sets-debug") << "Check universe sets..." << std::endl
;
810 // all elements must be in universal set
811 const std::vector
<Node
>& sec
= d_state
.getSetsEqClasses();
812 for (const Node
& s
: sec
)
814 // if equivalence class contains a variable
815 Node v
= d_state
.getVariableSet(s
);
818 // the variable in the equivalence class
819 std::map
<TypeNode
, Node
> univ_set
;
820 const std::map
<Node
, Node
>& smems
= d_state
.getMembers(s
);
821 for (const std::pair
<const Node
, Node
>& it2
: smems
)
823 Node e
= it2
.second
[0];
824 TypeNode tn
= NodeManager::currentNM()->mkSetType(e
.getType());
826 std::map
<TypeNode
, Node
>::iterator itu
= univ_set
.find(tn
);
827 if (itu
== univ_set
.end())
829 Node ueqc
= d_state
.getUnivSetEqClass(tn
);
830 // if the universe does not yet exist, or is not in this
834 u
= d_state
.getUnivSet(tn
);
844 Assert(it2
.second
.getKind() == kind::MEMBER
);
845 std::vector
<Node
> exp
;
846 exp
.push_back(it2
.second
);
847 if (v
!= it2
.second
[1])
849 exp
.push_back(v
.eqNode(it2
.second
[1]));
851 Node fact
= nm
->mkNode(kind::MEMBER
, it2
.second
[0], u
);
852 d_im
.assertInference(fact
, exp
, "upuniv");
853 if (d_state
.isInConflict())
865 void TheorySetsPrivate::checkDisequalities()
868 Trace("sets") << "TheorySetsPrivate: check disequalities..." << std::endl
;
869 NodeManager
* nm
= NodeManager::currentNM();
870 for (NodeBoolMap::const_iterator it
= d_deq
.begin(); it
!= d_deq
.end(); ++it
)
877 Node deq
= (*it
).first
;
878 // check if it is already satisfied
879 Assert(d_equalityEngine
->hasTerm(deq
[0])
880 && d_equalityEngine
->hasTerm(deq
[1]));
881 Node r1
= d_equalityEngine
->getRepresentative(deq
[0]);
882 Node r2
= d_equalityEngine
->getRepresentative(deq
[1]);
883 bool is_sat
= d_state
.isSetDisequalityEntailed(r1
, r2
);
884 Trace("sets-debug") << "Check disequality " << deq
885 << ", is_sat = " << is_sat
<< std::endl
;
886 // will process regardless of sat/processed/unprocessed
894 if (d_termProcessed
.find(deq
) != d_termProcessed
.end())
896 // already added lemma
899 d_termProcessed
.insert(deq
);
900 d_termProcessed
.insert(deq
[1].eqNode(deq
[0]));
901 Trace("sets") << "Process Disequality : " << deq
.negate() << std::endl
;
902 TypeNode elementType
= deq
[0].getType().getSetElementType();
903 Node x
= d_state
.getSkolemCache().mkTypedSkolemCached(
904 elementType
, deq
[0], deq
[1], SkolemCache::SK_DISEQUAL
, "sde");
905 Node mem1
= nm
->mkNode(MEMBER
, x
, deq
[0]);
906 Node mem2
= nm
->mkNode(MEMBER
, x
, deq
[1]);
907 Node lem
= nm
->mkNode(OR
, deq
, nm
->mkNode(EQUAL
, mem1
, mem2
).negate());
908 lem
= Rewriter::rewrite(lem
);
909 d_im
.assertInference(lem
, d_true
, "diseq", 1);
910 d_im
.flushPendingLemmas();
911 if (d_im
.hasProcessed())
918 void TheorySetsPrivate::checkReduceComprehensions()
920 NodeManager
* nm
= NodeManager::currentNM();
921 const std::vector
<Node
>& comps
= d_state
.getComprehensionSets();
922 for (const Node
& n
: comps
)
924 if (d_termProcessed
.find(n
) != d_termProcessed
.end())
926 // already reduced it
929 d_termProcessed
.insert(n
);
930 Node v
= nm
->mkBoundVar(n
[2].getType());
931 Node body
= nm
->mkNode(AND
, n
[1], v
.eqNode(n
[2]));
932 // must do substitution
933 std::vector
<Node
> vars
;
934 std::vector
<Node
> subs
;
935 for (const Node
& cv
: n
[0])
938 Node cvs
= nm
->mkBoundVar(cv
.getType());
941 body
= body
.substitute(vars
.begin(), vars
.end(), subs
.begin(), subs
.end());
942 Node bvl
= nm
->mkNode(BOUND_VAR_LIST
, subs
);
943 body
= nm
->mkNode(EXISTS
, bvl
, body
);
944 Node mem
= nm
->mkNode(MEMBER
, v
, n
);
946 nm
->mkNode(FORALL
, nm
->mkNode(BOUND_VAR_LIST
, v
), body
.eqNode(mem
));
947 Trace("sets-comprehension")
948 << "Comprehension reduction: " << lem
<< std::endl
;
949 d_im
.flushLemma(lem
);
953 /**************************** TheorySetsPrivate *****************************/
954 /**************************** TheorySetsPrivate *****************************/
955 /**************************** TheorySetsPrivate *****************************/
957 void TheorySetsPrivate::check(Theory::Effort level
)
959 Trace("sets-check") << "Sets check effort " << level
<< std::endl
;
960 if (level
== Theory::EFFORT_LAST_CALL
)
964 while (!d_external
.done() && !d_state
.isInConflict())
966 // Get all the assertions
967 Assertion assertion
= d_external
.get();
968 TNode fact
= assertion
.d_assertion
;
969 Trace("sets-assert") << "Assert from input " << fact
<< std::endl
;
971 assertFact(fact
, fact
);
973 Trace("sets-check") << "Sets finished assertions effort " << level
975 // invoke full effort check, relations check
976 if (!d_state
.isInConflict())
978 if (level
== Theory::EFFORT_FULL
)
980 if (!d_external
.d_valuation
.needCheck())
983 if (!d_state
.isInConflict() && !d_im
.hasSentLemma()
984 && d_full_check_incomplete
)
986 d_external
.d_out
->setIncomplete();
991 Trace("sets-check") << "Sets finish Check effort " << level
<< std::endl
;
992 } /* TheorySetsPrivate::check() */
994 /************************ Sharing ************************/
995 /************************ Sharing ************************/
996 /************************ Sharing ************************/
998 void TheorySetsPrivate::addSharedTerm(TNode n
)
1000 Debug("sets") << "[sets] TheorySetsPrivate::addSharedTerm( " << n
<< ")"
1002 d_equalityEngine
->addTriggerTerm(n
, THEORY_SETS
);
1005 void TheorySetsPrivate::addCarePairs(TNodeTrie
* t1
,
1015 Node f1
= t1
->getData();
1016 Node f2
= t2
->getData();
1017 if (!d_state
.areEqual(f1
, f2
))
1019 Trace("sets-cg") << "Check " << f1
<< " and " << f2
<< std::endl
;
1020 vector
<pair
<TNode
, TNode
> > currentPairs
;
1021 for (unsigned k
= 0; k
< f1
.getNumChildren(); ++k
)
1025 Assert(d_equalityEngine
->hasTerm(x
));
1026 Assert(d_equalityEngine
->hasTerm(y
));
1027 Assert(!d_state
.areDisequal(x
, y
));
1028 Assert(!areCareDisequal(x
, y
));
1029 if (!d_equalityEngine
->areEqual(x
, y
))
1032 << "Arg #" << k
<< " is " << x
<< " " << y
<< std::endl
;
1033 if (d_equalityEngine
->isTriggerTerm(x
, THEORY_SETS
)
1034 && d_equalityEngine
->isTriggerTerm(y
, THEORY_SETS
))
1036 TNode x_shared
= d_equalityEngine
->getTriggerTermRepresentative(
1038 TNode y_shared
= d_equalityEngine
->getTriggerTermRepresentative(
1040 currentPairs
.push_back(make_pair(x_shared
, y_shared
));
1042 else if (isCareArg(f1
, k
) && isCareArg(f2
, k
))
1044 // splitting on sets (necessary for handling set of sets properly)
1045 if (x
.getType().isSet())
1047 Assert(y
.getType().isSet());
1048 if (!d_state
.areDisequal(x
, y
))
1050 Trace("sets-cg-lemma")
1051 << "Should split on : " << x
<< "==" << y
<< std::endl
;
1052 d_im
.split(x
.eqNode(y
));
1058 for (unsigned c
= 0; c
< currentPairs
.size(); ++c
)
1060 Trace("sets-cg-pair") << "Pair : " << currentPairs
[c
].first
<< " "
1061 << currentPairs
[c
].second
<< std::endl
;
1062 d_external
.addCarePair(currentPairs
[c
].first
, currentPairs
[c
].second
);
1072 if (depth
< (arity
- 1))
1074 // add care pairs internal to each child
1075 for (std::pair
<const TNode
, TNodeTrie
>& t
: t1
->d_data
)
1077 addCarePairs(&t
.second
, NULL
, arity
, depth
+ 1, n_pairs
);
1080 // add care pairs based on each pair of non-disequal arguments
1081 for (std::map
<TNode
, TNodeTrie
>::iterator it
= t1
->d_data
.begin();
1082 it
!= t1
->d_data
.end();
1085 std::map
<TNode
, TNodeTrie
>::iterator it2
= it
;
1087 for (; it2
!= t1
->d_data
.end(); ++it2
)
1089 if (!d_equalityEngine
->areDisequal(it
->first
, it2
->first
, false))
1091 if (!areCareDisequal(it
->first
, it2
->first
))
1094 &it
->second
, &it2
->second
, arity
, depth
+ 1, n_pairs
);
1102 // add care pairs based on product of indices, non-disequal arguments
1103 for (std::pair
<const TNode
, TNodeTrie
>& tt1
: t1
->d_data
)
1105 for (std::pair
<const TNode
, TNodeTrie
>& tt2
: t2
->d_data
)
1107 if (!d_equalityEngine
->areDisequal(tt1
.first
, tt2
.first
, false))
1109 if (!areCareDisequal(tt1
.first
, tt2
.first
))
1111 addCarePairs(&tt1
.second
, &tt2
.second
, arity
, depth
+ 1, n_pairs
);
1120 void TheorySetsPrivate::computeCareGraph()
1122 const std::map
<Kind
, std::vector
<Node
> >& ol
= d_state
.getOperatorList();
1123 for (const std::pair
<const Kind
, std::vector
<Node
> >& it
: ol
)
1126 if (k
== kind::SINGLETON
|| k
== kind::MEMBER
)
1128 unsigned n_pairs
= 0;
1129 Trace("sets-cg-summary") << "Compute graph for sets, op=" << k
<< "..."
1130 << it
.second
.size() << std::endl
;
1131 Trace("sets-cg") << "Build index for " << k
<< "..." << std::endl
;
1132 std::map
<TypeNode
, TNodeTrie
> index
;
1135 for (TNode f1
: it
.second
)
1137 Assert(d_equalityEngine
->hasTerm(f1
));
1138 Trace("sets-cg-debug") << "...build for " << f1
<< std::endl
;
1139 Assert(d_equalityEngine
->hasTerm(f1
));
1140 // break into index based on operator, and type of first argument (since
1141 // some operators are parametric)
1142 TypeNode tn
= f1
[0].getType();
1143 std::vector
<TNode
> reps
;
1144 bool hasCareArg
= false;
1145 for (unsigned j
= 0; j
< f1
.getNumChildren(); j
++)
1147 reps
.push_back(d_equalityEngine
->getRepresentative(f1
[j
]));
1148 if (isCareArg(f1
, j
))
1155 Trace("sets-cg-debug") << "......adding." << std::endl
;
1156 index
[tn
].addTerm(f1
, reps
);
1157 arity
= reps
.size();
1161 Trace("sets-cg-debug") << "......skip." << std::endl
;
1167 for (std::pair
<const TypeNode
, TNodeTrie
>& tt
: index
)
1169 Trace("sets-cg") << "Process index " << tt
.first
<< "..."
1171 addCarePairs(&tt
.second
, nullptr, arity
, 0, n_pairs
);
1174 Trace("sets-cg-summary") << "...done, # pairs = " << n_pairs
<< std::endl
;
1179 bool TheorySetsPrivate::isCareArg(Node n
, unsigned a
)
1181 if (d_equalityEngine
->isTriggerTerm(n
[a
], THEORY_SETS
))
1185 else if ((n
.getKind() == kind::MEMBER
|| n
.getKind() == kind::SINGLETON
)
1186 && a
== 0 && n
[0].getType().isSet())
1196 EqualityStatus
TheorySetsPrivate::getEqualityStatus(TNode a
, TNode b
)
1198 Assert(d_equalityEngine
->hasTerm(a
) && d_equalityEngine
->hasTerm(b
));
1199 if (d_equalityEngine
->areEqual(a
, b
))
1201 // The terms are implied to be equal
1202 return EQUALITY_TRUE
;
1204 if (d_equalityEngine
->areDisequal(a
, b
, false))
1206 // The terms are implied to be dis-equal
1207 return EQUALITY_FALSE
;
1209 return EQUALITY_UNKNOWN
;
1211 Node aModelValue = d_external.d_valuation.getModelValue(a);
1212 if(aModelValue.isNull()) { return EQUALITY_UNKNOWN; }
1213 Node bModelValue = d_external.d_valuation.getModelValue(b);
1214 if(bModelValue.isNull()) { return EQUALITY_UNKNOWN; }
1215 if( aModelValue == bModelValue ) {
1216 // The term are true in current model
1217 return EQUALITY_TRUE_IN_MODEL;
1219 return EQUALITY_FALSE_IN_MODEL;
1223 // //TODO: can we be more precise sometimes?
1224 // return EQUALITY_UNKNOWN;
1227 /******************** Model generation ********************/
1228 /******************** Model generation ********************/
1229 /******************** Model generation ********************/
1233 * This function is a helper function to print sets as
1234 * Set A = { a0, a1, a2, }
1236 * (union (singleton a0) (union (singleton a1) (singleton a2)))
1238 void traceSetElementsRecursively(stringstream
& stream
, const Node
& set
)
1240 Assert(set
.getType().isSet());
1241 if (set
.getKind() == SINGLETON
)
1243 stream
<< set
[0] << ", ";
1245 if (set
.getKind() == UNION
)
1247 traceSetElementsRecursively(stream
, set
[0]);
1248 traceSetElementsRecursively(stream
, set
[1]);
1252 std::string
traceElements(const Node
& set
)
1254 std::stringstream stream
;
1255 traceSetElementsRecursively(stream
, set
);
1256 return stream
.str();
1261 bool TheorySetsPrivate::collectModelInfo(TheoryModel
* m
)
1263 Trace("sets-model") << "Set collect model info" << std::endl
;
1265 // Compute terms appearing in assertions and shared terms
1266 d_external
.computeRelevantTerms(termSet
);
1268 // Assert equalities and disequalities to the model
1269 if (!m
->assertEqualityEngine(d_equalityEngine
, &termSet
))
1274 NodeManager
* nm
= NodeManager::currentNM();
1275 std::map
<Node
, Node
> mvals
;
1276 // If cardinality is enabled, we need to use the ordered equivalence class
1277 // list computed by the cardinality solver, where sets equivalence classes
1278 // are assigned model values based on their position in the cardinality
1280 const std::vector
<Node
>& sec
= d_card_enabled
1281 ? d_cardSolver
->getOrderedSetsEqClasses()
1282 : d_state
.getSetsEqClasses();
1283 Valuation
& val
= getValuation();
1284 for (int i
= (int)(sec
.size() - 1); i
>= 0; i
--)
1287 if (termSet
.find(eqc
) == termSet
.end())
1289 Trace("sets-model") << "* Do not assign value for " << eqc
1290 << " since is not relevant." << std::endl
;
1294 std::vector
<Node
> els
;
1295 bool is_base
= !d_card_enabled
|| d_cardSolver
->isModelValueBasic(eqc
);
1299 << "Collect elements of base eqc " << eqc
<< std::endl
;
1300 // members that must be in eqc
1301 const std::map
<Node
, Node
>& emems
= d_state
.getMembers(eqc
);
1304 for (const std::pair
<const Node
, Node
>& itmm
: emems
)
1306 Node t
= nm
->mkNode(kind::SINGLETON
, itmm
.first
);
1313 // make the slack elements for the equivalence class based on set
1315 d_cardSolver
->mkModelValueElementsFor(val
, eqc
, els
, mvals
, m
);
1317 Node rep
= NormalForm::mkBop(kind::UNION
, els
, eqc
.getType());
1318 rep
= Rewriter::rewrite(rep
);
1319 Trace("sets-model") << "* Assign representative of " << eqc
<< " to "
1320 << rep
<< std::endl
;
1322 if (!m
->assertEquality(eqc
, rep
, true))
1326 m
->assertSkeleton(rep
);
1328 Trace("sets-model") << "Set " << eqc
<< " = { " << traceElements(rep
)
1329 << " }" << std::endl
;
1333 // handle slack elements constraints for finite types
1336 const std::map
<TypeNode
, std::vector
<TNode
> >& slackElements
=
1337 d_cardSolver
->getFiniteTypeSlackElements();
1338 for (const std::pair
<TypeNode
, std::vector
<TNode
> >& pair
: slackElements
)
1340 const std::vector
<Node
>& members
=
1341 d_cardSolver
->getFiniteTypeMembers(pair
.first
);
1342 m
->setAssignmentExclusionSetGroup(pair
.second
, members
);
1343 Trace("sets-model") << "ExclusionSet: Group " << pair
.second
1344 << " is excluded from set" << members
<< std::endl
;
1350 /********************** Helper functions ***************************/
1351 /********************** Helper functions ***************************/
1352 /********************** Helper functions ***************************/
1354 Node
mkAnd(const std::vector
<TNode
>& conjunctions
)
1356 Assert(conjunctions
.size() > 0);
1358 std::set
<TNode
> all
;
1359 for (unsigned i
= 0; i
< conjunctions
.size(); ++i
)
1361 TNode t
= conjunctions
[i
];
1362 if (t
.getKind() == kind::AND
)
1364 for (TNode::iterator child_it
= t
.begin(); child_it
!= t
.end();
1367 Assert((*child_it
).getKind() != kind::AND
);
1368 all
.insert(*child_it
);
1377 Assert(all
.size() > 0);
1378 if (all
.size() == 1)
1380 // All the same, or just one
1381 return conjunctions
[0];
1384 NodeBuilder
<> conjunction(kind::AND
);
1385 std::set
<TNode
>::const_iterator it
= all
.begin();
1386 std::set
<TNode
>::const_iterator it_end
= all
.end();
1387 while (it
!= it_end
)
1395 bool TheorySetsPrivate::propagate(TNode literal
)
1397 Debug("sets-prop") << " propagate(" << literal
<< ")" << std::endl
;
1399 // If already in conflict, no more propagation
1400 if (d_state
.isInConflict())
1402 Debug("sets-prop") << "TheoryUF::propagate(" << literal
1403 << "): already in conflict" << std::endl
;
1408 bool ok
= d_external
.d_out
->propagate(literal
);
1411 d_state
.notifyInConflict();
1415 } /* TheorySetsPrivate::propagate(TNode) */
1417 OutputChannel
* TheorySetsPrivate::getOutputChannel()
1419 return d_external
.d_out
;
1422 Valuation
& TheorySetsPrivate::getValuation() { return d_external
.d_valuation
; }
1424 void TheorySetsPrivate::conflict(TNode a
, TNode b
)
1426 Node conf
= explain(a
.eqNode(b
));
1427 d_im
.conflict(conf
);
1428 Debug("sets") << "[sets] conflict: " << a
<< " iff " << b
<< ", explanation "
1429 << conf
<< std::endl
;
1430 Trace("sets-lemma") << "Equality Conflict : " << conf
<< std::endl
;
1433 Node
TheorySetsPrivate::explain(TNode literal
)
1435 Debug("sets") << "TheorySetsPrivate::explain(" << literal
<< ")" << std::endl
;
1437 bool polarity
= literal
.getKind() != kind::NOT
;
1438 TNode atom
= polarity
? literal
: literal
[0];
1439 std::vector
<TNode
> assumptions
;
1441 if (atom
.getKind() == kind::EQUAL
)
1443 d_equalityEngine
->explainEquality(atom
[0], atom
[1], polarity
, assumptions
);
1445 else if (atom
.getKind() == kind::MEMBER
)
1447 d_equalityEngine
->explainPredicate(atom
, polarity
, assumptions
);
1451 Debug("sets") << "unhandled: " << literal
<< "; (" << atom
<< ", "
1452 << polarity
<< "); kind" << atom
.getKind() << std::endl
;
1456 return mkAnd(assumptions
);
1459 void TheorySetsPrivate::preRegisterTerm(TNode node
)
1461 Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node
<< ")"
1463 switch (node
.getKind())
1468 // add trigger predicate for equality and membership
1469 d_equalityEngine
->addTriggerPredicate(node
);
1472 case kind::CARD
: d_equalityEngine
->addTriggerTerm(node
, THEORY_SETS
); break;
1473 default: d_equalityEngine
->addTerm(node
); break;
1477 TrustNode
TheorySetsPrivate::expandDefinition(Node node
)
1479 Debug("sets-proc") << "expandDefinition : " << node
<< std::endl
;
1481 if (node
.getKind() == kind::CHOOSE
)
1483 // (choose A) is expanded as
1484 // (witness ((x elementType))
1486 // (= A (as emptyset setType))
1487 // (= x chooseUf(A))
1488 // (and (member x A) (= x chooseUf(A)))
1490 NodeManager
* nm
= NodeManager::currentNM();
1492 TypeNode setType
= set
.getType();
1493 Node chooseSkolem
= getChooseFunction(setType
);
1494 Node apply
= NodeManager::currentNM()->mkNode(APPLY_UF
, chooseSkolem
, set
);
1496 Node witnessVariable
= nm
->mkBoundVar(setType
.getSetElementType());
1498 Node equal
= witnessVariable
.eqNode(apply
);
1499 Node emptySet
= nm
->mkConst(EmptySet(setType
));
1500 Node isEmpty
= set
.eqNode(emptySet
);
1501 Node member
= nm
->mkNode(MEMBER
, witnessVariable
, set
);
1502 Node memberAndEqual
= member
.andNode(equal
);
1503 Node ite
= nm
->mkNode(kind::ITE
, isEmpty
, equal
, memberAndEqual
);
1504 Node witnessVariables
= nm
->mkNode(BOUND_VAR_LIST
, witnessVariable
);
1505 Node witness
= nm
->mkNode(WITNESS
, witnessVariables
, ite
);
1506 return TrustNode::mkTrustRewrite(node
, witness
, nullptr);
1509 return TrustNode::null();
1512 Node
TheorySetsPrivate::getChooseFunction(const TypeNode
& setType
)
1514 std::map
<TypeNode
, Node
>::iterator it
= d_chooseFunctions
.find(setType
);
1515 if (it
!= d_chooseFunctions
.end())
1520 NodeManager
* nm
= NodeManager::currentNM();
1521 TypeNode chooseUf
= nm
->mkFunctionType(setType
, setType
.getSetElementType());
1522 stringstream stream
;
1523 stream
<< "chooseUf" << setType
.getId();
1524 string name
= stream
.str();
1525 Node chooseSkolem
= nm
->mkSkolem(
1526 name
, chooseUf
, "choose function", NodeManager::SKOLEM_EXACT_NAME
);
1527 d_chooseFunctions
[setType
] = chooseSkolem
;
1528 return chooseSkolem
;
1531 void TheorySetsPrivate::presolve() { d_state
.reset(); }
1534 } // namespace theory