diff options
| author | Martin Brain <martin.brain@cs.ox.ac.uk> | 2014-12-03 21:29:43 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-12-03 21:58:28 -0500 |
| commit | cf6bc6c57dd579b8f75b7d20922eda0eaa92b2f7 (patch) | |
| tree | 582afecddf7d64953d8562ab57dd915db6cc852f /src/parser/smt2/smt2.cpp | |
| parent | 2121eaac7e63875f1e6ba53076535d25fd561c04 (diff) | |
Floating point infrastructure.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 62814ca25..7740d0b94 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -95,6 +95,41 @@ void Smt2::addStringOperators() { Parser::addOperator(kind::STRING_LENGTH); } +void Smt2::addFloatingPointOperators() { + Parser::addOperator(kind::FLOATINGPOINT_FP); + Parser::addOperator(kind::FLOATINGPOINT_EQ); + Parser::addOperator(kind::FLOATINGPOINT_ABS); + Parser::addOperator(kind::FLOATINGPOINT_NEG); + Parser::addOperator(kind::FLOATINGPOINT_PLUS); + Parser::addOperator(kind::FLOATINGPOINT_SUB); + Parser::addOperator(kind::FLOATINGPOINT_MULT); + Parser::addOperator(kind::FLOATINGPOINT_DIV); + Parser::addOperator(kind::FLOATINGPOINT_FMA); + Parser::addOperator(kind::FLOATINGPOINT_SQRT); + Parser::addOperator(kind::FLOATINGPOINT_REM); + Parser::addOperator(kind::FLOATINGPOINT_RTI); + Parser::addOperator(kind::FLOATINGPOINT_MIN); + Parser::addOperator(kind::FLOATINGPOINT_MAX); + Parser::addOperator(kind::FLOATINGPOINT_LEQ); + Parser::addOperator(kind::FLOATINGPOINT_LT); + Parser::addOperator(kind::FLOATINGPOINT_GEQ); + Parser::addOperator(kind::FLOATINGPOINT_GT); + Parser::addOperator(kind::FLOATINGPOINT_ISN); + Parser::addOperator(kind::FLOATINGPOINT_ISSN); + Parser::addOperator(kind::FLOATINGPOINT_ISZ); + Parser::addOperator(kind::FLOATINGPOINT_ISINF); + Parser::addOperator(kind::FLOATINGPOINT_ISNAN); + Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR); + Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT); + Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL); + Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR); + Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR); + Parser::addOperator(kind::FLOATINGPOINT_TO_UBV); + Parser::addOperator(kind::FLOATINGPOINT_TO_SBV); + Parser::addOperator(kind::FLOATINGPOINT_TO_REAL); +} + + void Smt2::addTheory(Theory theory) { switch(theory) { case THEORY_ARRAYS: @@ -172,6 +207,15 @@ void Smt2::addTheory(Theory theory) { Parser::addOperator(kind::APPLY_UF); break; + case THEORY_FP: + defineType("RoundingMode", getExprManager()->roundingModeType()); + defineType("Float16", getExprManager()->mkFloatingPointType(5, 11)); + defineType("Float32", getExprManager()->mkFloatingPointType(8, 24)); + defineType("Float64", getExprManager()->mkFloatingPointType(11, 53)); + defineType("Float128", getExprManager()->mkFloatingPointType(15, 113)); + addFloatingPointOperators(); + break; + default: std::stringstream ss; ss << "internal error: unsupported theory " << theory; @@ -222,6 +266,8 @@ bool Smt2::isTheoryEnabled(Theory theory) const { return d_logic.isTheoryEnabled(theory::THEORY_STRINGS); case THEORY_UF: return d_logic.isTheoryEnabled(theory::THEORY_UF); + case THEORY_FP: + return d_logic.isTheoryEnabled(theory::THEORY_FP); default: std::stringstream ss; ss << "internal error: unsupported theory " << theory; @@ -301,6 +347,11 @@ void Smt2::setLogic(const std::string& name) { if(d_logic.isQuantified()) { addTheory(THEORY_QUANTIFIERS); } + + if (d_logic.isTheoryEnabled(theory::THEORY_FP)) { + addTheory(THEORY_FP); + } + }/* Smt2::setLogic() */ void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) { |