From f5ed28fe24f6b887630a48dcf476c462c0c227a1 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 17 Jun 2016 18:38:16 -0500 Subject: Cleanup from last commit, treat sep.nil as variable kind. --- src/parser/smt2/Smt2.g | 8 ++++---- src/parser/smt2/smt2.cpp | 6 ++---- 2 files changed, 6 insertions(+), 8 deletions(-) (limited to 'src/parser/smt2') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index b3fe59b79..29d3e45b6 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1607,10 +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.getKind() == CVC4::kind::SEP_NIL_REF) { + //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 a SEP_NIL variable. + expr = EXPR_MANAGER->mkSepNil(type); } else { if(f.getType() != type) { PARSER_STATE->parseError("Type ascription not satisfied."); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 90fc11803..a46eae475 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -167,16 +167,14 @@ void Smt2::addFloatingPointOperators() { } void Smt2::addSepOperators() { - //addOperator(kind::SEP_NIL, "sep.nil"); addOperator(kind::SEP_STAR, "sep"); addOperator(kind::SEP_PTO, "pto"); addOperator(kind::SEP_WAND, "wand"); - addOperator(kind::EMP_STAR, "emp"); - //Parser::addOperator(kind::SEP_NIL); + addOperator(kind::SEP_EMP, "emp"); Parser::addOperator(kind::SEP_STAR); Parser::addOperator(kind::SEP_PTO); Parser::addOperator(kind::SEP_WAND); - Parser::addOperator(kind::EMP_STAR); + Parser::addOperator(kind::SEP_EMP); } void Smt2::addTheory(Theory theory) { -- cgit v1.2.3