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

/*++
Copyright (c) 2017 Microsoft Corporation

Module Name:

    <name>

Abstract:

    <abstract>

Author:

    Lev Nachmanson (levnach)

Revision History:


--*/
#pragma once

#include "util/vector.h"
#include "math/lp/indexed_vector.h"
#include "math/lp/lp_settings.h"
namespace lp {


void print_vector_as_doubles(const vector<mpq> & t, std::ostream & out) {
    for (unsigned i = 0; i < t.size(); ++i)
        out << t[i].get_double() << std::setprecision(3) << " ";
    out << std::endl;
}

template <typename T>
void indexed_vector<T>::resize(unsigned data_size) {
    m_data.resize(data_size, numeric_traits<T>::zero());
}

template <typename T>
void indexed_vector<T>::set_value(const T& value, unsigned index) {
    m_data[index] = value;
    SASSERT(std::find(m_index.begin(), m_index.end(), index) == m_index.end());
    m_index.push_back(index);
}

template <typename T>
void indexed_vector<T>::clear() {
    for (unsigned i : m_index)
        m_data[i] = numeric_traits<T>::zero();
    m_index.resize(0);
}
template <typename T>
void indexed_vector<T>::clear_all() {
    unsigned i = static_cast<unsigned>(m_data.size());
    while (i--)  m_data[i] = numeric_traits<T>::zero();
    m_index.resize(0);
}
template <typename T>
void indexed_vector<T>::erase_from_index(unsigned j) {
    auto it = std::find(m_index.begin(), m_index.end(), j);
    if (it != m_index.end())
        m_index.erase(it);
}

template <typename T>
void indexed_vector<T>::erase(unsigned j) {
    auto it = std::find(m_index.begin(), m_index.end(), j);
    if (it != m_index.end()) {
        m_data[j] = 0;
        m_index.erase(it);
    }
}


template <typename T>
void indexed_vector<T>::print(std::ostream & out) {
    out << "m_index " << std::endl;
    for (unsigned i = 0; i < m_index.size(); ++i) {
        out << m_index[i] << " ";
    }
    out << std::endl;
    print_vector(m_data, out);
}

}