smt-scope 0.1.7

A library for parsing and analysing SMT traces.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45

mod cdcl;
mod dependencies;
mod generalise;
mod graph;
mod misc;
mod problem_behaviour;
mod proofs;
mod redundancy;

pub use cdcl::*;
pub use dependencies::*;
pub use graph::*;
pub use misc::*;
pub use problem_behaviour::*;
pub use proofs::*;
pub use redundancy::*;

use crate::Z3Parser;

pub struct AllAnalyses {
    pub log_info: LogInfo,
    pub cdcl_info: CdclAnalysis,
    pub redundancy: RedundancyAnalysis,
    pub inst_graph: InstGraph,
    pub quant_info: QuantifierAnalysis,
    pub proof_info: ProofAnalysis,
}

/// Run all available analyses. Used for testing.
pub fn run_all(parser: &Z3Parser) -> AllAnalyses {
    let log_info = LogInfo::new(parser);
    let cdcl_info = CdclAnalysis::new(parser);
    let redundancy = RedundancyAnalysis::new(parser);
    let inst_graph = InstGraph::new(parser).unwrap();
    let quant_info = QuantifierAnalysis::new(parser, &inst_graph);
    let proof_info = ProofAnalysis::new(parser, &inst_graph);
    AllAnalyses {
        log_info,
        cdcl_info,
        redundancy,
        inst_graph,
        quant_info,
        proof_info,
    }
}