z3-src 501.0.1

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

/*++
Copyright (c) 2014 Microsoft Corporation

Module Name:

    bvsls_opt_engine.h

Abstract:

    Optimization extensions to bvsls

Author:

    Christoph (cwinter) 2014-03-28

Notes:

--*/
#pragma once

#include "ast/sls/sls_bv_engine.h"

class bvsls_opt_engine : public sls_engine {
    sls_tracker   & m_hard_tracker;
    sls_tracker     m_obj_tracker;
    sls_evaluator   m_obj_evaluator;
    model_ref       m_best_model;
    mpz             m_best_model_score;
    unsigned        m_obj_bv_sz;
    expr          * m_obj_e;

public:
    bvsls_opt_engine(ast_manager & m, params_ref const & p);

    class optimization_result {
    public:
        lbool is_sat;
        expr_ref optimum;
        optimization_result(ast_manager & m) : is_sat(l_undef), optimum(m) {}
    };

    optimization_result optimize(expr_ref const & objective, model_ref initial_model = model_ref(), bool maximize=true);

    void get_model(model_ref & result) { result = m_best_model; }

protected:
    void setup_opt_tracker(expr_ref const & objective, bool _max);
    expr_ref maximize();    

    bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp, 
                 mpz & best_score, unsigned & best_const, mpz & best_value);

    mpz find_best_move(ptr_vector<func_decl> & to_evaluate, mpz & score,
                       unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move,
                       mpz const & max_score, expr * objective);

    mpz top_score() {
        mpz res(0);
        obj_hashtable<expr> const & top_exprs = m_obj_tracker.get_top_exprs();
        for (auto* e : top_exprs)
            m_mpz_manager.add(res, m_obj_tracker.get_value(e), res);
        return res;
    }

    void save_model(mpz const & score);
    bool randomize_wrt_hard();
};