diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-20 12:53:12 -0600 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-20 10:53:12 -0800 |
| commit | 05a2414a2742ee0c7e5af40ac9c725cb49d1f196 (patch) | |
| tree | 8392f1b56aedc1a9ea107790cf7741af64b6607f /src/parser | |
| parent | 4ef569cfd91bccabb6e704dcc4ecd55a9fa0a8ea (diff) | |
Minor fixes and additions for transcendental functions (#1612)
Also adds parsing support for PI in smt2 with syntax "real.pi".
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d424fefad..b9a2a8805 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2348,6 +2348,10 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] | FP_RTN_FULL_TOK { expr = MK_CONST(roundTowardNegative); } | FP_RTZ_FULL_TOK { expr = MK_CONST(roundTowardZero); } + | REAL_PI_TOK { + expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->realType(), kind::PI); + } + | RENOSTR_TOK { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_EMPTY, nvec ); @@ -3191,6 +3195,8 @@ TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }? 'tupSe // tokenized and handled directly when // processing a term +REAL_PI_TOK : 'real.pi'; + FP_PINF_TOK : '+oo'; FP_NINF_TOK : '-oo'; FP_PZERO_TOK : '+zero'; |