z3-src 415.4.4

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) 2011 Microsoft Corporation

Module Name:

    permutation.cpp

Abstract:

    Goodies for managing permutations.

Author:

    Leonardo de Moura (leonardo) 2011-06-10.

Revision History:

--*/
#include "util/permutation.h"

permutation::permutation(unsigned size) {
    reset(size);
}

void permutation::reset(unsigned size) {
    m_p.reset();
    m_inv_p.reset();
    for (unsigned i = 0; i < size; i++) {
        m_p.push_back(i);
        m_inv_p.push_back(i);
    }
}

void permutation::swap(unsigned i, unsigned j) noexcept {
    unsigned i_prime = m_p[i];
    unsigned j_prime = m_p[j];
    std::swap(m_p[i], m_p[j]);
    std::swap(m_inv_p[i_prime], m_inv_p[j_prime]); 
    SASSERT(check_invariant());
}

/**
   \brief Move i after j.
*/
void permutation::move_after(unsigned i, unsigned j) {
    if (i >= j)
        return;
    unsigned i_prime = m_p[i];
    for (unsigned k = i; k < j; k++) {
        m_p[k] = m_p[k+1];
        m_inv_p[m_p[k]] = k;
    }
    m_p[j] = i_prime;
    m_inv_p[i_prime] = j;
    SASSERT(check_invariant());
}

void permutation::display(std::ostream & out) const {
    unsigned n = m_p.size();
    for (unsigned i = 0; i < n; i++) {
        if (i > 0)
            out << " ";
        out << i << ":" << m_p[i];
    }
}

bool permutation::check_invariant() const {
    SASSERT(m_p.size() == m_inv_p.size());
    unsigned n = m_p.size();
    bool_vector check_vector(n, false); // To check for duplicate and out-of-range values
    for (unsigned i = 0; i < n; i++) {
        unsigned pi = m_p[i];
        SASSERT(m_p[i] < n);
        SASSERT(m_inv_p[i] < n);
        SASSERT(m_p[m_inv_p[i]] == i);
        SASSERT(m_inv_p[m_p[i]] == i);
        // Check the inversion hasn't been checked yet
        if (check_vector[pi]) {
            return false;
        }
        // Mark this value as checked
        check_vector[pi] = true;
    }
    return true;
}