diff options
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 52 | ||||
| -rw-r--r-- | src/theory/theory.cpp | 34 | ||||
| -rw-r--r-- | src/theory/theory.h | 17 | ||||
| -rw-r--r-- | test/regress/regress0/tptp/DAT001=1.p | 1 |
4 files changed, 77 insertions, 27 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index bfd7a5509..e3b48a4da 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -2226,35 +2226,53 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& void TheoryDatatypes::getRelevantTerms( std::set<Node>& termSet ) { // Compute terms appearing in assertions and shared terms - computeRelevantTerms(termSet); - + std::set<Kind> irr_kinds; + // testers are not relevant for model construction + irr_kinds.insert(APPLY_TESTER); + computeRelevantTerms(termSet, irr_kinds); + + Trace("dt-cmi") << "Have " << termSet.size() << " relevant terms..." + << std::endl; + //also include non-singleton equivalence classes TODO : revisit this eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ TNode r = (*eqcs_i); bool addedFirst = false; Node first; - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, &d_equalityEngine ); - while( !eqc_i.isFinished() ){ - TNode n = (*eqc_i); - if( first.isNull() ){ - first = n; - //always include all datatypes - if( n.getType().isDatatype() ){ - addedFirst = true; - termSet.insert( n ); + TypeNode rtn = r.getType(); + if (!rtn.isBoolean()) + { + eq::EqClassIterator eqc_i = eq::EqClassIterator(r, &d_equalityEngine); + while (!eqc_i.isFinished()) + { + TNode n = (*eqc_i); + if (first.isNull()) + { + first = n; + // always include all datatypes + if (rtn.isDatatype()) + { + addedFirst = true; + termSet.insert(n); + } } - }else{ - if( !addedFirst ){ - addedFirst = true; - termSet.insert( first ); + else + { + if (!addedFirst) + { + addedFirst = true; + termSet.insert(first); + } + termSet.insert(n); } - termSet.insert( n ); + ++eqc_i; } - ++eqc_i; } ++eqcs_i; } + Trace("dt-cmi") << "After adding non-singletons, has " << termSet.size() + << " relevant terms..." << std::endl; } std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* out) { diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 10504b487..311776693 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -232,17 +232,24 @@ std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() cons return currentlyShared; } - -void Theory::collectTerms(TNode n, set<Node>& termSet) const +void Theory::collectTerms(TNode n, + set<Kind>& irrKinds, + set<Node>& termSet) const { if (termSet.find(n) != termSet.end()) { return; } - Trace("theory::collectTerms") << "Theory::collectTerms: adding " << n << endl; - termSet.insert(n); - if (n.getKind() == kind::NOT || n.getKind() == kind::EQUAL || !isLeaf(n)) { + Kind nk = n.getKind(); + if (irrKinds.find(nk) == irrKinds.end()) + { + Trace("theory::collectTerms") + << "Theory::collectTerms: adding " << n << endl; + termSet.insert(n); + } + if (nk == kind::NOT || nk == kind::EQUAL || !isLeaf(n)) + { for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) { - collectTerms(*child_it, termSet); + collectTerms(*child_it, irrKinds, termSet); } } } @@ -250,18 +257,29 @@ void Theory::collectTerms(TNode n, set<Node>& termSet) const void Theory::computeRelevantTerms(set<Node>& termSet, bool includeShared) const { + set<Kind> irrKinds; + computeRelevantTerms(termSet, irrKinds, includeShared); +} + +void Theory::computeRelevantTerms(set<Node>& termSet, + set<Kind>& irrKinds, + bool includeShared) const +{ // Collect all terms appearing in assertions + irrKinds.insert(kind::EQUAL); + irrKinds.insert(kind::NOT); context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end(); for (; assert_it != assert_it_end; ++assert_it) { - collectTerms(*assert_it, termSet); + collectTerms(*assert_it, irrKinds, termSet); } if (!includeShared) return; // Add terms that are shared terms + set<Kind> kempty; context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end(); for (; shared_it != shared_it_end; ++shared_it) { - collectTerms(*shared_it, termSet); + collectTerms(*shared_it, kempty, termSet); } } diff --git a/src/theory/theory.h b/src/theory/theory.h index 3721806ad..2c3c727cb 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -161,14 +161,27 @@ private: /** * Helper function for computeRelevantTerms */ - void collectTerms(TNode n, std::set<Node>& termSet) const; + void collectTerms(TNode n, + std::set<Kind>& irrKinds, + std::set<Node>& termSet) const; /** * Scans the current set of assertions and shared terms top-down * until a theory-leaf is reached, and adds all terms found to * termSet. This is used by collectModelInfo to delimit the set of - * terms that should be used when constructing a model + * terms that should be used when constructing a model. + * + * irrKinds: The kinds of terms that appear in assertions that should *not* + * be included in termSet. Note that the kinds EQUAL and NOT are always + * treated as irrelevant kinds. + * + * includeShared: Whether to include shared terms in termSet. Notice that + * shared terms are not influenced by irrKinds. */ + void computeRelevantTerms(std::set<Node>& termSet, + std::set<Kind>& irrKinds, + bool includeShared = true) const; + /** same as above, but with empty irrKinds */ void computeRelevantTerms(std::set<Node>& termSet, bool includeShared = true) const; /** diff --git a/test/regress/regress0/tptp/DAT001=1.p b/test/regress/regress0/tptp/DAT001=1.p index 922a6cfc3..f30db563a 100644 --- a/test/regress/regress0/tptp/DAT001=1.p +++ b/test/regress/regress0/tptp/DAT001=1.p @@ -1,3 +1,4 @@ +% COMMAND-LINE: --no-finite-model-find %------------------------------------------------------------------------------ % File : DAT001=1 : TPTP v5.5.0. Released v5.0.0. % Domain : Data Structures |