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

/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    bv1_blaster_tactic.cpp

Abstract:

    Probe for checking if a goal is in the QF_BV fragment that uses only =, extract, and concat.

Author:

    Leonardo (leonardo) 2011-10-25

Notes:

--*/
#include "tactic/bv/bv1_blaster_tactic.h"
#include "tactic/tactic.h"
#include "ast/bv_decl_plugin.h"
#include "ast/for_each_expr.h"

class is_qfbv_eq_probe : public probe {
    struct not_target : public std::exception {};

    struct visitor {
        family_id m_bv_fid;
        visitor(family_id bv_fid) : m_bv_fid(bv_fid) {}
        void operator()(var const* n) { throw not_target(); }
        void operator()(app const* n) {
            if (n->get_family_id() == m_bv_fid) {
                switch (n->get_decl_kind()) {
                case OP_BV_NUM:
                case OP_EXTRACT:
                case OP_CONCAT:
                    return;
                default:
                    throw not_target();
                }
            }
        }
        void operator()(quantifier const* n) { throw not_target(); }
    };

public:
    result operator()(goal const& g) override {
        bv_util util(g.m());
        expr_fast_mark1 visited;
        visitor proc(util.get_family_id());
        try {
            for (unsigned i = 0; i < g.size(); ++i)
                for_each_expr_core<visitor, expr_fast_mark1, false, true>(proc, visited, g.form(i));
        }
        catch (const not_target&) {
            return false;
        }
        return true;
    }
};

probe* mk_is_qfbv_eq_probe() {
    return alloc(is_qfbv_eq_probe);
}