From 35d080bfb56ff96fd41b31ce7025c019193f6abc Mon Sep 17 00:00:00 2001
From: makaimann <makaim@stanford.edu>
Date: Thu, 8 Oct 2020 09:35:56 -0700
Subject: [PATCH] Get correct NodeManagerScope for toStrings in API (#5216)

Gets the correct `NodeManagerScope` for getting the `toString` of a term, op, or sort. The following program had strange output:
```
#include "cvc4/api/cvc4cpp.h"
using namespace CVC4::api;
using namespace std;
int main()
{
  Solver s;
  Term x = s.mkConst(s.getIntegerSort(), "x");
  cout << "x = " << x << endl;
  Solver s2;
  cout << "x = " << x << endl;
  return 0;
}
```

It was outputting:
```
x = x
x = var_267
```

Fixing the scope makes the output `x = x` both times, as expected.
---
 src/api/cvc4cpp.cpp        | 25 +++++++++++++++++++++++--
 test/unit/api/op_black.h   | 10 ++++++++++
 test/unit/api/sort_black.h | 14 ++++++++++++++
 test/unit/api/term_black.h | 11 +++++++++++
 4 files changed, 58 insertions(+), 2 deletions(-)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index ecec6f8c3..165854476 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1060,7 +1060,15 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
                   .toType());
 }
 
-std::string Sort::toString() const { return d_type->toString(); }
+std::string Sort::toString() const
+{
+  if (d_solver != nullptr)
+  {
+    NodeManagerScope scope(d_solver->getNodeManager());
+    return d_type->toString();
+  }
+  return d_type->toString();
+}
 
 // !!! This is only temporarily available until the parser is fully migrated
 // to the new API. !!!
@@ -1481,6 +1489,11 @@ std::string Op::toString() const
   {
     CVC4_API_CHECK(!d_node->isNull())
         << "Expecting a non-null internal expression";
+    if (d_solver != nullptr)
+    {
+      NodeManagerScope scope(d_solver->getNodeManager());
+      return d_node->toString();
+    }
     return d_node->toString();
   }
 }
@@ -1858,7 +1871,15 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) const
   }
 }
 
-std::string Term::toString() const { return d_node->toString(); }
+std::string Term::toString() const
+{
+  if (d_solver != nullptr)
+  {
+    NodeManagerScope scope(d_solver->getNodeManager());
+    return d_node->toString();
+  }
+  return d_node->toString();
+}
 
 Term::const_iterator::const_iterator()
     : d_solver(nullptr), d_origNode(nullptr), d_pos(0)
diff --git a/test/unit/api/op_black.h b/test/unit/api/op_black.h
index 65f6e9e57..da0bc8427 100644
--- a/test/unit/api/op_black.h
+++ b/test/unit/api/op_black.h
@@ -31,6 +31,8 @@ class OpBlack : public CxxTest::TestSuite
   void testGetIndicesUint();
   void testGetIndicesPairUint();
 
+  void testOpScopingToString();
+
  private:
   Solver d_solver;
 };
@@ -185,3 +187,11 @@ void OpBlack::testGetIndicesPairUint()
   TS_ASSERT_THROWS(floatingpoint_to_fp_generic_ot.getIndices<std::string>(),
                    CVC4ApiException&);
 }
+
+void OpBlack::testOpScopingToString()
+{
+  Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
+  std::string op_repr = bitvector_repeat_ot.toString();
+  Solver solver2;
+  TS_ASSERT_EQUALS(bitvector_repeat_ot.toString(), op_repr);
+}
diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
index e9f0e04ea..02e5d814d 100644
--- a/test/unit/api/sort_black.h
+++ b/test/unit/api/sort_black.h
@@ -54,6 +54,8 @@ class SortBlack : public CxxTest::TestSuite
   void testSortCompare();
   void testSortSubtyping();
 
+  void testSortScopedToString();
+
  private:
   Solver d_solver;
 };
@@ -385,3 +387,15 @@ void SortBlack::testSortSubtyping()
   TS_ASSERT(!setSortR.isComparableTo(setSortI));
   TS_ASSERT(!setSortR.isSubsortOf(setSortI));
 }
+
+void SortBlack::testSortScopedToString()
+{
+  std::string name = "uninterp-sort";
+  Sort bvsort8 = d_solver.mkBitVectorSort(8);
+  Sort uninterp_sort = d_solver.mkUninterpretedSort(name);
+  TS_ASSERT_EQUALS(bvsort8.toString(), "(_ BitVec 8)");
+  TS_ASSERT_EQUALS(uninterp_sort.toString(), name);
+  Solver solver2;
+  TS_ASSERT_EQUALS(bvsort8.toString(), "(_ BitVec 8)");
+  TS_ASSERT_EQUALS(uninterp_sort.toString(), name);
+}
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index cb8ad944a..786b60bb3 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -46,6 +46,8 @@ class TermBlack : public CxxTest::TestSuite
   void testConstArray();
   void testConstSequenceElements();
 
+  void testTermScopedToString();
+
  private:
   Solver d_solver;
 };
@@ -796,3 +798,12 @@ void TermBlack::testConstSequenceElements()
   Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1));
   TS_ASSERT_THROWS(su.getConstSequenceElements(), CVC4ApiException&);
 }
+
+void TermBlack::testTermScopedToString()
+{
+  Sort intsort = d_solver.getIntegerSort();
+  Term x = d_solver.mkConst(intsort, "x");
+  TS_ASSERT_EQUALS(x.toString(), "x");
+  Solver solver2;
+  TS_ASSERT_EQUALS(x.toString(), "x");
+}
-- 
2.30.2