Permalink
Browse files

first attempt for constraint decomposition

  • Loading branch information...
Philippe Delrieu Philippe Delrieu
Philippe Delrieu authored and Philippe Delrieu committed Nov 2, 2016
1 parent e2d2b96 commit eab2aee3fd6e5c19c82fcc1193ac80aec2673968
Showing with 37 additions and 38 deletions.
  1. +1 −0 .gitignore
  2. +1 −0 src/libpcp/lib.rs
  3. +34 −38 src/libpcp/propagators/cumulative.rs
  4. +1 −0 src/libpcp/propagators/mod.rs
View
@@ -3,6 +3,7 @@
*.so
*.rlib
*.dll
*.DS_Store
# Executables
*.exe
View
@@ -18,6 +18,7 @@
#![crate_type = "dylib"]
#![feature(alloc, unboxed_closures, fnbox, fn_traits)]
#![feature(question_mark)]
#![feature(test)]
extern crate test;
@@ -15,14 +15,18 @@
use kernel::*;
use kernel::Trilean::*;
use propagators::PropagatorKind;
use propagators::cmp::{x_leq_y, XLessYPlusZ};
use propagation::*;
use propagation::events::*;
use term::ops::*;
use gcollections::ops::*;
use std::fmt::{Formatter, Debug, Error};
use num::traits::Num;
use std::ops::{Add, Sub};
//use propagation::CStoreFD;
pub type CStore<VStore> = CStoreFD<VStore>;
#[derive(Clone)]
pub struct Cumulative<V>
{
starts: Vec<V>,
@@ -33,9 +37,9 @@ pub struct Cumulative<V>
impl<V> PropagatorKind for Cumulative<V> {}
impl<V> Cumulative<V> {
impl<V> Cumulative<V> where V: Clone {
pub fn new(starts: Vec<V>, durations: Vec<usize>, resources: Vec<usize>, capacity: usize) -> Cumulative<V> {
Cumulative { starts: starts, durations: durations, resources: resources, capacity: capacity }
Cumulative { starts: starts, durations: durations, resources: resources, capacity: capacity}
}
}
@@ -47,24 +51,24 @@ impl<V> Debug for Cumulative<V> where
}
}
impl<Store, B, DomV, V> Subsumption<Store> for Cumulative<V> where
V: StoreRead<Store, Value=DomV>,
DomV: Bounded<Bound=B> + Debug,
B: PartialOrd + Num
impl<Store, DomV, V> Subsumption<Store> for Cumulative<V> where
V: StoreRead<Store, Value=DomV> + Clone + Debug,
DomV: Bounded + Disjoint + Debug + Add + Sub + Clone,
{
fn is_subsumed(&self, store: &Store) -> Trilean {
let starts = self.starts.read(store);
if x.upper() <= y.lower() + z.lower() {
False
}
else if x.lower() > y.upper() + z.upper() {
True
}
else {
Unknown
let mut cstore = CStore::empty();
for j in 0..self.starts.len() - 1 {
for i in 0..self.starts.len() - 1 {
if i != j {
// `s[i] <= s[j] /\ s[j] < s[i] + d[i]`
cstore.alloc(x_leq_y(self.starts[i].clone(), self.starts[j].clone()));
cstore.alloc(XLessYPlusZ::new(self.starts[j].clone(), self.starts[i].clone(), self.durations[i].clone()));
}
}
}
cstore.is_subsumed(store)
}
}
@@ -74,24 +78,16 @@ impl<Store, B, DomV, V> Propagator<Store> for Cumulative<V> where
B: PartialOrd + Num,
{
fn propagate(&mut self, store: &mut Store) -> bool {
let x = self.x.read(store);
let y = self.y.read(store);
let z = self.z.read(store);
self.x.update(store, x.strict_shrink_left(y.lower() + z.lower())) &&
self.y.update(store, y.strict_shrink_right(x.upper() - z.lower())) &&
self.z.update(store, z.strict_shrink_right(x.upper() - y.lower()))
}
}
impl<X, Y, Z> PropagatorDependencies<FDEvent> for XGreaterYPlusZ<X, Y, Z> where
X: ViewDependencies<FDEvent>,
Y: ViewDependencies<FDEvent>,
Z: ViewDependencies<FDEvent>
impl<V> PropagatorDependencies<FDEvent> for Cumulative<V> where
V: ViewDependencies<FDEvent>
{
fn dependencies(&self) -> Vec<(usize, FDEvent)> {
let mut deps = self.x.dependencies(FDEvent::Bound);
deps.append(&mut self.y.dependencies(FDEvent::Bound));
deps.append(&mut self.z.dependencies(FDEvent::Bound));
let mut deps = self.starts.iter().flat_map(|v| v.dependencies(FDEvent::Bound)).collect();
deps.append(self.durations.iter().flat_map(|v| v.dependencies(FDEvent::Bound)).collect());
deps.append(self.resources.iter().flat_map(|v| v.dependencies(FDEvent::Bound)).collect());
deps
}
}
@@ -107,7 +103,7 @@ mod test {
use propagators::test::*;
#[test]
fn x_greater_y_plus_z_test() {
fn cumulative_test() {
let dom0_10 = (0,10).to_interval();
let dom10_20 = (10,20).to_interval();
let dom10_11 = (10,11).to_interval();
@@ -118,21 +114,21 @@ mod test {
let dom1_1 = (1,1).to_interval();
let dom2_2 = (2,2).to_interval();
x_greater_y_plus_z_test_one(1, dom0_10, dom0_10, dom0_10,
culmulative_test_one(1, dom0_10, dom0_10, dom0_10,
Unknown, Unknown, vec![(0, Bound), (1, Bound), (2, Bound)], true);
x_greater_y_plus_z_test_one(2, dom10_11, dom5_15, dom5_15,
culmulative_test_one(2, dom10_11, dom5_15, dom5_15,
Unknown, True, vec![(0, Assignment), (1, Assignment), (2, Assignment)], true);
x_greater_y_plus_z_test_one(3, dom10_20, dom1_1, dom1_1,
culmulative_test_one(3, dom10_20, dom1_1, dom1_1,
True, True, vec![], true);
x_greater_y_plus_z_test_one(4, dom1_1, dom1_1, dom1_1,
culmulative_test_one(4, dom1_1, dom1_1, dom1_1,
False, False, vec![], false);
x_greater_y_plus_z_test_one(5, dom2_2, dom1_1, dom1_1,
culmulative_test_one(5, dom2_2, dom1_1, dom1_1,
False, False, vec![], false);
x_greater_y_plus_z_test_one(6, dom6_10, dom5_10, dom1_10,
culmulative_test_one(6, dom6_10, dom5_10, dom1_10,
Unknown, Unknown, vec![(0, Bound), (1, Bound), (2, Bound)], true);
}
fn x_greater_y_plus_z_test_one(test_num: u32,
fn culmulative_test_one(test_num: u32,
x: Interval<i32>, y: Interval<i32>, z: Interval<i32>,
before: Trilean, after: Trilean,
delta_expected: Vec<(usize, FDEvent)>, propagate_success: bool)
@@ -18,6 +18,7 @@
pub mod cmp;
pub mod distinct;
pub mod cumulative;
pub use propagators::cmp::*;
pub use propagators::distinct::*;

0 comments on commit eab2aee

Please sign in to comment.