Source

z3 / src / cmd_context / cmd_context.h

Full commit
  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
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    cmd_context.h

Abstract:
    Ultra-light command context.
    It provides a generic command pluging infrastructure.
    A command context also provides names (aka symbols) to Z3 objects. 
    These names are used to reference Z3 objects in commands.

Author:

    Leonardo (leonardo) 2011-03-01

Notes:

--*/
#ifndef _CMD_CONTEXT_H_
#define _CMD_CONTEXT_H_

#include<sstream>
#include"ast.h"
#include"ast_printer.h"
#include"pdecl.h"
#include"dictionary.h"
#include"solver.h"
#include"datatype_decl_plugin.h"
#include"stopwatch.h"
#include"cmd_context_types.h"
#include"event_handler.h"
#include"sexpr.h"
#include"tactic_manager.h"
#include"check_logic.h"
#include"progress_callback.h"
#include"scoped_ptr_vector.h"

struct front_end_params;

class func_decls {
    func_decl * m_decls;
public:
    func_decls():m_decls(0) {}
    func_decls(ast_manager & m, func_decl * f);
    void finalize(ast_manager & m);
    bool contains(func_decl * f) const;
    bool insert(ast_manager & m, func_decl * f);
    void erase(ast_manager & m, func_decl * f);
    bool more_than_one() const;
    bool clash(func_decl * f) const;
    bool empty() const { return m_decls == 0; }
    func_decl * first() const;
    func_decl * find(unsigned arity, sort * const * domain, sort * range) const;
    func_decl * find(ast_manager & m, unsigned num_args, expr * const * args, sort * range) const;
};

/**
   \brief Generic wrapper.
*/
class object_ref {
    unsigned m_ref_count;
public:
    object_ref():m_ref_count(0) {}
    virtual ~object_ref() {}
    virtual void finalize(cmd_context & ctx) = 0;
    void inc_ref(cmd_context & ctx) {
        m_ref_count++;
    }
    void dec_ref(cmd_context & ctx) {
        SASSERT(m_ref_count > 0);
        m_ref_count--;
        if (m_ref_count == 0) {
            finalize(ctx);
            dealloc(this);
        }
    }
    virtual char const * kind() const = 0;
};

class ast_object_ref : public object_ref {
    ast * m_ast;
public:
    ast_object_ref(cmd_context & ctx, ast * a);
    virtual void finalize(cmd_context & ctx);
    ast * get_ast() const { return m_ast; }
    static char const * cls_kind() { return "AST"; }
    virtual char const * kind() const { return cls_kind(); }
};

class stream_ref {
    std::string    m_default_name;
    std::ostream & m_default;
    std::string    m_name;
    std::ostream * m_stream;
    bool           m_owner;
public:
    stream_ref(std::string n, std::ostream & d):m_default_name(n), m_default(d), m_name(n), m_stream(&d), m_owner(false) {}
    ~stream_ref() { reset(); }
    void set(char const * name);
    void reset();
    std::ostream & operator*() { return *m_stream; }
    char const * name() const { return m_name.c_str(); }
};

struct builtin_decl {
    family_id      m_fid;
    decl_kind      m_decl;
    builtin_decl * m_next;
    builtin_decl():m_fid(null_family_id), m_decl(0), m_next(0) {}
    builtin_decl(family_id fid, decl_kind k, builtin_decl * n = 0):m_fid(fid), m_decl(k), m_next(n) {}
};

class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context {
public:
    enum status {
        UNSAT, SAT, UNKNOWN
    };
    
    enum check_sat_state {
        css_unsat, css_sat, css_unknown, css_clear
    };
    
    typedef std::pair<unsigned, expr*> macro;

    struct scoped_watch {
        cmd_context &   m_ctx;
    public:
        scoped_watch(cmd_context & ctx):m_ctx(ctx) { m_ctx.m_watch.reset(); m_ctx.m_watch.start(); }
        ~scoped_watch() { m_ctx.m_watch.stop(); }
    };

protected:
    bool                         m_main_ctx;
    front_end_params *           m_params;
    bool                         m_params_owner;
    symbol                       m_logic;
    bool                         m_interactive_mode;
    bool                         m_global_decls;
    bool                         m_print_success;
    unsigned                     m_random_seed;
    bool                         m_produce_unsat_cores;
    bool                         m_produce_assignments;
    status                       m_status;
    bool                         m_numeral_as_real;
    bool                         m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
    bool                         m_exit_on_error;
    
    static std::ostringstream    g_error_stream;

    ast_manager *                m_manager;
    bool                         m_own_manager;
    pdecl_manager *              m_pmanager;
    sexpr_manager *              m_sexpr_manager;
    check_logic                  m_check_logic;
    stream_ref                   m_regular;
    stream_ref                   m_diagnostic;
    dictionary<cmd*>             m_cmds;    
    dictionary<builtin_decl>     m_builtin_decls;
    scoped_ptr_vector<builtin_decl> m_extra_builtin_decls; // make sure that dynamically allocated builtin_decls are deleted
    dictionary<object_ref*>      m_object_refs; // anything that can be named.
    dictionary<sexpr*>           m_user_tactic_decls;

    dictionary<func_decls>       m_func_decls;
    obj_map<func_decl, symbol>   m_func_decl2alias;
    dictionary<psort_decl*>      m_psort_decls;
    dictionary<macro>            m_macros;
    // the following fields m_func_decls_stack, m_psort_decls_stack and m_exprs_stack are used when m_global_decls == false
    typedef std::pair<symbol, func_decl *> sf_pair;
    svector<sf_pair>             m_func_decls_stack;
    svector<symbol>              m_psort_decls_stack;
    svector<symbol>              m_macros_stack;
    // 
    ptr_vector<pdecl>            m_aux_pdecls;
    ptr_vector<expr>             m_assertions;
    vector<std::string>          m_assertion_strings;
    ptr_vector<expr>             m_assertion_names; // named assertions are represented using boolean variables.

    struct scope {
        unsigned m_func_decls_stack_lim;
        unsigned m_psort_decls_stack_lim;
        unsigned m_macros_stack_lim;
        unsigned m_aux_pdecls_lim;
        // only m_assertions_lim is relevant when m_global_decls = true
        unsigned m_assertions_lim;
    };

    svector<scope>               m_scopes;
    ref<solver>                  m_solver;
    ref<check_sat_result>        m_check_sat_result;

    stopwatch                    m_watch;

    class dt_eh : public new_datatype_eh {
        cmd_context &             m_owner;
        datatype_util             m_dt_util;
    public:
        dt_eh(cmd_context & owner);
        virtual ~dt_eh();
        virtual void operator()(sort * dt);
    };

    friend class dt_eh;
    scoped_ptr<dt_eh>             m_dt_eh;

    class pp_env;
    friend class pp_env;

    scoped_ptr<pp_env>            m_pp_env;
    pp_env & get_pp_env() const;

    void register_builtin_sorts(decl_plugin * p);
    void register_builtin_ops(decl_plugin * p);
    void register_plugin(symbol const & name, decl_plugin * p, bool install_names);
    void init_manager_core(bool new_manager);
    void init_manager();
    void init_external_manager();
    void reset_cmds();
    void finalize_cmds();

    void restore_func_decls(unsigned old_sz);
    void restore_psort_decls(unsigned old_sz);
    void restore_macros(unsigned old_sz);
    void restore_aux_pdecls(unsigned old_sz);
    void restore_assertions(unsigned old_sz);

    void erase_func_decl_core(symbol const & s, func_decl * f);
    void erase_psort_decl_core(symbol const & s);
    void erase_macro_core(symbol const & s);

