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

#pragma once
/**++
Copyright (c) 2020 Arie Gurfinkel

Module Name:

    spacer_arith_kernel.cpp

Abstract:

    Compute kernel of a matrix

Author:

    Hari Govind
    Arie Gurfinkel

Notes:

--*/

#include "spacer_matrix.h"
#include "util/statistics.h"
namespace spacer {

/**
   Computes a kernel of a matrix.
*/
class spacer_arith_kernel {
  public:
    class plugin {
      public:
        virtual ~plugin() = default;
        virtual bool compute_kernel(const spacer_matrix &in_matrix,
                                    spacer_matrix &out_kernel,
                                    vector<unsigned> &basics) = 0;
        virtual void collect_statistics(statistics &st) const = 0;
        virtual void reset_statistics() = 0;
        virtual void reset() = 0;
    };

  protected:
    struct stats {
        unsigned m_failed;
        stats() { reset(); }
        void reset() { m_failed = 0; }
    };
    stats m_st;

    /// Input matrix for which kernel is to be computed
    const spacer_matrix &m_matrix;

    /// Output matrix representing the kernel
    spacer_matrix m_kernel;
    /// columns in the kernel that correspond to basic vars
    vector<unsigned> m_basic_vars;

    scoped_ptr<plugin> m_plugin;

  public:
    spacer_arith_kernel(spacer_matrix &matrix)
        : m_matrix(matrix), m_kernel(0, 0) {}
    virtual ~spacer_arith_kernel() = default;

    void set_plugin(spacer_arith_kernel::plugin *plugin) { m_plugin = plugin; }

    /// Computes kernel of a matrix
    /// returns true if the computation was successful
    /// use \p spacer_arith_kernel::get_kernel() to get the kernel
    bool compute_kernel();
    bool operator()() { return compute_kernel(); }

    const spacer_matrix &get_kernel() const { return m_kernel; }
    const vector<unsigned> &get_basic_vars() const { return m_basic_vars; }

    void reset() {
        m_kernel = spacer_matrix(0, 0);
        if (m_plugin) m_plugin->reset();
    }

    virtual void collect_statistics(statistics &st) const {
        st.update("SPACER arith kernel failed", m_st.m_failed);
        if (m_plugin) { m_plugin->collect_statistics(st); }
    }
    virtual void reset_statistics() {
        m_st.reset();
        if (m_plugin) m_plugin->reset_statistics();
    }
};

spacer_arith_kernel::plugin *mk_simplex_kernel_plugin();

} // namespace spacer