minion_rs/
ast.rs

1//! Types used for representing Minion models in Rust.
2
3use std::{collections::HashMap, fmt::Display};
4
5use crate::print::{print_const_array, print_constraint_array, print_var_array};
6
7pub type VarName = String;
8pub type Tuple = (Constant, Constant);
9pub type TwoVars = (Var, Var);
10
11/// A Minion model.
12#[non_exhaustive]
13#[derive(Debug, Clone, PartialEq, Eq)]
14pub struct Model {
15    pub named_variables: SymbolTable,
16    pub constraints: Vec<Constraint>,
17}
18
19impl Model {
20    /// Creates an empty Minion model.
21    pub fn new() -> Model {
22        Model {
23            named_variables: SymbolTable::new(),
24            constraints: Vec::new(),
25        }
26    }
27}
28
29impl Default for Model {
30    fn default() -> Self {
31        Self::new()
32    }
33}
34
35/// All supported Minion constraints.
36#[non_exhaustive]
37#[derive(Debug, Clone, PartialEq, Eq)]
38pub enum Constraint {
39    Difference(TwoVars, Var),
40    Div(TwoVars, Var),
41    DivUndefZero(TwoVars, Var),
42    Modulo(TwoVars, Var),
43    ModuloUndefZero(TwoVars, Var),
44    Pow(TwoVars, Var),
45    Product(TwoVars, Var),
46    WeightedSumGeq(Vec<Constant>, Vec<Var>, Var),
47    WeightedSumLeq(Vec<Constant>, Vec<Var>, Var),
48    CheckAssign(Box<Constraint>),
49    CheckGsa(Box<Constraint>),
50    ForwardChecking(Box<Constraint>),
51    Reify(Box<Constraint>, Var),
52    ReifyImply(Box<Constraint>, Var),
53    ReifyImplyQuick(Box<Constraint>, Var),
54    WatchedAnd(Vec<Constraint>),
55    WatchedOr(Vec<Constraint>),
56    GacAllDiff(Vec<Var>),
57    AllDiff(Vec<Var>),
58    AllDiffMatrix(Vec<Var>, Constant),
59    WatchSumGeq(Vec<Var>, Constant),
60    WatchSumLeq(Vec<Var>, Constant),
61    OccurrenceGeq(Vec<Var>, Constant, Constant),
62    OccurrenceLeq(Vec<Var>, Constant, Constant),
63    Occurrence(Vec<Var>, Constant, Var),
64    LitSumGeq(Vec<Var>, Vec<Constant>, Constant),
65    Gcc(Vec<Var>, Vec<Constant>, Vec<Var>),
66    GccWeak(Vec<Var>, Vec<Constant>, Vec<Var>),
67    LexLeqRv(Vec<Var>, Vec<Var>),
68    LexLeq(Vec<Var>, Vec<Var>),
69    LexLess(Vec<Var>, Vec<Var>),
70    LexLeqQuick(Vec<Var>, Vec<Var>),
71    LexLessQuick(Vec<Var>, Vec<Var>),
72    WatchVecNeq(Vec<Var>, Vec<Var>),
73    WatchVecExistsLess(Vec<Var>, Vec<Var>),
74    Hamming(Vec<Var>, Vec<Var>, Constant),
75    NotHamming(Vec<Var>, Vec<Var>, Constant),
76    FrameUpdate(Vec<Var>, Vec<Var>, Vec<Var>, Vec<Var>, Constant),
77    //HaggisGac(Vec<Var>,Vec<
78    //HaggisGacStable
79    //ShortStr2
80    //ShortcTupleStr2
81    NegativeTable(Vec<Var>, Vec<Tuple>),
82    Table(Vec<Var>, Vec<Tuple>),
83    GacSchema(Vec<Var>, Vec<Tuple>),
84    LightTable(Vec<Var>, Vec<Tuple>),
85    Mddc(Vec<Var>, Vec<Tuple>),
86    NegativeMddc(Vec<Var>, Vec<Tuple>),
87    Str2Plus(Vec<Var>, Var),
88    Max(Vec<Var>, Var),
89    Min(Vec<Var>, Var),
90    NvalueGeq(Vec<Var>, Var),
91    NvalueLeq(Vec<Var>, Var),
92    SumLeq(Vec<Var>, Var),
93    SumGeq(Vec<Var>, Var),
94    Element(Vec<Var>, Var, Var),
95    ElementOne(Vec<Var>, Var, Var),
96    ElementUndefZero(Vec<Var>, Var, Var),
97    WatchElement(Vec<Var>, Var, Var),
98    WatchElementOne(Vec<Var>, Var, Var),
99    WatchElementOneUndefZero(Vec<Var>, Var, Var),
100    WatchElementUndefZero(Vec<Var>, Var, Var),
101    WLiteral(Var, Constant),
102    WNotLiteral(Var, Constant),
103    WInIntervalSet(Var, Vec<Constant>),
104    WInRange(Var, Vec<Constant>),
105    WInset(Var, Vec<Constant>),
106    WNotInRange(Var, Vec<Constant>),
107    WNotInset(Var, Vec<Constant>),
108    Abs(Var, Var),
109    DisEq(Var, Var),
110    Eq(Var, Var),
111    MinusEq(Var, Var),
112    GacEq(Var, Var),
113    WatchLess(Var, Var),
114    WatchNeq(Var, Var),
115    Ineq(Var, Var, Constant),
116    False,
117    True,
118}
119
120#[allow(clippy::todo, unused_variables)]
121impl Display for Constraint {
122    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
123        match self {
124            Constraint::Difference(_, var) => write!(f, "difference({var}"),
125            Constraint::Div(_, var) => write!(f, "div({var}"),
126            Constraint::DivUndefZero(_, var) => write!(f, "div_undefzero({var})"),
127            Constraint::Modulo(_, var) => write!(f, "modulo({var})"),
128            Constraint::ModuloUndefZero(_, var) => write!(f, "mod_undefzero({var})"),
129            Constraint::Pow(_, var) => write!(f, "pow({var})"),
130            Constraint::Product(_, var) => write!(f, "product({var})"),
131            Constraint::WeightedSumGeq(constants, vars, var) => {
132                write!(
133                    f,
134                    "weightedsumgeq({},{},{var})",
135                    print_const_array(constants),
136                    print_var_array(vars)
137                )
138            }
139            Constraint::WeightedSumLeq(constants, vars, var) => {
140                write!(
141                    f,
142                    "weightedsumleq({},{},{var})",
143                    print_const_array(constants),
144                    print_var_array(vars)
145                )
146            }
147            Constraint::CheckAssign(constraint) => {
148                todo!("don't know how to print checkassign constriant...")
149            }
150            Constraint::CheckGsa(constraint) => {
151                todo!("don't know how to print checkgsa constraint...")
152            }
153            Constraint::ForwardChecking(constraint) => {
154                todo!("don't know how to print forwardchecking constraint...")
155            }
156            Constraint::Reify(constraint, var) => write!(f, "reify({constraint},{var})"),
157            Constraint::ReifyImply(constraint, var) => write!(f, "reifyimply({constraint},{var})"),
158            Constraint::ReifyImplyQuick(constraint, var) => {
159                write!(f, "reifyimply-quick({constraint},{var})")
160            }
161            Constraint::WatchedAnd(constraints) => {
162                write!(f, "watched-and({})", print_constraint_array(constraints))
163            }
164            Constraint::WatchedOr(constraints) => {
165                write!(f, "watched-or({})", print_constraint_array(constraints))
166            }
167            Constraint::GacAllDiff(vars) => write!(f, "gacalldiff({})", print_var_array(vars)),
168            Constraint::AllDiff(vars) => write!(f, "alldiff({})", print_var_array(vars)),
169            Constraint::AllDiffMatrix(vars, constant) => {
170                write!(f, "alldiffmatrix({},{constant})", print_var_array(vars))
171            }
172            Constraint::WatchSumGeq(vars, constant) => {
173                write!(f, "watchsumgeq({},{constant})", print_var_array(vars))
174            }
175            Constraint::WatchSumLeq(vars, constant) => {
176                write!(f, "watchsumleq({},{constant})", print_var_array(vars))
177            }
178            Constraint::OccurrenceGeq(vars, constant, constant1) => write!(
179                f,
180                "occurrencegeq({},{constant},{constant1})",
181                print_var_array(vars)
182            ),
183            Constraint::OccurrenceLeq(vars, constant, constant1) => write!(
184                f,
185                "occurrenceleq({},{constant},{constant1})",
186                print_var_array(vars)
187            ),
188            Constraint::Occurrence(vars, constant, var) => {
189                write!(f, "occurrence({},{constant},{var})", print_var_array(vars))
190            }
191            Constraint::LitSumGeq(vars, constants, constant) => write!(
192                f,
193                "litsumgeq({},{},{constant})",
194                print_var_array(vars),
195                print_const_array(constants)
196            ),
197            Constraint::Gcc(vars, constants, vars1) => write!(
198                f,
199                "gcc({},{},{})",
200                print_var_array(vars),
201                print_const_array(constants),
202                print_var_array(vars1)
203            ),
204            Constraint::GccWeak(vars, constants, vars1) => write!(
205                f,
206                "gccweak({},{},{})",
207                print_var_array(vars),
208                print_const_array(constants),
209                print_var_array(vars1)
210            ),
211            Constraint::LexLeqRv(vars, vars1) => write!(
212                f,
213                "lexleq[rv]({},{})",
214                print_var_array(vars),
215                print_var_array(vars1)
216            ),
217            Constraint::LexLeq(vars, vars1) => write!(
218                f,
219                "lexleq({},{})",
220                print_var_array(vars),
221                print_var_array(vars1)
222            ),
223            Constraint::LexLeqQuick(vars, vars1) => write!(
224                f,
225                "lexleq[quick]({},{})",
226                print_var_array(vars),
227                print_var_array(vars1)
228            ),
229            Constraint::LexLess(vars, vars1) => write!(
230                f,
231                "lexless({},{})",
232                print_var_array(vars),
233                print_var_array(vars1)
234            ),
235            Constraint::LexLessQuick(vars, vars1) => write!(
236                f,
237                "lexless[quick]({},{})",
238                print_var_array(vars),
239                print_var_array(vars1)
240            ),
241            Constraint::WatchVecNeq(vars, vars1) => write!(
242                f,
243                "watchvecneq({},{})",
244                print_var_array(vars),
245                print_var_array(vars1)
246            ),
247            Constraint::WatchVecExistsLess(vars, vars1) => {
248                todo!("don't know how to print watchvecexistsless...")
249            }
250            Constraint::Hamming(vars, vars1, constant) => write!(
251                f,
252                "hamming({},{},{constant})",
253                print_var_array(vars),
254                print_var_array(vars1)
255            ),
256            Constraint::NotHamming(vars, vars1, constant) => {
257                todo!("don't know how to print nothamming...")
258            }
259            Constraint::FrameUpdate(vars, vars1, vars2, vars3, constant) => {
260                todo!("don't know how to print frame update...")
261            }
262            Constraint::NegativeTable(_, _)
263            | Constraint::Table(_, _)
264            | Constraint::GacSchema(_, _)
265            | Constraint::LightTable(_, _)
266            | Constraint::Mddc(_, _)
267            | Constraint::Str2Plus(_, _)
268            | Constraint::NegativeMddc(_, _) => {
269                todo!("tuples not properly implemented yet, so can't print them...")
270            }
271            Constraint::Max(vars, var) => write!(f, "max({},{var})", print_var_array(vars)),
272            Constraint::Min(vars, var) => write!(f, "min({},{var})", print_var_array(vars)),
273            Constraint::NvalueGeq(vars, var) => {
274                write!(f, "nvaluegeq({},{var})", print_var_array(vars))
275            }
276            Constraint::NvalueLeq(vars, var) => {
277                write!(f, "nvalueleq({},{var})", print_var_array(vars))
278            }
279            Constraint::SumLeq(vars, var) => write!(f, "sumleq({},{var})", print_var_array(vars)),
280            Constraint::SumGeq(vars, var) => write!(f, "sumgeq({},{var})", print_var_array(vars)),
281            Constraint::Element(vars, var, var1) => {
282                write!(f, "element({},{var},{var1})", print_var_array(vars))
283            }
284            Constraint::ElementOne(vars, var, var1) => {
285                write!(f, "element_one({},{var},{var1})", print_var_array(vars))
286            }
287            Constraint::ElementUndefZero(vars, var, var1) => write!(
288                f,
289                "element_undefzero({},{var},{var1})",
290                print_var_array(vars)
291            ),
292            Constraint::WatchElement(vars, var, var1) => {
293                write!(f, "watchelement({},{var},{var1})", print_var_array(vars))
294            }
295            Constraint::WatchElementUndefZero(vars, var, var1) => write!(
296                f,
297                "watchelement_undefzero({},{var},{var1})",
298                print_var_array(vars)
299            ),
300            Constraint::WatchElementOne(vars, var, var1) => write!(
301                f,
302                "watchelement_one({},{var},{var1})",
303                print_var_array(vars)
304            ),
305            Constraint::WatchElementOneUndefZero(vars, var, var1) => write!(
306                f,
307                "watchelement_one_undefzero({},{var},{var1})",
308                print_var_array(vars)
309            ),
310            Constraint::WLiteral(var, constant) => write!(f, "w-literal({var},{constant})"),
311            Constraint::WNotLiteral(var, constant) => write!(f, "w-notliteral({var},{constant})"),
312            Constraint::WInIntervalSet(var, constants) => {
313                write!(f, "w-inintervalset({var},{})", print_const_array(constants))
314            }
315            Constraint::WInRange(var, constants) => {
316                write!(f, "w-inrange({var},{})", print_const_array(constants))
317            }
318            Constraint::WNotInRange(var, constants) => {
319                write!(f, "w-notinrange({var},{})", print_const_array(constants))
320            }
321            Constraint::WInset(var, constants) => {
322                write!(f, "w-inset({var},{})", print_const_array(constants))
323            }
324            Constraint::WNotInset(var, constants) => {
325                write!(f, "w-notinset({var},{})", print_const_array(constants))
326            }
327            Constraint::Abs(var, var1) => write!(f, "abs({var},{var1})"),
328            Constraint::DisEq(var, var1) => write!(f, "diseq({var},{var1})"),
329            Constraint::Eq(var, var1) => write!(f, "eq({var},{var1})"),
330            Constraint::MinusEq(var, var1) => write!(f, "minuseq({var},{var1})"),
331            Constraint::GacEq(var, var1) => todo!("don't know how to print gaceq..."),
332            Constraint::WatchLess(var, var1) => write!(f, "watchless({var},{var1})"),
333            Constraint::WatchNeq(var, var1) => write!(f, "watchneq({var},{var1})"),
334            Constraint::Ineq(var, var1, constant) => write!(f, "ineq({var},{var1},{constant})"),
335            Constraint::False => write!(f, "false"),
336            Constraint::True => write!(f, "true"),
337        }
338    }
339}
340
341/// Representation of a Minion Variable.
342///
343/// A variable can either be a named variable, or an anomynous "constant as a variable".
344///
345/// The latter is not stored in the symbol table, or counted in Minions internal list of all
346/// variables, but is used to allow the use of a constant in the place of a variable in a
347/// constraint.
348#[derive(Debug, Clone, Eq, PartialEq)]
349pub enum Var {
350    NameRef(VarName),
351    ConstantAsVar(i32),
352}
353
354impl Display for Var {
355    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
356        match self {
357            Var::NameRef(n) => write!(f, "{n}"),
358            Var::ConstantAsVar(c) => write!(f, "{c}"),
359        }
360    }
361}
362/// Representation of a Minion constant.
363#[non_exhaustive]
364#[derive(Debug, Eq, PartialEq, Clone, Copy)]
365pub enum Constant {
366    Bool(bool),
367    Integer(i32),
368}
369
370impl Display for Constant {
371    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
372        match self {
373            Constant::Bool(true) => write!(f, "1"),
374            Constant::Bool(false) => write!(f, "0"),
375            Constant::Integer(i) => write!(f, "{i}"),
376        }
377    }
378}
379
380/// Representation of variable domains.
381#[derive(Debug, Copy, Clone, Eq, PartialEq)]
382#[non_exhaustive]
383pub enum VarDomain {
384    Bound(i32, i32),
385    Discrete(i32, i32),
386    // FIXME: should be a list of i32!
387    // we don't use this anyways, so commenting out for now...
388    // SparseBound(i32,i32),
389    Bool,
390}
391
392#[derive(Debug, Clone, Eq, PartialEq)]
393#[non_exhaustive]
394/// Stores all named variables in a Minion model alongside their domains.
395///
396/// Named variables referenced in [constraints](Constraint) must be in the symbol table for the
397/// model to be valid. In the future, this will raise some sort of type error.
398pub struct SymbolTable {
399    table: HashMap<VarName, VarDomain>,
400
401    // order of all variables
402    var_order: Vec<VarName>,
403
404    // search order
405    search_var_order: Vec<VarName>,
406}
407
408impl SymbolTable {
409    fn new() -> SymbolTable {
410        SymbolTable {
411            table: HashMap::new(),
412            var_order: Vec::new(),
413            search_var_order: Vec::new(),
414        }
415    }
416
417    /// Creates a new search variable and adds it to the symbol table.
418    ///
419    /// # Returns
420    ///
421    /// If a variable already exists with the given name, `None` is returned.
422    pub fn add_var(&mut self, name: VarName, vartype: VarDomain) -> Option<()> {
423        if self.table.contains_key(&name) {
424            return None;
425        }
426
427        self.table.insert(name.clone(), vartype);
428        self.var_order.push(name.clone());
429        self.search_var_order.push(name);
430
431        Some(())
432    }
433
434    /// Creates a new auxiliary variable and adds it to the symbol table.
435    ///
436    /// This variable will excluded from Minions search and printing order.
437    ///
438    /// # Returns
439    ///
440    /// If a variable already exists with the given name, `None` is returned.
441    pub fn add_aux_var(&mut self, name: VarName, vartype: VarDomain) -> Option<()> {
442        if self.table.contains_key(&name) {
443            return None;
444        }
445
446        self.table.insert(name.clone(), vartype);
447        self.var_order.push(name);
448
449        Some(())
450    }
451
452    /// Gets the domain of a named variable.
453    ///
454    /// # Returns
455    ///
456    /// `None` if no variable is known by that name.
457    pub fn get_vartype(&self, name: VarName) -> Option<VarDomain> {
458        self.table.get(&name).cloned()
459    }
460
461    /// Gets the canonical ordering of all variables.
462    pub fn get_variable_order(&self) -> Vec<VarName> {
463        self.var_order.clone()
464    }
465
466    /// Gets the canonical ordering of search variables (i.e excluding aux vars).
467    pub fn get_search_variable_order(&self) -> Vec<VarName> {
468        self.search_var_order.clone()
469    }
470
471    pub fn contains(&self, name: VarName) -> bool {
472        self.table.contains_key(&name)
473    }
474}
minion_rs/ast.rs

minion_rs/
ast.rs
