fix variable naming bug for internal (fresh) constants clashing with external names

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/ast_smt2_pp.cpp

@@ -31,25 +31,11 @@ using namespace format_ns;
 #define MAX_INDENT   16
 #define SMALL_INDENT 2
 
-format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len) const {
+format * smt2_pp_environment::pp_fdecl_name(symbol const & s0, unsigned & len, bool is_skolem) const {
     ast_manager & m = get_manager();
-    if (is_smt2_quoted_symbol(s)) {
-        std::string str = mk_smt2_quoted_symbol(s);
-        len = static_cast<unsigned>(str.length());
-        return mk_string(m, str.c_str());
-    }
-    else if (s.is_numerical()) {
-        std::string str = s.str();
-        len = static_cast<unsigned>(str.length());
-        return mk_string(m, str.c_str());
-    }
-    else if (!s.bare_str()) {
-        return mk_string(m, "null");
-    }
-    else {
-        len = static_cast<unsigned>(strlen(s.bare_str()));
-        return mk_string(m, s.bare_str());
-    }
+    symbol s = m_renaming.get_symbol(s0, is_skolem);
+    len = static_cast<unsigned>(strlen(s.bare_str()));
+    return mk_string(m, s.bare_str());    
 }
 
 format * smt2_pp_environment::pp_fdecl_name(func_decl * f, unsigned & len) const {
@@ -68,7 +54,7 @@ format * smt2_pp_environment::pp_fdecl_name(func_decl * f, unsigned & len) const
     }
     else {
         symbol s = f->get_name();
-        return pp_fdecl_name(s, len);
+        return pp_fdecl_name(s, len, f->is_skolem());
     }
 }
 

src/ast/ast_smt2_pp.h

@@ -31,10 +31,12 @@ Revision History:
 #include "ast/dl_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/datatype_decl_plugin.h"
+#include "ast/ast_smt_pp.h"
 #include "util/smt2_util.h"
 
 class smt2_pp_environment {
 protected:
+    mutable smt_renaming m_renaming;
     format_ns::format * mk_neg(format_ns::format * f) const;
     format_ns::format * mk_float(rational const & val) const;
     bool is_indexed_fdecl(func_decl * f) const;
@@ -61,7 +63,7 @@ public:
     virtual format_ns::format * pp_string_literal(app * t);
     virtual format_ns::format * pp_sort(sort * s);
     virtual format_ns::format * pp_fdecl_ref(func_decl * f);
-    format_ns::format * pp_fdecl_name(symbol const & fname, unsigned & len) const;
+    format_ns::format * pp_fdecl_name(symbol const & fname, unsigned & len, bool is_skolem) const;
     format_ns::format * pp_fdecl_name(func_decl * f, unsigned & len) const;
 };
 

src/ast/ast_smt_pp.cpp

@@ -70,7 +70,10 @@ symbol smt_renaming::fix_symbol(symbol s, int k) {
         return symbol(buffer.str().c_str());
     }
 
-    if (is_smt2_quoted_symbol(s)) {
+    if (!s.bare_str()) {
+        buffer << "null";
+    }
+    else if (is_smt2_quoted_symbol(s)) {
         buffer << mk_smt2_quoted_symbol(s);
     }
     else {
@@ -129,14 +132,21 @@ smt_renaming::smt_renaming() {
     }
 }
 
-
+// Ensure that symbols that are used both with skolems and non-skolems are named apart.
 symbol smt_renaming::get_symbol(symbol s0, bool is_skolem) {
     sym_b sb;
     symbol s;
     if (m_translate.find(s0, sb)) {
         if (is_skolem == sb.is_skolem)
             return sb.name;
-        NOT_IMPLEMENTED_YET();
+        int k = 0;
+        symbol s1;
+        do {
+            s = fix_symbol(s0, k++);
+        }
+        while (s == s0 || (m_rev_translate.find(s, s1) && s1 != s0));
+        m_rev_translate.insert(s, s0);
+        return s;
     }
 
     int k = 0;

src/cmd_context/cmd_context.cpp

@@ -389,7 +389,7 @@ protected:
     datalog::dl_decl_util m_dlutil;
 
     format_ns::format * pp_fdecl_name(symbol const & s, func_decls const & fs, func_decl * f, unsigned & len) {
-        format_ns::format * f_name = smt2_pp_environment::pp_fdecl_name(s, len);
+        format_ns::format * f_name = smt2_pp_environment::pp_fdecl_name(s, len, f->is_skolem());
         if (!fs.more_than_one())
             return f_name;
         if (!fs.clash(f))
@@ -399,7 +399,7 @@ protected:
 
     format_ns::format * pp_fdecl_ref_core(symbol const & s, func_decls const & fs, func_decl * f) {
         unsigned len;
-        format_ns::format * f_name = smt2_pp_environment::pp_fdecl_name(s, len);
+        format_ns::format * f_name = smt2_pp_environment::pp_fdecl_name(s, len, f->is_skolem());
         if (!fs.more_than_one())
             return f_name;
         return pp_signature(f_name, f);

src/sat/ba_solver.cpp

@@ -1173,7 +1173,7 @@ namespace sat {
                 break;
             case justification::CLAUSE: {
                 inc_bound(offset); 
-                clause & c = *(s().m_cls_allocator.get_clause(js.get_clause_offset()));
+                clause & c = s().get_clause(js);
                 unsigned i = 0;
                 if (consequent != null_literal) {
                     inc_coeff(consequent, offset);
@@ -3780,7 +3780,7 @@ namespace sat {
             break;
         case justification::CLAUSE: {
             ineq.reset(offset);
-            clause & c = *(s().m_cls_allocator.get_clause(js.get_clause_offset()));
+            clause & c = s().get_clause(js);
             for (literal l : c) ineq.push(l, offset);
             break;
         }