1 /********************* */
2 /*! \file cardinality_extension.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 Implementation of an extension of the theory sets for handling
13 ** cardinality constraints.
16 #include "theory/sets/cardinality_extension.h"
18 #include "expr/emptyset.h"
19 #include "expr/node_algorithm.h"
20 #include "options/sets_options.h"
21 #include "theory/sets/normal_form.h"
22 #include "theory/theory_model.h"
23 #include "theory/valuation.h"
26 using namespace CVC4::kind
;
32 CardinalityExtension::CardinalityExtension(SolverState
& s
,
34 eq::EqualityEngine
& e
,
36 context::UserContext
* u
)
41 d_finite_type_constants_processed(false)
43 d_true
= NodeManager::currentNM()->mkConst(true);
44 d_zero
= NodeManager::currentNM()->mkConst(Rational(0));
45 // we do congruence over cardinality
46 d_ee
.addFunctionKind(CARD
);
49 void CardinalityExtension::reset()
51 d_eqc_to_card_term
.clear();
52 d_t_card_enabled
.clear();
53 d_finite_type_elements
.clear();
54 d_finite_type_slack_elements
.clear();
57 void CardinalityExtension::registerTerm(Node n
)
59 Trace("sets-card-debug") << "Register term : " << n
<< std::endl
;
60 Assert(n
.getKind() == CARD
);
61 TypeNode tnc
= n
[0].getType().getSetElementType();
62 d_t_card_enabled
[tnc
] = true;
63 Node r
= d_ee
.getRepresentative(n
[0]);
64 if (d_eqc_to_card_term
.find(r
) == d_eqc_to_card_term
.end())
66 d_eqc_to_card_term
[r
] = n
;
67 registerCardinalityTerm(n
[0]);
69 Trace("sets-card-debug") << "...finished register term" << std::endl
;
72 void CardinalityExtension::checkFiniteTypes()
74 for (std::pair
<const TypeNode
, bool>& pair
: d_t_card_enabled
)
76 TypeNode type
= pair
.first
;
77 if (pair
.second
&& type
.isInterpretedFinite())
79 checkFiniteType(type
);
84 void CardinalityExtension::checkFiniteType(TypeNode
& t
)
86 Assert(t
.isInterpretedFinite());
88 // get the cardinality of the finite type t
89 Cardinality card
= t
.getCardinality();
91 // cardinality of an interpreted finite type t is infinite when t
92 // is infinite without --fmf
94 if (card
.isInfinite())
96 // TODO (#1123): support uninterpreted sorts with --finite-model-find
97 std::stringstream message
;
98 message
<< "The cardinality " << card
<< " of the finite type " << t
99 << " is not supported yet.";
100 throw LogicException(message
.str());
103 // get the universe set (as univset (Set t))
104 NodeManager
* nm
= NodeManager::currentNM();
105 Node univ
= d_state
.getUnivSet(nm
->mkSetType(t
));
106 std::map
<Node
, Node
>::iterator it
= d_univProxy
.find(univ
);
110 if (it
== d_univProxy
.end())
112 // Force cvc4 to build the cardinality graph for the universe set
113 proxy
= d_state
.getProxy(univ
);
114 d_univProxy
[univ
] = proxy
;
121 // get all equivalent classes of type t
122 vector
<Node
> representatives
= d_state
.getSetsEqClasses(t
);
124 Node typeCardinality
= nm
->mkConst(Rational(card
.getFiniteCardinality()));
126 Node cardUniv
= nm
->mkNode(kind::CARD
, proxy
);
127 Node leq
= nm
->mkNode(kind::LEQ
, cardUniv
, typeCardinality
);
129 // (=> true (<= (card (as univset t)) cardUniv)
130 if (!d_state
.isEntailed(leq
, true))
132 d_im
.assertInference(leq
, d_true
, "finite type cardinality", 1);
135 // add subset lemmas for sets, and membership lemmas for negative members
136 for (Node
& representative
: representatives
)
138 // the universe set is a subset of itself
139 if (representative
!= d_ee
.getRepresentative(univ
))
141 // here we only add representatives with variables to avoid adding
142 // infinite equivalent generated terms to the cardinality graph
143 Node variable
= d_state
.getVariableSet(representative
);
144 if (variable
.isNull())
149 // (=> true (subset representative (as univset t))
150 Node subset
= nm
->mkNode(kind::SUBSET
, variable
, proxy
);
151 // subset terms are rewritten as union terms: (subset A B) implies (=
153 subset
= Rewriter::rewrite(subset
);
154 if (!d_state
.isEntailed(subset
, true))
156 d_im
.assertInference(subset
, d_true
, "univset is a super set", 1);
159 // negative members are members in the universe set
160 const std::map
<Node
, Node
>& negativeMembers
=
161 d_state
.getNegativeMembers(representative
);
163 for (const std::pair
<Node
, Node
>& negativeMember
: negativeMembers
)
165 Node member
= nm
->mkNode(MEMBER
, negativeMember
.first
, univ
);
166 // negativeMember.second is the reason for the negative membership and
167 // has kind MEMBER. So we specify the negation as the reason for the
168 // negative membership lemma
169 Node notMember
= nm
->mkNode(NOT
, negativeMember
.second
);
171 // (not (member negativeMember representative)))
172 // (member negativeMember (as univset t)))
173 d_im
.assertInference(
174 member
, notMember
, "negative members are in the universe", 1);
180 void CardinalityExtension::check()
184 if (d_im
.hasProcessed())
189 if (d_im
.hasProcessed())
194 if (d_im
.hasProcessed())
198 // The last step will either do nothing (in which case we are SAT), or request
199 // that a new set term is introduced.
200 std::vector
<Node
> intro_sets
;
201 checkNormalForms(intro_sets
);
202 if (intro_sets
.empty())
206 Assert(intro_sets
.size() == 1);
207 Trace("sets-intro") << "Introduce term : " << intro_sets
[0] << std::endl
;
208 Trace("sets-intro") << " Actual Intro : ";
209 d_state
.debugPrintSet(intro_sets
[0], "sets-nf");
210 Trace("sets-nf") << std::endl
;
211 Node k
= d_state
.getProxy(intro_sets
[0]);
212 AlwaysAssert(!k
.isNull());
215 void CardinalityExtension::checkRegister()
217 Trace("sets") << "Cardinality graph..." << std::endl
;
218 NodeManager
* nm
= NodeManager::currentNM();
219 // first, ensure cardinality relationships are added as lemmas for all
220 // non-basic set terms
221 const std::vector
<Node
>& setEqc
= d_state
.getSetsEqClasses();
222 for (const Node
& eqc
: setEqc
)
224 const std::vector
<Node
>& nvsets
= d_state
.getNonVariableSets(eqc
);
225 for (Node n
: nvsets
)
227 if (!d_state
.isCongruent(n
))
229 // if setminus, do for intersection instead
230 if (n
.getKind() == SETMINUS
)
232 n
= Rewriter::rewrite(nm
->mkNode(INTERSECTION
, n
[0], n
[1]));
234 registerCardinalityTerm(n
);
238 Trace("sets") << "Done cardinality graph" << std::endl
;
241 void CardinalityExtension::registerCardinalityTerm(Node n
)
243 TypeNode tnc
= n
.getType().getSetElementType();
244 if (d_t_card_enabled
.find(tnc
) == d_t_card_enabled
.end())
246 // if no cardinality constraints for sets of this type, we can ignore
249 if (d_card_processed
.find(n
) != d_card_processed
.end())
254 d_card_processed
.insert(n
);
255 NodeManager
* nm
= NodeManager::currentNM();
256 Trace("sets-card") << "Cardinality lemmas for " << n
<< " : " << std::endl
;
257 std::vector
<Node
> cterms
;
258 if (n
.getKind() == INTERSECTION
)
260 for (unsigned e
= 0; e
< 2; e
++)
262 Node s
= nm
->mkNode(SETMINUS
, n
[e
], n
[1 - e
]);
265 Node pos_lem
= nm
->mkNode(GEQ
, nm
->mkNode(CARD
, n
), d_zero
);
266 d_im
.assertInference(pos_lem
, d_emp_exp
, "pcard", 1);
272 for (unsigned k
= 0, csize
= cterms
.size(); k
< csize
; k
++)
275 Node nk
= d_state
.getProxy(nn
);
276 Node pos_lem
= nm
->mkNode(GEQ
, nm
->mkNode(CARD
, nk
), d_zero
);
277 d_im
.assertInference(pos_lem
, d_emp_exp
, "pcard", 1);
280 Node lem
= nm
->mkNode(EQUAL
, nm
->mkNode(CARD
, nk
), nm
->mkNode(CARD
, nn
));
281 lem
= Rewriter::rewrite(lem
);
282 Trace("sets-card") << " " << k
<< " : " << lem
<< std::endl
;
283 d_im
.assertInference(lem
, d_emp_exp
, "card", 1);
286 d_im
.flushPendingLemmas();
289 void CardinalityExtension::checkCardCycles()
291 Trace("sets") << "Check cardinality cycles..." << std::endl
;
292 // build order of equivalence classes, also build cardinality graph
293 const std::vector
<Node
>& setEqc
= d_state
.getSetsEqClasses();
295 d_card_parent
.clear();
296 for (const Node
& s
: setEqc
)
298 std::vector
<Node
> curr
;
299 std::vector
<Node
> exp
;
300 checkCardCyclesRec(s
, curr
, exp
);
301 if (d_im
.hasProcessed())
306 Trace("sets") << "Done check cardinality cycles" << std::endl
;
309 void CardinalityExtension::checkCardCyclesRec(Node eqc
,
310 std::vector
<Node
>& curr
,
311 std::vector
<Node
>& exp
)
313 NodeManager
* nm
= NodeManager::currentNM();
314 if (std::find(curr
.begin(), curr
.end(), eqc
) != curr
.end())
316 Trace("sets-debug") << "Found venn region loop..." << std::endl
;
319 // all regions must be equal
320 std::vector
<Node
> conc
;
321 for (const Node
& cc
: curr
)
323 conc
.push_back(curr
[0].eqNode(cc
));
325 Node fact
= conc
.size() == 1 ? conc
[0] : nm
->mkNode(AND
, conc
);
326 d_im
.assertInference(fact
, exp
, "card_cycle");
327 d_im
.flushPendingLemmas();
331 // should be guaranteed based on not exploring equal parents
336 if (std::find(d_oSetEqc
.begin(), d_oSetEqc
.end(), eqc
) != d_oSetEqc
.end())
341 const std::vector
<Node
>& nvsets
= d_state
.getNonVariableSets(eqc
);
344 // no non-variable sets, trivial
345 d_oSetEqc
.push_back(eqc
);
349 TypeNode tn
= eqc
.getType();
350 bool is_empty
= eqc
== d_state
.getEmptySetEqClass(tn
);
351 Node emp_set
= d_state
.getEmptySet(tn
);
352 for (const Node
& n
: nvsets
)
354 Kind nk
= n
.getKind();
355 if (nk
!= INTERSECTION
&& nk
!= SETMINUS
)
359 Trace("sets-debug") << "Build cardinality parents for " << n
<< "..."
361 std::vector
<Node
> sib
;
362 unsigned true_sib
= 0;
363 if (n
.getKind() == INTERSECTION
)
366 for (unsigned e
= 0; e
< 2; e
++)
368 Node sm
= Rewriter::rewrite(nm
->mkNode(SETMINUS
, n
[e
], n
[1 - e
]));
375 Node si
= Rewriter::rewrite(nm
->mkNode(INTERSECTION
, n
[0], n
[1]));
378 Node osm
= Rewriter::rewrite(nm
->mkNode(SETMINUS
, n
[1], n
[0]));
382 Node u
= Rewriter::rewrite(nm
->mkNode(UNION
, n
[0], n
[1]));
383 if (!d_ee
.hasTerm(u
))
387 unsigned n_parents
= true_sib
+ (u
.isNull() ? 0 : 1);
388 // if this set is empty
391 Assert(d_state
.areEqual(n
, emp_set
));
392 Trace("sets-debug") << " empty, parents equal siblings" << std::endl
;
393 std::vector
<Node
> conc
;
394 // parent equal siblings
395 for (unsigned e
= 0; e
< true_sib
; e
++)
397 if (d_ee
.hasTerm(sib
[e
]) && !d_state
.areEqual(n
[e
], sib
[e
]))
399 conc
.push_back(n
[e
].eqNode(sib
[e
]));
402 d_im
.assertInference(conc
, n
.eqNode(emp_set
), "cg_emp");
403 d_im
.flushPendingLemmas();
404 if (d_im
.hasProcessed())
410 // justify why there is no edge to parents (necessary?)
411 for (unsigned e
= 0; e
< n_parents
; e
++)
413 Node p
= (e
== true_sib
) ? u
: n
[e
];
418 std::vector
<Node
> card_parents
;
419 std::vector
<int> card_parent_ids
;
420 // check if equal to a parent
421 for (unsigned e
= 0; e
< n_parents
; e
++)
423 Trace("sets-debug") << " check parent " << e
<< "/" << n_parents
425 bool is_union
= e
== true_sib
;
426 Node p
= (e
== true_sib
) ? u
: n
[e
];
427 Trace("sets-debug") << " check relation to parent " << p
428 << ", isu=" << is_union
<< "..." << std::endl
;
429 // if parent is empty
430 if (d_state
.areEqual(p
, emp_set
))
432 Trace("sets-debug") << " it is empty..." << std::endl
;
433 Assert(!d_state
.areEqual(n
, emp_set
));
434 d_im
.assertInference(n
.eqNode(emp_set
), p
.eqNode(emp_set
), "cg_emppar");
435 d_im
.flushPendingLemmas();
436 if (d_im
.hasProcessed())
440 // if we are equal to a parent
442 else if (d_state
.areEqual(p
, n
))
444 Trace("sets-debug") << " it is equal to this..." << std::endl
;
445 std::vector
<Node
> conc
;
446 std::vector
<int> sib_emp_indices
;
449 for (unsigned s
= 0; s
< sib
.size(); s
++)
451 sib_emp_indices
.push_back(s
);
456 sib_emp_indices
.push_back(e
);
458 // sibling(s) are empty
459 for (unsigned si
: sib_emp_indices
)
461 if (!d_state
.areEqual(sib
[si
], emp_set
))
463 conc
.push_back(sib
[si
].eqNode(emp_set
));
468 << "Sibling " << sib
[si
] << " is already empty." << std::endl
;
471 if (!is_union
&& nk
== INTERSECTION
&& !u
.isNull())
473 // union is equal to other parent
474 if (!d_state
.areEqual(u
, n
[1 - e
]))
476 conc
.push_back(u
.eqNode(n
[1 - e
]));
480 << "...derived " << conc
.size() << " conclusions" << std::endl
;
481 d_im
.assertInference(conc
, n
.eqNode(p
), "cg_eqpar");
482 d_im
.flushPendingLemmas();
483 if (d_im
.hasProcessed())
490 Trace("sets-cdg") << "Card graph : " << n
<< " -> " << p
<< std::endl
;
491 // otherwise, we a syntactic subset of p
492 card_parents
.push_back(p
);
493 card_parent_ids
.push_back(is_union
? 2 : e
);
496 Assert(d_card_parent
[n
].empty());
497 Trace("sets-debug") << "get parent representatives..." << std::endl
;
498 // for each parent, take their representatives
499 for (unsigned k
= 0, numcp
= card_parents
.size(); k
< numcp
; k
++)
501 Node cpk
= card_parents
[k
];
502 Node eqcc
= d_ee
.getRepresentative(cpk
);
503 Trace("sets-debug") << "Check card parent " << k
<< "/"
504 << card_parents
.size() << std::endl
;
506 // if parent is singleton, then we should either be empty to equal to it
507 Node eqccSingleton
= d_state
.getSingletonEqClass(eqcc
);
508 if (!eqccSingleton
.isNull())
510 bool eq_parent
= false;
511 std::vector
<Node
> exps
;
512 d_state
.addEqualityToExp(cpk
, eqccSingleton
, exps
);
513 if (d_state
.areDisequal(n
, emp_set
))
515 exps
.push_back(n
.eqNode(emp_set
).negate());
520 const std::map
<Node
, Node
>& pmemsE
= d_state
.getMembers(eqc
);
523 Node pmem
= pmemsE
.begin()->second
;
524 exps
.push_back(pmem
);
525 d_state
.addEqualityToExp(n
, pmem
[1], exps
);
529 // must be equal to parent
532 Node conc
= n
.eqNode(cpk
);
533 d_im
.assertInference(conc
, exps
, "cg_par_sing");
534 d_im
.flushPendingLemmas();
539 Trace("sets-nf") << "Split empty : " << n
<< std::endl
;
540 d_im
.split(n
.eqNode(emp_set
), 1);
542 Assert(d_im
.hasProcessed());
548 for (unsigned l
= 0, numcpn
= d_card_parent
[n
].size(); l
< numcpn
; l
++)
550 Node cpnl
= d_card_parent
[n
][l
];
555 Trace("sets-debug") << " parents " << l
<< " and " << k
556 << " are equal, ids = " << card_parent_ids
[l
]
557 << " " << card_parent_ids
[k
] << std::endl
;
559 if (n
.getKind() != INTERSECTION
)
563 Assert(card_parent_ids
[l
] != 2);
564 std::vector
<Node
> conc
;
565 if (card_parent_ids
[k
] == 2)
567 // intersection is equal to other parent
568 unsigned pid
= 1 - card_parent_ids
[l
];
569 if (!d_state
.areEqual(n
[pid
], n
))
572 << " one of them is union, make equal to other..."
574 conc
.push_back(n
[pid
].eqNode(n
));
579 if (!d_state
.areEqual(cpk
, n
))
582 << " neither is union, make equal to one parent..."
584 // intersection is equal to one of the parents
585 conc
.push_back(cpk
.eqNode(n
));
588 d_im
.assertInference(conc
, cpk
.eqNode(cpnl
), "cg_pareq");
589 d_im
.flushPendingLemmas();
590 if (d_im
.hasProcessed())
597 d_card_parent
[n
].push_back(eqcc
);
601 // now recurse on parents (to ensure their normal will be computed after
603 exp
.push_back(eqc
.eqNode(n
));
604 for (const Node
& cpnc
: d_card_parent
[n
])
606 checkCardCyclesRec(cpnc
, curr
, exp
);
607 if (d_im
.hasProcessed())
615 // parents now processed, can add to ordered list
616 d_oSetEqc
.push_back(eqc
);
619 void CardinalityExtension::checkNormalForms(std::vector
<Node
>& intro_sets
)
621 Trace("sets") << "Check normal forms..." << std::endl
;
622 // now, build normal form for each equivalence class
623 // d_oSetEqc is now sorted such that for each d_oSetEqc[i], d_oSetEqc[j],
624 // if d_oSetEqc[i] is a strict syntactic subterm of d_oSetEqc[j], then i<j.
627 for (int i
= (int)(d_oSetEqc
.size() - 1); i
>= 0; i
--)
629 checkNormalForm(d_oSetEqc
[i
], intro_sets
);
630 if (d_im
.hasProcessed() || !intro_sets
.empty())
635 Trace("sets") << "Done check normal forms" << std::endl
;
638 void CardinalityExtension::checkNormalForm(Node eqc
,
639 std::vector
<Node
>& intro_sets
)
641 TypeNode tn
= eqc
.getType();
642 Trace("sets") << "Compute normal form for " << eqc
<< std::endl
;
643 Trace("sets-nf") << "Compute N " << eqc
<< "..." << std::endl
;
644 if (eqc
== d_state
.getEmptySetEqClass(tn
))
647 Trace("sets-nf") << "----> N " << eqc
<< " => {}" << std::endl
;
650 // flat/normal forms are sets of equivalence classes
652 std::vector
<Node
> comps
;
653 std::map
<Node
, std::map
<Node
, std::vector
<Node
> > >::iterator it
=
655 if (it
!= d_ff
.end())
657 for (std::pair
<const Node
, std::vector
<Node
> >& itf
: it
->second
)
659 std::sort(itf
.second
.begin(), itf
.second
.end());
666 comps
.push_back(itf
.first
);
668 Trace("sets-nf") << " F " << itf
.first
<< " : " << itf
.second
670 Trace("sets-nf-debug") << " ...";
671 d_state
.debugPrintSet(itf
.first
, "sets-nf-debug");
672 Trace("sets-nf-debug") << std::endl
;
677 Trace("sets-nf") << "(no flat forms)" << std::endl
;
679 std::map
<Node
, std::vector
<Node
> >& ffeqc
= d_ff
[eqc
];
680 Assert(d_nf
.find(eqc
) == d_nf
.end());
681 std::vector
<Node
>& nfeqc
= d_nf
[eqc
];
682 NodeManager
* nm
= NodeManager::currentNM();
684 Node emp_set
= d_state
.getEmptySet(tn
);
687 for (unsigned j
= 0, csize
= comps
.size(); j
< csize
; j
++)
692 c
.push_back(comps
[j
]);
693 std::vector
<Node
> only
[2];
694 std::vector
<Node
> common
;
695 Trace("sets-nf-debug") << "Compare venn regions of " << base
<< " vs "
696 << comps
[j
] << std::endl
;
697 unsigned k
[2] = {0, 0};
698 while (k
[0] < ffeqc
[c
[0]].size() || k
[1] < ffeqc
[c
[1]].size())
701 for (unsigned e
= 0; e
< 2; e
++)
703 if (k
[e
] == ffeqc
[c
[e
]].size())
705 for (; k
[1 - e
] < ffeqc
[c
[1 - e
]].size(); ++k
[1 - e
])
707 only
[1 - e
].push_back(ffeqc
[c
[1 - e
]][k
[1 - e
]]);
714 if (ffeqc
[c
[0]][k
[0]] == ffeqc
[c
[1]][k
[1]])
716 common
.push_back(ffeqc
[c
[0]][k
[0]]);
720 else if (ffeqc
[c
[0]][k
[0]] < ffeqc
[c
[1]][k
[1]])
722 only
[0].push_back(ffeqc
[c
[0]][k
[0]]);
727 only
[1].push_back(ffeqc
[c
[1]][k
[1]]);
732 if (!only
[0].empty() || !only
[1].empty())
734 if (Trace
.isOn("sets-nf-debug"))
736 Trace("sets-nf-debug") << "Unique venn regions : " << std::endl
;
737 for (unsigned e
= 0; e
< 2; e
++)
739 Trace("sets-nf-debug") << " " << c
[e
] << " : { ";
740 for (unsigned l
= 0; l
< only
[e
].size(); l
++)
744 Trace("sets-nf-debug") << ", ";
746 Trace("sets-nf-debug") << "[" << only
[e
][l
] << "]";
748 Trace("sets-nf-debug") << " }" << std::endl
;
751 // try to make one empty, prefer the unique ones first
752 for (unsigned e
= 0; e
< 3; e
++)
754 unsigned sz
= e
== 2 ? common
.size() : only
[e
].size();
755 for (unsigned l
= 0; l
< sz
; l
++)
757 Node r
= e
== 2 ? common
[l
] : only
[e
][l
];
758 Trace("sets-nf-debug") << "Try split empty : " << r
<< std::endl
;
759 Trace("sets-nf-debug") << " actual : ";
760 d_state
.debugPrintSet(r
, "sets-nf-debug");
761 Trace("sets-nf-debug") << std::endl
;
762 Assert(!d_state
.areEqual(r
, emp_set
));
763 if (!d_state
.areDisequal(r
, emp_set
) && !d_state
.hasMembers(r
))
765 // guess that its equal empty if it has no explicit members
766 Trace("sets-nf") << " Split empty : " << r
<< std::endl
;
767 Trace("sets-nf") << "Actual Split : ";
768 d_state
.debugPrintSet(r
, "sets-nf");
769 Trace("sets-nf") << std::endl
;
770 d_im
.split(r
.eqNode(emp_set
), 1);
771 Assert(d_im
.hasProcessed());
776 for (const Node
& o0
: only
[0])
778 for (const Node
& o1
: only
[1])
780 bool disjoint
= false;
781 Trace("sets-nf-debug")
782 << "Try split " << o0
<< " against " << o1
<< std::endl
;
784 for (unsigned e
= 0; e
< 2; e
++)
786 Node r1
= e
== 0 ? o0
: o1
;
787 Node r2
= e
== 0 ? o1
: o0
;
788 // check if their intersection exists modulo equality
789 Node r1r2i
= d_state
.getBinaryOpTerm(INTERSECTION
, r1
, r2
);
792 Trace("sets-nf-debug")
793 << "Split term already exists, but not in cardinality "
795 << r1r2i
<< ", should be empty." << std::endl
;
796 // their intersection is empty (probably?)
797 // e.g. these are two disjoint venn regions, proceed to next
799 Assert(d_state
.areEqual(emp_set
, r1r2i
));
806 // simply introduce their intersection
808 Node kca
= d_state
.getProxy(o0
);
809 Node kcb
= d_state
.getProxy(o1
);
811 Rewriter::rewrite(nm
->mkNode(INTERSECTION
, kca
, kcb
));
812 Trace("sets-nf") << " Intro split : " << o0
<< " against " << o1
813 << ", term is " << intro
<< std::endl
;
814 intro_sets
.push_back(intro
);
815 Assert(!d_ee
.hasTerm(intro
));
820 // should never get here
826 // normal form is flat form of base
827 nfeqc
.insert(nfeqc
.end(), ffeqc
[base
].begin(), ffeqc
[base
].end());
828 Trace("sets-nf") << "----> N " << eqc
<< " => F " << base
<< std::endl
;
832 Trace("sets-nf") << "failed to build N " << eqc
<< std::endl
;
837 // must ensure disequal from empty
838 if (!eqc
.isConst() && !d_state
.areDisequal(eqc
, emp_set
)
839 && !d_state
.hasMembers(eqc
))
841 Trace("sets-nf-debug") << "Split on leaf " << eqc
<< std::endl
;
842 d_im
.split(eqc
.eqNode(emp_set
));
847 // normal form is this equivalence class
848 nfeqc
.push_back(eqc
);
849 Trace("sets-nf") << "----> N " << eqc
<< " => { " << eqc
<< " }"
855 Assert(d_im
.hasProcessed());
858 // Send to parents (a parent is a set that contains a term in this equivalence
859 // class as a direct child).
860 const std::vector
<Node
>& nvsets
= d_state
.getNonVariableSets(eqc
);
863 // no non-variable sets
866 std::map
<Node
, std::map
<Node
, bool> > parents_proc
;
867 for (const Node
& n
: nvsets
)
869 Trace("sets-nf-debug") << "Carry nf for term " << n
<< std::endl
;
870 if (d_card_parent
[n
].empty())
875 Assert(d_localBase
.find(n
) != d_localBase
.end());
876 Node cbase
= d_localBase
[n
];
877 Trace("sets-nf-debug") << "Card base is " << cbase
<< std::endl
;
878 for (const Node
& p
: d_card_parent
[n
])
880 Trace("sets-nf-debug") << "Check parent " << p
<< std::endl
;
881 if (parents_proc
[cbase
].find(p
) != parents_proc
[cbase
].end())
883 Trace("sets-nf-debug") << "..already processed parent " << p
<< " for "
884 << cbase
<< std::endl
;
887 parents_proc
[cbase
][p
] = true;
888 Trace("sets-nf-debug") << "Carry nf to parent ( " << cbase
<< ", [" << p
889 << "] ), from " << n
<< "..." << std::endl
;
891 std::vector
<Node
>& ffpc
= d_ff
[p
][cbase
];
892 for (const Node
& nfeqci
: nfeqc
)
894 if (std::find(ffpc
.begin(), ffpc
.end(), nfeqci
) == ffpc
.end())
896 ffpc
.insert(ffpc
.end(), nfeqc
.begin(), nfeqc
.end());
900 // if it is a duplicate venn region, it must be empty since it is
901 // coming from syntactically disjoint siblings
908 void CardinalityExtension::checkMinCard()
910 NodeManager
* nm
= NodeManager::currentNM();
911 const std::vector
<Node
>& setEqc
= d_state
.getSetsEqClasses();
912 for (int i
= (int)(setEqc
.size() - 1); i
>= 0; i
--)
914 Node eqc
= setEqc
[i
];
915 TypeNode tn
= eqc
.getType().getSetElementType();
916 if (d_t_card_enabled
.find(tn
) == d_t_card_enabled
.end())
918 // cardinality is not enabled for this type, skip
921 // get members in class
922 const std::map
<Node
, Node
>& pmemsE
= d_state
.getMembers(eqc
);
925 // no members, trivial
928 std::vector
<Node
> exp
;
929 std::vector
<Node
> members
;
931 std::map
<Node
, Node
>::iterator it
= d_eqc_to_card_term
.find(eqc
);
932 if (it
!= d_eqc_to_card_term
.end())
934 cardTerm
= it
->second
;
938 cardTerm
= nm
->mkNode(CARD
, eqc
);
940 for (const std::pair
<const Node
, Node
>& itmm
: pmemsE
)
942 members
.push_back(itmm
.first
);
943 exp
.push_back(nm
->mkNode(MEMBER
, itmm
.first
, cardTerm
[0]));
945 if (members
.size() > 1)
947 exp
.push_back(nm
->mkNode(DISTINCT
, members
));
949 if (!members
.empty())
952 nm
->mkNode(GEQ
, cardTerm
, nm
->mkConst(Rational(members
.size())));
953 Node expn
= exp
.size() == 1 ? exp
[0] : nm
->mkNode(AND
, exp
);
954 d_im
.assertInference(conc
, expn
, "mincard", 1);
958 d_im
.flushPendingLemmas();
961 bool CardinalityExtension::isModelValueBasic(Node eqc
)
963 return d_nf
[eqc
].size() == 1 && d_nf
[eqc
][0] == eqc
;
966 void CardinalityExtension::mkModelValueElementsFor(
969 std::vector
<Node
>& els
,
970 const std::map
<Node
, Node
>& mvals
,
973 TypeNode elementType
= eqc
.getType().getSetElementType();
974 if (isModelValueBasic(eqc
))
976 std::map
<Node
, Node
>::iterator it
= d_eqc_to_card_term
.find(eqc
);
977 if (it
!= d_eqc_to_card_term
.end())
979 // slack elements from cardinality value
980 Node v
= val
.getModelValue(it
->second
);
981 Trace("sets-model") << "Cardinality of " << eqc
<< " is " << v
983 Assert(v
.getConst
<Rational
>() <= LONG_MAX
)
984 << "Exceeded LONG_MAX in sets model";
985 unsigned vu
= v
.getConst
<Rational
>().getNumerator().toUnsignedInt();
986 Assert(els
.size() <= vu
);
987 NodeManager
* nm
= NodeManager::currentNM();
988 if (elementType
.isInterpretedFinite())
990 // get all members of this finite type
991 collectFiniteTypeSetElements(model
);
993 while (els
.size() < vu
)
995 if (elementType
.isInterpretedFinite())
997 // At this point we are sure the formula is satisfiable and all
998 // cardinality constraints are satisfied. Since this type is finite,
999 // there is only one single cardinality graph for all sets of this
1000 // type because the universe cardinality constraint has been added by
1001 // CardinalityExtension::checkFiniteType. This means we have enough
1002 // slack elements of this finite type for all disjoint leaves in the
1003 // cardinality graph. Therefore we can safely add new distinct slack
1004 // elements for the leaves without worrying about conflicts with the
1005 // current members of this finite type.
1007 Node slack
= nm
->mkSkolem("slack", elementType
);
1008 Node singleton
= nm
->mkNode(SINGLETON
, slack
);
1009 els
.push_back(singleton
);
1010 d_finite_type_slack_elements
[elementType
].push_back(slack
);
1011 Trace("sets-model") << "Added slack element " << slack
<< " to set "
1012 << eqc
<< std::endl
;
1017 nm
->mkNode(SINGLETON
, nm
->mkSkolem("msde", elementType
)));
1023 Trace("sets-model") << "No slack elements for " << eqc
<< std::endl
;
1028 Trace("sets-model") << "Build value for " << eqc
1029 << " based on normal form, size = " << d_nf
[eqc
].size()
1031 // it is union of venn regions
1032 for (unsigned j
= 0; j
< d_nf
[eqc
].size(); j
++)
1034 std::map
<Node
, Node
>::const_iterator itm
= mvals
.find(d_nf
[eqc
][j
]);
1035 if (itm
!= mvals
.end())
1037 els
.push_back(itm
->second
);
1047 void CardinalityExtension::collectFiniteTypeSetElements(TheoryModel
* model
)
1049 if (d_finite_type_constants_processed
)
1053 for (const Node
& set
: getOrderedSetsEqClasses())
1055 if (!set
.getType().isInterpretedFinite())
1059 if (!isModelValueBasic(set
))
1061 // only consider leaves in the cardinality graph
1064 for (const std::pair
<const Node
, Node
>& pair
: d_state
.getMembers(set
))
1066 Node member
= pair
.first
;
1067 Node modelRepresentative
= model
->getRepresentative(member
);
1068 std::vector
<Node
>& elements
= d_finite_type_elements
[member
.getType()];
1069 if (std::find(elements
.begin(), elements
.end(), modelRepresentative
)
1072 elements
.push_back(modelRepresentative
);
1076 d_finite_type_constants_processed
= true;
1079 const std::vector
<Node
>& CardinalityExtension::getFiniteTypeMembers(
1082 return d_finite_type_elements
[typeNode
];
1086 } // namespace theory