From a6b48affa1382dc9b307e2c82dc5a16eac549d08 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 28 Apr 2022 11:38:28 -0500 Subject: [PATCH] Move datatype split inference scheme to its own method (#8664) --- src/theory/datatypes/theory_datatypes.cpp | 377 +++++++++++----------- src/theory/datatypes/theory_datatypes.h | 8 + 2 files changed, 196 insertions(+), 189 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index c5ebd0cef..5824b46cf 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -210,195 +210,8 @@ void TheoryDatatypes::postCheck(Effort level) Trace("datatypes-debug") << "Check for splits " << endl; do { d_im.reset(); - // 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 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(); - 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++) - { - 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()); - } - else - { - success = false; - // assert that the cardinality of this type is more than one - getSingletonLemma(type, false); - } - } - 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 - { - 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; - } - } - } + // check for splits + checkSplit(); if (d_im.hasSentLemma()) { // clear pending facts: we added a lemma, so internal inferences are @@ -1709,6 +1522,192 @@ Node TheoryDatatypes::searchForCycle(TNode n, } } +void TheoryDatatypes::checkSplit() +{ + // 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 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(); + 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++) + { + 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()); + } + else + { + success = false; + // assert that the cardinality of this type is more than one + getSingletonLemma(type, false); + } + } + 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 + { + 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) + { + return; + } + } + } +} + bool TheoryDatatypes::hasTerm(TNode a) { return d_equalityEngine->hasTerm(a); } bool TheoryDatatypes::areEqual( TNode a, TNode b ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index a9072b419..ed0501cef 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -249,6 +249,14 @@ private: std::map& proc, std::vector& explanation, bool firstTime = true); + /** + * Applying splitting. + * + * This checks if we should add a splitting inference for datatype terms + * currently in the equality engine. If so, we add pending lemmas on the + * inference manager. + */ + void checkSplit(); /** for checking whether two codatatype terms must be equal */ void separateBisimilar(std::vector& part, std::vector >& part_out, -- 2.30.2