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
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

/*++
Copyright (c) 2020 Microsoft Corporation

Module Name:

    theory_sls
    
Abstract:

    Interface to Concurrent SLS solver
    
Author:

    Nikolaj Bjorner (nbjorner) 2024-10-24

--*/
#pragma once


#include "util/rlimit.h"
#include "ast/sls/sat_ddfw.h"
#include "smt/smt_theory.h"
#include "model/model.h"


#ifdef SINGLE_THREAD

namespace smt {
    class theory_sls : public theory {
        model_ref m_model;
    public:
        theory_sls(context& ctx);
        model_ref get_model() { return m_model; }
        char const* get_name() const override { return "sls"; }
        smt::theory* mk_fresh(context* new_ctx) override { return alloc(theory_sls, *new_ctx); }
        void display(std::ostream& out) const override {}
        bool internalize_atom(app* atom, bool gate_ctx) override { return false; }
        bool internalize_term(app* term) override { return false; }
        void new_eq_eh(theory_var v1, theory_var v2) override {}
        void new_diseq_eh(theory_var v1, theory_var v2) override {}
    };
}

#else

#include "ast/sls/sls_smt_plugin.h"


namespace smt {

    class theory_sls : public theory, public sls::smt_context {
        struct stats {
            unsigned m_num_guided_sls = 0;
            unsigned m_num_restart_sls = 0;
        };
        stats m_stats;
        mutable model_ref m_model;
        mutable sls::smt_plugin* m_smt_plugin = nullptr;
        unsigned m_trail_lim = 0;
        bool m_checking = false;
        bool m_parallel_mode = true;
        unsigned m_restart_gap = 1;
        unsigned m_restart_ls_steps = 100000;
        unsigned m_restart_ls_steps_inc = 10000;
        unsigned m_restart_ls_steps_max = 300000;
        unsigned m_final_check_ls_steps = 30000;
        unsigned m_final_check_ls_steps_delta = 10000;
        unsigned m_final_check_ls_steps_min = 10000;
        bool     m_has_unassigned_clause_after_resolve = false;
        unsigned m_after_resolve_decide_gap = 4;
        unsigned m_after_resolve_decide_count = 0;
        unsigned m_resolve_count = 0;
        unsigned m_resolve_gap = 0;
        unsigned m_max_propagation_scope = 0;
        unsigned m_propagation_scope = 0;
        mutable bool     m_init_search = false;
        mutable ::statistics m_st;
        vector<sat::literal_vector> m_shared_clauses;


        void bounded_run(unsigned num_steps);
        void inc_restart_ls_steps() {
            if (m_restart_ls_steps < m_restart_ls_steps_max)
                m_restart_ls_steps += m_restart_ls_steps_inc;
        }
        void dec_final_check_ls_steps() {
            if (m_final_check_ls_steps > m_final_check_ls_steps_min)
                m_final_check_ls_steps -= m_final_check_ls_steps_delta;
        }

        bool shared_clauses_are_true() const;
        void check_for_unassigned_clause_after_resolve();
        void propagate_local_search();

        void run_guided_sls();
        void finalize() const;

        void update_propagation_scope();

    public:
        theory_sls(context& ctx);
        ~theory_sls() override;

        model_ref get_model() { return m_model; }

        // smt::theory interface
        char const* get_name() const override { return "sls"; }
        void init() override;
        void pop_scope_eh(unsigned n) override;
        smt::theory* mk_fresh(context* new_ctx) override { return alloc(theory_sls, *new_ctx); }
        void collect_statistics(::statistics& st) const override;
        void propagate() override;
        void display(std::ostream& out) const override;
        bool internalize_atom(app * atom, bool gate_ctx) override { return false; }
        bool internalize_term(app* term) override { return false; }
        void new_eq_eh(theory_var v1, theory_var v2) override {}
        void new_diseq_eh(theory_var v1, theory_var v2) override {}
        void restart_eh() override;
        final_check_status final_check_eh(unsigned) override;

        // sls::smt_context interface
        ast_manager& get_manager() override { return m; }
        params_ref get_params() override;
        void set_value(expr* t, expr* v) override;
        void force_phase(sat::literal lit) override;
        void set_has_new_best_phase(bool b) override;
        bool get_best_phase(sat::bool_var v) override;
        expr* bool_var2expr(sat::bool_var v) override;
        void set_finished() override;
        unsigned get_num_bool_vars() const override;
        void inc_activity(sat::bool_var v, double inc) override;
        bool parallel_mode() const override { return m_parallel_mode; }
        bool get_smt_value(expr* v, expr_ref& value) override;
        void init_search_eh() override;

    };

}

#endif