diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-24 17:01:38 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-24 17:01:38 -0500 |
commit | 22916321f5c26fdc632df24f3c1fef45beaeb918 (patch) | |
tree | a8a43b5aea9b8a4efbe5069eacb720e5506fc423 /src/theory/sets | |
parent | 25d3eea9614a0882a5c18c455e5a14d118a78dce (diff) |
Improvements to sets + cardinality + quantifiers (#2200)
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 32 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 2 |
2 files changed, 24 insertions, 10 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 7b5244a04..49954c111 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -533,6 +533,7 @@ void TheorySetsPrivate::fullEffortCheck(){ d_bop_index.clear(); d_op_list.clear(); d_card_enabled = false; + d_t_card_enabled.clear(); d_rels_enabled = false; d_eqc_to_card_term.clear(); @@ -622,12 +623,23 @@ void TheorySetsPrivate::fullEffortCheck(){ }else if( n.getKind()==kind::CARD ){ d_card_enabled = true; TypeNode tnc = n[0].getType().getSetElementType(); + d_t_card_enabled[tnc] = true; if( tnc.isInterpretedFinite() ){ std::stringstream ss; - ss << "ERROR: cannot use cardinality on sets with finite element type." << std::endl; + ss << "ERROR: cannot use cardinality on sets with finite element " + "type (term is " + << n << ")." << std::endl; throw LogicException(ss.str()); //TODO: extend approach for this case } + // if we do not handle the kind, set incomplete + Kind nk = n[0].getKind(); + if (nk == kind::UNIVERSE_SET || d_rels->isRelationKind(nk)) + { + d_full_check_incomplete = true; + Trace("sets-incomplete") + << "Sets : incomplete because of " << n << "." << std::endl; + } Node r = d_equalityEngine.getRepresentative( n[0] ); if( d_eqc_to_card_term.find( r )==d_eqc_to_card_term.end() ){ d_eqc_to_card_term[ r ] = n; @@ -1037,6 +1049,12 @@ void TheorySetsPrivate::checkCardBuildGraph( std::vector< Node >& lemmas ) { } void TheorySetsPrivate::registerCardinalityTerm( Node n, std::vector< Node >& lemmas ){ + TypeNode tnc = n.getType().getSetElementType(); + if (d_t_card_enabled.find(tnc) == d_t_card_enabled.end()) + { + // if no cardinality constraints for sets of this type, we can ignore + return; + } if( d_card_processed.find( n )==d_card_processed.end() ){ d_card_processed.insert( n ); Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl; @@ -1724,16 +1742,10 @@ void TheorySetsPrivate::check(Theory::Effort level) { fullEffortCheck(); if( !d_conflict && !d_sentLemma ){ //invoke relations solver - d_rels->check(level); - if( d_card_enabled && ( d_rels_enabled || options::setsExt() ) ){ - //if cardinality constraints are enabled, - // then model construction may fail in there are relational operators, or universe set. - // TODO: should internally check model, return unknown if fail - d_full_check_incomplete = true; - Trace("sets-incomplete") << "Sets : incomplete because of extended operators." << std::endl; - } + d_rels->check(level); } - if( d_full_check_incomplete ){ + if (!d_conflict && !d_sentLemma && d_full_check_incomplete) + { d_external.d_out->setIncomplete(); } } diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 57a7aaf65..31aec85c3 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -141,6 +141,8 @@ private: //cardinality private: bool d_card_enabled; + /** element types of sets for which cardinality is enabled */ + std::map<TypeNode, bool> d_t_card_enabled; bool d_rels_enabled; std::map< Node, Node > d_eqc_to_card_term; NodeSet d_card_processed; |