From: Andrew Reynolds Date: Thu, 28 Apr 2022 13:42:58 +0000 (-0500) Subject: Clean code for datatypes split (#8667) X-Git-Tag: cvc5-1.0.1~210 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f033b058ca1d55bdd967c2c496f0db9e8e96bb84;p=cvc5.git Clean code for datatypes split (#8667) Non-moving version of #8664. --- diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 7d135ee59..c5ebd0cef 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -210,151 +210,194 @@ void TheoryDatatypes::postCheck(Effort level) Trace("datatypes-debug") << "Check for splits " << endl; do { d_im.reset(); - std::map< TypeNode, Node > rec_singletons; + // get the relevant term set, currently all datatype equivalence classes + // in the equality engine + std::set termSetReps; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine); - while( !eqcs_i.isFinished() ){ - Node n = (*eqcs_i); - //TODO : avoid irrelevant (pre-registered but not asserted) terms here? + while (!eqcs_i.isFinished()) + { + Node eqc = (*eqcs_i); + ++eqcs_i; + if (eqc.getType().isDatatype()) + { + termSetReps.insert(eqc); + } + } + std::map rec_singletons; + for (const Node& n : termSetReps) + { + Trace("datatypes-debug") + << "Process equivalence class " << n << std::endl; + EqcInfo* eqc = getOrMakeEqcInfo(n); + // if there are more than 1 possible constructors for eqc + if (hasLabel(eqc, n)) + { + Trace("datatypes-debug") + << "Has constructor " << eqc->d_constructor.get() << std::endl; + continue; + } + Trace("datatypes-debug") << "No constructor..." << std::endl; TypeNode tn = n.getType(); - if( tn.isDatatype() ){ - Trace("datatypes-debug") << "Process equivalence class " << n << std::endl; - EqcInfo* eqc = getOrMakeEqcInfo( n ); - //if there are more than 1 possible constructors for eqc - if( !hasLabel( eqc, n ) ){ - Trace("datatypes-debug") << "No constructor..." << std::endl; - TypeNode tt = tn; - const DType& dt = tt.getDType(); - Trace("datatypes-debug") - << "Datatype " << dt.getName() << " is " - << dt.getCardinalityClass(tt) << " " - << dt.isRecursiveSingleton(tt) << std::endl; - bool continueProc = true; - if( dt.isRecursiveSingleton( tt ) ){ - Trace("datatypes-debug") << "Check recursive singleton..." << std::endl; - //handle recursive singleton case - std::map< TypeNode, Node >::iterator itrs = rec_singletons.find( tn ); - if( itrs!=rec_singletons.end() ){ - Node eq = n.eqNode( itrs->second ); - if( d_singleton_eq.find( eq )==d_singleton_eq.end() ){ - d_singleton_eq[eq] = true; - // get assumptions - bool success = true; - std::vector< Node > assumptions; - //if there is at least one uninterpreted sort occurring within the datatype and the logic is not quantified, add lemmas ensuring cardinality is more than one, - // do not infer the equality if at least one sort was processed. - //otherwise, if the logic is quantified, under the assumption that all uninterpreted sorts have cardinality one, - // infer the equality. - for( unsigned i=0; isecond); - assumptions.push_back(assumption); - Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions ); - Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl; - d_im.lemma(lemma, InferenceId::DATATYPES_REC_SINGLETON_EQ); - } - } - }else{ - rec_singletons[tn] = n; - } - //do splitting for quantified logics (incomplete anyways) - continueProc = ( getQuantifiersEngine()!=NULL ); - } - if( continueProc ){ - Trace("datatypes-debug") << "Get possible cons..." << std::endl; - //all other cases - std::vector< bool > pcons; - getPossibleCons( eqc, n, pcons ); - //check if we do not need to resolve the constructor type for this equivalence class. - // this is if there are no selectors for this equivalence class, and its possible values are infinite, - // then do not split. - int consIndex = -1; - int fconsIndex = -1; - bool needSplit = true; - for (size_t j = 0, psize = pcons.size(); j < psize; j++) + const DType& dt = tn.getDType(); + Trace("datatypes-debug") << "Datatype " << dt.getName() << " is " + << dt.getCardinalityClass(tn) << " " + << dt.isRecursiveSingleton(tn) << std::endl; + if (dt.isRecursiveSingleton(tn)) + { + Trace("datatypes-debug") + << "Check recursive singleton..." << std::endl; + bool isQuantifiedLogic = logicInfo().isQuantified(); + // handle recursive singleton case + std::map::iterator itrs = rec_singletons.find(tn); + if (itrs != rec_singletons.end()) + { + Node eq = n.eqNode(itrs->second); + if (d_singleton_eq.find(eq) == d_singleton_eq.end()) + { + d_singleton_eq[eq] = true; + // get assumptions + bool success = true; + std::vector assumptions; + // if there is at least one uninterpreted sort occurring within + // the datatype and the logic is not quantified, add lemmas + // ensuring cardinality is more than one, + // do not infer the equality if at least one sort was processed. + // otherwise, if the logic is quantified, under the assumption + // that all uninterpreted sorts have cardinality one, + // infer the equality. + for (size_t i = 0; i < dt.getNumRecursiveSingletonArgTypes(tn); + i++) { - if( pcons[j] ) { - if( consIndex==-1 ){ - consIndex = j; - } - Trace("datatypes-debug") << j << " compute finite..." - << std::endl; - // Notice that we split here on all datatypes except the - // truly infinite ones. It is possible to also not split - // on those that are interpreted-finite when finite model - // finding is disabled, but as a heuristic we choose to split - // on those too. - bool ifin = dt[j].getCardinalityClass(tt) - != CardinalityClass::INFINITE; - Trace("datatypes-debug") << "...returned " << ifin - << std::endl; - if (!ifin) - { - if( !eqc || !eqc->d_selectors ){ - needSplit = false; - } - }else{ - if( fconsIndex==-1 ){ - fconsIndex = j; - } - } + TypeNode type = dt.getRecursiveSingletonArgType(tn, i); + if (isQuantifiedLogic) + { + // under the assumption that the cardinality of this type is + // one + Node a = getSingletonLemma(type, true); + assumptions.push_back(a.negate()); } - } - - if( needSplit ) { - if( dt.getNumConstructors()==1 ){ - //this may not be necessary? - //if only one constructor, then this term must be this constructor - Node t = utils::mkTester(n, 0, dt); - d_im.addPendingInference( - t, InferenceId::DATATYPES_SPLIT, d_true); - Trace("datatypes-infer") << "DtInfer : 1-cons (full) : " << t << std::endl; - }else{ - Assert(consIndex != -1 || dt.isSygus()); - if (options().datatypes.dtBinarySplit && consIndex != -1) - { - Node test = utils::mkTester(n, consIndex, dt); - Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; - test = rewrite(test); - NodeBuilder nb(kind::OR); - nb << test << test.notNode(); - Node lemma = nb; - d_im.lemma(lemma, InferenceId::DATATYPES_BINARY_SPLIT); - d_im.requirePhase(test, true); - } - else - { - Trace("dt-split") << "*************Split for constructors on " << n << endl; - Node lemma = utils::mkSplit(n, dt); - Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl; - d_im.sendDtLemma(lemma, - InferenceId::DATATYPES_SPLIT, - LemmaProperty::SEND_ATOMS); - } - if (!options().datatypes.dtBlastSplits) - { - break; - } + else + { + success = false; + // assert that the cardinality of this type is more than one + getSingletonLemma(type, false); } - }else{ - Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl; + } + if (success) + { + Node assumption = n.eqNode(itrs->second); + assumptions.push_back(assumption); + Node lemma = + assumptions.size() == 1 + ? assumptions[0] + : NodeManager::currentNM()->mkNode(OR, assumptions); + Trace("dt-singleton") + << "*************Singleton equality lemma " << lemma + << std::endl; + d_im.lemma(lemma, InferenceId::DATATYPES_REC_SINGLETON_EQ); } } - }else{ - Trace("datatypes-debug") << "Has constructor " << eqc->d_constructor.get() << std::endl; + } + else + { + rec_singletons[tn] = n; + } + // do splitting for quantified logics (incomplete anyways) + if (!isQuantifiedLogic) + { + continue; + } + } + Trace("datatypes-debug") << "Get possible cons..." << std::endl; + // all other cases + std::vector pcons; + getPossibleCons(eqc, n, pcons); + // check if we do not need to resolve the constructor type for this + // equivalence class. + // this is if there are no selectors for this equivalence class, and its + // possible values are infinite, + // then do not split. + int consIndex = -1; + int fconsIndex = -1; + bool needSplit = true; + for (size_t j = 0, psize = pcons.size(); j < psize; j++) + { + if (!pcons[j]) + { + continue; + } + if (consIndex == -1) + { + consIndex = j; + } + Trace("datatypes-debug") << j << " compute finite..." << std::endl; + // Notice that we split here on all datatypes except the + // truly infinite ones. It is possible to also not split + // on those that are interpreted-finite when finite model + // finding is disabled, but as a heuristic we choose to split + // on those too. + bool ifin = + dt[j].getCardinalityClass(tn) != CardinalityClass::INFINITE; + Trace("datatypes-debug") << "...returned " << ifin << std::endl; + if (!ifin) + { + if (!eqc || !eqc->d_selectors) + { + needSplit = false; + break; + } + } + else if (fconsIndex == -1) + { + fconsIndex = j; + } + } + if (!needSplit) + { + Trace("dt-split-debug") + << "Do not split constructor for " << n << " : " << n.getType() + << " " << dt.getNumConstructors() << std::endl; + continue; + } + if (dt.getNumConstructors() == 1) + { + // this may not be necessary? + // if only one constructor, then this term must be this constructor + Node t = utils::mkTester(n, 0, dt); + d_im.addPendingInference(t, InferenceId::DATATYPES_SPLIT, d_true); + Trace("datatypes-infer") + << "DtInfer : 1-cons (full) : " << t << std::endl; + } + else + { + Assert(consIndex != -1 || dt.isSygus()); + if (options().datatypes.dtBinarySplit && consIndex != -1) + { + Node test = utils::mkTester(n, consIndex, dt); + Trace("dt-split") << "*************Split for possible constructor " + << dt[consIndex] << " for " << n << endl; + test = rewrite(test); + NodeBuilder nb(kind::OR); + nb << test << test.notNode(); + Node lemma = nb; + d_im.lemma(lemma, InferenceId::DATATYPES_BINARY_SPLIT); + d_im.requirePhase(test, true); + } + else + { + Trace("dt-split") + << "*************Split for constructors on " << n << endl; + Node lemma = utils::mkSplit(n, dt); + Trace("dt-split-debug") + << "Split lemma is : " << lemma << std::endl; + d_im.sendDtLemma( + lemma, InferenceId::DATATYPES_SPLIT, LemmaProperty::SEND_ATOMS); + } + if (!options().datatypes.dtBlastSplits) + { + break; } } - ++eqcs_i; } if (d_im.hasSentLemma()) {