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.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index ecec6f8c37af84a6f5274d5192140e2fbf3ae539..16585447669ad222d0cca1a0189ed9eb201ad567 100644 (file)
--- 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 65f6e9e57f1f47a0580f12797b677d2cb22bb5bc..da0bc842773780e2e01611f0f3101b93061dd656 100644 (file)
--- 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 e9f0e04ea172e0b3eb2466c75b8c4218e870e055..02e5d814da2e2f9e5942d9f415566a7d787d6c3a 100644 (file)
--- 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 cb8ad944a94dc84c88db73449fe4a08dc9acafad..786b60bb375310d3124289cb450a3b802c471c56 100644 (file)
--- 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");
+}