diff options
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'; |