diff options
author | makaimann <makaim@stanford.edu> | 2020-10-08 09:35:56 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-08 09:35:56 -0700 |
commit | 35d080bfb56ff96fd41b31ce7025c019193f6abc (patch) | |
tree | 71eb7ddcb5743d0ee85899738eb2903098964df6 | |
parent | 900a7217f8843a17f5ea6bb744b6013f2f394ed7 (diff) |
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.
-rw-r--r-- | src/api/cvc4cpp.cpp | 25 | ||||
-rw-r--r-- | test/unit/api/op_black.h | 10 | ||||
-rw-r--r-- | test/unit/api/sort_black.h | 14 | ||||
-rw-r--r-- | 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"); +} |