diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 41428ed89..b3fe59b79 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1607,6 +1607,10 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] Debug("parser") << "Empty set encountered: " << f << " " << f2 << " " << type << std::endl; expr = MK_CONST( ::CVC4::EmptySet(type) ); + } else if(f.getKind() == CVC4::kind::NIL_REF) { + //hack: We don't want the nil reference to be a constant: for instance, it could be of type Int but is not a const rational. + // However, the expression has 0 children. So we convert to (sep_nil tmp) here. + expr = MK_EXPR(CVC4::kind::SEP_NIL, PARSER_STATE->mkBoundVar("__tmp",type) ); } else { if(f.getType() != type) { PARSER_STATE->parseError("Type ascription not satisfied."); @@ -1911,6 +1915,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | EMPTYSET_TOK { expr = MK_CONST( ::CVC4::EmptySet(Type())); } + | NILREF_TOK + { expr = MK_CONST( ::CVC4::NilRef(Type())); } // NOTE: Theory constants go here ; @@ -2646,6 +2652,7 @@ FMFCARDVAL_TOK : 'fmf.card.val'; INST_CLOSURE_TOK : 'inst-closure'; EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset'; +NILREF_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'sep.nil'; // Other set theory operators are not // tokenized and handled directly when // processing a term |