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());
87 NodeManager
* nm
= NodeManager::currentNM();
88 // get the universe set (as univset (Set t))
89 Node univ
= d_state
.getUnivSet(nm
->mkSetType(t
));
90 std::map
<Node
, Node
>::iterator it
= d_univProxy
.find(univ
);
92 if (it
== d_univProxy
.end())
94 // Force cvc4 to build the cardinality graph for the universe set
95 proxy
= d_state
.getProxy(univ
);
96 d_univProxy
[univ
] = proxy
;
103 // get all equivalent classes of type t
104 vector
<Node
> representatives
= d_state
.getSetsEqClasses(t
);
105 // get the cardinality of the finite type t
106 Cardinality card
= t
.getCardinality();
107 if (!card
.isFinite())
109 // TODO (#1123): support uninterpreted sorts with --finite-model-find
110 std::stringstream message
;
111 message
<< "The cardinality " << card
<< " of the finite type " << t
112 << " is not supported yet." << endl
;
113 Assert(false) << message
.str().c_str();
116 Node typeCardinality
= nm
->mkConst(Rational(card
.getFiniteCardinality()));
118 Node cardUniv
= nm
->mkNode(kind::CARD
, proxy
);
119 Node leq
= nm
->mkNode(kind::LEQ
, cardUniv
, typeCardinality
);
121 // (=> true (<= (card (as univset t)) cardUniv)
122 if (!d_state
.isEntailed(leq
, true))
124 d_im
.assertInference(leq
, d_true
, "finite type cardinality", 1);
127 // add subset lemmas for sets, and membership lemmas for negative members
128 for (Node
& representative
: representatives
)
130 // the universe set is a subset of itself
131 if (representative
!= d_ee
.getRepresentative(univ
))
133 // here we only add representatives with variables to avoid adding
134 // infinite equivalent generated terms to the cardinality graph
135 Node variable
= d_state
.getVariableSet(representative
);
136 if (variable
.isNull())
141 // (=> true (subset representative (as univset t))
142 Node subset
= nm
->mkNode(kind::SUBSET
, variable
, proxy
);
143 // subset terms are rewritten as union terms: (subset A B) implies (=
145 subset
= Rewriter::rewrite(subset
);
146 if (!d_state
.isEntailed(subset
, true))
148 d_im
.assertInference(subset
, d_true
, "univset is a super set", 1);
151 // negative members are members in the universe set
152 const std::map
<Node
, Node
>& negativeMembers
=
153 d_state
.getNegativeMembers(representative
);
155 for (const std::pair
<Node
, Node
>& negativeMember
: negativeMembers
)
157 Node member
= nm
->mkNode(MEMBER
, negativeMember
.first
, univ
);
158 // negativeMember.second is the reason for the negative membership and
159 // has kind MEMBER. So we specify the negation as the reason for the
160 // negative membership lemma
161 Node notMember
= nm
->mkNode(NOT
, negativeMember
.second
);
163 // (not (member negativeMember representative)))
164 // (member negativeMember (as univset t)))
165 d_im
.assertInference(
166 member
, notMember
, "negative members are in the universe", 1);
172 void CardinalityExtension::check()
176 if (d_im
.hasProcessed())
181 if (d_im
.hasProcessed())
186 if (d_im
.hasProcessed())
190 // The last step will either do nothing (in which case we are SAT), or request
191 // that a new set term is introduced.
192 std::vector
<Node
> intro_sets
;
193 checkNormalForms(intro_sets
);
194 if (intro_sets
.empty())
198 Assert(intro_sets
.size() == 1);
199 Trace("sets-intro") << "Introduce term : " << intro_sets
[0] << std::endl
;
200 Trace("sets-intro") << " Actual Intro : ";
201 d_state
.debugPrintSet(intro_sets
[0], "sets-nf");
202 Trace("sets-nf") << std::endl
;
203 Node k
= d_state
.getProxy(intro_sets
[0]);
204 AlwaysAssert(!k
.isNull());
207 void CardinalityExtension::checkRegister()
209 Trace("sets") << "Cardinality graph..." << std::endl
;
210 NodeManager
* nm
= NodeManager::currentNM();
211 // first, ensure cardinality relationships are added as lemmas for all
212 // non-basic set terms
213 const std::vector
<Node
>& setEqc
= d_state
.getSetsEqClasses();
214 for (const Node
& eqc
: setEqc
)
216 const std::vector
<Node
>& nvsets
= d_state
.getNonVariableSets(eqc
);
217 for (Node n
: nvsets
)
219 if (!d_state
.isCongruent(n
))
221 // if setminus, do for intersection instead
222 if (n
.getKind() == SETMINUS
)
224 n
= Rewriter::rewrite(nm
->mkNode(INTERSECTION
, n
[0], n
[1]));
226 registerCardinalityTerm(n
);
230 Trace("sets") << "Done cardinality graph" << std::endl
;
233 void CardinalityExtension::registerCardinalityTerm(Node n
)
235 TypeNode tnc
= n
.getType().getSetElementType();
236 if (d_t_card_enabled
.find(tnc
) == d_t_card_enabled
.end())
238 // if no cardinality constraints for sets of this type, we can ignore
241 if (d_card_processed
.find(n
) != d_card_processed
.end())
246 d_card_processed
.insert(n
);
247 NodeManager
* nm
= NodeManager::currentNM();
248 Trace("sets-card") << "Cardinality lemmas for " << n
<< " : " << std::endl
;
249 std::vector
<Node
> cterms
;
250 if (n
.getKind() == INTERSECTION
)
252 for (unsigned e
= 0; e
< 2; e
++)
254 Node s
= nm
->mkNode(SETMINUS
, n
[e
], n
[1 - e
]);
257 Node pos_lem
= nm
->mkNode(GEQ
, nm
->mkNode(CARD
, n
), d_zero
);
258 d_im
.assertInference(pos_lem
, d_emp_exp
, "pcard", 1);
264 for (unsigned k
= 0, csize
= cterms
.size(); k
< csize
; k
++)
267 Node nk
= d_state
.getProxy(nn
);
268 Node pos_lem
= nm
->mkNode(GEQ
, nm
->mkNode(CARD
, nk
), d_zero
);
269 d_im
.assertInference(pos_lem
, d_emp_exp
, "pcard", 1);
272 Node lem
= nm
->mkNode(EQUAL
, nm
->mkNode(CARD
, nk
), nm
->mkNode(CARD
, nn
));
273 lem
= Rewriter::rewrite(lem
);
274 Trace("sets-card") << " " << k
<< " : " << lem
<< std::endl
;
275 d_im
.assertInference(lem
, d_emp_exp
, "card", 1);
278 d_im
.flushPendingLemmas();
281 void CardinalityExtension::checkCardCycles()
283 Trace("sets") << "Check cardinality cycles..." << std::endl
;
284 // build order of equivalence classes, also build cardinality graph
285 const std::vector
<Node
>& setEqc
= d_state
.getSetsEqClasses();
287 d_card_parent
.clear();
288 for (const Node
& s
: setEqc
)
290 std::vector
<Node
> curr
;
291 std::vector
<Node
> exp
;
292 checkCardCyclesRec(s
, curr
, exp
);
293 if (d_im
.hasProcessed())
298 Trace("sets") << "Done check cardinality cycles" << std::endl
;
301 void CardinalityExtension::checkCardCyclesRec(Node eqc
,
302 std::vector
<Node
>& curr
,
303 std::vector
<Node
>& exp
)
305 NodeManager
* nm
= NodeManager::currentNM();
306 if (std::find(curr
.begin(), curr
.end(), eqc
) != curr
.end())
308 Trace("sets-debug") << "Found venn region loop..." << std::endl
;
311 // all regions must be equal
312 std::vector
<Node
> conc
;
313 for (const Node
& cc
: curr
)
315 conc
.push_back(curr
[0].eqNode(cc
));
317 Node fact
= conc
.size() == 1 ? conc
[0] : nm
->mkNode(AND
, conc
);
318 d_im
.assertInference(fact
, exp
, "card_cycle");
319 d_im
.flushPendingLemmas();
323 // should be guaranteed based on not exploring equal parents
328 if (std::find(d_oSetEqc
.begin(), d_oSetEqc
.end(), eqc
) != d_oSetEqc
.end())
333 const std::vector
<Node
>& nvsets
= d_state
.getNonVariableSets(eqc
);
336 // no non-variable sets, trivial
337 d_oSetEqc
.push_back(eqc
);
341 TypeNode tn
= eqc
.getType();
342 bool is_empty
= eqc
== d_state
.getEmptySetEqClass(tn
);
343 Node emp_set
= d_state
.getEmptySet(tn
);
344 for (const Node
& n
: nvsets
)
346 Kind nk
= n
.getKind();
347 if (nk
!= INTERSECTION
&& nk
!= SETMINUS
)
351 Trace("sets-debug") << "Build cardinality parents for " << n
<< "..."
353 std::vector
<Node
> sib
;
354 unsigned true_sib
= 0;
355 if (n
.getKind() == INTERSECTION
)
358 for (unsigned e
= 0; e
< 2; e
++)
360 Node sm
= Rewriter::rewrite(nm
->mkNode(SETMINUS
, n
[e
], n
[1 - e
]));
367 Node si
= Rewriter::rewrite(nm
->mkNode(INTERSECTION
, n
[0], n
[1]));
370 Node osm
= Rewriter::rewrite(nm
->mkNode(SETMINUS
, n
[1], n
[0]));
374 Node u
= Rewriter::rewrite(nm
->mkNode(UNION
, n
[0], n
[1]));
375 if (!d_ee
.hasTerm(u
))
379 unsigned n_parents
= true_sib
+ (u
.isNull() ? 0 : 1);
380 // if this set is empty
383 Assert(d_state
.areEqual(n
, emp_set
));
384 Trace("sets-debug") << " empty, parents equal siblings" << std::endl
;
385 std::vector
<Node
> conc
;
386 // parent equal siblings
387 for (unsigned e
= 0; e
< true_sib
; e
++)
389 if (d_ee
.hasTerm(sib
[e
]) && !d_state
.areEqual(n
[e
], sib
[e
]))
391 conc
.push_back(n
[e
].eqNode(sib
[e
]));
394 d_im
.assertInference(conc
, n
.eqNode(emp_set
), "cg_emp");
395 d_im
.flushPendingLemmas();
396 if (d_im
.hasProcessed())
402 // justify why there is no edge to parents (necessary?)
403 for (unsigned e
= 0; e
< n_parents
; e
++)
405 Node p
= (e
== true_sib
) ? u
: n
[e
];
410 std::vector
<Node
> card_parents
;
411 std::vector
<int> card_parent_ids
;
412 // check if equal to a parent
413 for (unsigned e
= 0; e
< n_parents
; e
++)
415 Trace("sets-debug") << " check parent " << e
<< "/" << n_parents
417 bool is_union
= e
== true_sib
;
418 Node p
= (e
== true_sib
) ? u
: n
[e
];
419 Trace("sets-debug") << " check relation to parent " << p
420 << ", isu=" << is_union
<< "..." << std::endl
;
421 // if parent is empty
422 if (d_state
.areEqual(p
, emp_set
))
424 Trace("sets-debug") << " it is empty..." << std::endl
;
425 Assert(!d_state
.areEqual(n
, emp_set
));
426 d_im
.assertInference(n
.eqNode(emp_set
), p
.eqNode(emp_set
), "cg_emppar");
427 d_im
.flushPendingLemmas();
428 if (d_im
.hasProcessed())
432 // if we are equal to a parent
434 else if (d_state
.areEqual(p
, n
))
436 Trace("sets-debug") << " it is equal to this..." << std::endl
;
437 std::vector
<Node
> conc
;
438 std::vector
<int> sib_emp_indices
;
441 for (unsigned s
= 0; s
< sib
.size(); s
++)
443 sib_emp_indices
.push_back(s
);
448 sib_emp_indices
.push_back(e
);
450 // sibling(s) are empty
451 for (unsigned si
: sib_emp_indices
)
453 if (!d_state
.areEqual(sib
[si
], emp_set
))
455 conc
.push_back(sib
[si
].eqNode(emp_set
));
460 << "Sibling " << sib
[si
] << " is already empty." << std::endl
;
463 if (!is_union
&& nk
== INTERSECTION
&& !u
.isNull())
465 // union is equal to other parent
466 if (!d_state
.areEqual(u
, n
[1 - e
]))
468 conc
.push_back(u
.eqNode(n
[1 - e
]));
472 << "...derived " << conc
.size() << " conclusions" << std::endl
;
473 d_im
.assertInference(conc
, n
.eqNode(p
), "cg_eqpar");
474 d_im
.flushPendingLemmas();
475 if (d_im
.hasProcessed())
482 Trace("sets-cdg") << "Card graph : " << n
<< " -> " << p
<< std::endl
;
483 // otherwise, we a syntactic subset of p
484 card_parents
.push_back(p
);
485 card_parent_ids
.push_back(is_union
? 2 : e
);
488 Assert(d_card_parent
[n
].empty());
489 Trace("sets-debug") << "get parent representatives..." << std::endl
;
490 // for each parent, take their representatives
491 for (unsigned k
= 0, numcp
= card_parents
.size(); k
< numcp
; k
++)
493 Node cpk
= card_parents
[k
];
494 Node eqcc
= d_ee
.getRepresentative(cpk
);
495 Trace("sets-debug") << "Check card parent " << k
<< "/"
496 << card_parents
.size() << std::endl
;
498 // if parent is singleton, then we should either be empty to equal to it
499 Node eqccSingleton
= d_state
.getSingletonEqClass(eqcc
);
500 if (!eqccSingleton
.isNull())
502 bool eq_parent
= false;
503 std::vector
<Node
> exps
;
504 d_state
.addEqualityToExp(cpk
, eqccSingleton
, exps
);
505 if (d_state
.areDisequal(n
, emp_set
))
507 exps
.push_back(n
.eqNode(emp_set
).negate());
512 const std::map
<Node
, Node
>& pmemsE
= d_state
.getMembers(eqc
);
515 Node pmem
= pmemsE
.begin()->second
;
516 exps
.push_back(pmem
);
517 d_state
.addEqualityToExp(n
, pmem
[1], exps
);
521 // must be equal to parent
524 Node conc
= n
.eqNode(cpk
);
525 d_im
.assertInference(conc
, exps
, "cg_par_sing");
526 d_im
.flushPendingLemmas();
531 Trace("sets-nf") << "Split empty : " << n
<< std::endl
;
532 d_im
.split(n
.eqNode(emp_set
), 1);
534 Assert(d_im
.hasProcessed());
540 for (unsigned l
= 0, numcpn
= d_card_parent
[n
].size(); l
< numcpn
; l
++)
542 Node cpnl
= d_card_parent
[n
][l
];
547 Trace("sets-debug") << " parents " << l
<< " and " << k
548 << " are equal, ids = " << card_parent_ids
[l
]
549 << " " << card_parent_ids
[k
] << std::endl
;
551 if (n
.getKind() != INTERSECTION
)
555 Assert(card_parent_ids
[l
] != 2);
556 std::vector
<Node
> conc
;
557 if (card_parent_ids
[k
] == 2)
559 // intersection is equal to other parent
560 unsigned pid
= 1 - card_parent_ids
[l
];
561 if (!d_state
.areEqual(n
[pid
], n
))
564 << " one of them is union, make equal to other..."
566 conc
.push_back(n
[pid
].eqNode(n
));
571 if (!d_state
.areEqual(cpk
, n
))
574 << " neither is union, make equal to one parent..."
576 // intersection is equal to one of the parents
577 conc
.push_back(cpk
.eqNode(n
));
580 d_im
.assertInference(conc
, cpk
.eqNode(cpnl
), "cg_pareq");
581 d_im
.flushPendingLemmas();
582 if (d_im
.hasProcessed())
589 d_card_parent
[n
].push_back(eqcc
);
593 // now recurse on parents (to ensure their normal will be computed after
595 exp
.push_back(eqc
.eqNode(n
));
596 for (const Node
& cpnc
: d_card_parent
[n
])
598 checkCardCyclesRec(cpnc
, curr
, exp
);
599 if (d_im
.hasProcessed())
607 // parents now processed, can add to ordered list
608 d_oSetEqc
.push_back(eqc
);
611 void CardinalityExtension::checkNormalForms(std::vector
<Node
>& intro_sets
)
613 Trace("sets") << "Check normal forms..." << std::endl
;
614 // now, build normal form for each equivalence class
615 // d_oSetEqc is now sorted such that for each d_oSetEqc[i], d_oSetEqc[j],
616 // if d_oSetEqc[i] is a strict syntactic subterm of d_oSetEqc[j], then i<j.
619 for (int i
= (int)(d_oSetEqc
.size() - 1); i
>= 0; i
--)
621 checkNormalForm(d_oSetEqc
[i
], intro_sets
);
622 if (d_im
.hasProcessed() || !intro_sets
.empty())
627 Trace("sets") << "Done check normal forms" << std::endl
;
630 void CardinalityExtension::checkNormalForm(Node eqc
,
631 std::vector
<Node
>& intro_sets
)
633 TypeNode tn
= eqc
.getType();
634 Trace("sets") << "Compute normal form for " << eqc
<< std::endl
;
635 Trace("sets-nf") << "Compute N " << eqc
<< "..." << std::endl
;
636 if (eqc
== d_state
.getEmptySetEqClass(tn
))
639 Trace("sets-nf") << "----> N " << eqc
<< " => {}" << std::endl
;
642 // flat/normal forms are sets of equivalence classes
644 std::vector
<Node
> comps
;
645 std::map
<Node
, std::map
<Node
, std::vector
<Node
> > >::iterator it
=
647 if (it
!= d_ff
.end())
649 for (std::pair
<const Node
, std::vector
<Node
> >& itf
: it
->second
)
651 std::sort(itf
.second
.begin(), itf
.second
.end());
658 comps
.push_back(itf
.first
);
660 Trace("sets-nf") << " F " << itf
.first
<< " : " << itf
.second
662 Trace("sets-nf-debug") << " ...";
663 d_state
.debugPrintSet(itf
.first
, "sets-nf-debug");
664 Trace("sets-nf-debug") << std::endl
;
669 Trace("sets-nf") << "(no flat forms)" << std::endl
;
671 std::map
<Node
, std::vector
<Node
> >& ffeqc
= d_ff
[eqc
];
672 Assert(d_nf
.find(eqc
) == d_nf
.end());
673 std::vector
<Node
>& nfeqc
= d_nf
[eqc
];
674 NodeManager
* nm
= NodeManager::currentNM();
676 Node emp_set
= d_state
.getEmptySet(tn
);
679 for (unsigned j
= 0, csize
= comps
.size(); j
< csize
; j
++)
684 c
.push_back(comps
[j
]);
685 std::vector
<Node
> only
[2];
686 std::vector
<Node
> common
;
687 Trace("sets-nf-debug") << "Compare venn regions of " << base
<< " vs "
688 << comps
[j
] << std::endl
;
689 unsigned k
[2] = {0, 0};
690 while (k
[0] < ffeqc
[c
[0]].size() || k
[1] < ffeqc
[c
[1]].size())
693 for (unsigned e
= 0; e
< 2; e
++)
695 if (k
[e
] == ffeqc
[c
[e
]].size())
697 for (; k
[1 - e
] < ffeqc
[c
[1 - e
]].size(); ++k
[1 - e
])
699 only
[1 - e
].push_back(ffeqc
[c
[1 - e
]][k
[1 - e
]]);
706 if (ffeqc
[c
[0]][k
[0]] == ffeqc
[c
[1]][k
[1]])
708 common
.push_back(ffeqc
[c
[0]][k
[0]]);
712 else if (ffeqc
[c
[0]][k
[0]] < ffeqc
[c
[1]][k
[1]])
714 only
[0].push_back(ffeqc
[c
[0]][k
[0]]);
719 only
[1].push_back(ffeqc
[c
[1]][k
[1]]);
724 if (!only
[0].empty() || !only
[1].empty())
726 if (Trace
.isOn("sets-nf-debug"))
728 Trace("sets-nf-debug") << "Unique venn regions : " << std::endl
;
729 for (unsigned e
= 0; e
< 2; e
++)
731 Trace("sets-nf-debug") << " " << c
[e
] << " : { ";
732 for (unsigned l
= 0; l
< only
[e
].size(); l
++)
736 Trace("sets-nf-debug") << ", ";
738 Trace("sets-nf-debug") << "[" << only
[e
][l
] << "]";
740 Trace("sets-nf-debug") << " }" << std::endl
;
743 // try to make one empty, prefer the unique ones first
744 for (unsigned e
= 0; e
< 3; e
++)
746 unsigned sz
= e
== 2 ? common
.size() : only
[e
].size();
747 for (unsigned l
= 0; l
< sz
; l
++)
749 Node r
= e
== 2 ? common
[l
] : only
[e
][l
];
750 Trace("sets-nf-debug") << "Try split empty : " << r
<< std::endl
;
751 Trace("sets-nf-debug") << " actual : ";
752 d_state
.debugPrintSet(r
, "sets-nf-debug");
753 Trace("sets-nf-debug") << std::endl
;
754 Assert(!d_state
.areEqual(r
, emp_set
));
755 if (!d_state
.areDisequal(r
, emp_set
) && !d_state
.hasMembers(r
))
757 // guess that its equal empty if it has no explicit members
758 Trace("sets-nf") << " Split empty : " << r
<< std::endl
;
759 Trace("sets-nf") << "Actual Split : ";
760 d_state
.debugPrintSet(r
, "sets-nf");
761 Trace("sets-nf") << std::endl
;
762 d_im
.split(r
.eqNode(emp_set
), 1);
763 Assert(d_im
.hasProcessed());
768 for (const Node
& o0
: only
[0])
770 for (const Node
& o1
: only
[1])
772 bool disjoint
= false;
773 Trace("sets-nf-debug")
774 << "Try split " << o0
<< " against " << o1
<< std::endl
;
776 for (unsigned e
= 0; e
< 2; e
++)
778 Node r1
= e
== 0 ? o0
: o1
;
779 Node r2
= e
== 0 ? o1
: o0
;
780 // check if their intersection exists modulo equality
781 Node r1r2i
= d_state
.getBinaryOpTerm(INTERSECTION
, r1
, r2
);
784 Trace("sets-nf-debug")
785 << "Split term already exists, but not in cardinality "
787 << r1r2i
<< ", should be empty." << std::endl
;
788 // their intersection is empty (probably?)
789 // e.g. these are two disjoint venn regions, proceed to next
791 Assert(d_state
.areEqual(emp_set
, r1r2i
));
798 // simply introduce their intersection
800 Node kca
= d_state
.getProxy(o0
);
801 Node kcb
= d_state
.getProxy(o1
);
803 Rewriter::rewrite(nm
->mkNode(INTERSECTION
, kca
, kcb
));
804 Trace("sets-nf") << " Intro split : " << o0
<< " against " << o1
805 << ", term is " << intro
<< std::endl
;
806 intro_sets
.push_back(intro
);
807 Assert(!d_ee
.hasTerm(intro
));
812 // should never get here
818 // normal form is flat form of base
819 nfeqc
.insert(nfeqc
.end(), ffeqc
[base
].begin(), ffeqc
[base
].end());
820 Trace("sets-nf") << "----> N " << eqc
<< " => F " << base
<< std::endl
;
824 Trace("sets-nf") << "failed to build N " << eqc
<< std::endl
;
829 // must ensure disequal from empty
830 if (!eqc
.isConst() && !d_state
.areDisequal(eqc
, emp_set
)
831 && !d_state
.hasMembers(eqc
))
833 Trace("sets-nf-debug") << "Split on leaf " << eqc
<< std::endl
;
834 d_im
.split(eqc
.eqNode(emp_set
));
839 // normal form is this equivalence class
840 nfeqc
.push_back(eqc
);
841 Trace("sets-nf") << "----> N " << eqc
<< " => { " << eqc
<< " }"
847 Assert(d_im
.hasProcessed());
850 // Send to parents (a parent is a set that contains a term in this equivalence
851 // class as a direct child).
852 const std::vector
<Node
>& nvsets
= d_state
.getNonVariableSets(eqc
);
855 // no non-variable sets
858 std::map
<Node
, std::map
<Node
, bool> > parents_proc
;
859 for (const Node
& n
: nvsets
)
861 Trace("sets-nf-debug") << "Carry nf for term " << n
<< std::endl
;
862 if (d_card_parent
[n
].empty())
867 Assert(d_localBase
.find(n
) != d_localBase
.end());
868 Node cbase
= d_localBase
[n
];
869 Trace("sets-nf-debug") << "Card base is " << cbase
<< std::endl
;
870 for (const Node
& p
: d_card_parent
[n
])
872 Trace("sets-nf-debug") << "Check parent " << p
<< std::endl
;
873 if (parents_proc
[cbase
].find(p
) != parents_proc
[cbase
].end())
875 Trace("sets-nf-debug") << "..already processed parent " << p
<< " for "
876 << cbase
<< std::endl
;
879 parents_proc
[cbase
][p
] = true;
880 Trace("sets-nf-debug") << "Carry nf to parent ( " << cbase
<< ", [" << p
881 << "] ), from " << n
<< "..." << std::endl
;
883 std::vector
<Node
>& ffpc
= d_ff
[p
][cbase
];
884 for (const Node
& nfeqci
: nfeqc
)
886 if (std::find(ffpc
.begin(), ffpc
.end(), nfeqci
) == ffpc
.end())
888 ffpc
.insert(ffpc
.end(), nfeqc
.begin(), nfeqc
.end());
892 // if it is a duplicate venn region, it must be empty since it is
893 // coming from syntactically disjoint siblings
900 void CardinalityExtension::checkMinCard()
902 NodeManager
* nm
= NodeManager::currentNM();
903 const std::vector
<Node
>& setEqc
= d_state
.getSetsEqClasses();
904 for (int i
= (int)(setEqc
.size() - 1); i
>= 0; i
--)
906 Node eqc
= setEqc
[i
];
907 TypeNode tn
= eqc
.getType().getSetElementType();
908 if (d_t_card_enabled
.find(tn
) == d_t_card_enabled
.end())
910 // cardinality is not enabled for this type, skip
913 // get members in class
914 const std::map
<Node
, Node
>& pmemsE
= d_state
.getMembers(eqc
);
917 // no members, trivial
920 std::vector
<Node
> exp
;
921 std::vector
<Node
> members
;
923 std::map
<Node
, Node
>::iterator it
= d_eqc_to_card_term
.find(eqc
);
924 if (it
!= d_eqc_to_card_term
.end())
926 cardTerm
= it
->second
;
930 cardTerm
= nm
->mkNode(CARD
, eqc
);
932 for (const std::pair
<const Node
, Node
>& itmm
: pmemsE
)
934 members
.push_back(itmm
.first
);
935 exp
.push_back(nm
->mkNode(MEMBER
, itmm
.first
, cardTerm
[0]));
937 if (members
.size() > 1)
939 exp
.push_back(nm
->mkNode(DISTINCT
, members
));
941 if (!members
.empty())
944 nm
->mkNode(GEQ
, cardTerm
, nm
->mkConst(Rational(members
.size())));
945 Node expn
= exp
.size() == 1 ? exp
[0] : nm
->mkNode(AND
, exp
);
946 d_im
.assertInference(conc
, expn
, "mincard", 1);
950 d_im
.flushPendingLemmas();
953 bool CardinalityExtension::isModelValueBasic(Node eqc
)
955 return d_nf
[eqc
].size() == 1 && d_nf
[eqc
][0] == eqc
;
958 void CardinalityExtension::mkModelValueElementsFor(
961 std::vector
<Node
>& els
,
962 const std::map
<Node
, Node
>& mvals
,
965 TypeNode elementType
= eqc
.getType().getSetElementType();
966 if (isModelValueBasic(eqc
))
968 std::map
<Node
, Node
>::iterator it
= d_eqc_to_card_term
.find(eqc
);
969 if (it
!= d_eqc_to_card_term
.end())
971 // slack elements from cardinality value
972 Node v
= val
.getModelValue(it
->second
);
973 Trace("sets-model") << "Cardinality of " << eqc
<< " is " << v
975 Assert(v
.getConst
<Rational
>() <= LONG_MAX
)
976 << "Exceeded LONG_MAX in sets model";
977 unsigned vu
= v
.getConst
<Rational
>().getNumerator().toUnsignedInt();
978 Assert(els
.size() <= vu
);
979 NodeManager
* nm
= NodeManager::currentNM();
980 if (elementType
.isInterpretedFinite())
982 // get all members of this finite type
983 collectFiniteTypeSetElements(model
);
985 while (els
.size() < vu
)
987 if (elementType
.isInterpretedFinite())
989 // At this point we are sure the formula is satisfiable and all
990 // cardinality constraints are satisfied. Since this type is finite,
991 // there is only one single cardinality graph for all sets of this
992 // type because the universe cardinality constraint has been added by
993 // CardinalityExtension::checkFiniteType. This means we have enough
994 // slack elements of this finite type for all disjoint leaves in the
995 // cardinality graph. Therefore we can safely add new distinct slack
996 // elements for the leaves without worrying about conflicts with the
997 // current members of this finite type.
999 Node slack
= nm
->mkSkolem("slack", elementType
);
1000 Node singleton
= nm
->mkNode(SINGLETON
, slack
);
1001 els
.push_back(singleton
);
1002 d_finite_type_slack_elements
[elementType
].push_back(slack
);
1003 Trace("sets-model") << "Added slack element " << slack
<< " to set "
1004 << eqc
<< std::endl
;
1009 nm
->mkNode(SINGLETON
, nm
->mkSkolem("msde", elementType
)));
1015 Trace("sets-model") << "No slack elements for " << eqc
<< std::endl
;
1020 Trace("sets-model") << "Build value for " << eqc
1021 << " based on normal form, size = " << d_nf
[eqc
].size()
1023 // it is union of venn regions
1024 for (unsigned j
= 0; j
< d_nf
[eqc
].size(); j
++)
1026 std::map
<Node
, Node
>::const_iterator itm
= mvals
.find(d_nf
[eqc
][j
]);
1027 if (itm
!= mvals
.end())
1029 els
.push_back(itm
->second
);
1039 void CardinalityExtension::collectFiniteTypeSetElements(TheoryModel
* model
)
1041 if (d_finite_type_constants_processed
)
1045 for (const Node
& set
: getOrderedSetsEqClasses())
1047 if (!set
.getType().isInterpretedFinite())
1051 if (!isModelValueBasic(set
))
1053 // only consider leaves in the cardinality graph
1056 for (const std::pair
<const Node
, Node
>& pair
: d_state
.getMembers(set
))
1058 Node member
= pair
.first
;
1059 Node modelRepresentative
= model
->getRepresentative(member
);
1060 std::vector
<Node
>& elements
= d_finite_type_elements
[member
.getType()];
1061 if (std::find(elements
.begin(), elements
.end(), modelRepresentative
)
1064 elements
.push_back(modelRepresentative
);
1068 d_finite_type_constants_processed
= true;
1071 const std::vector
<Node
>& CardinalityExtension::getFiniteTypeMembers(
1074 return d_finite_type_elements
[typeNode
];
1078 } // namespace theory