Added support for parsing negative numerals in the SMT 2.0 frontend

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

RELEASE_NOTES

@@ -30,6 +30,10 @@ Version 4.2
 - Z3 by default switches to an incremental solver when a Solver object is used to solve many queries.
   In the this version, we switch back to the tactic framework if the incremental solver returns "unknown".
 
+- Allow negative numerals in the SMT 2.0 frontend. That is, Z3 SMT 2.0 parser now accepts numerals such as "-2". It is not needed to encode them as "(- 2)" anymore.
+  The parser still accepts -foo as a symbol. That is, it is *not* a shorthand for (- foo).
+  This feature is disabled when SMTLIB2_COMPLIANT=true is set in the command line.
+
 - Now, Z3 can be compiled inside cygwin using gcc.
 
 - Fixed bug in the unsat core generation.

lib/cmd_context.h

@@ -246,6 +246,7 @@ protected:
 public:
     cmd_context(front_end_params & params, bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
     ~cmd_context(); 
+    bool is_smtlib2_compliant() const { return m_params.m_smtlib2_compliant; }
     void set_logic(symbol const & s);
     bool has_logic() const { return m_logic != symbol::null; }
     symbol const & get_logic() const { return m_logic; }

lib/smt2parser.cpp

@@ -2353,7 +2353,7 @@ namespace smt2 {
     public:
         parser(cmd_context & ctx, std::istream & is, bool interactive):
             m_ctx(ctx), 
-            m_scanner(is, interactive), 
+            m_scanner(ctx, is, interactive), 
             m_curr(scanner::NULL_TOKEN),
             m_curr_cmd(0),
             m_num_bindings(0),

lib/smt2scanner.cpp

@@ -87,17 +87,12 @@ namespace smt2 {
             next();
         }
     }
-    
+
-    scanner::token scanner::read_symbol() {
+    scanner::token scanner::read_symbol_core() {
-        SASSERT(m_normalized[static_cast<unsigned>(curr())] == 'a' || curr() == ':');
-        m_string.reset();
-        m_string.push_back(curr());
-        next();
-        
         while (true) {
             char c = curr();
             char n = m_normalized[static_cast<unsigned char>(c)];
-            if (n == 'a' || n == '0') {
+            if (n == 'a' || n == '0' || n == '-') {
                 m_string.push_back(c);
                 next();
             }
@@ -110,6 +105,14 @@ namespace smt2 {
         }
     }
     
+    scanner::token scanner::read_symbol() {
+        SASSERT(m_normalized[static_cast<unsigned>(curr())] == 'a' || curr() == ':' || curr() == '-');
+        m_string.reset();
+        m_string.push_back(curr());
+        next();
+        read_symbol_core();
+    }
+    
     scanner::token scanner::read_number() {
         SASSERT('0' <= curr() && curr() <= '9');
         rational q(1);
@@ -140,6 +143,22 @@ namespace smt2 {
         TRACE("scanner", tout << "new number: " << m_number << "\n";);
         return is_float ? FLOAT_TOKEN : INT_TOKEN;
     }
+
+    scanner::token scanner::read_signed_number() {
+        SASSERT(curr() == '-');
+        next();
+        if ('0' <= curr() && curr() <= '9') {
+            scanner::token r = read_number();
+            m_number.neg();
+            return r;
+        }
+        else {
+            // it is a symbol.
+            m_string.reset();
+            m_string.push_back('-');
+            return read_symbol_core();
+        }
+    }
     
     scanner::token scanner::read_string() {
         SASSERT(curr() == '\"');
@@ -222,7 +241,8 @@ namespace smt2 {
         }
     }
     
-    scanner::scanner(std::istream& stream, bool interactive):
+    scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive):
+        m_ctx(ctx),
         m_interactive(interactive), 
         m_spos(0),
         m_curr(0), // avoid Valgrind warning
@@ -259,7 +279,7 @@ namespace smt2 {
         m_normalized[static_cast<int>('&')] = 'a';
         m_normalized[static_cast<int>('*')] = 'a';
         m_normalized[static_cast<int>('_')] = 'a';
-        m_normalized[static_cast<int>('-')] = 'a';
+        m_normalized[static_cast<int>('-')] = '-';
         m_normalized[static_cast<int>('+')] = 'a';
         m_normalized[static_cast<int>('=')] = 'a';
         m_normalized[static_cast<int>('<')] = 'a';
@@ -304,6 +324,11 @@ namespace smt2 {
                 return read_number();
             case '#':
                 return read_bv_literal();
+            case '-':
+                if (m_ctx.is_smtlib2_compliant())
+                    return read_symbol();
+                else
+                    return read_signed_number();
             case -1:
                 return EOF_TOKEN;
             default: {

lib/smt2scanner.h

@@ -31,6 +31,7 @@ namespace smt2 {
     
     class scanner {
     private:
+        cmd_context &      m_ctx;
         bool               m_interactive;
         int                m_spos; // position in the current line of the stream
         char               m_curr;  // current char;
@@ -73,7 +74,7 @@ namespace smt2 {
             EOF_TOKEN
         };
         
-        scanner(std::istream& stream, bool interactive = false);
+        scanner(cmd_context & ctx, std::istream& stream, bool interactive = false);
         
         ~scanner() {}    
         
@@ -85,10 +86,12 @@ namespace smt2 {
         char const * get_string() const { return m_string.begin(); }
         token scan();
         
+        token read_symbol_core();
         token read_symbol();
         token read_quoted_symbol();
         void read_comment();
         token read_number();
+        token read_signed_number();
         token read_string();
         token read_bv_literal();