add line/position information to unsupported command reports per zeph pull request

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/cmd_context/basic_cmds.cpp

@@ -205,7 +205,7 @@ UNARY_CMD(set_logic_cmd, "set-logic", "<symbol>", "set the background logic.", C
           if (ctx.set_logic(arg))
               ctx.print_success();
           else
-              ctx.print_unsupported(symbol::null);
+              ctx.print_unsupported(symbol::null, m_line, m_pos);
           );
 
 UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr *, { 
@@ -436,7 +436,7 @@ public:
 
     virtual void execute(cmd_context & ctx) {
         if (m_unsupported)
-            ctx.print_unsupported(m_option);
+            ctx.print_unsupported(m_option, m_line, m_pos);
         else
             ctx.print_success();
     }
@@ -472,7 +472,7 @@ public:
         // print_bool(ctx, );
         // }
         else if (opt == m_expand_definitions) {
-            ctx.print_unsupported(m_expand_definitions);
+            ctx.print_unsupported(m_expand_definitions, m_line, m_pos);
         }
         else if (opt == m_interactive_mode) {
             print_bool(ctx, ctx.interactive_mode());
@@ -523,7 +523,7 @@ public:
                 ctx.regular_stream() << gparams::get_value(opt) << std::endl;
             }
             catch (gparams::exception ex) {
-                ctx.print_unsupported(opt);
+                ctx.print_unsupported(opt, m_line, m_pos);
             }
         }
     }
@@ -585,7 +585,7 @@ public:
             ctx.display_statistics();
         }
         else {
-            ctx.print_unsupported(opt);
+            ctx.print_unsupported(opt, m_line, m_pos);
         }
     }
 };

src/cmd_context/cmd_context.h

@@ -262,7 +262,7 @@ protected:
     bool supported_logic(symbol const & s) const;
 
     void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; }
-    void print_unsupported_info(symbol const& s) { if (s != symbol::null) diagnostic_stream() << "; " << s << std::endl;}
+    void print_unsupported_info(symbol const& s, int line, int pos) { if (s != symbol::null) diagnostic_stream() << "; " << s << " line: " << line << " position: " << pos << std::endl;}
 
     void mk_solver();
 
@@ -292,7 +292,7 @@ public:
     void set_print_success(bool flag) { m_print_success = flag; }
     bool print_success_enabled() const { return m_print_success; }
     void print_success() { if (print_success_enabled())  regular_stream() << "success" << std::endl; }
-    void print_unsupported(symbol const & s) { print_unsupported_msg(); print_unsupported_info(s); }
+    void print_unsupported(symbol const & s, int line, int pos) { print_unsupported_msg(); print_unsupported_info(s, line, pos); }
     bool global_decls() const { return m_global_decls; }
     void set_global_decls(bool flag) { SASSERT(!has_manager()); m_global_decls = flag; }
     unsigned random_seed() const { return m_random_seed; }

src/parsers/smt2/smt2parser.cpp

@@ -2264,12 +2264,12 @@ namespace smt2 {
             while (!curr_is_rparen()) {
                 consume_sexpr();
             }
-            m_ctx.print_unsupported(s);
+            m_ctx.print_unsupported(s, m_scanner.get_line(), m_scanner.get_pos());
             next();
             return;
         }
 
-        void parse_ext_cmd() {
+        void parse_ext_cmd(int line, int pos) {
             symbol s = curr_id();
             m_curr_cmd = m_ctx.find_cmd(s);
             if (m_curr_cmd == 0) {
@@ -2283,6 +2283,7 @@ namespace smt2 {
             unsigned expr_spos  = size(m_expr_stack);
             unsigned sexpr_spos = size(m_sexpr_stack);
             unsigned sym_spos   = m_symbol_stack.size();
+            m_curr_cmd->set_line_pos(line, pos);
             m_curr_cmd->prepare(m_ctx);
             while (true) {
                 if (curr_is_rparen()) {
@@ -2313,6 +2314,8 @@ namespace smt2 {
         
         void parse_cmd() {
             SASSERT(curr_is_lparen());
+            int line = m_scanner.get_line();
+            int pos  = m_scanner.get_pos();
             next();
             check_identifier("invalid command, symbol expected");
             symbol s = curr_id();
@@ -2368,7 +2371,7 @@ namespace smt2 {
                 parse_reset();
                 return;
             }
-            parse_ext_cmd();
+            parse_ext_cmd(line, pos);
         }
 
     public:

src/smt/asserted_formulas.cpp

@@ -624,7 +624,8 @@ void asserted_formulas::propagate_values() {
                         if (m_manager.proofs_enabled())
                             new_prs1.push_back(pr);
                     }
-                    TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\nproof: " << mk_pp(pr, m_manager) << "\n";);
+                    TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n";
+                          if (pr) tout << "proof: " << mk_pp(pr, m_manager) << "\n";);
                     m_simplifier.cache_result(lhs, rhs, pr);
                     found = true;
                     continue;

src/util/cmd_context_types.h

@@ -82,8 +82,11 @@ typedef std::pair<symbol, sort*> sorted_var;
 */
 class cmd {
     symbol m_name;
+protected:
+    int    m_line;
+    int    m_pos;
 public:
-    cmd(char const * n):m_name(n) {}
+    cmd(char const * n):m_name(n), m_line(0), m_pos(0) {}
     virtual ~cmd() {}
     virtual void reset(cmd_context & ctx) {}
     virtual void finalize(cmd_context & ctx) {}
@@ -93,6 +96,7 @@ public:
     virtual unsigned get_arity() const { return 0; }
 
     // command invocation
+    void set_line_pos(int line, int pos) { m_line = line; m_pos = pos; }
     virtual void prepare(cmd_context & ctx) {}
     virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { UNREACHABLE(); return CPK_UINT; }
     virtual void set_next_arg(cmd_context & ctx, unsigned val) { UNREACHABLE(); }