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

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

Bug fix for reassociation pass.

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