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 /src/api/cvc4cpp.cpp | |
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.
Diffstat (limited to 'src/api/cvc4cpp.cpp')
-rw-r--r-- | src/api/cvc4cpp.cpp | 25 |
1 files changed, 23 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) |