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

/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    prime_generator.h

Abstract:

    Prime generator

Author:

    Leonardo (leonardo) 2011-12-23

Notes:

--*/
#pragma once

#include "util/vector.h"
#include "util/z3_exception.h"
#include "util/util.h"
#include "util/memory_manager.h"

class prime_generator_exception : public default_exception {
public:
    prime_generator_exception(char const * msg):default_exception(msg) {}
};

/**
   \brief Prime generator
*/
class prime_generator {
    svector<uint64_t> m_primes;
    void process_next_k_numbers(uint64_t k);
public:
    uint64_t operator()(unsigned idx);
    void initialize();
    void finalize();
};

class prime_iterator {
    unsigned          m_idx;
    prime_generator * m_generator;
    bool              m_global;
public:
    prime_iterator(prime_generator * g = nullptr);
    uint64_t next();
    static void initialize();
    static void finalize();
};

Z3_ADD_INITIALIZER(prime_iterator, prime_iterator::initialize, 0);
Z3_ADD_FINALIZER(prime_iterator, prime_iterator::finalize);