Small improvements (#98)

* Small improvements

* fmt

axiom-profiler-GUI/assets/html/style.css

@@ -437,6 +437,7 @@ ul.selected-info {
 .dot {
     display: inline-block;
     position: relative;
+    overflow-x: auto;
 }
 .dot.scaled {
     width: 100%;

axiom-profiler-GUI/src/screen/homepage/file.rs

@@ -294,7 +294,7 @@ impl Homepage {
         let stop_loading = self.stop_loading.clone();
         let link = link.clone();
 
-        log::trace!("Selected file \"{}\"", file_info.name);
+        log::debug!("Selected file \"{}\"", file_info.name);
         // Turn into stream
         let blob: &web_sys::Blob = file.as_ref();
         let stream = ReadableStream::from_raw(blob.stream().unchecked_into());
@@ -307,7 +307,7 @@ impl Homepage {
                 });
             }
             Err((_err, _stream)) => {
-                log::trace!("Loading to string \"{}\"", file_info.name);
+                log::debug!("Loading to string \"{}\"", file_info.name);
                 link.send_message(HomepageM::LoadingState(LoadingState::ReadingToString));
                 let reader = gloo::file::callbacks::read_as_text(&file, move |res| {
                     let text_data = match res {
@@ -320,7 +320,7 @@ impl Homepage {
                     let remaining_memory =
                         Self::BROWSER_MEM_LIMIT - text_data.len() - 64 * 1024 * 1024;
 
-                    log::trace!("Parsing \"{}\"", file_info.name);
+                    log::debug!("Parsing \"{}\"", file_info.name);
                     link.send_message(HomepageM::LoadingState(LoadingState::StartParsing));
                     wasm_bindgen_futures::spawn_local(async move {
                         let parser = Z3Parser::from_str(&text_data);

axiom-profiler-GUI/src/screen/homepage/mod.rs

@@ -184,7 +184,7 @@ impl Screen for Homepage {
                 self.load_example(example, response, link)
             }
             HomepageM::LoadingState(mut state) => {
-                log::trace!("New state \"{state:?}\"");
+                log::debug!("New state \"{state:?}\"");
                 if let (LoadingState::Parsing(parsing, _), LoadingState::Parsing(old, _)) =
                     (&mut state, &self.progress)
                 {

axiom-profiler-GUI/src/screen/inst_graph/render/mod.rs

@@ -46,7 +46,7 @@ impl Graph {
 
         for (can_select, idx, filter) in cmd.filters() {
             let output = filter.apply(graph, parser);
-            log::trace!("Applied filter {filter:?} -> {output:?}");
+            log::debug!("Applied filter {filter:?} -> {output:?}");
 
             modified |= output.modified;
             if !output.modified {
@@ -125,7 +125,7 @@ impl Graph {
         let (selected_nodes, selected_edges) = self.update_selected(&visible);
         let dimensions = GraphDimensions::of_graph(&visible);
 
-        log::trace!("Rendering graph with {dimensions:?}");
+        log::debug!("Rendering graph with {dimensions:?}");
         let new_permissions = dimensions.max(Self::default_permissions());
         self.filter.chain.set_permissions(new_permissions);
 
@@ -201,7 +201,7 @@ impl Graph {
                 },
             )
         );
-        // log::trace!("Graph DOT:\n{dot_output}");
+        // log::debug!("Graph DOT:\n{dot_output}");
         self.state = Ok(GraphState::RenderingGraph);
         let link = link.clone();
         wasm_bindgen_futures::spawn_local(async move {
@@ -219,7 +219,7 @@ impl Graph {
                 }
             };
             let elapsed = start.elapsed();
-            log::trace!(
+            log::debug!(
                 "Graph: Converting dot-String to SVG took {} seconds",
                 elapsed.as_secs()
             );

axiom-profiler-GUI/src/screen/ml/render.rs

@@ -52,7 +52,7 @@ pub fn MlgRenderer(props: &MlgrProps) -> Html {
     };
     ctxt.config.font_tag = true;
     let dot = MlgRenderer::generate_dot(graph, ctxt, &props.parser.colour_map);
-    log::trace!("ML Graph DOT:\n{dot}");
+    log::debug!("ML Graph DOT:\n{dot}");
 
     let warning = if graph.graph_incomplete {
         html! { <span class="warning" title="Error during graph construction, the graph is incomplete!">{"⚠️ Incomplete ⚠️"}</span> }
@@ -119,7 +119,7 @@ impl MlgRenderer {
         let cluster_fixed = cluster("fixed", "gray96", fixeds.join(join));
         let cluster_out = cluster("out", "aliceblue", outputs.join(join));
         format!(
-            "digraph {{{join}{}{join}{cluster_in}{join}{cluster_fixed}{join}{cluster_out}{join}{}\n}}",
+            "digraph {{{join}{}{join}{cluster_in}{join}{cluster_fixed}{join}{cluster_out}\n{}\n}}",
             settings.join(join),
             outside.join("\n"),
         )

axiom-profiler-GUI/src/utils/graphviz.rs

@@ -35,7 +35,7 @@ pub fn Dot(props: &DotProps) -> Html {
                     return;
                 }
             };
-            log::trace!(
+            log::debug!(
                 "Converting dot-String to SVG took {}ms",
                 elapsed.as_millis()
             );

smt-log-parser/src/cmd/args.rs

@@ -38,6 +38,9 @@ pub enum Commands {
         /// The maximum time to spend parsing each file (in seconds)
         #[arg(short, long, default_value_t = 15.0)]
         timeout: f32,
+        /// Whether to print out memory usage information
+        #[arg(short, long, default_value_t = false)]
+        memory: bool,
     },
     /// Try to reconstruct the `.smt2` file
     Reconstruct {

smt-log-parser/src/cmd/mod.rs

@@ -17,7 +17,11 @@ pub fn run() -> Result<(), String> {
             pretty_print,
         } => dependencies::run(logfile, depth, pretty_print)?,
         args::Commands::Stats { logfile, k } => stats::run(logfile, k)?,
-        args::Commands::Test { logfiles, timeout } => test::run(logfiles, timeout)?,
+        args::Commands::Test {
+            logfiles,
+            timeout,
+            memory,
+        } => test::run(logfiles, timeout, memory)?,
         args::Commands::Reconstruct { logfile, clean } => reconstruct::run(logfile, clean)?,
     }
 

smt-log-parser/src/cmd/test.rs

@@ -9,20 +9,20 @@ use wasm_timer::Instant;
 
 const MB: u64 = 1024_u64 * 1024_u64;
 
-pub fn run(logfiles: Vec<PathBuf>, timeout: f32) -> Result<(), String> {
+pub fn run(logfiles: Vec<PathBuf>, timeout: f32, memory: bool) -> Result<(), String> {
     for path in logfiles {
         let builder = std::thread::Builder::new().stack_size(8 * MB as usize);
         let t = builder
             .spawn(move || {
-                run_file(path, timeout);
+                run_file(path, timeout, memory);
             })
             .unwrap();
         t.join().unwrap();
     }
     Ok(())
 }
 
-fn run_file(path: PathBuf, timeout: f32) {
+fn run_file(path: PathBuf, timeout: f32, memory: bool) {
     let path = std::path::Path::new(&path);
     let filename = path
         .file_name()
@@ -42,8 +42,10 @@ fn run_file(path: PathBuf, timeout: f32) {
     let (_metadata, parser) = Z3Parser::from_file(path).unwrap();
     let (timeout, mut result) = parser.process_all_timeout(to);
     let elapsed_time = time.elapsed();
-    #[cfg(feature = "mem_dbg")]
-    result.mem_dbg(DbgFlags::default()).ok();
+    if memory {
+        #[cfg(feature = "mem_dbg")]
+        result.mem_dbg(DbgFlags::default()).ok();
+    }
     println!(
         "{} parsing after {} seconds (timeout {timeout:?})",
         if timeout.is_timeout() {
@@ -65,8 +67,10 @@ fn run_file(path: PathBuf, timeout: f32) {
             .unwrap()
             .map(|q| result[q.quant].kind.debug(&result))
             .collect();
-        #[cfg(feature = "mem_dbg")]
-        inst_graph.mem_dbg(DbgFlags::default()).ok();
+        if memory {
+            #[cfg(feature = "mem_dbg")]
+            inst_graph.mem_dbg(DbgFlags::default()).ok();
+        }
         println!(
             "Finished analysing after {} seconds. Found {sure_mls} sure mls, {maybe_mls} maybe mls. Quants involved {quants_involved:?}",
             (process_time - elapsed_time).as_secs_f32(),