1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
cmd_util.h
Abstract:
Macros for defining new SMT2 front-end cmds.
Author:
Leonardo (leonardo) 2011-04-01
Notes:
--*/
#pragma once
#define ATOMIC_CMD(CLS_NAME, NAME, DESCR, ACTION) \
class CLS_NAME : public cmd { \
public: \
CLS_NAME():cmd(NAME) {} \
char const * get_usage() const override { return 0; } \
char const * get_descr(cmd_context & ctx) const override { \
return DESCR; \
} \
unsigned get_arity() const override { return 0; } \
void execute(cmd_context & ctx) override { ACTION } \
}
#define UNARY_CMD(CLS_NAME, NAME, USAGE, DESCR, ARG_KIND, ARG_TYPE, ACTION) \
class CLS_NAME : public cmd { \
public: \
CLS_NAME():cmd(NAME) {} \
char const * get_usage() const override { return USAGE; } \
char const * get_descr(cmd_context & ctx) const override { \
return DESCR; \
} \
unsigned get_arity() const override { return 1; } \
cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { \
return ARG_KIND; \
} \
void set_next_arg(cmd_context & ctx, ARG_TYPE arg) override { ACTION } \
}
// Macro for creating commands where the first argument is a symbol
// The second argument cannot be a symbol
#define BINARY_SYM_CMD(CLS_NAME, NAME, USAGE, DESCR, ARG_KIND, ARG_TYPE, ACTION) \
class CLS_NAME : public cmd { \
symbol m_sym; \
public: \
CLS_NAME():cmd(NAME) {} \
char const * get_usage() const override { return USAGE; } \
char const * get_descr(cmd_context & ctx) const override { return DESCR; } \
unsigned get_arity() const override { return 2; } \
void prepare(cmd_context & ctx) override { m_sym = symbol::null; } \
cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { \
return m_sym == symbol::null ? CPK_SYMBOL : ARG_KIND; \
} \
void set_next_arg(cmd_context & ctx, symbol const & s) override { m_sym = s; } \
void set_next_arg(cmd_context & ctx, ARG_TYPE arg) override { ACTION } \
}
class ast;
class expr;
class symbol;
class cmd_context;
/**
\brief Return the AST that is referenced by the global variable v in the given command context.
*/
ast * get_ast_ref(cmd_context & ctx, symbol const & v);
/**
\brief Return the expression that is referenced by the global variable v in the given command context.
*/
expr * get_expr_ref(cmd_context & ctx, symbol const & v);
/**
\brief Store t in the global variable v.
*/
void store_expr_ref(cmd_context & ctx, symbol const & v, expr * t);