diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-13 17:36:01 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-13 17:36:01 +0200 |
commit | c369afa180b7cb3d9388c39d18fcb81e8246ff21 (patch) | |
tree | 149026fe09eb96fa338c3869ac7da78f12448a93 /src/theory/theory.cpp | |
parent | 96dcf80d249ecbf12f1e3a0cd473deade007a1c3 (diff) |
sygusComp2018: optimization for collect model info (#2105)
Diffstat (limited to 'src/theory/theory.cpp')
-rw-r--r-- | src/theory/theory.cpp | 34 |
1 files changed, 26 insertions, 8 deletions
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); } } |