1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 cmd_context_types.h 7 8 Abstract: 9 10 Author: 11 12 Leonardo (leonardo) 2011-04-22 13 14 Notes: 15 16 --*/ 17 #pragma once 18 19 #include "util/symbol.h" 20 #include "util/z3_exception.h" 21 #include<sstream> 22 class rational; 23 class expr; 24 class sort; 25 class func_decl; 26 class sexpr; 27 class cmd_context; 28 29 enum cmd_arg_kind { 30 CPK_UINT, CPK_BOOL, CPK_DOUBLE, CPK_NUMERAL, 31 CPK_DECIMAL, CPK_STRING, CPK_OPTION_VALUE, 32 CPK_KEYWORD, 33 CPK_SYMBOL, CPK_SYMBOL_LIST, 34 CPK_SORT, CPK_SORT_LIST, 35 CPK_EXPR, CPK_EXPR_LIST, 36 CPK_FUNC_DECL, CPK_FUNC_DECL_LIST, 37 CPK_SORTED_VAR, CPK_SORTED_VAR_LIST, 38 CPK_SEXPR, 39 CPK_INVALID 40 }; 41 42 std::ostream & operator<<(std::ostream & out, cmd_arg_kind k); 43 44 typedef cmd_arg_kind param_kind; 45 46 class cmd_exception : public default_exception { 47 int m_line; 48 int m_pos; 49 compose(char const * msg,symbol const & s)50 std::string compose(char const* msg, symbol const& s) { 51 std::stringstream stm; 52 stm << msg << s; 53 return stm.str(); 54 } 55 public: cmd_exception(char const * msg)56 cmd_exception(char const * msg):default_exception(msg), m_line(-1), m_pos(-1) {} cmd_exception(std::string && msg)57 cmd_exception(std::string && msg):default_exception(std::move(msg)), m_line(-1), m_pos(-1) {} cmd_exception(std::string && msg,int line,int pos)58 cmd_exception(std::string && msg, int line, int pos):default_exception(std::move(msg)), m_line(line), m_pos(pos) {} cmd_exception(char const * msg,symbol const & s)59 cmd_exception(char const * msg, symbol const & s): 60 default_exception(compose(msg,s)),m_line(-1),m_pos(-1) {} cmd_exception(char const * msg,symbol const & s,int line,int pos)61 cmd_exception(char const * msg, symbol const & s, int line, int pos): 62 default_exception(compose(msg,s)),m_line(line),m_pos(pos) {} 63 has_pos()64 bool has_pos() const { return m_line >= 0; } line()65 int line() const { SASSERT(has_pos()); return m_line; } pos()66 int pos() const { SASSERT(has_pos()); return m_pos; } 67 }; 68 69 class stop_parser_exception { 70 }; 71 72 typedef std::pair<symbol, sort*> sorted_var; 73 74 // A command may have a variable number of arguments. 75 #define VAR_ARITY UINT_MAX 76 77 /** 78 \brief Command abstract class. 79 80 Commands may have variable number of argumets. 81 */ 82 class cmd { 83 symbol m_name; 84 protected: 85 int m_line; 86 int m_pos; 87 public: cmd(char const * n)88 cmd(char const * n):m_name(n), m_line(0), m_pos(0) {} ~cmd()89 virtual ~cmd() {} reset(cmd_context & ctx)90 virtual void reset(cmd_context & ctx) {} finalize(cmd_context & ctx)91 virtual void finalize(cmd_context & ctx) {} get_name()92 virtual symbol get_name() const { return m_name; } get_usage()93 virtual char const * get_usage() const { return nullptr; } get_descr(cmd_context & ctx)94 virtual char const * get_descr(cmd_context & ctx) const { return nullptr; } get_arity()95 virtual unsigned get_arity() const { return 0; } 96 97 // command invocation set_line_pos(int line,int pos)98 void set_line_pos(int line, int pos) { m_line = line; m_pos = pos; } prepare(cmd_context & ctx)99 virtual void prepare(cmd_context & ctx) {} next_arg_kind(cmd_context & ctx)100 virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { UNREACHABLE(); return cmd_arg_kind::CPK_UINT; } set_next_arg(cmd_context & ctx,unsigned val)101 virtual void set_next_arg(cmd_context & ctx, unsigned val) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,bool val)102 virtual void set_next_arg(cmd_context & ctx, bool val) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,rational const & val)103 virtual void set_next_arg(cmd_context & ctx, rational const & val) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,double val)104 virtual void set_next_arg(cmd_context & ctx, double val) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,char const * val)105 virtual void set_next_arg(cmd_context & ctx, char const * val) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,symbol const & s)106 virtual void set_next_arg(cmd_context & ctx, symbol const & s) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,unsigned num,symbol const * slist)107 virtual void set_next_arg(cmd_context & ctx, unsigned num, symbol const * slist) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,sort * s)108 virtual void set_next_arg(cmd_context & ctx, sort * s) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,unsigned num,sort * const * slist)109 virtual void set_next_arg(cmd_context & ctx, unsigned num, sort * const * slist) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,expr * t)110 virtual void set_next_arg(cmd_context & ctx, expr * t) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,unsigned num,expr * const * tlist)111 virtual void set_next_arg(cmd_context & ctx, unsigned num, expr * const * tlist) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,sorted_var const & sv)112 virtual void set_next_arg(cmd_context & ctx, sorted_var const & sv) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,unsigned num,sorted_var const * svlist)113 virtual void set_next_arg(cmd_context & ctx, unsigned num, sorted_var const * svlist) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,func_decl * f)114 virtual void set_next_arg(cmd_context & ctx, func_decl * f) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,unsigned num,func_decl * const * flist)115 virtual void set_next_arg(cmd_context & ctx, unsigned num, func_decl * const * flist) { UNREACHABLE(); } set_next_arg(cmd_context & ctx,sexpr * n)116 virtual void set_next_arg(cmd_context & ctx, sexpr * n) { UNREACHABLE(); } failure_cleanup(cmd_context & ctx)117 virtual void failure_cleanup(cmd_context & ctx) {} execute(cmd_context & ctx)118 virtual void execute(cmd_context & ctx) {} 119 }; 120 121 122