lemma/inversion/
target.rs

1use crate::{LiteralValue, OperationResult};
2
3/// Desired outcome for an inversion query
4#[derive(Debug, Clone, PartialEq)]
5pub struct Target {
6    /// The comparison operator
7    pub op: TargetOp,
8
9    /// The desired outcome (value or veto)
10    /// None means "any value" (wildcard for non-veto results)
11    pub outcome: Option<OperationResult>,
12}
13
14/// Comparison operators for targets
15#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
16pub enum TargetOp {
17    /// Equal to (=)
18    Eq,
19    /// Not equal to (≠)
20    Neq,
21    /// Less than (<)
22    Lt,
23    /// Less than or equal to (≤)
24    Lte,
25    /// Greater than (>)
26    Gt,
27    /// Greater than or equal to (≥)
28    Gte,
29}
30
31impl Target {
32    /// Create a target for a specific value with equality operator
33    pub fn value(value: LiteralValue) -> Self {
34        Self {
35            op: TargetOp::Eq,
36            outcome: Some(OperationResult::Value(value)),
37        }
38    }
39
40    /// Create a target for a specific veto message
41    pub fn veto(message: Option<String>) -> Self {
42        Self {
43            op: TargetOp::Eq,
44            outcome: Some(OperationResult::Veto(message)),
45        }
46    }
47
48    /// Create a target for any veto
49    pub fn any_veto() -> Self {
50        Self::veto(None)
51    }
52
53    /// Create a target for any value (non-veto)
54    pub fn any_value() -> Self {
55        Self {
56            op: TargetOp::Eq,
57            outcome: None,
58        }
59    }
60
61    /// Create a target with a custom operator
62    pub fn with_op(op: TargetOp, outcome: OperationResult) -> Self {
63        Self {
64            op,
65            outcome: Some(outcome),
66        }
67    }
68}
lemma/inversion/target.rs

lemma/inversion/
target.rs
