z3-src 503.2.2

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

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    tactic_manager.cpp

Abstract:

    Collection of tactics, simplifiers & probes

Author:

    Leonardo (leonardo) 2012-03-06

Notes:

--*/
#include "cmd_context/tactic_manager.h"
#include "tactic/tactic.h"

tactic_manager::~tactic_manager() {
    finalize_tactic_manager();
}

void tactic_manager::finalize_tactic_manager() {
    std::for_each(m_tactics.begin(), m_tactics.end(), delete_proc<tactic_cmd>());
    m_tactics.reset();
    m_name2tactic.reset();

    std::for_each(m_simplifiers.begin(), m_simplifiers.end(), delete_proc<simplifier_cmd>());
    m_simplifiers.reset();
    m_name2simplifier.reset();

    std::for_each(m_probes.begin(), m_probes.end(), delete_proc<probe_info>());
    m_probes.reset();
    m_name2probe.reset();
}

void tactic_manager::insert(tactic_cmd * c) {
    symbol const & s = c->get_name();
    SASSERT(!m_name2tactic.contains(s));
    m_name2tactic.insert(s, c);
    m_tactics.push_back(c);
}

void tactic_manager::insert(simplifier_cmd * c) {
    symbol const & s = c->get_name();
    SASSERT(!m_name2simplifier.contains(s));
    m_name2simplifier.insert(s, c);
    m_simplifiers.push_back(c);
}

void tactic_manager::insert(probe_info * p) {
    symbol const & s = p->get_name();
    SASSERT(!m_name2probe.contains(s));
    m_name2probe.insert(s, p);
    m_probes.push_back(p);
}

tactic_cmd * tactic_manager::find_tactic_cmd(symbol const & s) const {
    tactic_cmd * c = nullptr;
    m_name2tactic.find(s, c);
    return c;
}

simplifier_cmd * tactic_manager::find_simplifier_cmd(symbol const & s) const {
    simplifier_cmd * c = nullptr;
    m_name2simplifier.find(s, c);
    return c;
}

probe_info * tactic_manager::find_probe(symbol const & s) const {
    probe_info * p = nullptr;
    m_name2probe.find(s, p);
    return p;
}

void install_tactics(tactic_manager & ctx) {
    for (auto * r = tactic_registration::g_head; r; r = r->next)
        ctx.insert(alloc(tactic_cmd, symbol(r->name), r->descr, r->factory));
    for (auto * r = probe_registration::g_head; r; r = r->next)
        ctx.insert(alloc(probe_info, symbol(r->name), r->descr, r->factory()));
    for (auto * r = simplifier_registration::g_head; r; r = r->next)
        ctx.insert(alloc(simplifier_cmd, symbol(r->name), r->descr, r->factory));
}