lemma/inversion/
target.rs

1//! Target specification for inversion queries
2
3use crate::{LiteralValue, OperationResult};
4use serde::Serialize;
5
6/// Desired outcome for an inversion query
7#[derive(Debug, Clone, PartialEq, Serialize)]
8pub struct Target {
9    /// The comparison operator
10    pub op: TargetOp,
11
12    /// The desired outcome (value or veto)
13    /// None means "any value" (wildcard for non-veto results)
14    pub outcome: Option<OperationResult>,
15}
16
17/// Comparison operators for targets
18#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize)]
19pub enum TargetOp {
20    /// Equal to (=)
21    Eq,
22    /// Not equal to (!=)
23    Neq,
24    /// Less than (<)
25    Lt,
26    /// Less than or equal to (<=)
27    Lte,
28    /// Greater than (>)
29    Gt,
30    /// Greater than or equal to (>=)
31    Gte,
32}
33
34impl Target {
35    /// Create a target for a specific value with equality operator
36    pub fn value(value: LiteralValue) -> Self {
37        Self {
38            op: TargetOp::Eq,
39            outcome: Some(OperationResult::Value(value)),
40        }
41    }
42
43    /// Create a target for a specific veto message
44    pub fn veto(message: Option<String>) -> Self {
45        Self {
46            op: TargetOp::Eq,
47            outcome: Some(OperationResult::Veto(message)),
48        }
49    }
50
51    /// Create a target for any veto
52    pub fn any_veto() -> Self {
53        Self::veto(None)
54    }
55
56    /// Create a target for any value (non-veto)
57    pub fn any_value() -> Self {
58        Self {
59            op: TargetOp::Eq,
60            outcome: None,
61        }
62    }
63
64    /// Create a target with a custom operator
65    pub fn with_op(op: TargetOp, outcome: OperationResult) -> Self {
66        Self {
67            op,
68            outcome: Some(outcome),
69        }
70    }
71
72    /// Format target for display
73    pub fn format(&self) -> String {
74        let op_str = match self.op {
75            TargetOp::Eq => "=",
76            TargetOp::Neq => "!=",
77            TargetOp::Lt => "<",
78            TargetOp::Lte => "<=",
79            TargetOp::Gt => ">",
80            TargetOp::Gte => ">=",
81        };
82
83        let value_str = match &self.outcome {
84            None => "any".to_string(),
85            Some(OperationResult::Value(v)) => v.to_string(),
86            Some(OperationResult::Veto(Some(msg))) => format!("veto({})", msg),
87            Some(OperationResult::Veto(None)) => "veto".to_string(),
88        };
89
90        format!("{} {}", op_str, value_str)
91    }
92}
lemma/inversion/target.rs

lemma/inversion/
target.rs
