Function pcp::propagators::cmp::x_geq_y_plus_z

source · 
pub fn x_geq_y_plus_z<VStore, Domain, Bound>(
    x: Var<VStore>,
    y: Var<VStore>,
    z: Var<VStore>
) -> XGreaterEqYPlusZ<VStore>where
    VStore: VStoreConcept<Item = Domain> + 'static,
    Domain: Collection<Item = Bound> + IntDomain,
    Bound: IntBound,
Examples found in repository?
src/libpcp/propagators/cmp/x_less_y_plus_z.rs (line 67)
66
67
68

  fn not(&self) -> Formula<VStore> {
    Box::new(x_geq_y_plus_z(self.x.bclone(), self.y.bclone(), self.z.bclone()))
  }
More examples
Hide additional examples
src/libpcp/propagators/cmp/x_eq_y_plus_z.rs (line 39)
37
38
39
40
41
42

  pub fn new(x: Var<VStore>, y: Var<VStore>, z: Var<VStore>) -> Self {
    XEqYPlusZ {
      geq: x_geq_y_plus_z(x.bclone(), y.bclone(), z.bclone()),
      leq: x_leq_y_plus_z(x, y, z)
    }
  }
src/libpcp/propagators/cumulative.rs (line 100)
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)));
      }
    }
  }