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

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

Work on a Z3 based reassociation pass.

File size: 3.6 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    private:
36        CharacterizationMap * const     mPredecessor;
37        ForwardMap                      mForward;
38        BackwardMap                     mBackward;
39    };
40
41protected:
42
43    BooleanReassociationPass(Z3_context ctx, Z3_solver solver, PabloFunction & f);
44    bool processScopes(PabloFunction & function);
45    void processScopes(PabloBlock * const block, CharacterizationMap & map);
46    void distributeScope(PabloBlock * const block, CharacterizationMap & map);
47
48    void transformAST(PabloBlock * const block, CharacterizationMap & C, Graph & G);
49    void resolveNestedUsages(PabloBlock * const block, PabloAST * const expr, const Vertex u, CharacterizationMap &C, StatementMap & S, Graph & G, const Statement * const ignoreIfThis = nullptr) const;
50
51    bool contractGraph(StatementMap & M, Graph & G) const;
52
53    bool reduceGraph(CharacterizationMap & C, StatementMap & S, Graph & G) const;
54
55    bool factorGraph(const PabloAST::ClassTypeId typeId, Graph & G, std::vector<Vertex> & factors) const;
56    bool factorGraph(Graph & G) const;
57
58    static Vertex makeVertex(const PabloAST::ClassTypeId typeId, PabloAST * const expr, Graph & G, Z3_ast node = nullptr);
59    static Vertex makeVertex(const PabloAST::ClassTypeId typeId, PabloAST * const expr, StatementMap & M, Graph & G, Z3_ast node = nullptr);
60    static Vertex makeVertex(const PabloAST::ClassTypeId typeId, PabloAST * const expr, CharacterizationMap & C, StatementMap & M, Graph & G);
61    void removeVertex(const Vertex u, StatementMap & M, Graph & G) const;
62    void removeVertex(const Vertex u, Graph & G) const;
63
64    bool redistributeGraph(CharacterizationMap & C, StatementMap & M, Graph & G) const;
65
66    void rewriteAST(PabloBlock * const block, Graph & G);
67
68    Statement * characterize(Statement * const stmt, CharacterizationMap & map);
69
70    Z3_ast makeVar() const;
71
72private:
73    Z3_context const            mContext;
74    Z3_solver const             mSolver;
75    Z3_ast                      mInFile;
76    PabloFunction &             mFunction;
77    bool                        mModified;
78};
79
80}
81
82#endif // BOOLEANREASSOCIATIONPASS_H
Note: See TracBrowser for help on using the repository browser.