z3-src 501.0.1

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

#pragma once

#include "ast/ast.h"
#include <functional>

class term_enumeration {
    struct imp;
    imp* m_imp;
public:
    term_enumeration(ast_manager& m);
    ~term_enumeration();

    void add_production(func_decl* f);
    void add_production(expr* e);
    // void add_production(sort *s, std::function<expr *()> g);

    // cost function associated with expressions.
    // terms are enumerated with increasing cost.

    void set_cost(std::function<unsigned(expr*)> const& cost);

    class iterator {
        struct iter_imp;
        iter_imp* m_imp;
    public:
        iterator(imp& i, sort* s);
        iterator(std::nullptr_t);
        ~iterator();
        expr* operator*();
        iterator operator++(int);
        iterator& operator++();
        bool operator!=(iterator const& other) const {
            return !(*this == other);
        }
        bool operator==(iterator const &other) const;
    };

    class terms {
        imp* m_imp;
        sort* m_sort;
    public:
        terms(imp* i, sort* s);
        iterator begin();
        iterator end();
    };

    terms enum_terms(sort* s);

    // -- tuple enumeration --
    // Iterate over vectors of terms, one term per input sort. Produces all
    // combinations (dovetailed, since individual streams may be infinite).

    class tuple_iterator {
        struct timp;
        timp* m_imp;
    public:
        tuple_iterator(imp& i, unsigned n, sort* const* sorts);
        tuple_iterator(std::nullptr_t);
        ~tuple_iterator();
        expr_ref_vector operator*();
        tuple_iterator& operator++();
        bool operator!=(tuple_iterator const& other) const {
            return !(*this == other);
        }
        bool operator==(tuple_iterator const& other) const;
    };

    class tuples {
        imp*             m_imp;
        ptr_vector<sort> m_sorts;
    public:
        tuples(imp* i, unsigned n, sort* const* sorts);
        tuple_iterator begin();
        tuple_iterator end();
    };

    tuples enum_tuples(unsigned n, sort* const* sorts);
    tuples enum_tuples(sort_ref_vector const& sorts);

    std::ostream& display(std::ostream& out) const;
};