Function pcp::propagators::cmp::x_leq_y
source · pub fn x_leq_y<VStore, Domain, Bound>(
x: Var<VStore>,
y: Var<VStore>
) -> XLessEqY<VStore>where
VStore: VStoreConcept<Item = Domain> + 'static,
Domain: Collection<Item = Bound> + IntDomain,
Bound: IntBound,
Examples found in repository?
src/libpcp/search/branching/binary_split.rs (line 41)
32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
fn distribute(&mut self, space: Space<VStore, CStore, R>, var_idx: usize, val: Bound) ->
(<Space<VStore, CStore, R> as Freeze>::FrozenState, Vec<Branch<Space<VStore, CStore, R>>>)
{
// See notes in Enumerate::distribute.
Branch::distribute(space,
vec![
Box::new(move |space: &mut Space<VStore, CStore, R>| {
let x = Box::new(Identity::<Domain>::new(var_idx)) as Var<VStore>;
let v = Box::new(Constant::new(val)) as Var<VStore>;
let x_less_v = x_leq_y::<_,_,Bound>(x.bclone(), v.bclone());
space.cstore.alloc(Box::new(x_less_v));
}),
Box::new(move |space: &mut Space<VStore, CStore, R>| {
let x = Box::new(Identity::<Domain>::new(var_idx)) as Var<VStore>;
let v = Box::new(Constant::new(val)) as Var<VStore>;
let x_geq_v = x_greater_y(x, v);
space.cstore.alloc(Box::new(x_geq_v));
})
]
)
}
More examples
src/libpcp/propagators/cumulative.rs (line 76)
57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103
pub fn join<CStore>(&mut self, vstore: &mut VStore, cstore: &mut CStore) where
CStore: IntCStore<VStore> + 'static
{
let tasks = self.starts.len();
// Special case where only one task needs to be scheduled.
if tasks == 1 {
// c >= r[j]
cstore.alloc(Box::new(x_geq_y(self.capacity_var(), self.resource_at(0))));
}
else {
// forall( j in tasks ) (...)
for j in 0..tasks {
let mut resource_vars = vec![];
self.intermediate.push(vec![]);
for i in 0..tasks {
if i != j {
// conj <-> s[i] <= s[j] /\ s[j] < s[i] + d[i]
let conj = Box::new(Conjunction::new(vec![
// s[i] <= s[j]
Box::new(x_leq_y(self.start_at(i), self.start_at(j))),
// s[j] < s[i] + d[i]
Box::new(XLessYPlusZ::new(self.start_at(j), self.start_at(i), self.duration_at(i)))]));
// bi <-> conj
let bi = Boolean::new(vstore);
let equiv = equivalence(Box::new(bi.clone()), conj);
cstore.alloc(equiv);
// r = bi * r[i]
let ri = self.resource_at(i);
let ri_ub = ri.read(vstore).upper();
let r_dom = Domain::new(Bound::zero(), ri_ub);
// let hole = Domain::new(Bound::one(), ri_ub.clone() - Bound::one());
let r = vstore.alloc(r_dom);
self.intermediate.last_mut().unwrap().push(r.index());
let r = Box::new(r) as Var<VStore>;
cstore.alloc(Box::new(XEqYMulZ::new(r.bclone(), Box::new(bi), ri)));
resource_vars.push(r);
}
}
// sum( i in tasks where i != j )(...)
let sum = Box::new(Sum::new(resource_vars));
// c >= r[j] + sum
cstore.alloc(Box::new(x_geq_y_plus_z(self.capacity_var(), self.resource_at(j), sum)));
}
}
}