source: icGREP/icgrep-devel/icgrep/pablo/optimizers/booleanreassociationpass.h @ 5233

Last change on this file since 5233 was 5202, checked in by nmedfort, 3 years ago

Initial work on adding types to PabloAST and mutable Var objects.

File size: 4.2 KB
Line 
1#ifndef BOOLEANREASSOCIATIONPASS_H
2#define BOOLEANREASSOCIATIONPASS_H
3
4#include <pablo/codegenstate.h>
5#include <boost/graph/adjacency_list.hpp>
6#include <boost/container/flat_map.hpp>
7#include <z3.h>
8
9namespace pablo {
10
11class BooleanReassociationPass {
12public:
13    using TypeId = PabloAST::ClassTypeId;
14    using VertexData = std::tuple<TypeId, PabloAST *, Z3_ast>;
15    using Graph = boost::adjacency_list<boost::vecS, boost::vecS, boost::bidirectionalS, VertexData, PabloAST *>;
16    using Vertex = Graph::vertex_descriptor;
17    using VertexMap = std::unordered_map<Z3_ast, Vertex>;
18    using StatementMap = boost::container::flat_map<PabloAST *, Vertex>;
19    using DistributionGraph = boost::adjacency_list<boost::hash_setS, boost::vecS, boost::bidirectionalS, Vertex>;
20
21    static bool optimize(PabloFunction & function);
22
23protected:
24
25    struct CharacterizationMap {
26        using ForwardMap = boost::container::flat_map<PabloAST *, Z3_ast>;
27        using BackwardMap = boost::container::flat_map<Z3_ast, PabloAST *>;
28        using iterator = ForwardMap::const_iterator;
29        Z3_ast add(PabloAST * const expr, Z3_ast node, const bool forwardOnly = false);
30        Z3_ast get(PabloAST * const expr) const;
31        PabloAST * findKey(Z3_ast const node) const;
32        iterator begin() const { return mForward.cbegin(); }
33        iterator end() const { return mForward.cend(); }
34        inline CharacterizationMap() : mPredecessor(nullptr) {}
35        inline CharacterizationMap(CharacterizationMap & predecessor) : mPredecessor(&predecessor) {}
36        CharacterizationMap * predecessor() const { return mPredecessor; }
37    private:
38        CharacterizationMap * const     mPredecessor;
39        ForwardMap                      mForward;
40        BackwardMap                     mBackward;
41    };
42
43protected:
44
45    BooleanReassociationPass(Z3_context ctx, Z3_params params, Z3_tactic tactic, PabloFunction & f);
46    bool processScopes(PabloFunction & function);
47    void processScopes(PabloBlock * const block, CharacterizationMap & C);
48    void distributeScope(PabloBlock * const block, CharacterizationMap & C);
49
50    Vertex transcribeSel(Sel * const stmt, CharacterizationMap & C, StatementMap & S, VertexMap & M, Graph & G);
51    void transformAST(CharacterizationMap & C, Graph & G);
52    void resolveNestedUsages(PabloAST * const expr, const Vertex u, CharacterizationMap & C, StatementMap & S, VertexMap &M, Graph & G, const Statement * const ignoreIfThis = nullptr) const;
53
54    bool contractGraph(VertexMap & M, Graph & G) const;
55
56    void reduceVertex(const Vertex u, CharacterizationMap & C, VertexMap & M, Graph & G);
57
58    bool factorGraph(TypeId typeId, Graph & G, std::vector<Vertex> & factors) const;
59    bool factorGraph(Graph & G) const;
60
61    static Vertex makeVertex(TypeId typeId, PabloAST * const expr, Graph & G, Z3_ast node = nullptr);
62    static Vertex makeVertex(TypeId typeId, PabloAST * const expr, StatementMap & M, Graph & G, Z3_ast node = nullptr);
63    static Vertex makeVertex(TypeId typeId, PabloAST * const expr, CharacterizationMap & C, StatementMap & S, VertexMap & M, Graph & G);
64
65    void removeVertex(const Vertex u, VertexMap & M, Graph & G) const;
66    void removeVertex(const Vertex u, Graph & G) const;
67
68    Z3_ast computeDefinition(TypeId typeId, const Vertex u, Graph & G, const bool use_expensive_minimization = false) const;
69    Vertex updateIntermediaryDefinition(TypeId typeId, const Vertex u, VertexMap & M, Graph & G);
70    Vertex updateSinkDefinition(TypeId typeId, const Vertex u, CharacterizationMap &C, VertexMap & M, Graph & G);
71    bool redistributeGraph(CharacterizationMap & C, VertexMap & M, Graph & G);
72
73    bool rewriteAST(Graph & G);
74
75    Statement * characterize(Statement * const stmt, CharacterizationMap & map);
76
77    Z3_ast simplify(Z3_ast node, bool use_expensive_minimization = false) const;
78
79    Z3_ast makeVar();
80
81private:
82    PabloBlock *                mBlock;
83    Z3_context const            mContext;
84    Z3_params const             mParams;
85    Z3_tactic const             mTactic;
86    Z3_ast                      mInFile;
87    std::vector<Z3_ast>         mRefs;
88    PabloFunction &             mFunction;
89    bool                        mModified;
90};
91
92}
93
94#endif // BOOLEANREASSOCIATIONPASS_H
Note: See TracBrowser for help on using the repository browser.