diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-12-03 17:00:58 -0600 |
|---|---|---|
| committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-12-03 17:00:58 -0600 |
| commit | 854c414f056e306dd8678fd7459ee9dee8b8d6b3 (patch) | |
| tree | e8c3d4bfb114ea4032f3805bf446b90303c8b1c8 | |
| parent | aa0a875dfd40bd9dfa810238327db51498b74677 (diff) | |
Skip non-cardinality types in sets min card inference (#2734)
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 83c66c2d3..1c302573e 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1543,6 +1543,12 @@ void TheorySetsPrivate::checkMinCard( std::vector< Node >& lemmas ) { for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){ Node eqc = d_set_eqc[i]; + TypeNode tn = eqc.getType().getSetElementType(); + if (d_t_card_enabled.find(tn) == d_t_card_enabled.end()) + { + // cardinality is not enabled for this type, skip + continue; + } //get members in class std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc ); if( itm!=d_pol_mems[0].end() ){ |