From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 26 Feb 2020 06:40:52 +0000 (-0600)
Subject: Minor cleaning of smt2 parser (#3823)
X-Git-Tag: cvc5-1.0.0~3603
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b28ff31b6713791f27b4860f439aaa3f63aab9d7;p=cvc5.git

Minor cleaning of smt2 parser (#3823)

Towards parser migration, will make the diff of the eventual conversion a bit smaller.
---

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 2dceba768..dca61fe48 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1306,14 +1306,8 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
     { /*symtab = PARSER_STATE->getSymbolTable();
       PARSER_STATE->useDeclarationsFrom(new SymbolTable());*/ }
     formula[f] ( COMMA formula[f2] )? RPAREN
-    { /*SymbolTable* old = PARSER_STATE->getSymbolTable();
-      PARSER_STATE->useDeclarationsFrom(symtab);
-      delete old;*/
+    {
       PARSER_STATE->unimplementedFeature("predicate subtyping not supported in this release");
-      /*t = f2.isNull() ?
-        EXPR_MANAGER->mkPredicateSubtype(f) :
-        EXPR_MANAGER->mkPredicateSubtype(f, f2);
-      */
     }
 
     /* subrange types */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index e1f8031da..66831c0c4 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1536,16 +1536,6 @@ datatypesDef[bool isCo,
   }
   ;
 
-pattern[CVC4::Expr& expr]
-@declarations {
-  std::vector<Expr> patexpr;
-}
-  : LPAREN_TOK termList[patexpr,expr] RPAREN_TOK
-    {
-      expr = MK_EXPR(kind::INST_PATTERN, patexpr);
-    }
-  ;
-
 simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
 @declarations {
   CVC4::Kind k;
@@ -1568,13 +1558,6 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
     }
   | str[s,false]
     { sexpr = SExpr(s); }
-//  | LPAREN_TOK STRCST_TOK
-//      ( INTEGER_LITERAL {
-//      s_vec.push_back( atoi( AntlrInput::tokenText($INTEGER_LITERAL) ) + 65 );
-//    } )* RPAREN_TOK
-//   {
-//  sexpr = SExpr( MK_CONST( ::CVC4::String(s_vec) ) );
-//  }
   | symbol[s,CHECK_NONE,SYM_SORT]
     { sexpr = SExpr(SExpr::Keyword(s)); }
   | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK
@@ -2512,15 +2495,6 @@ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes,
      * "defined" as an unresolved type; don't worry, we check
      * below. */
   : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); }
-   /* ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
-        t = PARSER_STATE->mkSort(id2);
-        params.push_back( t );
-      }
-      ( symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
-        t = PARSER_STATE->mkSort(id2);
-        params.push_back( t ); }
-      )* ']'
-    )?*/ //AJR: this isn't necessary if we use z3's style
     { datatypes.push_back(Datatype(EXPR_MANAGER, id, params, isCo));
       if(!PARSER_STATE->isUnresolvedType(id)) {
         // if not unresolved, must be undeclared
@@ -2649,7 +2623,6 @@ ATTRIBUTE_PATTERN_TOK : ':pattern';
 ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern';
 ATTRIBUTE_NAMED_TOK : ':named';
 ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level';
-ATTRIBUTE_RR_PRIORITY : ':rr-priority';
 
 // operators (NOTE: theory symbols go here)
 EXISTS_TOK        : 'exists';
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 88d8b527b..8c2b50b04 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -934,6 +934,19 @@ void Smt2::includeFile(const std::string& filename) {
   }
 }
 
+bool Smt2::isAbstractValue(const std::string& name)
+{
+  return name.length() >= 2 && name[0] == '@' && name[1] != '0'
+         && name.find_first_not_of("0123456789", 1) == std::string::npos;
+}
+
+Expr Smt2::mkAbstractValue(const std::string& name)
+{
+  assert(isAbstractValue(name));
+  // remove the '@'
+  return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1))));
+}
+
 void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
   if( type.isInteger() ){
     ops.push_back(getExprManager()->mkConst(Rational(0)));
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 6427b32d5..954bca314 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -333,19 +333,15 @@ class Smt2 : public Parser
     return d_lastNamedTerm;
   }
 
-  bool isAbstractValue(const std::string& name) {
-    return name.length() >= 2 && name[0] == '@' && name[1] != '0' &&
-      name.find_first_not_of("0123456789", 1) == std::string::npos;
-  }
-
-  Expr mkAbstractValue(const std::string& name) {
-    assert(isAbstractValue(name));
-    return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1))));
-  }
+  /** Does name denote an abstract value? (of the form '@n' for numeral n). */
+  bool isAbstractValue(const std::string& name);
 
-  void mkSygusVar(const std::string& name,
-                  const Type& type,
-                  bool isPrimed = false);
+  /** Make abstract value
+   *
+   * Abstract values are used for processing get-value calls. The argument
+   * name should be such that isAbstractValue(name) is true.
+   */
+  Expr mkAbstractValue(const std::string& name);
 
   void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops );