Transitive reduction is optional.

Author: gsvgit

cfpq_add_context/add_contexts.py

@@ -29,28 +29,19 @@ def transitive_reduction(assigns, vertices_with_other_edges):
     endpoints = vertices_with_other_edges.diag(name = "endpoints") 
     assigns_transposed = Matrix(BOOL, assigns.ncols, assigns.ncols, name = "assigns_transposed")
     assigns_transposed("any") << assigns.T
-    frontier = vertices_with_other_edges.diag(name = "frontier")
-    #filter("any") << frontier
+    frontier = vertices_with_other_edges.diag(name = "frontier")    
     visited = Matrix(BOOL, assigns.ncols, assigns.ncols, name = "visited")
     visited("any") << frontier
     while True:
-        print ("Frontier nvals = ", frontier.nvals)
-        #print("Frontier: ", frontier)
+        print ("Frontier nvals = ", frontier.nvals)        
         if frontier.nvals == 0:
             break
         new_frontier = Matrix(BOOL, assigns.ncols, assigns.ncols, name = "new_frontier")        
-        new_frontier(~visited.S) << Matrix.mxm(frontier, assigns, "any_pair")
-        #print("New frontier: ", new_frontier)
-        filter = Matrix(BOOL, assigns.ncols, assigns.ncols, name = "filter")
-        #print("Endpoints: ", endpoints)
+        new_frontier(~visited.S) << Matrix.mxm(frontier, assigns, "any_pair")        
+        filter = Matrix(BOOL, assigns.ncols, assigns.ncols, name = "filter")        
         x = new_frontier.reduce_rowwise("any").diag() 
         filter(~x.S) << endpoints
 
-        #print("Filter: ", filter)        
-        #to_result = Matrix(BOOL, assigns.ncols, assigns.ncols, name = "to_result")
-        #to_result << (Matrix.mxm(new_frontier, filter, "any_pair"))
-        #print("To result: ", to_result)
-
         result("any") << (Matrix.mxm(new_frontier, filter, "any_pair"))
 
         print ("Result nvals = ", result.nvals)
@@ -59,12 +50,12 @@ def transitive_reduction(assigns, vertices_with_other_edges):
 
         new_frontier_2 = Matrix(BOOL, assigns.ncols, assigns.ncols, name = "new_frontier_2")
         new_frontier_2(~result.S) << new_frontier
-        #print("New frontier 2: ", new_frontier_2)
+        
         frontier = new_frontier_2
 
     return result
 
-def to_label_decomposed_graph(graph, automata_size, initial_graph_size):
+def to_label_decomposed_graph(graph, automata_size, initial_graph_size, do_transitive_reduction=False):
     vertex_count = graph.nrows
     alloc = Matrix(BOOL, graph.ncols, graph.nrows, name = "alloc_after_intersection")
     alloc << graph.select(graphblas.select.select_alloc)
@@ -74,11 +65,11 @@ def to_label_decomposed_graph(graph, automata_size, initial_graph_size):
     alloc_r << alloc.T
     print("Boolean matrix for alloc_r nvals: ", alloc_r.nvals)
 
-    print("mask start")
-    mask_v = Vector(BOOL, graph.ncols, name = "mask_vector")
-    ####exit_mask_v = Vector(BOOL, graph.ncols, name = "exit_mask_vector")
-    mask_v("any") << alloc.reduce_columnwise("any")
-    mask_v("any") << alloc.reduce_rowwise("any")
+    if (do_transitive_reduction):
+        print("mask start")
+        mask_v = Vector(BOOL, graph.ncols, name = "mask_vector")
+        mask_v("any") << alloc.reduce_columnwise("any")
+        mask_v("any") << alloc.reduce_rowwise("any")
 
     print("entrypoints start")
 
@@ -97,11 +88,12 @@ def to_label_decomposed_graph(graph, automata_size, initial_graph_size):
     store_i << graph.select(graphblas.select.select_store).apply(graphblas.unary.decode_store)
     print("Matrix for store_i nvals: ", store_i.nvals)
 
