diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 27 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_private.h | 19 |
2 files changed, 37 insertions, 9 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 71857b7a5..93fca2324 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -738,22 +738,21 @@ void TheorySetsPrivate::checkSubtypes( std::vector< Node >& lemmas ) { std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].find( s ); if( it!=d_pol_mems[0].end() ){ for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - if( !it2->first.getType().isSubtypeOf( mct ) ){ + if (!it2->first.getType().isSubtypeOf(mct)) + { Node mctt = d_most_common_type_term[s]; std::vector< Node > exp; exp.push_back( it2->second ); Assert( ee_areEqual( mctt, it2->second[1] ) ); exp.push_back( mctt.eqNode( it2->second[1] ) ); - Node etc = TypeNode::getEnsureTypeCondition( it2->first, mct ); - if( !etc.isNull() ){ + Node tc_k = getTypeConstraintSkolem(it2->first, mct); + if (!tc_k.isNull()) + { + Node etc = tc_k.eqNode(it2->first); assertInference( etc, exp, lemmas, "subtype-clash" ); if( d_conflict ){ return; - } - }else{ - // very strange situation : we have a member in a set that is not a subtype, and we do not have a type condition for it - d_full_check_incomplete = true; - Trace("sets-incomplete") << "Sets : incomplete because of unknown type constraint." << std::endl; + } } } } @@ -1686,6 +1685,18 @@ void TheorySetsPrivate::lastCallEffortCheck() { } +Node TheorySetsPrivate::getTypeConstraintSkolem(Node n, TypeNode tn) +{ + std::map<TypeNode, Node>::iterator it = d_tc_skolem[n].find(tn); + if (it == d_tc_skolem[n].end()) + { + Node k = NodeManager::currentNM()->mkSkolem("tc_k", tn); + d_tc_skolem[n][tn] = k; + return k; + } + return it->second; +} + /**************************** TheorySetsPrivate *****************************/ /**************************** TheorySetsPrivate *****************************/ /**************************** TheorySetsPrivate *****************************/ diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index b57f208bd..e708ad539 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -158,7 +158,24 @@ private: private: //for universe set NodeBoolMap d_var_elim; void lastCallEffortCheck(); -public: + + private: + /** type constraint skolems + * + * The sets theory solver outputs equality lemmas of the form: + * n = d_tc_skolem[n][tn] + * where the type of d_tc_skolem[n][tn] is tn, and the type + * of n is not a subtype of tn. This is required to handle benchmarks like + * test/regress/regress0/sets/sets-of-sets-subtypes.smt2 + * where for s : (Set Int) and t : (Set Real), we have that + * ( s = t ^ y in t ) implies ( exists k : Int. y = k ) + * The type constraint Skolem for (y, Int) is the skolemization of k above. + */ + std::map<Node, std::map<TypeNode, Node> > d_tc_skolem; + /** get type constraint skolem for n and tn */ + Node getTypeConstraintSkolem(Node n, TypeNode tn); + + public: /** * Constructs a new instance of TheorySetsPrivate w.r.t. the provided |