From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 11 Dec 2012 22:55:29 +0000 (-0500)
Subject: Ignore unknown term annotations (giving a warning).  Resolves bug 479.
X-Git-Tag: cvc5-1.0.0~7469^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5eaeeb2156a9d035250ed8ec5af6391995bb10f5;p=cvc5.git

Ignore unknown term annotations (giving a warning).  Resolves bug 479.
---

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 721dedc70..65d46220b 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -16,6 +16,7 @@
 
 #include <iostream>
 #include <fstream>
+#include <sstream>
 #include <iterator>
 #include <stdint.h>
 #include <cassert>
@@ -500,6 +501,14 @@ Expr Parser::nextExpression() throw(ParserException) {
   return result;
 }
 
+void Parser::attributeNotSupported(const std::string& attr) {
+  if(d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) {
+    stringstream ss;
+    ss << "warning: Attribute " << attr << " not supported (ignoring this and all following uses)";
+    d_input->warning(ss.str());
+    d_attributesWarnedAbout.insert(attr);
+  }
+}
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/parser.h b/src/parser/parser.h
index fc956b463..958c8a5b5 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -144,6 +144,9 @@ class CVC4_PUBLIC Parser {
   /** The set of operators available in the current logic. */
   std::set<Kind> d_logicOperators;
 
+  /** The set of attributes already warned about. */
+  std::set<std::string> d_attributesWarnedAbout;
+
   /**
    * The current set of unresolved types.  We can get by with this NOT
    * being on the scope, because we can only have one DATATYPE
@@ -451,6 +454,9 @@ public:
     d_input->warning(msg);
   }
 
+  /** Issue a warning to the user, but only once per attribute. */
+  void attributeNotSupported(const std::string& attr);
+
   /** Raise a parse error with the given message. */
   inline void parseError(const std::string& msg) throw(ParserException) {
     d_input->parseError(msg);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 87cf2083d..648666091 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -629,7 +629,7 @@ pattern[CVC4::Expr& expr]
     }
   ;
 
-simpleSymbolicExpr[CVC4::SExpr& sexpr]
+simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
 @declarations {
   CVC4::Kind k;
   std::string s;
@@ -647,6 +647,10 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr]
       ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k);
       sexpr = SExpr(ss.str());
     }
+  ;
+
+simpleSymbolicExpr[CVC4::SExpr& sexpr]
+  : simpleSymbolicExprNoKeyword[sexpr]
   | KEYWORD
     { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
   ;
@@ -715,8 +719,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = MK_EXPR(kind, args);
       }
     }
-  | LPAREN_TOK AS_TOK term[f, f2] sortSymbol[type, CHECK_DECLARED] RPAREN_TOK 
-    {     
+  | LPAREN_TOK AS_TOK term[f, f2] sortSymbol[type, CHECK_DECLARED] RPAREN_TOK
+    {
       if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) {
         std::vector<CVC4::Expr> v;
         Expr e = f.getOperator();
@@ -928,22 +932,31 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
   Expr patexpr;
   std::vector<Expr> patexprs;
   Expr e2;
+  bool hasValue = false;
 }
-: KEYWORD
+  : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )?
   {
     attr = AntlrInput::tokenText($KEYWORD);
-    //EXPR_MANAGER->setNamedAttribute( expr, attr );
-    if( attr==":rewrite-rule" ){
-      //do nothing
-    } else if( attr==":axiom" || attr==":conjecture" ){
+    // EXPR_MANAGER->setNamedAttribute( expr, attr );
+    if(attr == ":rewrite-rule") {
+      if(hasValue) {
+        std::stringstream ss;
+        ss << "warning: Attribute " << attr << " does not take a value (ignoring)";
+        PARSER_STATE->warning(ss.str());
+      }
+      // do nothing
+    } else if(attr == ":axiom" || attr == ":conjecture") {
+      if(hasValue) {
+        std::stringstream ss;
+        ss << "warning: Attribute " << attr << " does not take a value (ignoring)";
+        PARSER_STATE->warning(ss.str());
+      }
       std::string attr_name = attr;
       attr_name.erase( attr_name.begin() );
       Command* c = new SetUserAttributeCommand( attr_name, expr );
       PARSER_STATE->preemptCommand(c);
     } else {
-      std::stringstream ss;
-      ss << "Attribute `" << attr << "' not supported";
-      PARSER_STATE->parseError(ss.str());
+      PARSER_STATE->attributeNotSupported(attr);
     }
   }
   | ATTRIBUTE_PATTERN_TOK LPAREN_TOK ( term[patexpr, e2] { patexprs.push_back( patexpr ); }  )+ RPAREN_TOK
@@ -951,6 +964,11 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       attr = std::string(":pattern");
       retExpr = MK_EXPR(kind::INST_PATTERN, patexprs);
     }
+  | ATTRIBUTE_NO_PATTERN_TOK LPAREN_TOK term[patexpr, e2]+ RPAREN_TOK
+    {
+      attr = std::string(":no-pattern");
+      PARSER_STATE->attributeNotSupported(attr);
+    }
   | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
     {
       attr = std::string(":named");
@@ -1098,7 +1116,7 @@ quantOp[CVC4::Kind& kind]
 @init {
   Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
-  : EXISTS_TOK      { $kind = CVC4::kind::EXISTS; }
+  : EXISTS_TOK    { $kind = CVC4::kind::EXISTS; }
   | FORALL_TOK    { $kind = CVC4::kind::FORALL; }
   ;
 
@@ -1374,6 +1392,7 @@ SIMPLIFY_TOK : 'simplify';
 
 // attributes
 ATTRIBUTE_PATTERN_TOK : ':pattern';
+ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern';
 ATTRIBUTE_NAMED_TOK : ':named';
 
 // operators (NOTE: theory symbols go here)