-    mask_v("any") << load_i.reduce_columnwise("any")
-    mask_v("any") << load_i.reduce_rowwise("any")
+    if (do_transitive_reduction):
+        mask_v("any") << load_i.reduce_columnwise("any")
+        mask_v("any") << load_i.reduce_rowwise("any")
 
-    mask_v("any") << store_i.reduce_columnwise("any")
-    mask_v("any") << store_i.reduce_rowwise("any")
+        mask_v("any") << store_i.reduce_columnwise("any")
+        mask_v("any") << store_i.reduce_rowwise("any")
 
     store_block_count = store_i.reduce_scalar("max").get(0) + 1
     load_block_count = load_i.reduce_scalar("max").get(0) + 1
@@ -136,8 +128,8 @@ def to_label_decomposed_graph(graph, automata_size, initial_graph_size):
     assign << graph.select(graphblas.select.select_assign)
     print("Boolean matrix for assign nvals: ", assign.nvals)
 
-    
-    assign << transitive_reduction(assign, mask_v)
+    if (do_transitive_reduction):
+        assign << transitive_reduction(assign, mask_v)
 
     assign_r = Matrix(BOOL, graph.ncols, graph.nrows, name = "assign_r_after_intersection")
     assign_r << assign.T
@@ -184,7 +176,7 @@ def get_new_v_id(v_id):
                                              ncols=first_free_v_id, name = "remapped_graph")
     return result
 
-def add_context(file_path, max_num_of_contexts, depth):
+def add_context(file_path, max_num_of_contexts, depth, do_transitive_reduction):
     load_graph_start = time.perf_counter()
 
     graph,number_of_contexts = load_graph(file_path, max_num_of_contexts)
@@ -216,7 +208,7 @@ def add_context(file_path, max_num_of_contexts, depth):
     print("Vertices in intersection: ", result.ncols)
     print("Edges in intersection: ", result.nvals)
 
-    decomposed_result = to_label_decomposed_graph(result, automata.nrows, graph.nrows)
+    decomposed_result = to_label_decomposed_graph(result, automata.nrows, graph.nrows, do_transitive_reduction)
     decomposition_end = time.perf_counter()
     print("Graph decomposition completed in ", decomposition_end - vertices_remapping_end)
 

cfpq_cli/run_all_pairs_cflr.py

@@ -29,13 +29,14 @@ def run_all_pairs_cflr(
         expected_path: str = "",
         max_num_of_contexts = 30,
         trace_graphblas = False,
+        do_transitive_reduction = False,
         depth=1,
 ):
     if trace_graphblas: graphblas.ss.burble.enable()
     total_start = time()
     algo = get_all_pairs_cfl_reachability_algo(algo_name)
     if add_contexts:
-        graph,initial_graph_nvertices = add_context(graph_path, max_num_of_contexts,depth)
+        graph,initial_graph_nvertices = add_context(graph_path, max_num_of_contexts, depth, do_transitive_reduction)
     else:
         graph = LabelDecomposedGraph.read_from_pocr_graph_file(graph_path)
     grammar = CnfGrammarTemplate.read_from_pocr_cnf_file(grammar_path)
@@ -108,6 +109,9 @@ def main(raw_args: List[str]):
     parser.add_argument('--trace-graphblas', dest='trace_graphblas', default=False,
                         help='Turn GraphBLAS burble on.'
                         )                        
+    parser.add_argument('--do-transitive-reduction', dest='do_transitive_reduction', default=False,
+                        help='Perform transitive reduction of ASSIGN relation before CFL-r main loop.'
+                        )                                                
     parser.add_argument('--expected_path', dest='expected_path', default="",
                         help='If specified, it will be checked wether solver\'s result is overapproximation of represented in the file.'
                         )
@@ -124,7 +128,8 @@ def main(raw_args: List[str]):
         time_limit_sec=args.time_limit,
         out_path=args.out,
         max_num_of_contexts=args.max_num_of_contexts,
-        depth = args.depth,
+        depth=args.depth,
+        do_transitive_reduction=args.do_transitive_reduction,
         settings=settings_manager.read_args(args)
     )
     settings_manager.report_unused()