Add enode blame asserted

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

@@ -41,9 +41,6 @@ html {
     -ms-user-select: none;
     user-select: none;
 }
-.margin-left-half {
-    margin-left: 0.5em;
-}
 
 div.page .full-page {
     position: absolute;
@@ -55,6 +52,7 @@ div.page .full-page {
 
 div.page .overlay {
     background-color: #fff;
+    z-index: 10;
 }
 div.page .overlay .close-button {
     position: absolute;
@@ -397,8 +395,13 @@ li input.td-matcher, li input.td-formatter {
     padding-inline-start: 20px;
 }
 
+.expand-collapse {
+    cursor: pointer;
+}
+
 .quant-graph {
     max-height: 400px;
+    margin: 5px;
 }
 
 /* Graph view */

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

@@ -47,13 +47,11 @@ pub fn Summary(props: &SummaryProps) -> Html {
     let cfg = use_context::<Rc<ConfigurationProvider>>().unwrap();
     let term_display = use_context::<Rc<TermDisplayContext>>().unwrap();
 
-    let mut config = cfg.config.display;
-    config.ast_depth_limit = NonMaxU32::new(3);
     let inner = SummaryPropsInner {
         parser: props.parser.clone(),
         analysis: props.analysis.clone(),
         term_display: term_display.clone(),
-        config,
+        config: cfg.config.display,
     };
 
     let graph = props.analysis.clone().map(|analysis| {
@@ -66,13 +64,14 @@ pub fn Summary(props: &SummaryProps) -> Html {
     });
 
     html! {<div class="summary">
-        <DetailContainer>
+        <article class="pf-content"><DetailContainer>
             <Metrics ..inner.clone() />
             <MostQuants ..inner.clone() />
             <CostQuants ..inner.clone() />
-            <CostProofs ..inner.clone() />
+        </DetailContainer><DetailContainer>
+            <CostLemmas ..inner.clone() />
             <CostCdcl ..inner />
-        </DetailContainer>
+        </DetailContainer></article>
         {graph}
     </div>}
 }
@@ -178,34 +177,30 @@ pub fn CostQuants(props: &SummaryPropsInner) -> Html {
 }
 
 #[function_component]
-pub fn CostProofs(props: &SummaryPropsInner) -> Html {
+pub fn CostLemmas(props: &SummaryPropsInner) -> Html {
     props.analysis.as_ref().map(|analysis| {
         let parser = props.parser.parser.borrow();
         let analysis = analysis.borrow();
-        let ctxt = props.ctxt(&parser);
-        let proofs = analysis.proofs.hypothesis_cost.iter().take(DISPLAY_TOP_N);
-        let proofs = proofs.map(|&(p, c)| {
-            let p = format!("<code class=\"margin-left-half\">{}</code>", parser[p].result.with(&ctxt));
-            let right = Html::from_html_unchecked(p.into());
+        let lemmas = analysis.proofs.lemmas_cost.iter().take(DISPLAY_TOP_N);
+        let lemmas = lemmas.map(|&(l, c)| {
             let left = format_to_html(c as u64);
+            let right = collapsed_expanded(l, props.ctxt(&parser));
             (left, right)
         }).collect::<Vec<_>>();
-        html! {<Detail title="Most expensive hypotheses" hover="The hypotheses which were the most expensive to contradict." tip="Try providing their negation directly.">
-            <TreeList elements={proofs} />
+        html! {<Detail title="Most expensive lemmas" hover="The lemmas which were the most expensive to prove (by contradiction)." tip="Try providing them directly.">
+            <TreeList elements={lemmas} />
         </Detail>}
     }).unwrap_or_default()
 }
 
 #[function_component]
 pub fn CostCdcl(props: &SummaryPropsInner) -> Html {
     let parser = props.parser.parser.borrow();
-    let ctxt = props.ctxt(&parser);
     let cdcl = props.parser.cdcl.uncut_assigns.iter().take(DISPLAY_TOP_N);
     let cdcl = cdcl
         .map(|&(p, c)| {
-            let p = format!("<code class=\"margin-left-half\">{}</code>", p.with(&ctxt));
-            let right = Html::from_html_unchecked(p.into());
             let left = format_to_html(c);
+            let right = collapsed_expanded(p, props.ctxt(&parser));
             (left, right)
         })
         .collect::<Vec<_>>();
@@ -238,3 +233,48 @@ fn quants_ordered<'a, T: Ord + Copy + Debug, const REVERSE: bool>(
     }
     quants
 }
+
+fn collapsed_expanded<'a, D: Default>(
+    display: impl DisplayWithCtxt<DisplayCtxt<'a>, D> + Copy,
+    mut ctxt: DisplayCtxt<'a>,
+) -> Html {
+    let expanded = format!("<code>{}</code>", display.with(&ctxt));
+    ctxt.config.ast_depth_limit = NonMaxU32::new(2);
+    let collapsed = format!("<code>{}</code>", display.with(&ctxt));
+    if expanded == collapsed {
+        Html::from_html_unchecked(expanded.into())
+    } else {
+        let expanded = Html::from_html_unchecked(expanded.into());
+        let collapsed = Html::from_html_unchecked(collapsed.into());
+        html! {<ExpandOnFocus {collapsed} {expanded} />}
+    }
+}
+
+#[derive(Properties, Clone, PartialEq)]
+pub struct EofProps {
+    pub collapsed: Html,
+    pub expanded: Html,
+}
+
+#[function_component]
+pub fn ExpandOnFocus(props: &EofProps) -> Html {
+    let focused = use_state_eq(|| false);
+    let f = *focused;
+    let focused_ref = focused.clone();
+    let onblur = Callback::from(move |_| focused_ref.set(false));
+
+    let moved = use_mut_ref(|| false);
+    let moved_ref = moved.clone();
+    let onmousedown = Callback::from(move |_| *moved_ref.borrow_mut() = false);
+    let moved_ref = moved.clone();
+    let onmousemove = Callback::from(move |_| *moved_ref.borrow_mut() = true);
+    let (focused_ref, moved_ref) = (focused, moved);
+    let onmouseup = Callback::from(move |_| {
+        if !*moved_ref.borrow() {
+            focused_ref.set(!f)
+        }
+    });
+    html! {<div tabindex="0" class="expand-collapse" {onmousedown} {onmousemove} {onmouseup} {onblur}>
+        {if f { props.expanded.clone() } else { props.collapsed.clone() }}
+    </div>}
+}

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

@@ -180,8 +180,8 @@ impl
         match *self {
             Instantiation(inst) => match &parser[parser[inst].match_].kind {
                 MatchKind::TheorySolving { axiom_id, .. } => {
-                    let namespace = &parser[axiom_id.namespace];
-                    let id = axiom_id.id.map(|id| format!("[{id}]")).unwrap_or_default();
+                    let (namespace, id) = axiom_id.to_string_components(&parser.strings);
+                    let id = id.map(|id| format!("[{id}]")).unwrap_or_default();
                     format!("{namespace}{id}")
                 }
                 MatchKind::MBQI { quant, .. }

axiom-profiler-GUI/src/screen/inst_graph/display/node_info.rs

@@ -232,7 +232,7 @@ impl<'a, 'b> NodeInfo<'a, 'b> {
             .node
             .kind()
             .inst()
-            .and_then(|i| self.ctxt.parser[i].z3_generation)
+            .and_then(|i| self.ctxt.parser[i].kind.z3_generation())
         {
             extra_info.push(("z3 gen", z3gen.to_string()));
         }
@@ -405,6 +405,7 @@ impl<'a, 'b> EdgeInfo<'a, 'b> {
         use VisibleEdgeKind::*;
         match self.kind {
             Direct(_, EdgeKind::Yield) => "Yield".to_string(),
+            Direct(_, EdgeKind::Asserted) => "Asserted".to_string(),
             Direct(_, EdgeKind::Blame { pattern_term }) => {
                 format!("Blame pattern #{pattern_term}")
             }

axiom-profiler-GUI/src/screen/inst_graph/mode.rs

@@ -25,7 +25,7 @@ impl GraphMode {
                 true
             }
             (Self::Inst, _) => false,
-            (Self::Proof, Instantiation(..) | Proof(..)) => true,
+            (Self::Proof, Instantiation(..) | ENode(..) | Proof(..)) => true,
             (Self::Proof, _) => false,
             (Self::Cdcl, Cdcl(..)) => true,
             (Self::Cdcl, _) => false,

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

@@ -58,9 +58,9 @@ pub struct DetailContainerProps {
 
 #[function_component]
 pub fn DetailContainer(props: &DetailContainerProps) -> Html {
-    html! {<article class="pf-content"><div class="pf-grid-layout">
+    html! {<div class="pf-grid-layout">
         {props.children.clone()}
-    </div></article>}
+    </div>}
 }
 
 // Tree

smt-log-parser/src/analysis/dependencies.rs

@@ -65,7 +65,7 @@ impl QuantifierAnalysis {
                 }
                 let direct_dep = &mut qinfo.direct_deps[i];
 
-                let created_by = parser[blame.enode()].created_by;
+                let created_by = parser[blame.enode()].blame.inst();
                 let created_by =
                     created_by.and_then(|iidx| parser.get_inst(iidx).match_.kind.quant_idx());
                 *direct_dep.enode.entry(created_by).or_default() += 1;

smt-log-parser/src/analysis/graph/analysis/cost.rs

@@ -89,16 +89,16 @@ impl CostInitialiser for DefaultCost {
     }
     fn transfer(
         &mut self,
-        node: &Node,
+        child: &Node,
         _from_idx: RawNodeIndex,
-        idx: usize,
-        incoming: &[Self::Observed],
+        parent_idx: usize,
+        parents: &[Self::Observed],
     ) -> f64 {
-        let total = incoming.iter().sum::<usize>();
-        if total == 0 {
+        let total = parents.iter().sum::<usize>();
+        if total == 0 || child.kind().proof().is_some() {
             return 0.0;
         }
-        node.cost * incoming[idx] as f64 / total as f64
+        child.cost * parents[parent_idx] as f64 / total as f64
     }
 }
 
@@ -127,17 +127,17 @@ impl CostInitialiser<true> for ProofCost {
         &mut self,
         node: &Node,
         _from_idx: RawNodeIndex,
-        idx: usize,
-        incoming: &[Self::Observed],
+        child_idx: usize,
+        children: &[Self::Observed],
     ) -> f64 {
         if node.kind().proof().is_none() {
             return 0.0;
         }
 
-        let total = incoming.iter().sum::<usize>();
+        let total = children.iter().sum::<usize>();
         if total == 0 {
             return 0.0;
         }
-        node.cost * incoming[idx] as f64 / total as f64
+        node.cost * children[child_idx] as f64 / total as f64
     }
 }

smt-log-parser/src/analysis/graph/analysis/matching_loop/explain.rs

@@ -334,7 +334,7 @@ impl MlExplainer {
 
     fn add_enode(&mut self, parser: &Z3Parser, enode: ENodeIdx, result_enode: NodeIndex) -> bool {
         let enode_data = &parser[enode];
-        let created_by = enode_data.created_by;
+        let created_by = enode_data.blame.inst();
         let created_by = created_by.and_then(|cb| self.instantiations.get(&cb));
         if let Some(created_by) = created_by {
             self.graph
@@ -375,7 +375,7 @@ impl MlExplainer {
                 let eq_expl = &self.equalities().given[eq];
                 match eq_expl {
                     &EqualityExpl::Literal { eq, .. } => {
-                        let created_by = self.parser[eq].created_by;
+                        let created_by = self.parser[eq].blame.inst();
                         let created_by =
                             created_by.and_then(|iidx| self.explainer.instantiations.get(&iidx));
                         if let Some(created_by) = created_by {

smt-log-parser/src/analysis/graph/analysis/matching_loop/signature.rs

@@ -52,7 +52,7 @@ impl MlSignature {
                 let eq_len = blame.equalities().count();
                 let blame = blame.enode();
                 let eblame = &parser[blame];
-                let Some(created_by) = eblame.created_by else {
+                let Some(created_by) = eblame.blame.inst() else {
                     return (InstParent::Const(blame), eq_len);
                 };
                 match parser[parser[created_by].match_].kind.quant_idx() {

smt-log-parser/src/analysis/graph/raw.rs

@@ -15,8 +15,8 @@ use petgraph::{
 use crate::{
     graph_idx,
     items::{
-        CdclIdx, ENodeIdx, EqGivenIdx, EqTransIdx, EqualityExpl, GraphIdx, InstIdx, ProofIdx,
-        StackIdx, TransitiveExplSegmentKind,
+        CdclIdx, ENodeBlame, ENodeIdx, EqGivenIdx, EqTransIdx, EqualityExpl, GraphIdx, InstIdx,
+        ProofIdx, StackIdx, TransitiveExplSegmentKind,
     },
     DiGraph, FxHashMap, FxHashSet, NonMaxU32, Result, Z3Parser,
 };
@@ -101,11 +101,8 @@ impl RawInstGraph {
             stats,
         };
 
-        // Add instantiation blamed and yield edges
+        // Add instantiation blamed edges
         for (idx, inst) in parser.insts.insts.iter_enumerated() {
-            for yields in inst.yields_terms.iter() {
-                self_.add_edge(idx, *yields, EdgeKind::Yield);
-            }
             for (i, blame) in parser.insts.matches[inst.match_]
                 .pattern_matches()
                 .enumerate()
@@ -125,6 +122,15 @@ impl RawInstGraph {
             }
         }
 
+        // Add enode blamed edges
+        for (idx, enode) in parser.egraph.enodes.iter_enumerated() {
+            match enode.blame {
+                ENodeBlame::Inst(iidx) => self_.add_edge(iidx, idx, EdgeKind::Asserted),
+                ENodeBlame::Proof(pidx) => self_.add_edge(pidx, idx, EdgeKind::Yield),
+                ENodeBlame::BoolConst | ENodeBlame::Unknown => (),
+            }
+        }
+
         // Add given equality created edges
         for (idx, eq) in parser.egraph.equalities.given.iter_enumerated() {
             match eq {
@@ -571,6 +577,8 @@ impl NodeKind {
 pub enum EdgeKind {
     /// Instantiation -> ENode
     Yield,
+    /// Proof (asserted) -> ENode
+    Asserted,
     /// ENode -> Instantiation
     Blame { pattern_term: u16 },
     /// TransEquality -> Instantiation

smt-log-parser/src/analysis/proofs.rs

@@ -1,36 +1,26 @@
 use std::cmp::Reverse;
 
-use crate::{items::ProofIdx, F64Ord, FxHashMap, Z3Parser};
+use crate::{items::TermIdx, F64Ord, FxHashMap, Z3Parser};
 
 use super::InstGraph;
 
 pub struct ProofAnalysis {
-    /// The cost approximation that it took to disprove the hypothesis (may have
-    /// been disproved in conjunction with other hypotheses).
-    pub hypothesis_cost: Vec<(ProofIdx, f64)>,
+    /// The cost approximation that it took to prove each lemma (by
+    /// contradiction).
+    pub lemmas_cost: Vec<(TermIdx, f64)>,
 }
 
 impl ProofAnalysis {
     pub fn new(parser: &Z3Parser, graph: &InstGraph) -> Self {
-        let mut hypothesis = FxHashMap::<_, f64>::default();
-        for (idx, _) in parser.proofs().iter_enumerated() {
-            let node = &graph.raw[idx];
-            if !node.proof.proves_false() {
+        let mut lemmas = FxHashMap::<_, f64>::default();
+        for (idx, proof) in parser.proofs().iter_enumerated() {
+            if !proof.kind.is_lemma() {
                 continue;
             }
-            let cost = node.cost;
-            let hypotheses = graph.raw.hypotheses(parser, idx);
-            if hypotheses.is_empty() {
-                // proved unsat
-                continue;
-            }
-            let cost_div = cost / hypotheses.len() as f64;
-            for h in hypotheses {
-                *hypothesis.entry(h).or_default() += cost_div;
-            }
+            *lemmas.entry(proof.result).or_default() += graph.raw[idx].cost;
         }
-        let mut hypothesis_cost = hypothesis.into_iter().collect::<Vec<_>>();
-        hypothesis_cost.sort_by_key(|&(idx, cost)| (Reverse(F64Ord(cost)), idx));
-        Self { hypothesis_cost }
+        let mut lemmas_cost = lemmas.into_iter().collect::<Vec<_>>();
+        lemmas_cost.sort_unstable_by_key(|&(lemma, cost)| (Reverse(F64Ord(cost)), lemma));
+        Self { lemmas_cost }
     }
 }