diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-21 09:26:04 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-21 09:26:19 -0500 |
commit | a33dac29d9cc8520f62b6e4f4f9138ea4e3fbcd4 (patch) | |
tree | b92bc3f34aca16a4b4ed6d42b2c2ae909dff17d4 /src/theory | |
parent | 8a0d2b0577e174d2078026129dd01ea46f7f984a (diff) |
Handle subtypes in sets. Bug fixes for tuples with subtypes.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/datatypes_rewriter.h | 60 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.h | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/macros.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 287 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 7 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 16 |
8 files changed, 262 insertions, 142 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 0d58233c9..30cdf8893 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -36,7 +36,8 @@ public: Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl; if(in.getKind() == kind::APPLY_CONSTRUCTOR ){ - Type t = in.getType().toType(); + TypeNode tn = in.getType(); + Type t = tn.toType(); DatatypeType dt = DatatypeType(t); //check for parametric datatype constructors // to ensure a normal form, all parameteric datatype constructors must have a type ascription @@ -58,6 +59,13 @@ public: return RewriteResponse(REWRITE_DONE, inr); } } + if( tn.isTuple() ){ + Node nn = normalizeTupleConstructorApp( in ); + if( nn!=in ){ + Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: Rewrite tuple constructor " << in << " to " << nn << std::endl; + return RewriteResponse(REWRITE_AGAIN_FULL, nn); + } + } if( in.isConst() ){ Trace("datatypes-rewrite-debug") << "Normalizing constant " << in << std::endl; Node inn = normalizeConstant( in ); @@ -110,7 +118,7 @@ public: Expr constructorExpr = constructor.toExpr(); size_t selectorIndex = Datatype::indexOf(selectorExpr); size_t constructorIndex = Datatype::indexOf(constructorExpr); - const Datatype& dt = Datatype::datatypeOf(constructorExpr); + const Datatype& dt = Datatype::datatypeOf(selectorExpr); const DatatypeConstructor& c = dt[constructorIndex]; if(c.getNumArgs() > selectorIndex && c[selectorIndex].getSelector() == selectorExpr) { if( dt.isCodatatype() && in[0][selectorIndex].isConst() ){ @@ -235,15 +243,16 @@ public: static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) { Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2 << std::endl; if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) { - if( n1.getOperator() != n2.getOperator() ) { - Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl; - return true; - } else { - Assert( n1.getNumChildren() == n2.getNumChildren() ); - for( int i=0; i<(int)n1.getNumChildren(); i++ ) { - if( checkClash( n1[i], n2[i], rew ) ) { - return true; - } + if( n1.getOperator() != n2.getOperator()) { + if( n1.getNumChildren() != n2.getNumChildren() || !n1.getType().isTuple() || !n2.getType().isTuple() ){ + Trace("datatypes-rewrite-debug") << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() << " " << n2.getOperator() << std::endl; + return true; + } + } + Assert( n1.getNumChildren() == n2.getNumChildren() ); + for( unsigned i=0; i<n1.getNumChildren(); i++ ) { + if( checkClash( n1[i], n2[i], rew ) ) { + return true; } } }else if( n1!=n2 ){ @@ -601,11 +610,38 @@ public: return Node::null(); } } + + static Node normalizeTupleConstructorApp( Node n ){ + Assert( n.getType().isTuple() ); + Assert( n.getKind()==kind::APPLY_CONSTRUCTOR ); + const Datatype& dt = n.getType().getDatatype(); + //may apply a different constructor based on child types + std::vector< TypeNode > cht; + std::vector< Node > ch; + bool childTypeChange = false; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + TypeNode tci = n[i].getType(); + cht.push_back( tci ); + ch.push_back( n[i] ); + if( tci!=TypeNode::fromType( dt[0][i].getRangeType() ) ){ + childTypeChange = true; + } + } + if( childTypeChange ){ + TypeNode ttn = NodeManager::currentNM()->mkTupleType( cht ); + const Datatype& dtt = ttn.getDatatype(); + ch.insert( ch.begin(), Node::fromExpr( dtt[0].getConstructor() ) ); + return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, ch ); + } + return n; + } //normalize constant : apply to top-level codatatype constants static Node normalizeConstant( Node n ){ TypeNode tn = n.getType(); if( tn.isDatatype() ){ - if( tn.isCodatatype() ){ + if( tn.isTuple() ){ + return normalizeTupleConstructorApp( n ); + }else if( tn.isCodatatype() ){ return normalizeCodatatypeConstant( n ); }else{ std::vector< Node > children; diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 8a440974d..412b3d7ec 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -99,6 +99,19 @@ struct DatatypeConstructorTypeRule { return false; } } + //check whether it is in normal form? + TypeNode tn = n.getType(); + if( tn.isTuple() ){ + const Datatype& dt = tn.getDatatype(); + //may be the wrong constructor, if children types are subtypes + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( n[i].getType()!=TypeNode::fromType( dt[0][i].getRangeType() ) ){ + return false; + } + } + }else if( tn.isCodatatype() ){ + //TODO? + } return true; } }; /* struct DatatypeConstructorTypeRule */ diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 96d682a77..636bfdb59 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -419,13 +419,16 @@ Node QuantifierMacros::simplify( Node n ){ std::vector< Node > cond; TypeNode tno = op.getType(); for( unsigned i=0; i<children.size(); i++ ){ - if( !TermDb::getEnsureTypeCondition( children[i], tno[i], cond ) ){ + Node etc = TypeNode::getEnsureTypeCondition( children[i], tno[i] ); + if( etc.isNull() ){ //if this does fail, we are incomplete, since we are eliminating quantified formula corresponding to op, // and not ensuring it applies to n when its types are correct. //however, this should never fail: we never process types for which we cannot constuct conditions that ensure correct types, e.g. (is-int t). Assert( false ); success = false; break; + }else if( !etc.isConst() ){ + cond.push_back( etc ); } } if( success ){ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 4f58f7a2e..5ac5ae0cc 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1839,20 +1839,6 @@ Node TermDb::ensureType( Node n, TypeNode tn ) { } } -bool TermDb::getEnsureTypeCondition( Node n, TypeNode tn, std::vector< Node >& cond ) { - TypeNode ntn = n.getType(); - Assert( ntn.isComparableTo( tn ) ); - if( !ntn.isSubtypeOf( tn ) ){ - if( tn.isInteger() ){ - cond.push_back( NodeManager::currentNM()->mkNode( IS_INTEGER, n ) ); - return true; - } - return false; - }else{ - return true; - } -} - void TermDb::getRelevancyCondition( Node n, std::vector< Node >& cond ) { if( n.getKind()==APPLY_SELECTOR_TOTAL ){ unsigned scindex = Datatype::cindexOf(n.getOperator().toExpr()); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 5b29a72ce..c018172b5 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -473,8 +473,6 @@ public: bool containsVtsInfinity( Node n, bool isFree = false ); /** ensure type */ static Node ensureType( Node n, TypeNode tn ); - /** get ensure type condition */ - static bool getEnsureTypeCondition( Node n, TypeNode tn, std::vector< Node >& cond ); /** get relevancy condition */ static void getRelevancyCondition( Node n, std::vector< Node >& cond ); private: diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index fe8f970c5..0338eb1b3 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -157,7 +157,7 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){ } if( add ){ if( !s1.isNull() && s2.isNull() ){ - Assert( m2[1].getType()==s1.getType() ); + Assert( m2[1].getType().isComparableTo( s1.getType() ) ); Assert( ee_areEqual( m2[1], s1 ) ); Node exp = NodeManager::currentNM()->mkNode( kind::AND, m2[1].eqNode( s1 ), m2 ); if( s1.getKind()==kind::SINGLETON ){ @@ -518,6 +518,7 @@ void TheorySetsPrivate::fullEffortCheck(){ Assert( d_equalityEngine.consistent() ); d_sentLemma = false; d_addedFact = false; + d_full_check_incomplete = false; d_set_eqc.clear(); d_set_eqc_list.clear(); d_eqc_emptyset.clear(); @@ -526,6 +527,8 @@ void TheorySetsPrivate::fullEffortCheck(){ d_congruent.clear(); d_nvar_sets.clear(); d_var_set.clear(); + d_most_common_type.clear(); + d_most_common_type_term.clear(); d_pol_mems[0].clear(); d_pol_mems[1].clear(); d_members_index.clear(); @@ -543,9 +546,14 @@ void TheorySetsPrivate::fullEffortCheck(){ Node eqc = (*eqcs_i); bool isSet = false; TypeNode tn = eqc.getType(); + //common type node and term + TypeNode tnc; + Node tnct; if( tn.isSet() ){ isSet = true; d_set_eqc.push_back( eqc ); + tnc = tn.getSetElementType(); + tnct = eqc; } Trace("sets-eqc") << "[" << eqc << "] : "; eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); @@ -554,6 +562,17 @@ void TheorySetsPrivate::fullEffortCheck(){ if( n!=eqc ){ Trace("sets-eqc") << n << " "; } + TypeNode tnn = n.getType(); + if( isSet ){ + Assert( tnn.isSet() ); + TypeNode tnnel = tnn.getSetElementType(); + tnc = TypeNode::mostCommonTypeNode( tnc, tnnel ); + Assert( !tnc.isNull() ); + //update the common type term + if( tnc==tnnel ){ + tnct = n; + } + } if( n.getKind()==kind::MEMBER ){ if( eqc.isConst() ){ Node s = d_equalityEngine.getRepresentative( n[1] ); @@ -586,9 +605,15 @@ void TheorySetsPrivate::fullEffortCheck(){ d_congruent[n] = d_singleton_index[r]; } }else if( n.getKind()==kind::EMPTYSET ){ - d_eqc_emptyset[tn] = eqc; + d_eqc_emptyset[tnn] = eqc; }else if( n.getKind()==kind::UNIVERSE_SET ){ - d_eqc_univset[tn] = eqc; + if( options::setsExt() ){ + d_eqc_univset[tnn] = eqc; + }else{ + std::stringstream ss; + ss << "Symbols complement and universe set are not supported in default mode, try --sets-ext." << std::endl; + throw LogicException(ss.str()); + } }else{ Node r1 = d_equalityEngine.getRepresentative( n[0] ); Node r2 = d_equalityEngine.getRepresentative( n[1] ); @@ -604,8 +629,8 @@ void TheorySetsPrivate::fullEffortCheck(){ d_set_eqc_list[eqc].push_back( n ); }else if( n.getKind()==kind::CARD ){ d_card_enabled = true; - TypeNode tn = n[0].getType().getSetElementType(); - if( tn.isInterpretedFinite() ){ + TypeNode tnc = n[0].getType().getSetElementType(); + if( tnc.isInterpretedFinite() ){ std::stringstream ss; ss << "ERROR: cannot use cardinality on sets with finite element type." << std::endl; throw LogicException(ss.str()); @@ -631,6 +656,11 @@ void TheorySetsPrivate::fullEffortCheck(){ } ++eqc_i; } + if( isSet ){ + Assert( tnct.getType().getSetElementType()==tnc ); + d_most_common_type[eqc] = tnc; + d_most_common_type_term[eqc] = tnct; + } Trace("sets-eqc") << std::endl; ++eqcs_i; } @@ -655,46 +685,50 @@ void TheorySetsPrivate::fullEffortCheck(){ Trace("sets-mem") << std::endl; } } - - checkDownwardsClosure( lemmas ); - if( options::setsInferAsLemmas() ){ - flushLemmas( lemmas ); - } + checkSubtypes( lemmas ); + flushLemmas( lemmas, true ); if( !hasProcessed() ){ - checkUpwardsClosure( lemmas ); - flushLemmas( lemmas ); + + checkDownwardsClosure( lemmas ); + if( options::setsInferAsLemmas() ){ + flushLemmas( lemmas ); + } if( !hasProcessed() ){ - std::vector< Node > intro_sets; - //for cardinality - if( d_card_enabled ){ - checkCardBuildGraph( lemmas ); - flushLemmas( lemmas ); - if( !hasProcessed() ){ - checkMinCard( lemmas ); + checkUpwardsClosure( lemmas ); + flushLemmas( lemmas ); + if( !hasProcessed() ){ + std::vector< Node > intro_sets; + //for cardinality + if( d_card_enabled ){ + checkCardBuildGraph( lemmas ); flushLemmas( lemmas ); if( !hasProcessed() ){ - checkCardCycles( lemmas ); + checkMinCard( lemmas ); flushLemmas( lemmas ); if( !hasProcessed() ){ - checkNormalForms( lemmas, intro_sets ); + checkCardCycles( lemmas ); flushLemmas( lemmas ); + if( !hasProcessed() ){ + checkNormalForms( lemmas, intro_sets ); + flushLemmas( lemmas ); + } } } } - } - if( !hasProcessed() ){ - checkDisequalities( lemmas ); - flushLemmas( lemmas ); if( !hasProcessed() ){ - //introduce splitting on venn regions (absolute last resort) - if( d_card_enabled && !hasProcessed() && !intro_sets.empty() ){ - Assert( intro_sets.size()==1 ); - Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl; - Trace("sets-intro") << " Actual Intro : "; - debugPrintSet( intro_sets[0], "sets-nf" ); - Trace("sets-nf") << std::endl; - Node k = getProxy( intro_sets[0] ); - d_sentLemma = true; + checkDisequalities( lemmas ); + flushLemmas( lemmas ); + if( !hasProcessed() ){ + //introduce splitting on venn regions (absolute last resort) + if( d_card_enabled && !hasProcessed() && !intro_sets.empty() ){ + Assert( intro_sets.size()==1 ); + Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl; + Trace("sets-intro") << " Actual Intro : "; + debugPrintSet( intro_sets[0], "sets-nf" ); + Trace("sets-nf") << std::endl; + Node k = getProxy( intro_sets[0] ); + d_sentLemma = true; + } } } } @@ -705,6 +739,36 @@ void TheorySetsPrivate::fullEffortCheck(){ Trace("sets") << "----- End full effort check, conflict=" << d_conflict << ", lemma=" << d_sentLemma << std::endl; } +void TheorySetsPrivate::checkSubtypes( std::vector< Node >& lemmas ) { + for( unsigned i=0; i<d_set_eqc.size(); i++ ){ + Node s = d_set_eqc[i]; + TypeNode mct = d_most_common_type[s]; + 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 ) ){ + 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() ){ + 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; + } + } + } + } + } +} + void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) { Trace("sets") << "Downwards closure..." << std::endl; //downwards closure @@ -869,30 +933,44 @@ void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) { } } if( !hasProcessed() ){ - //universal sets - Trace("sets-debug") << "Check universe sets..." << std::endl; - //all elements must be in universal set - for( std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].begin(); it != d_pol_mems[0].end(); ++it ){ - //if equivalence class contains a variable - std::map< Node, Node >::iterator itv = d_var_set.find( it->first ); - if( itv!=d_var_set.end() ){ - TypeNode tn = it->first.getType(); - std::map< TypeNode, Node >::iterator itu = d_eqc_univset.find( tn ); - // if the universe does not yet exist, or is not in this equivalence class - if( itu==d_eqc_univset.end() || itu->second!=it->first ){ - Node u = getUnivSet( tn ); + if( options::setsExt() ){ + //universal sets + Trace("sets-debug") << "Check universe sets..." << std::endl; + //all elements must be in universal set + for( std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].begin(); it != d_pol_mems[0].end(); ++it ){ + //if equivalence class contains a variable + std::map< Node, Node >::iterator itv = d_var_set.find( it->first ); + if( itv!=d_var_set.end() ){ + //the variable in the equivalence class Node v = itv->second; + std::map< TypeNode, Node > univ_set; for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - Assert( it2->second.getKind()==kind::MEMBER ); - std::vector< Node > exp; - exp.push_back( it2->second ); - if( v!=it2->second[1] ){ - exp.push_back( v.eqNode( it2->second[1] ) ); + Node e = it2->second[0]; + TypeNode tn = NodeManager::currentNM()->mkSetType( e.getType() ); + Node u; + std::map< TypeNode, Node >::iterator itu = univ_set.find( tn ); + if( itu==univ_set.end() ){ + std::map< TypeNode, Node >::iterator itu = d_eqc_univset.find( tn ); + // if the universe does not yet exist, or is not in this equivalence class + if( itu==d_eqc_univset.end() || itu->second!=it->first ){ + u = getUnivSet( tn ); + } + univ_set[tn] = u; + }else{ + u = itu->second; } - Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, it2->second[0], u ); - assertInference( fact, exp, lemmas, "upuniv" ); - if( d_conflict ){ - return; + if( !u.isNull() ){ + Assert( it2->second.getKind()==kind::MEMBER ); + std::vector< Node > exp; + exp.push_back( it2->second ); + if( v!=it2->second[1] ){ + exp.push_back( v.eqNode( it2->second[1] ) ); + } + Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, it2->second[0], u ); + assertInference( fact, exp, lemmas, "upuniv" ); + if( d_conflict ){ + return; + } } } } @@ -1494,22 +1572,24 @@ void TheorySetsPrivate::checkMinCard( std::vector< Node >& lemmas ) { } } -void TheorySetsPrivate::flushLemmas( std::vector< Node >& lemmas ) { - //do lemmas +void TheorySetsPrivate::flushLemmas( std::vector< Node >& lemmas, bool preprocess ) { for( unsigned i=0; i<lemmas.size(); i++ ){ - Node lem = lemmas[i]; - if( d_lemmas_produced.find(lem)==d_lemmas_produced.end() ){ - Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl; - d_lemmas_produced.insert(lem); - d_external.d_out->lemma(lem); - d_sentLemma = true; - }else{ - Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl; - } + flushLemma( lemmas[i], preprocess ); } lemmas.clear(); } +void TheorySetsPrivate::flushLemma( Node lem, bool preprocess ) { + if( d_lemmas_produced.find(lem)==d_lemmas_produced.end() ){ + Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl; + d_lemmas_produced.insert(lem); + d_external.d_out->lemma(lem, false, preprocess); + d_sentLemma = true; + }else{ + Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl; + } +} + Node TheorySetsPrivate::getProxy( Node n ) { if( n.getKind()==kind::EMPTYSET || n.getKind()==kind::SINGLETON || n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS || n.getKind()==kind::UNION ){ NodeMap::const_iterator it = d_proxy.find( n ); @@ -1559,6 +1639,23 @@ Node TheorySetsPrivate::getUnivSet( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_univset.find( tn ); if( it==d_univset.end() ){ Node n = NodeManager::currentNM()->mkNullaryOperator(tn, kind::UNIVERSE_SET); + for( it = d_univset.begin(); it != d_univset.end(); ++it ){ + Node n1; + Node n2; + if( tn.isSubtypeOf( it->first ) ){ + n1 = n; + n2 = it->second; + }else if( it->first.isSubtypeOf( tn ) ){ + n1 = it->second; + n2 = n; + } + if( !n1.isNull() ){ + Node ulem = NodeManager::currentNM()->mkNode( kind::SUBSET, n1, n2 ); + Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type" << std::endl; + d_external.d_out->lemma( ulem ); + d_sentLemma = true; + } + } d_univset[tn] = n; return n; }else{ @@ -1594,41 +1691,7 @@ void TheorySetsPrivate::debugPrintSet( Node s, const char * c ) { void TheorySetsPrivate::lastCallEffortCheck() { Trace("sets") << "----- Last call effort check ------" << std::endl; - /* - //FIXME : this is messy, have to see if constants are handled by the decision procedure, and not UF - TheoryModel * m = d_external.d_valuation.getModel(); - //must process eliminated variables at last call effort when model is available - std::vector< Node > lemmas; - for(NodeBoolMap::const_iterator it=d_var_elim.begin(); it !=d_var_elim.end(); ++it) { - if( (*it).second ){ - Node v = (*it).first; - Trace("sets-var-elim") << "Process eliminated variable : " << v << std::endl; - Node mv = m->getValue( v ); - Trace("sets-var-elim") << "...value in model is : " << mv << std::endl; - Node u = getUnivSet( mv.getType() ); - Node mvc = mv; - std::vector< Node > conj; - while( mvc.getKind()==kind::UNION ){ - Node s = mvc[1]; - Assert( s.getKind()==kind::SINGLETON ); - conj.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, s[0], u ) ); - mvc = mvc[0]; - } - if( mvc.getKind()==kind::SINGLETON ){ - conj.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, mvc[0], u ) ); - } - if( !conj.empty() ){ - Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( kind::AND, conj ); - // cannot add antecedant here since the eliminated variable v should not be reintroduced - //lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, v.eqNode(mv), lem ); - Trace("sets-var-elim") << "...lemma is : " << lem << std::endl; - lemmas.push_back( lem ); - } - d_var_elim[v] = false; - } - } - flushLemmas( lemmas ); - */ + } /**************************** TheorySetsPrivate *****************************/ @@ -1659,12 +1722,17 @@ void TheorySetsPrivate::check(Theory::Effort level) { if( !d_conflict && !d_sentLemma ){ //invoke relations solver d_rels->check(level); - if( d_card_enabled && d_rels_enabled ){ - //incomplete if we have both cardinality constraints and relational operators? + 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_external.d_out->setIncomplete(); + d_full_check_incomplete = true; + Trace("sets-incomplete") << "Sets : incomplete because of extended operators." << std::endl; } } + if( d_full_check_incomplete ){ + d_external.d_out->setIncomplete(); + } } }else{ if( options::setsRelEager() ){ @@ -2094,22 +2162,21 @@ void TheorySetsPrivate::preRegisterTerm(TNode node) Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED; - //TODO: should allow variable elimination for sets - // however, this makes universe set incorrect + //TODO: allow variable elimination for sets when setsExt = true //this is based off of Theory::ppAssert Node var; if (in.getKind() == kind::EQUAL) { if (in[0].isVar() && !in[1].hasSubterm(in[0]) && (in[1].getType()).isSubtypeOf(in[0].getType()) ){ - if( !in[0].getType().isSet() ){ + if( !in[0].getType().isSet() || !options::setsExt() ){ outSubstitutions.addSubstitution(in[0], in[1]); var = in[0]; status = Theory::PP_ASSERT_STATUS_SOLVED; } }else if (in[1].isVar() && !in[0].hasSubterm(in[1]) && (in[0].getType()).isSubtypeOf(in[1].getType())){ - if( !in[1].getType().isSet() ){ + if( !in[1].getType().isSet() || !options::setsExt() ){ outSubstitutions.addSubstitution(in[1], in[0]); var = in[1]; status = Theory::PP_ASSERT_STATUS_SOLVED; @@ -2129,7 +2196,9 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou d_var_elim[var] = true; } */ - Assert( !var.getType().isSet() ); + if( options::setsExt() ){ + Assert( !var.getType().isSet() ); + } } return status; } diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index d11dff2af..667b7f253 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -70,13 +70,15 @@ private: // send lemma ( n OR (NOT n) ) immediately void split( Node n, int reqPol=0 ); void fullEffortCheck(); + void checkSubtypes( std::vector< Node >& lemmas ); void checkDownwardsClosure( std::vector< Node >& lemmas ); void checkUpwardsClosure( std::vector< Node >& lemmas ); void checkDisequalities( std::vector< Node >& lemmas ); bool isMember( Node x, Node s ); bool isSetDisequalityEntailed( Node s, Node t ); - void flushLemmas( std::vector< Node >& lemmas ); + void flushLemmas( std::vector< Node >& lemmas, bool preprocess = false ); + void flushLemma( Node lem, bool preprocess = false ); Node getProxy( Node n ); Node getCongruent( Node n ); Node getEmptySet( TypeNode tn ); @@ -114,6 +116,7 @@ private: bool d_sentLemma; bool d_addedFact; + bool d_full_check_incomplete; NodeMap d_proxy; NodeMap d_proxy_to_term; NodeSet d_lemmas_produced; @@ -128,6 +131,8 @@ private: std::map< Node, Node > d_congruent; std::map< Node, std::vector< Node > > d_nvar_sets; std::map< Node, Node > d_var_set; + std::map< Node, TypeNode > d_most_common_type; + std::map< Node, Node > d_most_common_type_term; std::map< Node, std::map< Node, Node > > d_pol_mems[2]; std::map< Node, std::map< Node, Node > > d_members_index; std::map< Node, Node > d_singleton_index; diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index a3abdf508..7462847b6 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -59,7 +59,15 @@ struct SetsBinaryOperatorTypeRule { } TypeNode secondSetType = n[1].getType(check); if(secondSetType != setType) { - throw TypeCheckingExceptionPrivate(n, "operator expects two sets of the same type"); + if( n.getKind() == kind::INTERSECTION ){ + setType = TypeNode::mostCommonTypeNode( secondSetType, setType ); + }else{ + setType = TypeNode::leastCommonTypeNode( secondSetType, setType ); + } + if( setType.isNull() ){ + throw TypeCheckingExceptionPrivate(n, "operator expects two sets of comparable types"); + } + } } return setType; @@ -88,7 +96,9 @@ struct SubsetTypeRule { } TypeNode secondSetType = n[1].getType(check); if(secondSetType != setType) { - throw TypeCheckingExceptionPrivate(n, "set subset operating on sets of different types"); + if( !setType.isComparableTo( secondSetType ) ){ + throw TypeCheckingExceptionPrivate(n, "set subset operating on sets of different types"); + } } } return nodeManager->booleanType(); @@ -105,7 +115,7 @@ struct MemberTypeRule { throw TypeCheckingExceptionPrivate(n, "checking for membership in a non-set"); } TypeNode elementType = n[0].getType(check); - if(!setType.getSetElementType().isSubtypeOf(elementType)) { + if(!elementType.isComparableTo(setType.getSetElementType())) { throw TypeCheckingExceptionPrivate(n, "member operating on sets of different types"); } } |