z3-src 503.2.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
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

/*++
Copyright (c) 2020 Microsoft Corporation

Module Name:

    sls_solver

Abstract:

    Interface to Concurrent SLS solver
    
Author:

    Nikolaj Bjorner (nbjorner) 2024-02-21


--*/

#include "sat/smt/sls_solver.h"
#include "sat/smt/euf_solver.h"
#include "ast/sls/sls_context.h"
#include "ast/for_each_expr.h"

namespace sls {


    solver::solver(euf::solver& ctx) :
        th_euf_solver(ctx, symbol("sls"), ctx.get_manager().mk_family_id("sls"))
    {}

#ifdef SINGLE_THREAD

#else

    solver::~solver() {
        finalize();
    }

    params_ref solver::get_params() {
        return s().params();
    }

    void solver::set_value(expr* t, expr* v) {
        ctx.user_propagate_initialize_value(t, v);
    }

    void solver::force_phase(sat::literal lit) {
        ctx.s().set_phase(lit);
    }

    void solver::set_has_new_best_phase(bool b) {
        ctx.s().set_has_new_best_phase(b);
    }

    bool solver::get_best_phase(sat::bool_var v) {
        return ctx.s().get_best_phase(v);
    }

    expr* solver::bool_var2expr(sat::bool_var v) {
        return ctx.bool_var2expr(v);
    }

    void solver::set_finished() {
        ctx.s().set_canceled();
    }

    unsigned solver::get_num_bool_vars() const {
        return s().num_vars();
    }

    void solver::finalize() {
        if (!m_smt_plugin)
            return;
        
        m_smt_plugin->finalize(m_model, m_st);
        m_model = nullptr;
        m_smt_plugin = nullptr;
    }

    bool solver::unit_propagate() {
        force_push();
        if (m_smt_plugin && !m_checking) {
            expr_ref_vector fmls(m);
            m_checking = true;
            m_smt_plugin->check(fmls, ctx.top_level_clauses());
            return true;
        }
        if (!m_smt_plugin)
            return false;
        if (!m_smt_plugin->completed())
            return false;
        m_smt_plugin->finalize(m_model, m_st);
        m_smt_plugin = nullptr;
        return true;
    }

    void solver::pop_core(unsigned n) {
        if (!m_smt_plugin)
            return;

        unsigned scope_lvl = s().scope_lvl();
        if (s().search_lvl() == scope_lvl - n) {
            for (; m_trail_lim < s().init_trail_size(); ++m_trail_lim) {
                auto lit = s().trail_literal(m_trail_lim);
                m_smt_plugin->add_unit(lit);
            }
        }

        m_smt_plugin->import_from_sls();
    }

    void solver::init_search() {
        if (m_smt_plugin)
            finalize();
        m_smt_plugin = alloc(sls::smt_plugin, *this);
        m_checking = false;
    }

    std::ostream& solver::display(std::ostream& out) const {
        return out << "theory-sls\n";
    }
     

#endif
}