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