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

/*++
Copyright (c) 2017 Microsoft Corporation

Module Name:

    <name>

Abstract:

    <abstract>

Author:

    Lev Nachmanson (levnach)

Revision History:


--*/
#pragma once

#include <cmath>
#include <string>
#include "math/lp/matrix.h"
namespace lp {
#ifdef Z3DEBUG
template <typename T, typename X>
bool matrix<T, X>::is_equal(const matrix<T, X>& other) {
    if (other.row_count() != row_count() || other.column_count() != column_count())
        return false;
    for (unsigned i = 0; i < row_count(); ++i) {
        for (unsigned j = 0; j < column_count(); ++j) {
            auto a = get_elem(i, j);
            auto b = other.get_elem(i, j);
            
            if (a != b) return false;
            
        }
    }
    return true;
}

template <typename T, typename X>
void apply_to_vector(matrix<T, X> & m, T * w) {
    // here m is a square matrix
    unsigned dim = m.row_count();

    T * wc = new T[dim];

    for (unsigned i = 0; i < dim; ++i) {
        wc[i] = w[i];
    }

    for (unsigned i = 0; i < dim; ++i) {
        T t = numeric_traits<T>::zero();
        for (unsigned j = 0; j < dim; ++j) {
            t += m(i, j) * wc[j];
        }
        w[i] = t;
    }
    delete [] wc;
}

#endif

unsigned get_width_of_column(unsigned j, vector<vector<std::string>> & A) {
    unsigned r = 0;
    for (unsigned i = 0; i < A.size(); ++i) {
        vector<std::string> & t = A[i];
        std::string str = t[j];
        unsigned s = static_cast<unsigned>(str.size());
        if (r < s) {
            r = s;
        }
    }
    return r;
}

void print_matrix_with_widths(vector<vector<std::string>> & A, vector<unsigned> & ws, std::ostream & out, unsigned blanks_in_front) {
    for (unsigned i = 0; i < A.size(); ++i) {
        for (unsigned j = 0; j < static_cast<unsigned>(A[i].size()); ++j) {
            if (i != 0 && j == 0)
                print_blanks(blanks_in_front, out);
            print_blanks(ws[j] - static_cast<unsigned>(A[i][j].size()), out);
            out << A[i][j] << " ";
        }
        out << std::endl;
    }
}

void print_string_matrix(vector<vector<std::string>> & A, std::ostream & out, unsigned blanks_in_front) {
    vector<unsigned> widths;

    if (!A.empty())
        for (unsigned j = 0; j < A[0].size(); ++j) {
            widths.push_back(get_width_of_column(j, A));
        }

    print_matrix_with_widths(A, widths, out, blanks_in_front);
    out << std::endl;
}

template <typename T>
void print_matrix(vector<vector<T>> & A, std::ostream & out, unsigned blanks_in_front = 0) {
    vector<vector<std::string>> s(A.size());
    for (unsigned i = 0; i < A.size(); ++i) {
        for (const auto & v : A[i]) {
            s[i].push_back(T_to_string(v));
        }
    }

    print_string_matrix(s, out, blanks_in_front);
}


template <typename T, typename X>
void print_matrix(matrix<T, X> const * m, std::ostream & out) {
    vector<vector<std::string>> A(m->row_count());
    for (unsigned i = 0; i < m->row_count(); ++i) {
        for (unsigned j = 0; j < m->column_count(); ++j) {
            A[i].push_back(T_to_string(m->get_elem(i, j)));
        }
    }

    print_string_matrix(A, out);
}

}