diff --git a/.vscode/settings.json b/.vscode/settings.json deleted file mode 100644 index 7a73a41b..00000000 --- a/.vscode/settings.json +++ /dev/null @@ -1,2 +0,0 @@ -{ -} \ No newline at end of file diff --git a/Cargo.toml b/Cargo.toml index b5f68995..143e7f24 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,4 +3,4 @@ members = [ "smt-log-parser", "axiom-profiler-GUI", -] \ No newline at end of file +] diff --git a/axiom-profiler-GUI/.cargo/config.toml b/axiom-profiler-GUI/.cargo/config.toml deleted file mode 100644 index e69de29b..00000000 diff --git a/smt-log-parser/.cargo/config.toml b/smt-log-parser/.cargo/config.toml deleted file mode 100644 index 2a3d8f84..00000000 --- a/smt-log-parser/.cargo/config.toml +++ /dev/null @@ -1 +0,0 @@ -[build] \ No newline at end of file diff --git a/smt-log-parser/Cargo.toml b/smt-log-parser/Cargo.toml index 324816d2..04faddd6 100644 --- a/smt-log-parser/Cargo.toml +++ b/smt-log-parser/Cargo.toml @@ -18,4 +18,4 @@ typed-index-collections = { version = "3.1", features = ["serde"] } fxhash = "0.2" duplicate = "1.0" gloo-console = "0.3.0" -fixedbitset = "0.4.2" +roaring = "0.10" diff --git a/smt-log-parser/src/parsers/z3/inst_graph.rs b/smt-log-parser/src/parsers/z3/inst_graph.rs index 5ef69bf9..4790df6d 100644 --- a/smt-log-parser/src/parsers/z3/inst_graph.rs +++ b/smt-log-parser/src/parsers/z3/inst_graph.rs @@ -10,7 +10,7 @@ use petgraph::{ }; use petgraph::{Direction, Graph}; use std::fmt; -use fixedbitset::FixedBitSet; +use roaring::bitmap::RoaringBitmap; use crate::items::{BlamedTermItem, InstIdx, QuantIdx, TermIdx, DepType, Dependency}; @@ -95,7 +95,7 @@ pub struct InstGraph { node_of_line_nr: FxHashMap, // line number => node-index cost_ranked_node_indices: Vec, branching_ranked_node_indices: Vec, - tr_closure: Vec, + tr_closure: Vec, } enum InstOrder { @@ -225,7 +225,7 @@ impl InstGraph { fn tr_closure_contains_edge(&self, from: NodeIndex, to: NodeIndex) -> bool { let topo_ord_from = self.orig_graph.node_weight(from).unwrap().topo_ord; let from_bitset = &self.tr_closure[topo_ord_from]; - from_bitset.contains(to.index()) + from_bitset.contains(to.index() as u32) } pub fn keep_n_most_costly(&mut self, n: usize) { @@ -625,7 +625,7 @@ impl InstGraph { } } log!("Building fixedbitsets"); - self.tr_closure = vec![FixedBitSet::with_capacity(self.orig_graph.node_count()); self.orig_graph.node_count()]; + self.tr_closure = vec![RoaringBitmap::new(); self.orig_graph.node_count()]; // note that we are storing the FixedBitSet's of each node index in topological order! log!("Computing transitive closure"); let mut topo = Topo::new(petgraph::visit::Reversed(&self.orig_graph)); @@ -634,12 +634,12 @@ impl InstGraph { while let Some((last, others)) = bitsets.split_last_mut() { if let Some(nx) = topo.next(petgraph::visit::Reversed(&self.orig_graph)) { // log!(format!("Visiting node {} with topo ord {} to compute bitset", nx.index(), ord)); - last.set(nx.index(), true); + last.insert(nx.index() as u32); for pred in self.orig_graph.neighbors_directed(nx, Incoming) { // log!(format!("Visiting predecessor {} of node {} to compute bitset", pred.index(), nx.index())); let pred_topo_ord = self.orig_graph.node_weight(pred).unwrap().topo_ord; let pred_bitset = others.get_mut(pred_topo_ord).unwrap(); - pred_bitset.union_with(last); + *pred_bitset |= &*last; // log!(format!("The bitset of pred {} with topo ord {} is {}", pred.index(), pred_topo_ord, pred_bitset)); } // log!(format!("After for loop of node {}", nx.index()));