summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/equality_query.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/equality_query.h')
-rw-r--r--src/theory/quantifiers/equality_query.h4
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index 9944bf703..86b07a643 100644
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -27,7 +27,6 @@ namespace CVC4 {
namespace theory {
namespace quantifiers {
-class TermDb;
class FirstOrderModel;
/** EqualityQueryQuantifiersEngine class
@@ -44,7 +43,6 @@ class EqualityQueryQuantifiersEngine : public QuantifiersUtil
{
public:
EqualityQueryQuantifiersEngine(QuantifiersState& qs,
- TermDb* tdb,
FirstOrderModel* m);
virtual ~EqualityQueryQuantifiersEngine();
/** reset */
@@ -72,8 +70,6 @@ class EqualityQueryQuantifiersEngine : public QuantifiersUtil
private:
/** the quantifiers state */
QuantifiersState& d_qstate;
- /** Pointer to the term database */
- TermDb* d_tdb;
/** Pointer to the model */
FirstOrderModel* d_model;
/** quantifiers equality inference */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback