z39_solver/domains/
config.rs

1/// Config domain: validate configuration constraints (deployments, resources, permissions)
2///
3/// The agent describes config variables and invariants.
4/// Z3 checks if the configuration is valid or finds conflicts.
5
6use serde::{Deserialize, Serialize};
7
8#[derive(Debug, Clone, Serialize, Deserialize)]
9pub struct ConfigCheckRequest {
10    /// Variables in the configuration
11    pub vars: Vec<ConfigVar>,
12    /// Invariant rules that must hold (SMT-LIB2 boolean expressions)
13    pub rules: Vec<String>,
14    /// What to check
15    pub mode: ConfigCheckMode,
16}
17
18#[derive(Debug, Clone, Serialize, Deserialize)]
19pub struct ConfigVar {
20    pub name: String,
21    pub var_type: ConfigVarType,
22    #[serde(default)]
23    pub allowed_values: Vec<String>,
24}
25
26#[derive(Debug, Clone, Serialize, Deserialize)]
27#[serde(rename_all = "snake_case")]
28pub enum ConfigVarType {
29    Bool,
30    Int { min: i32, max: i32 },
31    Enum,
32}
33
34#[derive(Debug, Clone, Serialize, Deserialize)]
35#[serde(rename_all = "snake_case")]
36pub enum ConfigCheckMode {
37    /// Check if rules are consistent (no contradictions)
38    Validate,
39    /// Find a config that satisfies all rules
40    FindValid,
41    /// Find a config that violates at least one rule
42    FindViolation,
43}
44
45pub fn encode_config(req: &ConfigCheckRequest) -> String {
46    let mut s = String::new();
47    s.push_str("(set-logic QF_LIA)\n");
48
49    // Declare variables
50    for v in &req.vars {
51        match &v.var_type {
52            ConfigVarType::Bool => {
53                s.push_str(&format!("(declare-const {} Bool)\n", v.name));
54            }
55            ConfigVarType::Int { min, max } => {
56                s.push_str(&format!("(declare-const {} Int)\n", v.name));
57                s.push_str(&format!("(assert (>= {} {}))\n", v.name, min));
58                s.push_str(&format!("(assert (<= {} {}))\n", v.name, max));
59            }
60            ConfigVarType::Enum => {
61                // Encode as integer with allowed values
62                s.push_str(&format!("(declare-const {} Int)\n", v.name));
63                if !v.allowed_values.is_empty() {
64                    let cases: Vec<String> = v.allowed_values.iter().enumerate()
65                        .map(|(i, _)| format!("(= {} {})", v.name, i))
66                        .collect();
67                    s.push_str(&format!("(assert (or {}))\n", cases.join(" ")));
68                }
69            }
70        }
71    }
72
73    match req.mode {
74        ConfigCheckMode::Validate | ConfigCheckMode::FindValid => {
75            for r in &req.rules {
76                s.push_str(&format!("(assert {r})\n"));
77            }
78        }
79        ConfigCheckMode::FindViolation => {
80            // Assert that NOT all rules hold
81            let negated: Vec<String> = req.rules.iter().map(|r| format!("(not {})", r)).collect();
82            s.push_str(&format!("(assert (or {}))\n", negated.join(" ")));
83        }
84    }
85
86    s.push_str("(check-sat)\n");
87    s.push_str("(get-model)\n");
88    s
89}
90
91pub fn interpret_config(req: &ConfigCheckRequest, is_unsat: bool, model: Option<&str>) -> String {
92    match req.mode {
93        ConfigCheckMode::Validate => {
94            if is_unsat {
95                "✗ invalid — rules are contradictory, no valid configuration exists".to_string()
96            } else {
97                let m = model.unwrap_or("unknown");
98                format!("✓ valid — rules are consistent. Example config: {m}")
99            }
100        }
101        ConfigCheckMode::FindValid => {
102            if is_unsat {
103                "✗ no valid configuration exists — rules are contradictory".to_string()
104            } else {
105                let m = model.unwrap_or("unknown");
106                format!("✓ valid configuration: {m}")
107            }
108        }
109        ConfigCheckMode::FindViolation => {
110            if is_unsat {
111                "✓ all rules always hold — no violation possible".to_string()
112            } else {
113                let m = model.unwrap_or("unknown");
114                format!("⚠ violation found: {m}")
115            }
116        }
117    }
118}
119
120pub async fn run(
121    z3_bin: &std::path::PathBuf,
122    payload: &str,
123    timeout_secs: u64,
124) -> Result<String, serde_json::Error> {
125    let req: ConfigCheckRequest = serde_json::from_str(payload)?;
126    let smt = encode_config(&req);
127    let result = crate::solver::solve(z3_bin, &smt, timeout_secs).await;
128    Ok(interpret_config(&req, result.is_unsat(), result.model.as_deref()))
129}
z39_solver/domains/config.rs

z39_solver/domains/
config.rs
