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<Node> 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<TypeNode, Node> 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<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 (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<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++)
- {
- 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
}
}
+void TheoryDatatypes::checkSplit()
+{
+ // get the relevant term set, currently all datatype equivalence classes
+ // in the equality engine
+ std::set<Node> 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<TypeNode, Node> 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<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 (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<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++)
+ {
+ 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 ){
projects / cvc5.git / commitdiff