Skip to main content

flux_verify_api/compiler/
thermal.rs

1use super::{parser, ConstraintProblem};
2
3/// Thermal domain parser.
4/// Extracts temperature bounds and safe ranges from natural language.
5pub fn parse(claim: &str) -> Result<ConstraintProblem, String> {
6    let lower = claim.to_lowercase();
7
8    // Extract the temperature to check
9    let temp_c = parser::extract_number_near(&lower, "temperature")
10        .or_else(|| parser::extract_number_near(&lower, "temp"))
11        .or_else(|| parser::extract_number_before(&lower, "°c"))
12        .or_else(|| parser::extract_number_before(&lower, "degrees"))
13        .ok_or("Could not extract temperature from claim")?;
14
15    // Extract safe range bounds (e.g., "safe range of X to Y", "range of X to Y")
16    let (min_safe, max_safe) = parser::extract_range(&lower)
17        .ok_or("Could not extract safe temperature range from claim")?;
18
19    Ok(ConstraintProblem {
20        domain: "thermal".into(),
21        variables: vec![
22            super::Variable { name: "temp_c".into(), value: temp_c, desc: "temperature (°C)".into() },
23            super::Variable { name: "min_safe".into(), value: min_safe, desc: "minimum safe temp (°C)".into() },
24            super::Variable { name: "max_safe".into(), value: max_safe, desc: "maximum safe temp (°C)".into() },
25        ],
26        constraints: vec![
27            super::Constraint::ThermalBound { temp_c, min_safe, max_safe },
28        ],
29        assertion: super::Assertion {
30            assertion_type: "in_range".into(),
31            expected: 0.0,
32            actual_expr: format!("temperature {}°C within [{}, {}]", temp_c, min_safe, max_safe),
33        },
34    })
35}