smt_scope/analysis/
proofs.rs

1use std::cmp::Reverse;
2
3use crate::{items::TermIdx, F64Ord, FxHashMap, Z3Parser};
4
5use super::InstGraph;
6
7pub struct ProofAnalysis {
8    /// The cost approximation that it took to prove each lemma (by
9    /// contradiction).
10    pub lemmas_cost: Vec<(TermIdx, f64)>,
11}
12
13impl ProofAnalysis {
14    pub fn new(parser: &Z3Parser, graph: &InstGraph) -> Self {
15        let mut lemmas = FxHashMap::<_, f64>::default();
16        for (idx, proof) in parser.proofs().iter_enumerated() {
17            if !proof.kind.is_lemma() {
18                continue;
19            }
20            *lemmas.entry(proof.result).or_default() += graph.raw[idx].cost;
21        }
22        let mut lemmas_cost = lemmas.into_iter().collect::<Vec<_>>();
23        lemmas_cost.sort_unstable_by_key(|&(lemma, cost)| (Reverse(F64Ord(cost)), lemma));
24        Self { lemmas_cost }
25    }
26}
smt_scope/analysis/proofs.rs

smt_scope/analysis/
proofs.rs
