X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Ftheory%2Fquantifiers%2Fdynamic_rewrite.h;h=6d2267adf18862a1add2e40979b886b8bfe239e8;hb=e37d0c385d698d46f14fb30e5a44de63c686fadb;hp=56f59147072085d1f28b43c06c2db66689a92cb7;hpb=f1d4d477d7cbfb6c8ba79232986a4135c5647e4a;p=cvc5.git

diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h
index 56f591470..6d2267adf 100644
--- a/src/theory/quantifiers/dynamic_rewrite.h
+++ b/src/theory/quantifiers/dynamic_rewrite.h
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file dynamic_rewriter.h
+/*! \file dynamic_rewrite.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** 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
@@ -14,13 +14,12 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
-#define __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
+#ifndef CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
+#define CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
 
 #include <map>
 
 #include "context/cdlist.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
@@ -55,7 +54,7 @@ class DynamicRewriter
   typedef context::CDList<Node> NodeList;
 
  public:
-  DynamicRewriter(const std::string& name, QuantifiersEngine* qe);
+  DynamicRewriter(const std::string& name, context::UserContext* u);
   ~DynamicRewriter() {}
   /** inform this class that the equality a = b holds. */
   void addRewrite(Node a, Node b);
@@ -63,10 +62,19 @@ class DynamicRewriter
    * Check whether this class knows that the equality a = b holds.
    */
   bool areEqual(Node a, Node b);
+  /**
+   * Convert node a to its internal representation, which replaces all
+   * interpreted operators in a by a unique uninterpreted symbol.
+   */
+  Node toInternal(Node a);
+  /**
+   * Convert internal node ai to its original representation. It is the case
+   * that toExternal(toInternal(a))=a. If ai is not a term returned by
+   * toInternal, this method returns null.
+   */
+  Node toExternal(Node ai);
 
  private:
-  /** pointer to the quantifiers engine */
-  QuantifiersEngine* d_qe;
   /** index over argument types to function skolems
    *
    * The purpose of this trie is to associate a class of interpreted operator
@@ -99,13 +107,10 @@ class DynamicRewriter
   };
   /** the internal operator symbol trie for this class */
   std::map<Node, OpInternalSymTrie> d_ois_trie;
-  /**
-   * Convert node a to its internal representation, which replaces all
-   * interpreted operators in a by a unique uninterpreted symbol.
-   */
-  Node toInternal(Node a);
   /** cache of the above function */
   std::map<Node, Node> d_term_to_internal;
+  /** inverse of the above map */
+  std::map<Node, Node> d_internal_to_term;
   /** stores congruence closure over terms given to this class. */
   eq::EqualityEngine d_equalityEngine;
   /** list of all equalities asserted to equality engine */
@@ -116,4 +121,4 @@ class DynamicRewriter
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */