flux_verify_api/compiler/
sonar.rs

1use super::{parser, ConstraintProblem};
2
3/// Sonar domain parser.
4/// Extracts sonar parameters from natural language and builds a constraint problem.
5pub fn parse(claim: &str) -> Result<ConstraintProblem, String> {
6    let lower = claim.to_lowercase();
7
8    // Extract frequency (kHz or Hz)
9    let frequency_hz = parser::extract_number_with_unit(&lower, &["khz", "hz"])
10        .or_else(|| parser::extract_number_before(&lower, "khz").map(|f| f * 1000.0))
11        .or_else(|| parser::extract_number_before(&lower, "hz"))
12        .ok_or("Could not extract frequency from claim")?;
13
14    // Normalize to Hz
15    let freq_normalized = if lower.contains("khz") && frequency_hz < 1000.0 {
16        frequency_hz * 1000.0
17    } else {
18        frequency_hz
19    };
20
21    // Extract depth
22    let depth_m = parser::extract_number_before(&lower, "m depth")
23        .or_else(|| parser::extract_number_before(&lower, "meters depth"))
24        .or_else(|| parser::extract_number_before(&lower, "depth"))
25        .or_else(|| parser::extract_number_near(&lower, "depth"))
26        .ok_or("Could not extract depth from claim")?;
27
28    // Extract range/distance
29    let range_m = parser::extract_number_before(&lower, "km")
30        .map(|km| km * 1000.0)
31        .or_else(|| parser::extract_number_before(&lower, "range"))
32        .or_else(|| parser::extract_number_near(&lower, "range"))
33        .ok_or("Could not extract range from claim")?;
34
35    // Extract target strength (optional, default -10 dB)
36    let target_strength_db = parser::extract_number_before(&lower, "db target")
37        .or_else(|| parser::extract_number_near(&lower, "target"))
38        .unwrap_or(10.0); // default 10 dB target strength
39
40    // Environmental defaults
41    let temp_c = parser::extract_number_near(&lower, "temperature").unwrap_or(15.0);
42    let salinity_ppt = parser::extract_number_near(&lower, "salinity").unwrap_or(35.0);
43
44    let frequency_khz = freq_normalized / 1000.0;
45
46    Ok(ConstraintProblem {
47        domain: "sonar".into(),
48        variables: vec![
49            super::Variable { name: "depth_m".into(), value: depth_m, desc: "depth (m)".into() },
50            super::Variable { name: "frequency_hz".into(), value: freq_normalized, desc: "frequency (Hz)".into() },
51            super::Variable { name: "range_m".into(), value: range_m, desc: "range (m)".into() },
52            super::Variable { name: "target_strength_db".into(), value: target_strength_db, desc: "target strength (dB)".into() },
53        ],
54        constraints: vec![
55            super::Constraint::SoundVelocity { depth_m, temp_c, salinity_ppt },
56            super::Constraint::Absorption { frequency_khz, depth_m, temp_c, salinity_ppt },
57            super::Constraint::TransmissionLoss { range_m, frequency_khz, depth_m, temp_c, salinity_ppt },
58        ],
59        assertion: super::Assertion {
60            assertion_type: "gt".into(),
61            expected: 0.0,
62            actual_expr: "signal excess (dB)".into(),
63        },
64    })
65}
flux_verify_api/compiler/sonar.rs

flux_verify_api/compiler/
sonar.rs
