z3-src 503.2.2

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
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

/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    z3_replayer.h

Abstract:

    Interpreter for Z3 logs

Author:

    Leonardo de Moura (leonardo) 2011-09-22

Notes:
    
--*/
#pragma once

#include "api/z3.h"
#include "util/z3_exception.h"

class z3_replayer;

typedef void (*z3_replayer_cmd)(z3_replayer &);

typedef default_exception z3_replayer_exception;

class z3_replayer {
    struct imp;
    imp *  m_imp;
public:
    z3_replayer(std::istream & in);
    ~z3_replayer();
    void parse();
    unsigned get_line() const;

    int get_int(unsigned pos) const;
    unsigned get_uint(unsigned pos) const;
    int64_t get_int64(unsigned pos) const;
    uint64_t get_uint64(unsigned pos) const;
    float get_float(unsigned pos) const;
    double get_double(unsigned pos) const;
    bool get_bool(unsigned pos) const;
    Z3_string get_str(unsigned pos) const;
    Z3_symbol get_symbol(unsigned pos) const;
    void * get_obj(unsigned pos) const;

    unsigned * get_uint_array(unsigned pos) const;
    int * get_int_array(unsigned pos) const;
    bool * get_bool_array(unsigned pos) const;
    Z3_symbol * get_symbol_array(unsigned pos) const;
    void ** get_obj_array(unsigned pos) const;

    bool * get_bool_addr(unsigned pos);
    int * get_int_addr(unsigned pos);
    int64_t * get_int64_addr(unsigned pos);
    unsigned * get_uint_addr(unsigned pos);
    uint64_t * get_uint64_addr(unsigned pos);
    Z3_string * get_str_addr(unsigned pos);
    void ** get_obj_addr(unsigned pos);

    void store_result(void * obj);
    void register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name);
};