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

/**
Copyright (c) 2017 Microsoft Corporation

Module Name:

    solver_pool.h

Abstract:

   Maintain a pool of solvers

Author:

    Nikolaj Bjorner
    Arie Gurfinkel

Notes:

    This is a revision of spacer_virtual_solver 
    consolidated with spacer_smt_context_manager
    by Arie Gurfinkel
    Use this module as a replacement for spacer_smt_context_manager.

--*/
#pragma once

#include "solver/solver.h"
#include "util/stopwatch.h"

class pool_solver;

class solver_pool {

    friend class pool_solver;
    
    struct stats {
        unsigned m_num_checks;
        unsigned m_num_sat_checks;
        unsigned m_num_undef_checks;
        stats() { reset(); }
        void reset() { memset(this, 0, sizeof(*this)); }
    };

    ref<solver>         m_base_solver;
    unsigned            m_num_pools;
    unsigned            m_current_pool;
    sref_vector<solver> m_solvers;
    stats               m_stats;

    stopwatch m_check_watch;
    stopwatch m_check_sat_watch;
    stopwatch m_check_undef_watch;
    stopwatch m_proof_watch;

    void refresh(solver* s);

    ptr_vector<solver> get_base_solvers() const;
  
public:
    solver_pool(solver* base_solver, unsigned num_pools);

    void collect_statistics(statistics &st) const;
    void reset_statistics();

    solver* mk_solver();

    void reset_solver(solver* s);
    void updt_params(const params_ref &p);

};