diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-09 14:38:54 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-09 14:38:54 -0600 |
| commit | bf98dd46aa92241d33901e84a437536ad5010be1 (patch) | |
| tree | f71903ac761f31d91090407877d5be9af1445771 /src/api/cvc4cpp.h | |
| parent | 4b894cc0201783a40cd92e9bffe7257d44f8f4e4 (diff) | |
Simplify handling of subtypes in smt2 printer (#5401)
This makes major simplifications to how subtypes are enforced in the smt2 printer.
It is now the principle that the smt2 prints things faithfully to the AST, regardless of whether it conforms to the smt2 standard.
It also fixes the current smt2 printing of to_real.
Conversely, this removes a hack from GetValueCommand which forced casting via x -> (/ x 1). This is now properly handled in Solver::getValue.
Some regressions change expected output as a result. Notice that internally generated Node may not conform to the smt2 standard, but user-level terms will.
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index ae6384e91..13d4f6e23 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -3462,6 +3462,8 @@ class CVC4_PUBLIC Solver Term mkTermFromKind(Kind kind) const; /* Helper for mkChar functions that take a string as argument. */ Term mkCharFromStrHelper(const std::string& s) const; + /** Get value helper, which accounts for subtyping */ + Term getValueHelper(Term term) const; /** * Helper function that ensures that a given term is of sort real (as opposed |