From 3ec9408775a4354e9256abf328d6a685232f9d3e Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Wed, 27 Nov 2024 11:15:22 +1100 Subject: [PATCH] Add decomposition for `regular` into `table_int` --- crates/huub/src/model/flatzinc.rs | 161 ++++++++++++++++++++++++---- share/minizinc/huub/fzn_regular.mzn | 18 ++++ 2 files changed, 158 insertions(+), 21 deletions(-) create mode 100644 share/minizinc/huub/fzn_regular.mzn diff --git a/crates/huub/src/model/flatzinc.rs b/crates/huub/src/model/flatzinc.rs index f12fb53..40e67f5 100644 --- a/crates/huub/src/model/flatzinc.rs +++ b/crates/huub/src/model/flatzinc.rs @@ -435,6 +435,79 @@ where } } + /// Convert a Flatzinc `regular_int` constraint to a set of + /// [`Constraint::TableInt`] constraints. + fn convert_regular_to_tables( + &mut self, + vars: Vec, + transitions: Vec>, + init_state: IntVal, + accept_states: HashSet, + ) -> Vec { + // TODO: Add the regular checking + // + + let mut table_constraints = Vec::new(); + let mut start: Vec> = Vec::new(); + let mut middle: Vec> = Vec::new(); + let mut end: Vec> = Vec::new(); + + for (i, state_trans) in transitions.iter().enumerate() { + let cur_state = i as IntVal + 1; + for (j, &next_state) in state_trans.iter().enumerate() { + let input_read = j as IntVal + 1; + + // Skip transitions to the "invalid" state + if next_state == 0 { + continue; + } + // If the current state is the initial state, add the transition to start + // table + if cur_state == init_state { + start.push(vec![input_read, next_state]); + } + // Add transition to the middle table (all valid transitions are allowed + // here) + middle.push(vec![cur_state, input_read, next_state]); + // If the resulting state is an accepting state, add the transition to the + // end table + if accept_states.contains(&next_state) { + end.push(vec![cur_state, input_read]); + } + } + } + + let state_vars = self + .prb + .new_int_vars(vars.len() - 1, (1..=transitions.len() as IntVal).into()) + .into_iter() + .map(IntView::from) + .collect_vec(); + + // Add table constraint to force a transition for the starting state + let sx: Vec = vec![vars[0].clone(), state_vars[0].clone()]; + table_constraints.push(Constraint::TableInt(sx, start)); + + // Add table constraint to force valid transition for the intermediate + // states + for i in 1..vars.len() - 1 { + let mx: Vec = vec![ + state_vars[i - 1].clone(), + vars[i].clone(), + state_vars[i].clone(), + ]; + table_constraints.push(Constraint::TableInt(mx, middle.clone())); + } + + // Add table constraint to force ending in an accepting state + let ex: Vec = vec![ + state_vars.last().unwrap().clone(), + vars.last().unwrap().clone(), + ]; + table_constraints.push(Constraint::TableInt(ex, end)); + table_constraints + } + /// Create branchers according to the search annotations in the FlatZinc instance fn create_branchers(&mut self) -> Result<(), FlatZincError> { let mut branchings = Vec::new(); @@ -1049,27 +1122,6 @@ where }); } } - "huub_disjunctive_strict" => { - if let [starts, durations] = c.args.as_slice() { - let starts = self - .arg_array(starts)? - .iter() - .map(|l| self.lit_int(l)) - .try_collect()?; - let durations = self - .arg_array(durations)? - .iter() - .map(|l| self.par_int(l)) - .try_collect()?; - self.prb += Constraint::DisjunctiveStrict(starts, durations); - } else { - return Err(FlatZincError::InvalidNumArgs { - name: "huub_disjunctive_strict", - found: c.args.len(), - expected: 2, - }); - } - } "huub_array_int_maximum" | "huub_array_int_minimum" => { let is_maximum = c.id.deref() == "huub_array_int_maximum"; if let [m, args] = c.args.as_slice() { @@ -1117,6 +1169,73 @@ where }); } } + "huub_disjunctive_strict" => { + if let [starts, durations] = c.args.as_slice() { + let starts = self + .arg_array(starts)? + .iter() + .map(|l| self.lit_int(l)) + .try_collect()?; + let durations = self + .arg_array(durations)? + .iter() + .map(|l| self.par_int(l)) + .try_collect()?; + self.prb += Constraint::DisjunctiveStrict(starts, durations); + } else { + return Err(FlatZincError::InvalidNumArgs { + name: "huub_disjunctive_strict", + found: c.args.len(), + expected: 2, + }); + } + } + "huub_regular" => { + if let [x, q, s, d, q0, f] = c.args.as_slice() { + let x: Vec<_> = self + .arg_array(x)? + .iter() + .map(|l| self.lit_int(l)) + .try_collect()?; + + let q = self.arg_par_int(q)?; + let s = self.arg_par_int(s)?; + let d: Vec<_> = self + .arg_array(d)? + .iter() + .map(|l| self.par_int(l)) + .try_collect()?; + if d.len() != (q * s) as usize { + return Err(FlatZincError::InvalidArgumentType { + expected: "array with an element for each combination of state and input value", + found: format!("array of size {}, for {q} states and {s} input values", d.len()) + }); + } + let d: Vec> = d + .into_iter() + .chunks(s as usize) + .into_iter() + .map(|c| c.collect()) + .collect(); + debug_assert!(d.last().map(|t| t.len() == s as usize).unwrap_or(true)); + + let q0 = self.arg_par_int(q0)?; + let f = self.arg_par_set(f)?; + let f: HashSet = f.iter().flat_map(|r| r.into_iter()).collect(); + + // Convert regular constraint in to table constraints and add them to the model + let tables = self.convert_regular_to_tables(x, d, q0, f); + for table in tables { + self.prb += table; + } + } else { + return Err(FlatZincError::InvalidNumArgs { + name: "huub_regular", + found: c.args.len(), + expected: 6, + }); + } + } "huub_table_int" => { if let [args, table] = c.args.as_slice() { let args = self.arg_array(args)?; diff --git a/share/minizinc/huub/fzn_regular.mzn b/share/minizinc/huub/fzn_regular.mzn new file mode 100644 index 0000000..8a6e89f --- /dev/null +++ b/share/minizinc/huub/fzn_regular.mzn @@ -0,0 +1,18 @@ +predicate fzn_regular( + array[int] of var int: x, + int: Q, + int: S, + array[int,int] of int: d, + int: q0, + set of int: F +) = + huub_regular(x, Q, S, array1d(d), q0, F); + +predicate huub_regular( + array[int] of var int: x, + int: Q, + int: S, + array[int] of int: d, + int: q0, + set of int: F +);