Graphiti
How to build
The following commands should successfully build the project.
# Setup the mathlib 4 cache
make setup
# Build Graphiti
lake build
The executable graphiti
can be built using the following, which requires an installation of rust
and
cargo
to install the oracle which is used for the rewrites.
make build-exe
The oracle will be installed under ./bin/graphiti_oracle
.
Executing the rewriter
Graphiti can be executed using:
lake exe graphiti --oracle ./bin/graphiti_oracle ./benchmarks/correct/gcd.dot -o out.dot -l out.json --no-dynamatic-dot
$ lake exe graphiti --help
graphiti -- v0.1.0
FORMAT
graphiti [OPTIONS...] FILE
OPTIONS
-h, --help Print this help text
-o, --output FILE Set output file
-l, --log FILE Set JSON log output
--log-stdout Set JSON log output to STDOUT
--no-dynamatic-dot Don't output dynamatic DOT, instead output the raw
dot that is easier for debugging purposes.
--parse-only Only parse the input without performing rewrites.
It will read a DOT graph from the input FILE, and then rewrite it using the internal rewrites. It will then print it as a dynamatic dot graph to the output.
The rewrites that were performed can be traced using the output JSON log file. This log file outputs data in the following format:
// List of objects, each representing a rewrite.
[
{
// name of the rewrite
"name": "combine-mux",
// type of rewrite, one of rewrite, abstraction or concretisation
"type": "Graphiti.RewriteType.rewrite",
// input dot graph that was received by the rewrite
"input_graph": "digraph { ... }",
// output dot graph that was produced by the rewrite
"output_graph": "digraph { ... }",
// a list of nodes making up the subgraph that was matched
"matched_subgraph": ["node1", "node2"],
// nodes that were untouched but renamed when going from input to output
// a null value means the node was removed
"renamed_input_nodes": {"a": "b", "c": "d", "e": null},
// name of nodes that were added to the output
"new_output_nodes": ["x", "y", "z"],
// optional debug information
"debug": null
},
{ "...": "..." }
]