graphiti: Add checkbox for sporadic equations (#532)

I noticed that sometimes graphiti can generate spurious vertices for sporadic equations. Add a checkbox to allow displaying them, otherwise explicitly filter them (in the correct way.) Also, clean-up the generate graph script and trivially optimize the closure computation.
teorth · Oct 12, 2024 · ce75901 · ce75901
1 parent 11c6ed9
commit ce75901
Show file tree

Hide file tree

Showing 3 changed files with 49 additions and 29 deletions.
diff --git a/home_page/graphiti/index.html b/home_page/graphiti/index.html
@@ -149,6 +149,17 @@
           >
         </div>
 
+        <div class="checkbox-container">
+          <input
+            type="checkbox"
+            id="show_sporadic_equations"
+            name="show_sporadic_equations"
+          />
+          <label for="show_sporadic_equations"
+            >Show sporadic equations (Equations numbered > 4694)</label
+          >
+        </div>
+
         <button type="submit">Submit</button>
       </form>
 
@@ -532,10 +543,14 @@ <h1 id="message"></h1>
 
         let vertices_to_delete = new Set();
 
-        // These mess up rendering now with the unknowns, get rid of them.
-        vertices_to_delete.add(5105)
-        vertices_to_delete.add(28393)
-        vertices_to_delete.add(374794)
+        if (params.show_sporadic_equations != "on") {
+          for (const key of Object.keys(graph_json.node_to_scc_map)) {
+            let eq_num = parseInt(key, 10);
+            if (eq_num > 4694) {
+              vertices_to_delete.add(eq_num);
+            }
+          }
+        }
 
         if (params.max_variables) {
           max_var = Number(params.max_variables);
@@ -691,13 +706,17 @@ <h1 id="message"></h1>
           dotFile += `]\n`;
         }
 
+        let implication_edges = 0;
         for (const [v, neighbors] of Object.entries(reduced_graph)) {
           for (const n of neighbors) {
             dotFile += `  ${v} -> ${n} [arrowhead="none"]\n`;
+            implication_edges += 1;
           }
         }
+        console.log(`Implication edge count: ${implication_edges}`);
 
         if (params.show_unknowns_conjectures == "on") {
+          let unknown_edges = 0;
           for (const scc_name of Object.keys(scc_to_node_map)) {
             if (!graph_json.unknowns[scc_name]) {
               continue;
@@ -707,9 +726,10 @@ <h1 id="message"></h1>
               .filter((x) => x in scc_to_node_map)
               .forEach((x) => {
                 dotFile += `  ${scc_name} -> ${x} [style="dotted",constraint=false]\n`;
+                unknown_edges += 1;
               });
-
           }
+          console.log(`Unknown edge count: ${unknown_edges}`);
         }
 
         dotFile += "}";

diff --git a/scripts/generate_graphiti_data.rb b/scripts/generate_graphiti_data.rb
@@ -31,37 +31,39 @@
   end
 }
 
-implications_graph = Graph.from_json(ARGV[0])
+implications_graph = Graph.from_json_array(JSON.parse(File.read(ARGV[0]))["implications"])
 condensed_graph, node_to_scc_map, scc_to_node_map = implications_graph.condensation
 
 condensed_closure = condensed_graph.transitive_closure
 
-condensed = {}
-condensed_closure.adj_list.each { |k, v| condensed[k] = v.to_a }
+unknowns = Graph.new
+Graph.from_json_array(JSON.parse(File.read(ARGV[1]))).adj_list.each { |v1, list|
+  list.each { |v2|
+    v1_scc = node_to_scc_map[v1]
+    v2_scc = node_to_scc_map[v2]
 
-unknowns = {}
-JSON.parse(File.read(ARGV[1])).each { |unknown|
-  unknown_lhs_eq = unknown["lhs"][8, unknown["lhs"].length].to_i
-  unknown_rhs_eq = unknown["rhs"][8, unknown["rhs"].length].to_i
+    if !v1_scc || !v2_scc
+      $stderr.puts "Unknown LHS/RHS mapping to SCC"
+      exit 1
+    end
 
-  unknown_lhs_scc = node_to_scc_map[unknown_lhs_eq]
-  unknown_rhs_scc = node_to_scc_map[unknown_rhs_eq]
+    unknowns.add_edge(v1_scc, v2_scc)
+  }
+}
 
-  if !unknown_lhs_scc || !unknown_rhs_scc
-    $stderr.puts "Unknown LHS/RHS mapping to SCC"
-    exit 1
-  end
+def graph2map(g)
+  out = {}
+  g.adj_list.each { |k, v| out[k] = v.to_a }
 
-  unknowns[unknown_lhs_scc] ||= []
-  unknowns[unknown_lhs_scc] << unknown_rhs_scc
-}
+  out
+end
 
 puts JSON.generate({
   "timestamp" => Time.now.utc.to_i,
   "commit_hash" => `git rev-parse HEAD`.chomp,
-  "condensed_graph" => condensed,
+  "condensed_graph" => graph2map(condensed_closure),
   "scc_to_node_map" => scc_to_node_map,
   "node_to_scc_map" => node_to_scc_map,
   "equations" => equations,
-  "unknowns" => unknowns
+  "unknowns" => graph2map(unknowns)
 })
diff --git a/scripts/graph.rb b/scripts/graph.rb
@@ -1,4 +1,3 @@
-require 'json'
 require 'set'
 
 class Graph
@@ -25,11 +24,10 @@ def self.from_csv(path)
     graph
   end
 
-  def self.from_json(path)
+  def self.from_json_array(arr)
     graph = Graph.new
-    JSON.parse(File.read(path))["implications"].each { |e|
+    arr.each { |e|
       lhs_eq, rhs_eq = e["lhs"], e["rhs"]
-
       graph.add_edge(lhs_eq[8, lhs_eq.length].to_i, rhs_eq[8, rhs_eq.length].to_i)
     }
 
@@ -233,9 +231,9 @@ def transitive_closure
     closure_graph = Graph.new
     vertices.each do |vertex|
       visited = Hash.new(false)
-      reachable = []
+      reachable = Set.new []
       closure_dfs(vertex, visited, reachable)
-      closure_graph.adj_list[vertex] = Set.new reachable
+      closure_graph.adj_list[vertex] = reachable
     end
     closure_graph
   end