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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146

/*++
Copyright (c) 2018 Microsoft Corporation

Module Name:

    recfun_rewriter.cpp

Abstract:

    Rewriter recursive function applications to values

Author:

    Nikolaj Bjorner (nbjorner) 2020-04-26


--*/


#include "ast/rewriter/recfun_rewriter.h"
#include "ast/rewriter/var_subst.h"
#include "ast/datatype_decl_plugin.h"
#include "ast/for_each_expr.h"
#include "params/rewriter_params.hpp"

void recfun_rewriter::updt_params(params_ref const &p) {
    rewriter_params rp(p);
    m_recfun_unfold = rp.unfold_recursive_functions();
}
    
br_status recfun_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
    if (m_rec.is_defined(f) && num_args > 0) {
        if (!m_rec.has_def(f))
            return BR_FAILED;
        recfun::def const& d = m_rec.get_def(f);
        if (!d.get_rhs())
            return BR_FAILED;
        auto r = d.get_rhs();
        bool safe_to_subst = true;
        for (unsigned i = 0; i < num_args; ++i) 
            if (!m.is_value(args[i]))
                safe_to_subst = false;
        if (!m_recfun_unfold) {
            for (auto t : subterms::all(expr_ref(r, m)))
                if (is_uninterp(t))
                    return BR_FAILED;
        }            

        // check if there is an argument that is a constructor
        // such that the recursive function can be partially evaluated.
        // At most one kind of accessor is allowed to prevent recursive
        // patterns that reconstruct the argument indirectly, unless the
        // argument is ground: accessors of a ground constructor term are
        // strictly smaller ground terms, so unfolding terminates.
        // Model evaluation relies on the ground case to check a quantifier over a
        // recursively defined function whose recursion argument is ground
        // (e.g. forall a. isList(a, items)) - see smt_model_finder.
        if (!safe_to_subst && !has_quantifiers(r)) {
            datatype::util u(m);
            for (unsigned i = 0; i < num_args; ++i) {
                auto arg = args[i];
                if (u.is_constructor(arg) && is_decreasing_arg(f, i, is_ground(arg))) {
                    safe_to_subst = true;
                    break;
                }
            }            
        }
        if (safe_to_subst) {
            var_subst sub(m);
            result = sub(d.get_rhs(), num_args, args);
            return BR_REWRITE_FULL;
        }
        return BR_FAILED;
        
    }
    else 
        return BR_FAILED;
}

bool recfun_rewriter::is_decreasing_arg(func_decl* f, unsigned i, bool allow_any_accessor) {
    if (!m_rec.is_defined(f) || !m_rec.has_def(f))
        return false;
    recfun::def const& d = m_rec.get_def(f);
    expr* r = d.get_rhs();
    if (!r || has_quantifiers(r))
        return false;
    datatype::util u(m);
    unsigned num_args = f->get_arity();
    unsigned idx = num_args - i - 1;
    func_decl* dec_fun = nullptr;
    for (auto t : subterms::all(expr_ref(r, m))) {
        if (is_app(t) && any_of(*to_app(t), [&](expr* e) { return is_var(e) && to_var(e)->get_idx() == idx; })) {
            if (!u.is_accessor(t) && !u.is_is(t) && !u.is_recognizer(t))
                return false;
            if (u.is_accessor(t)) {
                if (!allow_any_accessor && dec_fun && to_app(t)->get_decl() != dec_fun)
                    return false;
                dec_fun = to_app(t)->get_decl();
            }
        }
    }
    if (allow_any_accessor) {
        // Using the argument only through accessors does not make the
        // recursion decrease on it: the body may rebuild a constructor
        // term for position i from other data and recurse on a different
        // argument, e.g. (f (tail s) (mk (proj_1 t) ...)) recursing on a
        // sequence s. Unfolding such a ground constructor argument never
        // terminates. Require every recursive call to pass a strict
        // accessor chain of the argument at position i.
        if (!dec_fun)
            return false;
        for (auto t : subterms::all(expr_ref(r, m))) {
            if (!is_app(t) || to_app(t)->get_decl() != f)
                continue;
            expr* a = to_app(t)->get_arg(i);
            bool strict = false;
            while (is_app(a) && u.is_accessor(a)) {
                a = to_app(a)->get_arg(0);
                strict = true;
            }
            if (!strict || !is_var(a) || to_var(a)->get_idx() != idx)
                return false;
        }
    }
    return dec_fun != nullptr || !allow_any_accessor;
}

bool recfun_rewriter::is_recfun_with_ground_recursion_args(app* t) {
    func_decl* f = t->get_decl();
    if (!m_rec.is_defined(f) || !m_rec.has_def(f))
        return false;
    bool has_decreasing = false;
    unsigned i = 0;
    for (expr* arg : *t) {
        sort* s = arg->get_sort();
        if (!is_ground(arg)) {
            if (!m.is_uninterp(s))
                return false;
        }
        else if (m_dt.is_datatype(s) && is_decreasing_arg(f, i, true)) {
            has_decreasing = true;
        }
        ++i;
    }
    return has_decreasing;
}