diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-10-29 13:26:51 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-29 13:26:51 -0500 |
| commit | d23ba1433846b9baaf6149137aa999c1af60c516 (patch) | |
| tree | b75389566b726edcaf32cb0f8ab2059bba9e1528 /src/printer | |
| parent | 6898ab93a3858e78b20af38e537fe48ee9140c58 (diff) | |
Add mkInteger to the API (#5274)
This PR adds mkInteger to the API and update mkReal to ensure that the returned term has real sort.
The parsers are modified to parse numbers like "0" "5" as integers and "0.0" and "15.0" as reals.
This means subtyping is effectively eliminated from all theories except arithmetic.
Other changes:
Term::isValue is removed which was introduced to support parsing for constant arrays. It is no longer needed after this PR.
Benchmarks are updated to match the changes in the parsers
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 3 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 19 |
2 files changed, 16 insertions, 6 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index bab619dce..9ccf02301 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -644,6 +644,8 @@ void CvcPrinter::toStream( opType = PREFIX; break; case kind::TO_REAL: + case kind::CAST_TO_REAL: + { if (n[0].getKind() == kind::CONST_RATIONAL) { // print the constant as a rational @@ -655,6 +657,7 @@ void CvcPrinter::toStream( toStream(out, n[0], depth, types, false); } return; + } case kind::DIVISIBLE: out << "DIVISIBLE("; toStream(out, n[0], depth, types, false); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8815f9632..a0cd8cf9c 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -477,10 +477,10 @@ void Smt2Printer::toStream(std::ostream& out, bool typeChildren = false; // operators (op t1...tn) where at least one of t1...tn may require a type cast e.g. Int -> Real // operator Kind k = n.getKind(); - if(n.getNumChildren() != 0 && - k != kind::INST_PATTERN_LIST && - k != kind::APPLY_TYPE_ASCRIPTION && - k != kind::CONSTRUCTOR_TYPE) { + if (n.getNumChildren() != 0 && k != kind::INST_PATTERN_LIST + && k != kind::APPLY_TYPE_ASCRIPTION && k != kind::CONSTRUCTOR_TYPE + && k != kind::CAST_TO_REAL) + { out << '('; } switch(k) { @@ -603,11 +603,17 @@ void Smt2Printer::toStream(std::ostream& out, case kind::ABS: case kind::IS_INTEGER: case kind::TO_INTEGER: - case kind::TO_REAL: case kind::POW: parametricTypeChildren = true; out << smtKindString(k, d_variant) << " "; break; + case kind::TO_REAL: + case kind::CAST_TO_REAL: + { + // (to_real 5) is printed as 5.0 + out << n[0] << ".0"; + return; + } case kind::IAND: out << "(_ iand " << n.getOperator().getConst<IntAnd>().d_size << ") "; stillNeedToPrintParams = false; @@ -1029,7 +1035,8 @@ void Smt2Printer::toStream(std::ostream& out, } } } - if(n.getNumChildren() != 0) { + if (n.getNumChildren() != 0) + { out << parens.str() << ')'; } }/* Smt2Printer::toStream(TNode) */ |