Add unification constraint.
This constraint unifies two variables. This is done by substituting one variable for another in all of the current constraints, resulting a new set of constraints. We would like to make the equality constraint perform the more general substitution: "coef1 var1 -> coef2 var2 + constant". While this constraint is less general, it can be used when the variables are not integer quantities.
This commit is contained in:
David Wang
parent
4a331fdc1a
commit
f265a165dd
@ -35,6 +35,8 @@ pub trait Constraint {
|
||||
|
||||
pub use self::alldifferent::AllDifferent;
|
||||
pub use self::equality::Equality;
|
||||
pub use self::unify::Unify;
|
||||
|
||||
mod alldifferent;
|
||||
mod equality;
|
||||
mod unify;
|
||||
|
||||
109
src/constraint/unify.rs
Normal file
109
src/constraint/unify.rs
Normal file
@ -0,0 +1,109 @@
|
||||
//! Unify implementation.
|
||||
|
||||
use std::iter;
|
||||
use std::rc::Rc;
|
||||
|
||||
use ::{Constraint,PsResult,PuzzleSearch,VarToken};
|
||||
|
||||
pub struct Unify {
|
||||
var1: VarToken,
|
||||
var2: VarToken,
|
||||
}
|
||||
|
||||
impl Unify {
|
||||
/// Allocate a new Unify constraint.
|
||||
///
|
||||
/// # Examples
|
||||
///
|
||||
/// ```
|
||||
/// let mut send_more_money = puzzle_solver::Puzzle::new();
|
||||
/// let carry = send_more_money.new_vars_with_candidates_1d(4, &[0,1]);
|
||||
/// let vars = send_more_money.new_vars_with_candidates_1d(8,
|
||||
/// &[0,1,2,3,4,5,6,7,8,9]);
|
||||
///
|
||||
/// let m = vars[4];
|
||||
/// puzzle_solver::constraint::Unify::new(m, carry[3]);
|
||||
/// ```
|
||||
pub fn new(var1: VarToken, var2: VarToken) -> Self {
|
||||
Unify {
|
||||
var1: var1,
|
||||
var2: var2,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Constraint for Unify {
|
||||
fn vars<'a>(&'a self) -> Box<Iterator<Item=&'a VarToken> + 'a> {
|
||||
if self.var1 != self.var2 {
|
||||
Box::new(iter::once(&self.var1).chain(iter::once(&self.var2)))
|
||||
} else {
|
||||
Box::new(iter::empty())
|
||||
}
|
||||
}
|
||||
|
||||
fn on_updated(&self, search: &mut PuzzleSearch) -> PsResult<()> {
|
||||
if self.var1 != self.var2 {
|
||||
search.unify(self.var1, self.var2)
|
||||
} else {
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
fn substitute(&self, from: VarToken, to: VarToken)
|
||||
-> PsResult<Rc<Constraint>> {
|
||||
let var1 = if self.var1 == from { to } else { self.var1 };
|
||||
let var2 = if self.var2 == from { to } else { self.var2 };
|
||||
Ok(Rc::new(Unify{ var1: var1, var2: var2 }))
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use ::Puzzle;
|
||||
use super::Unify;
|
||||
|
||||
#[test]
|
||||
fn test_unify_alldifferent() {
|
||||
let mut puzzle = Puzzle::new();
|
||||
let v0 = puzzle.new_var_with_candidates(&[1,2]);
|
||||
let v1 = puzzle.new_var_with_candidates(&[1,2]);
|
||||
|
||||
puzzle.all_different(&[v0, v1]);
|
||||
puzzle.add_constraint(Unify::new(v0, v1));
|
||||
|
||||
let search = puzzle.step();
|
||||
assert!(search.is_none());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_unify_equality() {
|
||||
let mut puzzle = Puzzle::new();
|
||||
let v0 = puzzle.new_var_with_candidates(&[1,2,3,4]);
|
||||
let v1 = puzzle.new_var_with_candidates(&[1,2,3,4]);
|
||||
let v2 = puzzle.new_var_with_candidates(&[1,2,3,4]);
|
||||
|
||||
puzzle.equals(v0 + 2 * v1 + v2, 6);
|
||||
puzzle.add_constraint(Unify::new(v0, v1));
|
||||
|
||||
let search = puzzle.step().expect("contradiction");
|
||||
assert_eq!(search[v0], 1);
|
||||
assert_eq!(search[v1], 1);
|
||||
assert_eq!(search[v2], 3);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_unify_unify() {
|
||||
let mut puzzle = Puzzle::new();
|
||||
let v0 = puzzle.new_var_with_candidates(&[1]);
|
||||
let v1 = puzzle.new_var_with_candidates(&[1,2,3,4]);
|
||||
let v2 = puzzle.new_var_with_candidates(&[1,2,3,4]);
|
||||
|
||||
puzzle.add_constraint(Unify::new(v0, v1));
|
||||
puzzle.add_constraint(Unify::new(v1, v2));
|
||||
|
||||
let search = puzzle.step().expect("contradiction");
|
||||
assert_eq!(search[v0], 1);
|
||||
assert_eq!(search[v1], 1);
|
||||
assert_eq!(search[v2], 1);
|
||||
}
|
||||
}
|
||||
124
src/puzzle.rs
124
src/puzzle.rs
@ -25,6 +25,7 @@ enum Candidates {
|
||||
enum VarState {
|
||||
Assigned(Val),
|
||||
Unassigned(Candidates),
|
||||
Unified(VarToken),
|
||||
}
|
||||
|
||||
/// The puzzle to be solved.
|
||||
@ -442,6 +443,24 @@ impl PuzzleConstraints {
|
||||
}
|
||||
}
|
||||
|
||||
/// Create a new puzzle constraint container reflecting the
|
||||
/// substitution of "from" with "to".
|
||||
fn substitute(&self, from: VarToken, to: VarToken) -> PsResult<Self> {
|
||||
let VarToken(idx) = from;
|
||||
let mut new_constraints = self.constraints.clone();
|
||||
|
||||
for cidx in self.wake[idx].iter() {
|
||||
let rc = try!(self.constraints[cidx].substitute(from, to));
|
||||
new_constraints[cidx] = rc;
|
||||
}
|
||||
|
||||
let wake = Self::init_wake(&new_constraints, self.wake.len());
|
||||
Ok(PuzzleConstraints {
|
||||
constraints: new_constraints,
|
||||
wake: wake,
|
||||
})
|
||||
}
|
||||
|
||||
/// Determine which variables wake up which constraints.
|
||||
fn init_wake(constraints: &Vec<Rc<Constraint>>, num_vars: usize)
|
||||
-> Vec<BitSet> {
|
||||
@ -484,6 +503,7 @@ impl<'a> PuzzleSearch<'a> {
|
||||
match &self.vars[idx] {
|
||||
&VarState::Assigned(_) => true,
|
||||
&VarState::Unassigned(_) => false,
|
||||
&VarState::Unified(other) => self.is_assigned(other),
|
||||
}
|
||||
}
|
||||
|
||||
@ -496,6 +516,7 @@ impl<'a> PuzzleSearch<'a> {
|
||||
match &self.vars[idx] {
|
||||
&VarState::Assigned(val) => Some(val),
|
||||
&VarState::Unassigned(_) => None,
|
||||
&VarState::Unified(other) => self.get_assigned(other),
|
||||
}
|
||||
}
|
||||
|
||||
@ -506,6 +527,7 @@ impl<'a> PuzzleSearch<'a> {
|
||||
match &self.vars[idx] {
|
||||
&VarState::Assigned(_) => Box::new(iter::empty()),
|
||||
&VarState::Unassigned(ref cs) => cs.iter(),
|
||||
&VarState::Unified(other) => self.get_unassigned(other),
|
||||
}
|
||||
}
|
||||
|
||||
@ -523,6 +545,7 @@ impl<'a> PuzzleSearch<'a> {
|
||||
.ok_or(())
|
||||
}
|
||||
},
|
||||
&VarState::Unified(other) => self.get_min_max(other),
|
||||
}
|
||||
}
|
||||
|
||||
@ -538,9 +561,12 @@ impl<'a> PuzzleSearch<'a> {
|
||||
&Candidates::Value(v) => return bool_to_result(v == val),
|
||||
&Candidates::Set(_) => (),
|
||||
},
|
||||
&VarState::Unified(_) => (),
|
||||
}
|
||||
|
||||
if let &mut VarState::Unassigned(Candidates::Set(ref mut rc))
|
||||
if let &VarState::Unified(other) = &self.vars[idx] {
|
||||
self.set_candidate(other, val)
|
||||
} else if let &mut VarState::Unassigned(Candidates::Set(ref mut rc))
|
||||
= &mut self.vars[idx] {
|
||||
if rc.contains(&val) {
|
||||
let mut set = Rc::make_mut(rc);
|
||||
@ -568,9 +594,12 @@ impl<'a> PuzzleSearch<'a> {
|
||||
&Candidates::Value(v) => return bool_to_result(v != val),
|
||||
&Candidates::Set(_) => (),
|
||||
},
|
||||
&VarState::Unified(_) => (),
|
||||
}
|
||||
|
||||
if let &mut VarState::Unassigned(Candidates::Set(ref mut rc))
|
||||
if let &VarState::Unified(other) = &self.vars[idx] {
|
||||
self.remove_candidate(other, val)
|
||||
} else if let &mut VarState::Unassigned(Candidates::Set(ref mut rc))
|
||||
= &mut self.vars[idx] {
|
||||
if rc.contains(&val) {
|
||||
let mut set = Rc::make_mut(rc);
|
||||
@ -605,9 +634,12 @@ impl<'a> PuzzleSearch<'a> {
|
||||
},
|
||||
&Candidates::Set(_) => (),
|
||||
},
|
||||
&VarState::Unified(_) => (),
|
||||
}
|
||||
|
||||
if let &mut VarState::Unassigned(Candidates::Set(ref mut rc))
|
||||
if let &VarState::Unified(other) = &self.vars[idx] {
|
||||
self.bound_candidate_range(other, min, max)
|
||||
} else if let &mut VarState::Unassigned(Candidates::Set(ref mut rc))
|
||||
= &mut self.vars[idx] {
|
||||
let &curr_min = rc.iter().min().expect("candidates");
|
||||
let &curr_max = rc.iter().max().expect("candidates");
|
||||
@ -640,8 +672,8 @@ impl<'a> PuzzleSearch<'a> {
|
||||
|
||||
let next_unassigned = self.vars.iter().enumerate().min_by_key(
|
||||
|&(_, vs)| match vs {
|
||||
&VarState::Assigned(_) => ::std::usize::MAX,
|
||||
&VarState::Unassigned(ref cs) => cs.len(),
|
||||
_ => ::std::usize::MAX,
|
||||
});
|
||||
|
||||
if let Some((idx, &VarState::Unassigned(ref cs))) = next_unassigned {
|
||||
@ -667,13 +699,8 @@ impl<'a> PuzzleSearch<'a> {
|
||||
}
|
||||
} else {
|
||||
// No unassigned variables remaining.
|
||||
let mut vars = Vec::with_capacity(self.puzzle.num_vars);
|
||||
for var in self.vars.iter() {
|
||||
match var {
|
||||
&VarState::Assigned(val) => vars.push(val),
|
||||
&VarState::Unassigned(_) => unreachable!(),
|
||||
}
|
||||
}
|
||||
let vars = (0..self.puzzle.num_vars).map(|idx|
|
||||
self[VarToken(idx)]).collect();
|
||||
solutions.push(Solution{ vars: vars });
|
||||
}
|
||||
}
|
||||
@ -712,7 +739,8 @@ impl<'a> PuzzleSearch<'a> {
|
||||
0 => return Err(()),
|
||||
1 => cs.iter().next(),
|
||||
_ => None,
|
||||
}
|
||||
},
|
||||
&VarState::Unified(_) => None,
|
||||
};
|
||||
|
||||
if let Some(val) = gimme {
|
||||
@ -737,6 +765,62 @@ impl<'a> PuzzleSearch<'a> {
|
||||
|
||||
Ok(())
|
||||
}
|
||||
|
||||
/// Unify the "from" variable with the "to" variable.
|
||||
pub fn unify(&mut self, from: VarToken, to: VarToken)
|
||||
-> PsResult<()> {
|
||||
if from == to {
|
||||
return Ok(());
|
||||
}
|
||||
|
||||
// Some preliminary checks, and maybe swap "from" and "to" in
|
||||
// order to simplify our logic.
|
||||
let (from, to) = {
|
||||
let VarToken(search) = from;
|
||||
let VarToken(replace) = to;
|
||||
match (&self.vars[search], &self.vars[replace]) {
|
||||
(&VarState::Assigned(val1), &VarState::Assigned(val2)) =>
|
||||
return bool_to_result(val1 == val2),
|
||||
|
||||
// Unified variables should have been substituted out previously.
|
||||
(&VarState::Unified(_), _) | (_, &VarState::Unified(_)) =>
|
||||
panic!("internal representation corrupt"),
|
||||
|
||||
(&VarState::Unassigned(_), &VarState::Assigned(_)) =>
|
||||
(to, from),
|
||||
|
||||
(&VarState::Assigned(_), &VarState::Unassigned(_))
|
||||
| (&VarState::Unassigned(_), &VarState::Unassigned(_)) =>
|
||||
(from, to),
|
||||
}
|
||||
};
|
||||
|
||||
let VarToken(search) = from;
|
||||
let VarToken(replace) = to;
|
||||
|
||||
// Create new constraints to reflect the unification.
|
||||
let new_constraints = try!(self.constraints.substitute(from, to));
|
||||
self.constraints = Rc::new(new_constraints);
|
||||
self.wake.union_with(&self.constraints.wake[replace]);
|
||||
assert!(self.constraints.wake[search].is_empty());
|
||||
|
||||
// Take intersection of the candidates.
|
||||
if let &VarState::Assigned(val) = &self.vars[search] {
|
||||
try!(self.set_candidate(to, val));
|
||||
} else {
|
||||
if let (&mut VarState::Unassigned(Candidates::Set(ref mut rc1)),
|
||||
&mut VarState::Unassigned(Candidates::Set(ref mut rc2)))
|
||||
= get_two_mut(&mut self.vars, search, replace) {
|
||||
*rc2 = Rc::new(rc2.intersection(rc1).cloned().collect());
|
||||
if rc2.is_empty() {
|
||||
return Err(());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
self.vars[search] = VarState::Unified(to);
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl<'a> fmt::Debug for PuzzleSearch<'a> {
|
||||
@ -754,6 +838,9 @@ impl<'a> fmt::Debug for PuzzleSearch<'a> {
|
||||
write!(f, " {}", val)?;
|
||||
}
|
||||
},
|
||||
&VarState::Unified(VarToken(other)) => {
|
||||
write!(f, " var {}: var {}", idx, other)?;
|
||||
},
|
||||
}
|
||||
}
|
||||
write!(f, "}}")?;
|
||||
@ -774,6 +861,7 @@ impl<'a> Index<VarToken> for PuzzleSearch<'a> {
|
||||
match &self.vars[idx] {
|
||||
&VarState::Assigned(ref val) => val,
|
||||
&VarState::Unassigned(_) => panic!("unassigned"),
|
||||
&VarState::Unified(other) => &self[other],
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -786,6 +874,18 @@ fn bool_to_result(cond: bool) -> PsResult<()> {
|
||||
}
|
||||
}
|
||||
|
||||
fn get_two_mut<'a, T>(slice: &'a mut [T], a: usize, b: usize)
|
||||
-> (&'a mut T, &'a mut T) {
|
||||
assert!(a != b);
|
||||
if a < b {
|
||||
let (mut l, mut r) = slice.split_at_mut(b);
|
||||
(&mut l[a], &mut r[0])
|
||||
} else {
|
||||
let (l, r) = slice.split_at_mut(a);
|
||||
(&mut r[0], &mut l[b])
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use ::Puzzle;
|
||||
|
||||
Loading…
Reference in New Issue
Block a user