z3-src 503.0.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
86
87
88
89
90
91
92
93
94
95

/*++
Copyright (c) 2019 Microsoft Corporation

Module Name:

    dd_pdd.cpp

Abstract:

    Poly DD package 

Author:

    Nikolaj Bjorner (nbjorner) 2019-12-24
    Lev Nachmanson (levnach) 2019-12-24

Revision History:

--*/
#pragma once

#include "math/dd/dd_pdd.h"
#include "math/interval/dep_intervals.h"

namespace dd {
typedef dep_intervals::interval interval;
typedef dep_intervals::with_deps_t w_dep;
// calculates the interval of a pdd expression based on the given intervals of the variables
class pdd_interval {
    dep_intervals& m_dep_intervals;
    std::function<void (unsigned, bool, scoped_dep_interval&)> m_var2interval;

    // retrieve intervals after distributing multiplication over addition.
    template <w_dep wd>
    void get_interval_distributed(pdd const& p, scoped_dep_interval& i, scoped_dep_interval& ret) {
        bool deps = wd == w_dep::with_deps;
        if (p.is_val()) {
            if (deps)
                m_dep_intervals.mul<dep_intervals::with_deps>(p.val(), i, ret);
            else
                m_dep_intervals.mul<dep_intervals::without_deps>(p.val(), i, ret);
            return;
        }
        scoped_dep_interval hi(m()), lo(m()), t(m()), a(m());
        get_interval_distributed<wd>(p.lo(), i, lo);
        m_var2interval(p.var(), deps, a);
        if (deps) {
            m_dep_intervals.mul<dep_intervals::with_deps>(a, i, t);
            get_interval_distributed<wd>(p.hi(), t, hi);
            m_dep_intervals.add<dep_intervals::with_deps>(hi, lo, ret);
        }
        else {
            m_dep_intervals.mul<dep_intervals::without_deps>(a, i, t);
            get_interval_distributed<wd>(p.hi(), t, hi);
            m_dep_intervals.add<dep_intervals::without_deps>(hi, lo, ret);
        }
    }

public:
    
    pdd_interval(dep_intervals& d): m_dep_intervals(d) {}

    dep_intervals& m() { return m_dep_intervals; }

    std::function<void (unsigned, bool, scoped_dep_interval&)>& var2interval() { return m_var2interval; } // setter
    const std::function<void (unsigned, bool, scoped_dep_interval&)>& var2interval() const { return m_var2interval; } // getter

    template <w_dep wd>
    void get_interval(pdd const& p, scoped_dep_interval& ret) {
        if (p.is_val()) {
            m_dep_intervals.set_interval_for_scalar(ret, p.val());
            return;
        }
        bool deps = wd == w_dep::with_deps;
        scoped_dep_interval hi(m()), lo(m()), t(m()), a(m());
        m_var2interval(p.var(), deps, a);
        get_interval<wd>(p.hi(), hi);
        get_interval<wd>(p.lo(), lo);
        if (deps) {
            m_dep_intervals.mul<dep_intervals::with_deps>(hi, a, t);
            m_dep_intervals.add<dep_intervals::with_deps>(t, lo, ret);
        } else {
            m_dep_intervals.mul(hi, a, t);
            m_dep_intervals.add(t, lo, ret);
        }
    }

    template <w_dep wd>
    void get_interval_distributed(pdd const& p, scoped_dep_interval& ret) {
        scoped_dep_interval i(m());
        m_dep_intervals.set_interval_for_scalar(i, rational::one());        
        get_interval_distributed<wd>(p, i, ret);
    }
};
}