z3-src 503.0.0

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
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91

/*++
Copyright (c) 2017 Microsoft Corporation and Arie Gurfinkel

Module Name:

    spacer_dl_interface.h

Abstract:

    SMT2 interface for the datalog SPACER

Author:


Revision History:

--*/

#pragma once

#include "util/lbool.h"
#include "muz/base/dl_rule.h"
#include "muz/base/dl_rule_set.h"
#include "muz/base/dl_engine_base.h"
#include "util/statistics.h"

namespace datalog {
class context;
}

namespace spacer {

class context;

class dl_interface : public datalog::engine_base {
    datalog::context& m_ctx;
    datalog::rule_set m_spacer_rules;
    datalog::rule_set m_old_rules;
    context*          m_context;
    obj_map<func_decl, func_decl*> m_pred2slice;
    ast_ref_vector    m_refs;

    void check_reset();

public:
    dl_interface(datalog::context& ctx);
    ~dl_interface() override;

    lbool query(expr* query) override;

    lbool query_from_lvl(expr* query, unsigned lvl) override;

    void display_certificate(std::ostream& out) const override;

    void collect_statistics(statistics& st) const override;

    void reset_statistics() override;

    expr_ref get_answer() override;

    expr_ref get_ground_sat_answer() override;

    void get_rules_along_trace(datalog::rule_ref_vector& rules) override;

    unsigned get_num_levels(func_decl* pred) override;

    expr_ref get_cover_delta(int level, func_decl* pred) override;

    void add_cover(int level, func_decl* pred, expr* property) override;

    void add_invariant(func_decl* pred, expr* property) override;

    expr_ref get_reachable(func_decl *pred) override;

    void updt_params() override;

    model_ref get_model() override;

    proof_ref get_proof() override;

    void add_callback(void *state,
                      const datalog::t_new_lemma_eh new_lemma_eh,
                      const datalog::t_predecessor_eh predecessor_eh,
                      const datalog::t_unfold_eh unfold_eh) override;

    void add_constraint (expr *c, unsigned lvl) override;

};
}