diff options
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index bbe5b5459..c0e6bad5f 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3187,6 +3187,19 @@ Term Solver::mkCharFromStrHelper(const std::string& s) const return mkValHelper<CVC4::String>(CVC4::String(cpts)); } +Term Solver::getValueHelper(Term term) const +{ + Node value = d_smtEngine->getValue(*term.d_node); + Term res = Term(this, value); + // May need to wrap in real cast so that user know this is a real. + TypeNode tn = (*term.d_node).getType(); + if (!tn.isInteger() && value.getType().isInteger()) + { + return ensureRealSort(res); + } + return res; +} + Term Solver::mkTermFromKind(Kind kind) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -5130,7 +5143,7 @@ Term Solver::getValue(Term term) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(term); - return Term(this, d_smtEngine->getValue(*term.d_node)); + return getValueHelper(term); CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5153,7 +5166,7 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const this == terms[i].d_solver, "term", terms[i], i) << "term associated to this solver object"; /* Can not use emplace_back here since constructor is private. */ - res.push_back(Term(this, d_smtEngine->getValue(terms[i].d_node->toExpr()))); + res.push_back(getValueHelper(terms[i])); } return res; CVC4_API_SOLVER_TRY_CATCH_END; |