more major cleanup of quantifiers code, separating rewrite-rules-specific code from quantifiers-specific code

1 files changed, 25 insertions, 0 deletions

diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 1479f910e..18aaab01f 100755
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -18,6 +18,7 @@
 #define __CVC4__THEORY__QUANT_UTIL_H

 

 #include "theory/theory.h"

+#include "theory/uf/equality_engine.h"

 

 #include <ext/hash_set>

 #include <iostream>

@@ -71,6 +72,30 @@ public:
   std::map< Node, Node > d_phase_reqs_equality_term;

 };

 

+

+class EqualityQuery {

+public:

+  EqualityQuery(){}

+  virtual ~EqualityQuery(){};

+  /** contains term */

+  virtual bool hasTerm( Node a ) = 0;

+  /** get the representative of the equivalence class of a */

+  virtual Node getRepresentative( Node a ) = 0;

+  /** returns true if a and b are equal in the current context */

+  virtual bool areEqual( Node a, Node b ) = 0;

+  /** returns true is a and b are disequal in the current context */

+  virtual bool areDisequal( Node a, Node b ) = 0;

+  /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.

+      If cbqi is active, this will return a term in the equivalence class of "a" that does

+      not contain instantiation constants, if such a term exists.

+   */

+  virtual Node getInternalRepresentative( Node a ) = 0;

+  /** get the equality engine associated with this query */

+  virtual eq::EqualityEngine* getEngine() = 0;

+  /** get the equivalence class of a */

+  virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;

+};/* class EqualityQuery */

+

 }

 }