From aac53f510e1f21a46a49cb31475a8851a3097089 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 15 Dec 2020 17:55:06 -0600 Subject: Move trigger trie to own file (#5680) Also updates minor things to meet coding standards and makes it so that children in the trie are not dynamically allocated. --- src/theory/quantifiers/ematching/trigger.cpp | 60 ------------------ src/theory/quantifiers/ematching/trigger.h | 29 --------- src/theory/quantifiers/ematching/trigger_trie.cpp | 75 +++++++++++++++++++++++ src/theory/quantifiers/ematching/trigger_trie.h | 62 +++++++++++++++++++ 4 files changed, 137 insertions(+), 89 deletions(-) create mode 100644 src/theory/quantifiers/ematching/trigger_trie.cpp create mode 100644 src/theory/quantifiers/ematching/trigger_trie.h (limited to 'src/theory/quantifiers') diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 62aa1bcc0..654b1fd12 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -942,66 +942,6 @@ int Trigger::getActiveScore() { return d_mg->getActiveScore( d_quantEngine ); } -TriggerTrie::TriggerTrie() -{} - -TriggerTrie::~TriggerTrie() { - for(std::map< TNode, TriggerTrie* >::iterator i = d_children.begin(), iend = d_children.end(); - i != iend; ++i) { - TriggerTrie* current = (*i).second; - delete current; - } - d_children.clear(); - - for( unsigned i=0; i& nodes) -{ - std::vector temp; - temp.insert(temp.begin(), nodes.begin(), nodes.end()); - std::sort(temp.begin(), temp.end()); - TriggerTrie* tt = this; - for (const Node& n : temp) - { - std::map::iterator itt = tt->d_children.find(n); - if (itt == tt->d_children.end()) - { - return NULL; - } - else - { - tt = itt->second; - } - } - return tt->d_tr.empty() ? NULL : tt->d_tr[0]; -} - -void TriggerTrie::addTrigger(std::vector& nodes, inst::Trigger* t) -{ - std::vector temp; - temp.insert(temp.begin(), nodes.begin(), nodes.end()); - std::sort(temp.begin(), temp.end()); - TriggerTrie* tt = this; - for (const Node& n : temp) - { - std::map::iterator itt = tt->d_children.find(n); - if (itt == tt->d_children.end()) - { - TriggerTrie* ttn = new TriggerTrie; - tt->d_children[n] = ttn; - tt = ttn; - } - else - { - tt = itt->second; - } - } - tt->d_tr.push_back(t); -} - }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 7b0b51fb6..890811c8b 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -447,35 +447,6 @@ class Trigger { IMGenerator* d_mg; }; /* class Trigger */ -/** A trie of triggers. -* -* This class is used to cache all Trigger objects that are generated in the -* current context. We index Triggers in this data structure based on the -* value of Trigger::d_nodes. When a Trigger is added to this data structure, -* this Trie assumes responsibility for deleting it. -*/ -class TriggerTrie { -public: - TriggerTrie(); - ~TriggerTrie(); - /** get trigger - * This returns a Trigger t that is indexed by nodes, - * or NULL otherwise. - */ - Trigger* getTrigger(std::vector& nodes); - /** add trigger - * This adds t to the trie, indexed by nodes. - * In typical use cases, nodes is t->d_nodes. - */ - void addTrigger(std::vector& nodes, Trigger* t); - - private: - /** The trigger at this node in the trie. */ - std::vector d_tr; - /** The children of this node in the trie. */ - std::map< TNode, TriggerTrie* > d_children; -};/* class inst::Trigger::TriggerTrie */ - }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/ematching/trigger_trie.cpp b/src/theory/quantifiers/ematching/trigger_trie.cpp new file mode 100644 index 000000000..bb70a18fe --- /dev/null +++ b/src/theory/quantifiers/ematching/trigger_trie.cpp @@ -0,0 +1,75 @@ +/********************* */ +/*! \file trigger_trie.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of trigger trie class + **/ + +#include "theory/quantifiers/ematching/trigger_trie.h" + +namespace CVC4 { +namespace theory { +namespace inst { + +TriggerTrie::TriggerTrie() {} + +TriggerTrie::~TriggerTrie() +{ + for (size_t i = 0, ntriggers = d_tr.size(); i < ntriggers; i++) + { + delete d_tr[i]; + } +} + +inst::Trigger* TriggerTrie::getTrigger(std::vector& nodes) +{ + std::vector temp; + temp.insert(temp.begin(), nodes.begin(), nodes.end()); + std::sort(temp.begin(), temp.end()); + TriggerTrie* tt = this; + for (const Node& n : temp) + { + std::map::iterator itt = tt->d_children.find(n); + if (itt == tt->d_children.end()) + { + return nullptr; + } + else + { + tt = &(itt->second); + } + } + return tt->d_tr.empty() ? nullptr : tt->d_tr[0]; +} + +void TriggerTrie::addTrigger(std::vector& nodes, inst::Trigger* t) +{ + std::vector temp(nodes.begin(), nodes.end()); + std::sort(temp.begin(), temp.end()); + TriggerTrie* tt = this; + for (const Node& n : temp) + { + std::map::iterator itt = tt->d_children.find(n); + if (itt == tt->d_children.end()) + { + TriggerTrie* ttn = &tt->d_children[n]; + tt = ttn; + } + else + { + tt = &(itt->second); + } + } + tt->d_tr.push_back(t); +} + +} // namespace inst +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/ematching/trigger_trie.h b/src/theory/quantifiers/ematching/trigger_trie.h new file mode 100644 index 000000000..1ff995bb8 --- /dev/null +++ b/src/theory/quantifiers/ematching/trigger_trie.h @@ -0,0 +1,62 @@ +/********************* */ +/*! \file trigger_trie.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Mathias Preiner, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief trigger trie class + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H +#define CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H + +#include + +#include "expr/node.h" +#include "theory/quantifiers/ematching/trigger.h" + +namespace CVC4 { +namespace theory { + +namespace inst { + +/** A trie of triggers. + * + * This class is used to cache all Trigger objects that are generated in the + * current context. We index Triggers in this data structure based on the + * value of Trigger::d_nodes. When a Trigger is added to this data structure, + * this Trie assumes responsibility for deleting it. + */ +class TriggerTrie +{ + public: + TriggerTrie(); + ~TriggerTrie(); + /** + * This returns a Trigger t that is indexed by nodes, or nullptr otherwise. + */ + Trigger* getTrigger(std::vector& nodes); + /** + * This adds t to the trie, indexed by nodes. In typical use cases, nodes i + * t->d_nodes. + */ + void addTrigger(std::vector& nodes, Trigger* t); + private: + /** The trigger at this node in the trie. */ + std::vector d_tr; + /** The children of this node in the trie. */ + std::map d_children; +}; /* class inst::Trigger::TriggerTrie */ + +} // namespace inst +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H */ -- cgit v1.2.3