taco_cli/
taco_config.rs

1//! Module for implementing advanced specification options for the model checker.
2//!
3//! This module ties together all potential configuration options, such as for
4//! example BDD library or SMT checker options of the `TACO` model checker.
5
6use taco_bdd::BDDManagerConfig;
7
8use serde::Deserialize;
9
10use taco_model_checker::preprocessing::ExistingPreprocessors;
11use taco_smt_encoder::SMTSolverBuilderCfg;
12
13/// Type representing configuration options for the `TACO` model checker
14///
15/// This struct contains options for the SMT solver and the BDD manager that can
16/// be set using config files or environment variables. This type implements
17/// `serde::Deserialize` to easily parse the configuration out of structured
18/// configuration.
19#[derive(Debug, Clone, Deserialize, Default)]
20pub struct TACOConfig {
21    /// Options for the SMT solver
22    smt: Option<SMTSolverBuilderCfg>,
23    /// Options for the BDD manager
24    bdd: Option<BDDManagerConfig>,
25    /// Options for configuring which preprocessors to use
26    preprocessors: Option<Vec<ExistingPreprocessors>>,
27}
28
29impl TACOConfig {
30    /// Set the configuration for the SMT solver builder to the given value
31    pub fn set_smt_solver_builder_cfg(&mut self, cfg: SMTSolverBuilderCfg) {
32        self.smt = Some(cfg);
33    }
34
35    /// Set the configuration for the BDD manager to the given value
36    pub fn set_bdd_config(&mut self, cfg: BDDManagerConfig) {
37        self.bdd = Some(cfg);
38    }
39
40    /// Get BDD manager and SMT solver builder configuration
41    pub fn get_bdd_smt_config(&self) -> (Option<SMTSolverBuilderCfg>, Option<BDDManagerConfig>) {
42        (self.smt.clone(), self.bdd.clone())
43    }
44
45    /// Get the SMT solver builder configuration
46    pub fn get_smt_solver_builder_cfg(&self) -> Option<SMTSolverBuilderCfg> {
47        self.smt.clone()
48    }
49
50    pub fn get_preprocessors_cfg(&self) -> &Option<Vec<ExistingPreprocessors>> {
51        &self.preprocessors
52    }
53}
54
55#[cfg(test)]
56mod tests {
57
58    use taco_bdd::BDDManagerConfig;
59    use taco_model_checker::preprocessing::ExistingPreprocessors;
60    use taco_smt_encoder::SMTSolverBuilderCfg;
61
62    use crate::taco_config::TACOConfig;
63
64    #[test]
65    #[cfg(feature = "cudd")]
66    fn test_taco_config() {
67        let json_data = "{
68            \"smt\": {
69                \"command\": \"z3\"
70            },
71            \"bdd\": {
72                \"Cudd\": []
73            }
74        }";
75
76        let config: TACOConfig = serde_json::from_str(json_data).unwrap();
77
78        let expected_smt = Some(SMTSolverBuilderCfg::new(
79            "z3".to_string(),
80            vec![],
81            vec![],
82            false,
83        ));
84        let expected_bdd = Some(BDDManagerConfig::new_cudd());
85
86        assert_eq!(config.get_bdd_smt_config(), (expected_smt, expected_bdd));
87
88        let smt_config = Some(SMTSolverBuilderCfg::new(
89            "z3".to_string(),
90            vec![],
91            vec![],
92            false,
93        ));
94        let bdd_config = Some(BDDManagerConfig::new_oxidd());
95
96        let mut config = TACOConfig::default();
97        config.set_smt_solver_builder_cfg(smt_config.clone().unwrap());
98        config.set_bdd_config(bdd_config.clone().unwrap());
99        assert_eq!(config.get_bdd_smt_config(), (smt_config, bdd_config));
100    }
101
102    #[test]
103    fn test_taco_config_preprocessors() {
104        let json_data = "{
105            \"preprocessors\": [
106                \"DropSelfLoops\",
107                \"DropUnreachableLocations\",
108                \"ReplaceTrivialGuardsStatic\",
109                \"ReplaceTrivialGuardsSMT\",
110                \"RemoveUnusedVariables\",
111                \"DropUnsatisfiableRules\",
112                \"CollapseLocations\"
113            ]
114        }";
115
116        let config: TACOConfig = serde_json::from_str(json_data).unwrap();
117
118        let expected_preprocessors = Some(vec![
119            ExistingPreprocessors::DropSelfLoops,
120            ExistingPreprocessors::DropUnreachableLocations,
121            ExistingPreprocessors::ReplaceTrivialGuardsStatic,
122            ExistingPreprocessors::ReplaceTrivialGuardsSMT,
123            ExistingPreprocessors::RemoveUnusedVariables,
124            ExistingPreprocessors::DropUnsatisfiableRules,
125            ExistingPreprocessors::CollapseLocations,
126        ]);
127
128        assert_eq!(config.get_preprocessors_cfg(), &expected_preprocessors);
129    }
130}
taco_cli/taco_config.rs

taco_cli/
taco_config.rs
