smt_scope/analysis/
mod.rs

1mod cdcl;
2mod dependencies;
3mod generalise;
4mod graph;
5mod misc;
6mod problem_behaviour;
7mod proofs;
8mod redundancy;
9
10pub use cdcl::*;
11pub use dependencies::*;
12pub use graph::*;
13pub use misc::*;
14pub use problem_behaviour::*;
15pub use proofs::*;
16pub use redundancy::*;
17
18use crate::Z3Parser;
19
20pub struct AllAnalyses {
21    pub log_info: LogInfo,
22    pub cdcl_info: CdclAnalysis,
23    pub redundancy: RedundancyAnalysis,
24    pub inst_graph: InstGraph,
25    pub quant_info: QuantifierAnalysis,
26    pub proof_info: ProofAnalysis,
27}
28
29/// Run all available analyses. Used for testing.
30pub fn run_all(parser: &Z3Parser) -> AllAnalyses {
31    let log_info = LogInfo::new(parser);
32    let cdcl_info = CdclAnalysis::new(parser);
33    let redundancy = RedundancyAnalysis::new(parser);
34    let inst_graph = InstGraph::new(parser).unwrap();
35    let quant_info = QuantifierAnalysis::new(parser, &inst_graph);
36    let proof_info = ProofAnalysis::new(parser, &inst_graph);
37    AllAnalyses {
38        log_info,
39        cdcl_info,
40        redundancy,
41        inst_graph,
42        quant_info,
43        proof_info,
44    }
45}
smt_scope/analysis/mod.rs

smt_scope/analysis/
mod.rs
