summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2021-03-29 19:52:48 -0500
committerGitHub <noreply@github.com>2021-03-30 00:52:48 +0000
commit7e5fe049ad88405a90fd5a43caa872d646d4b8e2 (patch)
tree2fe225b29e2721c8d5237f0628e2a393a001bc99 /src/theory/quantifiers/term_database.h
parentef31c2518c194029a913fe2872e2040d2f5e4294 (diff)
Miscellaneous elimination of dependencies on quantifiers engine (#6238)
This should be the last PR before quantifiers engine will not be passed to quantifiers modules.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
-rw-r--r--src/theory/quantifiers/term_database.h4
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 6506a6123..bafaa8bdd 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -30,9 +30,6 @@
namespace CVC4 {
namespace theory {
-
-class QuantifiersEngine;
-
namespace quantifiers {
class QuantifiersState;
@@ -67,7 +64,6 @@ class DbList
* lazily for performance reasons.
*/
class TermDb : public QuantifiersUtil {
- friend class ::CVC4::theory::QuantifiersEngine;
using NodeBoolMap = context::CDHashMap<Node, bool, NodeHashFunction>;
using NodeList = context::CDList<Node>;
using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback