1 /*++
2 Copyright (c) 2017 Microsoft Corporation
3
4 Module Name:
5
6 dependency_converter.cpp
7
8 Abstract:
9
10 Utility for converting dependencies across subgoals.
11
12 Author:
13
14 Nikolaj Bjorner (nbjorner) 2017-11-19
15
16 Notes:
17
18
19 --*/
20
21 #include "tactic/dependency_converter.h"
22 #include "tactic/goal.h"
23
24 class unit_dependency_converter : public dependency_converter {
25 expr_dependency_ref m_dep;
26 public:
27
unit_dependency_converter(expr_dependency_ref & d)28 unit_dependency_converter(expr_dependency_ref& d) : m_dep(d) {}
29
operator ()()30 expr_dependency_ref operator()() override { return m_dep; }
31
translate(ast_translation & translator)32 dependency_converter * translate(ast_translation & translator) override {
33 expr_dependency_translation tr(translator);
34 expr_dependency_ref d(tr(m_dep), translator.to());
35 return alloc(unit_dependency_converter, d);
36 }
37
display(std::ostream & out)38 void display(std::ostream& out) override {
39 out << m_dep.get() << "\n";
40 }
41 };
42
43 class concat_dependency_converter : public dependency_converter {
44 dependency_converter_ref m_dc1;
45 dependency_converter_ref m_dc2;
46 public:
47
concat_dependency_converter(dependency_converter * c1,dependency_converter * c2)48 concat_dependency_converter(dependency_converter* c1, dependency_converter* c2) : m_dc1(c1), m_dc2(c2) {}
49
operator ()()50 expr_dependency_ref operator()() override {
51 expr_dependency_ref d1 = (*m_dc1)();
52 expr_dependency_ref d2 = (*m_dc2)();
53 ast_manager& m = d1.get_manager();
54 return expr_dependency_ref(m.mk_join(d1, d2), m);
55 }
56
translate(ast_translation & translator)57 dependency_converter * translate(ast_translation & translator) override {
58 return alloc(concat_dependency_converter, m_dc1->translate(translator), m_dc2->translate(translator));
59 }
60
display(std::ostream & out)61 void display(std::ostream& out) override {
62 m_dc1->display(out);
63 m_dc2->display(out);
64 }
65 };
66
67 class goal_dependency_converter : public dependency_converter {
68 ast_manager& m;
69 goal_ref_buffer m_goals;
70 public:
goal_dependency_converter(unsigned n,goal * const * goals)71 goal_dependency_converter(unsigned n, goal * const* goals) :
72 m(goals[0]->m()) {
73 for (unsigned i = 0; i < n; ++i) m_goals.push_back(goals[i]);
74 }
75
operator ()()76 expr_dependency_ref operator()() override {
77 expr_dependency_ref result(m.mk_empty_dependencies(), m);
78 for (goal_ref g : m_goals) {
79 dependency_converter_ref dc = g->dc();
80 if (dc) result = m.mk_join(result, (*dc)());
81 }
82 return result;
83 }
translate(ast_translation & translator)84 dependency_converter * translate(ast_translation & translator) override {
85 goal_ref_buffer goals;
86 for (goal_ref g : m_goals) goals.push_back(g->translate(translator));
87 return alloc(goal_dependency_converter, goals.size(), goals.data());
88 }
89
display(std::ostream & out)90 void display(std::ostream& out) override { out << "goal-dep\n"; }
91
92 };
93
concat(dependency_converter * mc1,dependency_converter * mc2)94 dependency_converter * dependency_converter::concat(dependency_converter * mc1, dependency_converter * mc2) {
95 if (!mc1) return mc2;
96 if (!mc2) return mc1;
97 return alloc(concat_dependency_converter, mc1, mc2);
98 }
99
unit(expr_dependency_ref & d)100 dependency_converter* dependency_converter::unit(expr_dependency_ref& d) {
101 return alloc(unit_dependency_converter, d);
102 }
103
concat(unsigned n,goal * const * goals)104 dependency_converter * dependency_converter::concat(unsigned n, goal * const* goals) {
105 if (n == 0) return nullptr;
106 return alloc(goal_dependency_converter, n, goals);
107 }
108