    bool logic_has_arith_core(symbol const & s) const;
    bool logic_has_bv_core(symbol const & s) const;
    bool logic_has_array_core(symbol const & s) const;
    bool logic_has_seq_core(symbol const & s) const;
    bool logic_has_arith() const;
    bool logic_has_bv() const;
    bool logic_has_seq() const;
    bool logic_has_array() const;
    bool logic_has_datatype() const;
    bool logic_has_floats() const;
    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;}

public:
    cmd_context(front_end_params * params = 0, bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
    ~cmd_context(); 
    bool is_smtlib2_compliant() const;
    void set_logic(symbol const & s);
    bool has_logic() const { return m_logic != symbol::null; }
    symbol const & get_logic() const { return m_logic; }
    bool is_logic(char const * l_name) const { return has_logic() && strcmp(m_logic.bare_str(), l_name) == 0; }
    bool numeral_as_real() const { return m_numeral_as_real; }
    void set_numeral_as_real(bool f) { m_numeral_as_real = f; }
    void set_interactive_mode(bool flag) { m_interactive_mode = flag; }
    void set_ignore_check(bool flag) { m_ignore_check = flag; }
    void set_exit_on_error(bool flag) { m_exit_on_error = flag; }
    bool exit_on_error() const { return m_exit_on_error; }
    bool interactive_mode() const { return m_interactive_mode; }
    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); }
    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; }
    void set_random_seed(unsigned s) { m_random_seed = s; }
    bool produce_models() const;
    bool produce_proofs() const;
    bool produce_unsat_cores() const { return m_produce_unsat_cores; }
    void set_produce_unsat_cores(bool flag) { m_produce_unsat_cores = flag; }
    bool produce_assignments() const { return m_produce_assignments; }
    void set_produce_assignments(bool flag) { m_produce_assignments = flag; }
    void set_status(status st) { m_status = st; }
    status get_status() const { return m_status; }
    std::string reason_unknown() const;

    bool has_manager() const { return m_manager != 0; }
    ast_manager & m() const { if (!m_manager) const_cast<cmd_context*>(this)->init_manager(); return *m_manager; }
    virtual ast_manager & get_ast_manager() { return m(); }
    pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
    sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
    front_end_params & params() const { return *m_params; }
 
    void set_solver(solver * s);
    solver * get_solver() const { return m_solver.get(); }
    void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }
    check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
    check_sat_state cs_state() const;
    void validate_model();
    
    bool is_func_decl(symbol const & s) const;
    bool is_sort_decl(symbol const& s) const { return m_psort_decls.contains(s); }
    void insert(cmd * c);
    void insert(symbol const & s, func_decl * f); 
    void insert(func_decl * f) { insert(f->get_name(), f); }
    void insert(symbol const & s, psort_decl * p);
    void insert(psort_decl * p) { insert(p->get_name(), p); }
    void insert(symbol const & s, unsigned arity, expr * t);
    void insert(symbol const & s, object_ref *);
    void insert(tactic_cmd * c) { tactic_manager::insert(c); }
    void insert(probe_info * p) { tactic_manager::insert(p); } 
    void insert_user_tactic(symbol const & s, sexpr * d); 
    void insert_aux_pdecl(pdecl * p);
    func_decl * find_func_decl(symbol const & s) const;
    func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices, 
                               unsigned arity, sort * const * domain, sort * range) const;
    psort_decl * find_psort_decl(symbol const & s) const;
    macro find_macro(symbol const & s) const;
    cmd * find_cmd(symbol const & s) const;
    sexpr * find_user_tactic(symbol const & s) const;
    object_ref * find_object_ref(symbol const & s) const;
    void mk_const(symbol const & s, expr_ref & result) const;
    void mk_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, sort * range, 
                expr_ref & r) const;
    void erase_cmd(symbol const & s);
    void erase_func_decl(symbol const & s);
    void erase_func_decl(symbol const & s, func_decl * f);
    void erase_func_decl(func_decl * f) { erase_func_decl(f->get_name(), f); }
    void erase_psort_decl(symbol const & s);
    void erase_macro(symbol const & s);
    void erase_object_ref(symbol const & s);
    void erase_user_tactic(symbol const & s);
    void reset_func_decls();
    void reset_psort_decls();
    void reset_macros();
    void reset_object_refs();
    void reset_user_tactics();
    void set_regular_stream(char const * name) { m_regular.set(name); }
    void set_diagnostic_stream(char const * name); 
    virtual std::ostream & regular_stream() { return *m_regular; }
    virtual std::ostream & diagnostic_stream() { return *m_diagnostic; }
    char const * get_regular_stream_name() const { return m_regular.name(); }
    char const * get_diagnostic_stream_name() const { return m_diagnostic.name(); }
    typedef dictionary<cmd*>::iterator cmd_iterator;
    cmd_iterator begin_cmds() const { return m_cmds.begin(); }
    cmd_iterator end_cmds() const { return m_cmds.end(); }

    typedef dictionary<sexpr*>::iterator user_tactic_iterator;
    user_tactic_iterator begin_user_tactics() const { return m_user_tactic_decls.begin(); }
    user_tactic_iterator end_user_tactics() const { return m_user_tactic_decls.end(); }

    void display_assertions();
    void display_statistics(bool show_total_time = false, double total_time = 0.0);
    void reset(bool finalize = false);
    void assert_expr(expr * t);
    void assert_expr(symbol const & name, expr * t);
    void push_assert_string(std::string const & s) { SASSERT(m_interactive_mode); m_assertion_strings.push_back(s); }
    void push();
    void push(unsigned n);
    void pop(unsigned n);
    void check_sat(unsigned num_assumptions, expr * const * assumptions);
    // display the result produced by a check-sat or check-sat-using commands in the regular stream
    void display_sat_result(lbool r);
    // check if result produced by check-sat or check-sat-using matches the known status
    void validate_check_sat_result(lbool r); 
    unsigned num_scopes() const { return m_scopes.size(); }

    dictionary<macro> const & get_macros() const { return m_macros; }

    bool is_model_available() const;

    double get_seconds() const { return m_watch.get_seconds(); }

    ptr_vector<expr>::const_iterator begin_assertions() const { return m_assertions.begin(); }
    ptr_vector<expr>::const_iterator end_assertions() const { return m_assertions.end(); }

    ptr_vector<expr>::const_iterator begin_assertion_names() const { return m_assertion_names.begin(); }
    ptr_vector<expr>::const_iterator end_assertion_names() const { return m_assertion_names.end(); }

    /**
       \brief Hack: consume assertions if there are no scopes.
       This method is useful for reducing memory consumption in huge benchmarks were incrementality is not an issue.
    */
    bool consume_assertions() {
        if (num_scopes() > 0)
            return false;
        restore_assertions(0);
        return true;
    }

    format_ns::format * pp(sort * s) const;
    virtual void pp(sort * s, format_ns::format_ref & r) const { r = pp(s); }
    virtual void pp(func_decl * f, format_ns::format_ref & r) const;
    virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const;
    virtual void pp(expr * n, format_ns::format_ref & r) const;
    virtual void display(std::ostream & out, sort * s, unsigned indent = 0) const;
    virtual void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const;
    virtual void display(std::ostream & out, expr * n, unsigned indent = 0) const;
    virtual void display(std::ostream & out, func_decl * f, unsigned indent = 0) const;

    // dump assertions in out using the pretty printer.
    void dump_assertions(std::ostream & out) const;

    // display assertions as a SMT2 benchmark.
    void display_smt2_benchmark(std::ostream & out, unsigned num, expr * const * assertions, symbol const & logic = symbol::null) const;


    virtual void slow_progress_sample();
    virtual void fast_progress_sample();
};

std::ostream & operator<<(std::ostream & out, cmd_context::status st);

#endif