zincite_check/
tables.rs

1//! Exact table signatures, row-major membership and Boolean completion.
2use super::*;
3
4#[derive(Clone, Copy, Debug, PartialEq, Eq)]
5pub(crate) struct TableName {
6    pub boolean: bool,
7    pub mode: RelationMode,
8}
9
10impl TableName {
11    pub fn from_name(name: &str) -> Option<Self> {
12        for base in [
13            name,
14            name.strip_prefix("gecode_").unwrap_or(""),
15            name.strip_prefix("fzn_").unwrap_or(""),
16        ] {
17            let (boolean, mode) = match base {
18                "gecode_table_int" => (false, RelationMode::Plain),
19                "gecode_table_int_reif" => (false, RelationMode::Reified),
20                "gecode_table_int_imp" => (false, RelationMode::Implied),
21                "gecode_table_bool" => (true, RelationMode::Plain),
22                "gecode_table_bool_reif" => (true, RelationMode::Reified),
23                "gecode_table_bool_imp" => (true, RelationMode::Implied),
24                _ => continue,
25            };
26            return Some(Self { boolean, mode });
27        }
28        None
29    }
30
31    pub fn kind(self) -> ValueType {
32        if self.boolean {
33            ValueType::Boolean
34        } else {
35            ValueType::Integer
36        }
37    }
38
39    #[cfg(feature = "prepare")]
40    pub fn signature(self) -> Vec<prepare::ArgumentType> {
41        let mut args = vec![
42            prepare::ArgumentType {
43                kind: self.kind(),
44                is_var: true,
45                is_array: true,
46            },
47            prepare::ArgumentType {
48                kind: self.kind(),
49                is_var: false,
50                is_array: true,
51            },
52        ];
53        if self.mode != RelationMode::Plain {
54            args.push(prepare::ArgumentType {
55                kind: ValueType::Boolean,
56                is_var: true,
57                is_array: false,
58            });
59        }
60        args
61    }
62}
63
64/// Fixed row-major table values. The candidate tuple supplies the row width.
65#[derive(Clone, Debug, Serialize, Deserialize)]
66#[serde(tag = "kind", content = "values", rename_all = "snake_case")]
67pub enum TableData {
68    Integer(
69        #[serde(
70            serialize_with = "serialize_integers",
71            deserialize_with = "deserialize_integers"
72        )]
73        Vec<i64>,
74    ),
75    Boolean(Vec<bool>),
76}
77
78impl TableData {
79    fn len(&self) -> usize {
80        match self {
81            Self::Integer(values) => values.len(),
82            Self::Boolean(values) => values.len(),
83        }
84    }
85
86    pub(crate) fn kind(&self) -> ValueType {
87        match self {
88            Self::Integer(_) => ValueType::Integer,
89            Self::Boolean(_) => ValueType::Boolean,
90        }
91    }
92}
93
94#[derive(Debug, Serialize, Deserialize)]
95pub(crate) struct Table {
96    pub tuple: Vec<Operand>,
97    pub table: TableData,
98    pub condition: RelationCondition,
99}
100
101impl Table {
102    pub fn operands(&self) -> Vec<&Operand> {
103        self.tuple.iter().chain(self.condition.operand()).collect()
104    }
105
106    pub fn validate_shape(&self) -> Result<(), &'static str> {
107        let width = self.tuple.len();
108        if (width == 0 && self.table.len() != 0)
109            || (width != 0 && !self.table.len().is_multiple_of(width))
110        {
111            return Err("table data must contain complete rows of the candidate tuple width");
112        }
113        Ok(())
114    }
115
116    pub fn membership(&self, values: &[Option<Value>]) -> Option<bool> {
117        // Resolve the whole tuple even when the table has no rows.
118        let tuple: Vec<_> = self
119            .tuple
120            .iter()
121            .map(|entry| entry.value(values))
122            .collect::<Option<_>>()?;
123        if tuple.is_empty() {
124            return Some(false);
125        }
126        Some(match &self.table {
127            TableData::Integer(table) => table.chunks_exact(tuple.len()).any(|row| {
128                row.iter()
129                    .zip(&tuple)
130                    .all(|(entry, value)| *entry == value.integer())
131            }),
132            TableData::Boolean(table) => table.chunks_exact(tuple.len()).any(|row| {
133                row.iter()
134                    .zip(&tuple)
135                    .all(|(entry, value)| value.boolean() == *entry)
136            }),
137        })
138    }
139
140    pub fn can_define(&self, output: usize) -> bool {
141        matches!(&self.condition, RelationCondition::Reified { result: Operand::Variable(slot) } if *slot == output)
142            && !self
143                .tuple
144                .iter()
145                .any(|entry| matches!(entry, Operand::Variable(slot) if *slot == output))
146    }
147}
148
149impl PreparedModel {
150    pub(crate) fn evaluate_table(
151        &self,
152        table: &Table,
153        values: &[Option<Value>],
154    ) -> Option<ViolationKind> {
155        let membership = table.membership(values).expect("available table tuple");
156        if table.condition.satisfied(membership, values) {
157            return None;
158        }
159        Some(ViolationKind::Table {
160            tuple: table
161                .tuple
162                .iter()
163                .map(|entry| self.argument(entry, values).expect("available table entry"))
164                .collect(),
165            table: table.table.clone(),
166            width: table.tuple.len(),
167            membership,
168            condition: self.condition_value(&table.condition, values),
169        })
170    }
171}
zincite_check/tables.rs

zincite_check/
tables.rs
