Also updates minor things to meet coding standards and makes it so that children in the trie are not dynamically allocated.
theory/quantifiers/ematching/instantiation_engine.h
theory/quantifiers/ematching/trigger.cpp
theory/quantifiers/ematching/trigger.h
+ theory/quantifiers/ematching/trigger_trie.cpp
+ theory/quantifiers/ematching/trigger_trie.h
theory/quantifiers/equality_infer.cpp
theory/quantifiers/equality_infer.h
theory/quantifiers/equality_query.cpp
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<d_tr.size(); i++ ){
- delete d_tr[i];
- }
-}
-
-inst::Trigger* TriggerTrie::getTrigger(std::vector<Node>& nodes)
-{
- std::vector<Node> 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<TNode, TriggerTrie*>::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<Node>& nodes, inst::Trigger* t)
-{
- std::vector<Node> 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<TNode, TriggerTrie*>::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 */
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<Node>& 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<Node>& nodes, Trigger* t);
-
- private:
- /** The trigger at this node in the trie. */
- std::vector<Trigger*> 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 */
--- /dev/null
+/********************* */
+/*! \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<Node>& nodes)
+{
+ std::vector<Node> 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<TNode, TriggerTrie>::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<Node>& nodes, inst::Trigger* t)
+{
+ std::vector<Node> temp(nodes.begin(), nodes.end());
+ std::sort(temp.begin(), temp.end());
+ TriggerTrie* tt = this;
+ for (const Node& n : temp)
+ {
+ std::map<TNode, TriggerTrie>::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
--- /dev/null
+/********************* */
+/*! \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 <vector>
+
+#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<Node>& nodes);
+ /**
+ * This adds t to the trie, indexed by nodes. In typical use cases, nodes i
+ * t->d_nodes.
+ */
+ void addTrigger(std::vector<Node>& nodes, Trigger* t);
+ private:
+ /** The trigger at this node in the trie. */
+ std::vector<Trigger*> d_tr;
+ /** The children of this node in the trie. */
+ std::map<TNode, TriggerTrie> d_children;
+}; /* class inst::Trigger::TriggerTrie */
+
+} // namespace inst
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H */
#include "context/cdlist.h"
#include "expr/attribute.h"
#include "expr/term_canonize.h"
-#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
#include "theory/quantifiers/equality_query.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/model_builder.h"
projects / cvc5.git / commitdiff