z3-src 415.4.3

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

/*++
Copyright (c) 2019 Microsoft Corporation

Module Name:

    special_relations_tactic.h

Abstract:

    Detect special relations in an axiomatization, 
    rewrite goal using special relations.

Author:

    Nikolaj Bjorner (nbjorner) 2019-03-28

Notes:

--*/
#pragma once

#include "tactic/tactic.h"
#include "tactic/tactical.h"
#include "ast/special_relations_decl_plugin.h"
#include "ast/pattern/expr_pattern_match.h"

class special_relations_tactic : public tactic {
    ast_manager& m;
    params_ref m_params;
    expr_pattern_match m_pm;
    svector<sr_property> m_properties;
    
    struct sp_axioms {
        unsigned_vector m_goal_indices;
        sr_property     m_sp_features;
        sp_axioms():m_sp_features(sr_none) {}
    };

    void collect_feature(goal const& g, unsigned idx, obj_map<func_decl, sp_axioms>& goal_features);
    void insert(obj_map<func_decl, sp_axioms>& goal_features, func_decl* f, unsigned idx, sr_property p);

    void initialize();
    void register_pattern(unsigned index, sr_property);

public:

    special_relations_tactic(ast_manager & m, params_ref const & ref = params_ref()): 
        m(m), m_params(ref), m_pm(m) {}

    void updt_params(params_ref const & p) override { m_params.append(p); }
    
    void collect_param_descrs(param_descrs & r) override { }
    
    void operator()(goal_ref const & in, goal_ref_buffer & result) override;
    
    void cleanup() override {}

    tactic * translate(ast_manager & m) override { return alloc(special_relations_tactic, m, m_params); }

    char const* name() const override { return "special_relations"; }

};

tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p = params_ref());


/*
  ADD_TACTIC("special-relations", "detect and replace by special relations.", "mk_special_relations_tactic(m, p)")
*/