Optimizations for datatypes: check for clashes modulo equality. Avoid building model...

[cvc5.git] / src / theory / quantifiers / rewrite_engine.h

diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index f8580361771ab06586b70d365a243d26afa4d59b..a16a6d5987cc38eb3031d85dc3ac6acfbf9fffce 100644 (file)
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -56,7 +56,9 @@ public:
 
   void check( Theory::Effort e );
   void registerQuantifier( Node f );
-  void assertNode( Node n );
+  void assertNode( Node n );  
+  /** Identify this module */
+  std::string identify() const { return "RewriteEngine"; }
 };
 
 }