+ /**
+ * 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);