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
86
87
88
89
90
91
92
93

/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    permutation.h

Abstract:

    Simple abstraction for managing permutations.

Author:

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

Revision History:

--*/
#pragma once

#include<ostream>
#include "util/vector.h"

class permutation {
    unsigned_vector m_p;
    unsigned_vector m_inv_p;
public:
    permutation(unsigned size = 0);
    void reset(unsigned size = 0);

    unsigned operator()(unsigned i) const { return m_p[i]; }
    unsigned inv(unsigned i_prime) const { return m_inv_p[i_prime]; }

    void swap(unsigned i, unsigned j) noexcept;
    void move_after(unsigned i, unsigned j);
    
    void display(std::ostream & out) const;
    bool check_invariant() const;
};

void swap(unsigned i, unsigned j) noexcept;

inline std::ostream & operator<<(std::ostream & out, permutation const & p) {
    p.display(out);
    return out;
}

/**
   \brief Apply permutation p to data.
   The algorithm does not use any extra memory.
   
   Requirement: swap(T, T) must be available.

   This version will perform destructive updates to p.
   Use apply_permutation if p must not be preserved
*/
template<typename T>
void apply_permutation_core(unsigned sz, T * data, unsigned * p) {
    int * p1 = reinterpret_cast<int*>(p);
    for (int i = 0; i < static_cast<int>(sz); i++) {
        if (p1[i] < 0)
            continue; // already processed
        int j = i;
        while (true) {
            SASSERT(j >= 0);
            int p_j = p1[j];
            SASSERT(p_j >= 0);
            SASSERT(p_j < static_cast<int>(sz));
            p1[j]   = - p1[j] - 1; // mark as done
            if (p_j == i)
                break; // cycle starting at i is done
            swap(data[j], data[p_j]);
            j = p_j;
        }
    }
}

/**
   \brief Apply permutation p to data.
   The algorithm does not use any extra memory.
   
   Requirement: swap(T, T) must be available.
*/
template<typename T>
void apply_permutation(unsigned sz, T * data, unsigned const * p) {
    apply_permutation_core(sz, data, const_cast<unsigned*>(p));
    // restore p
    int * p1 = reinterpret_cast<int*>(const_cast<unsigned*>(p));
    for (unsigned i = 0; i < sz; i++) { 
        p1[i] = - p1[i] - 1;
    }
}