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/smt/command.cpp | |
| 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/smt/command.cpp')
| -rw-r--r-- | src/smt/command.cpp | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index d6fb470a3..58ac57cc9 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1584,14 +1584,6 @@ void GetValueCommand::invoke(api::Solver* solver) { api::Term request = d_terms[i]; api::Term value = result[i]; - if (value.getSort().isInteger() - && request.getSort() == solver->getRealSort()) - { - // Need to wrap in division-by-one so that output printers know this - // is an integer-looking constant that really should be output as - // a rational. Necessary for SMT-LIB standards compliance. - value = solver->mkTerm(api::DIVISION, value, solver->mkReal(1)); - } result[i] = solver->mkTerm(api::SEXPR, request, value); } d_result = solver->mkTerm(api::SEXPR, result); |