flux_verify_api/compiler/
thermal.rs1use super::{parser, ConstraintProblem};
2
3pub fn parse(claim: &str) -> Result<ConstraintProblem, String> {
6 let lower = claim.to_lowercase();
7
8 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 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}