From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri, 6 Jun 2014 23:40:18 +0000 (-0400)
Subject: sets translator: fix for dags
X-Git-Tag: cvc5-1.0.0~6847^2~4
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=21965968150ec8d84b12a9555063e0a6451cb62a;p=cvc5.git

sets translator: fix for dags
---

diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index 6cf2b61e2..5b0a9c3d0 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -43,6 +43,7 @@ class Mapper {
   hash_map< Expr, Expr, ExprHashFunction > substitutions;
   ostringstream sout;
   ExprManager* em;
+  int depth;
 
   Expr add(SetType t, Expr e) {
 
@@ -140,7 +141,7 @@ class Mapper {
   }
 
 public:
-  Mapper(ExprManager* e) : em(e) {
+  Mapper(ExprManager* e) : em(e),depth(0) {
     sout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
   }
 
@@ -153,17 +154,24 @@ public:
 
   Expr collectSortsExpr(Expr e)
   {
+    if(substitutions.find(e) != substitutions.end()) {
+      return substitutions[e];
+    }
+    ++depth;
     Expr old_e = e;
     for(unsigned i = 0; i < e.getNumChildren(); ++i) {
       collectSortsExpr(e[i]);
     }
     e = e.substitute(substitutions);
+    // cout << "[debug] " << e << " " << e.getKind() << " " << theory::kindToTheoryId(e.getKind()) << endl;
     if(theory::kindToTheoryId(e.getKind()) == theory::THEORY_SETS) {
       SetType t = SetType(e.getType().isBoolean() ? e[1].getType() : e.getType());
       substitutions[e] = add(t, e);
       e = e.substitute(substitutions);
     }
-    // cout << old_e << " => " << e << endl;
+    substitutions[old_e] = e;
+    // cout << ";"; for(int i = 0; i < depth; ++i) cout << " "; cout << old_e << " => " << e << endl;
+    --depth;
     return e;
   }
 
@@ -187,6 +195,7 @@ int main(int argc, char* argv[])
     Options options;
     options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
     cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+    // cout << Expr::dag(0);
     ExprManager exprManager(options);
 
     Mapper m(&exprManager);