Skip to content

Commit

Permalink
refactor(lin sum): replace or_zero by a lit
Browse files Browse the repository at this point in the history
  • Loading branch information
@Shi-Raida
Shi-Raida committed Jun 15, 2023
1 parent 1902456 commit 730e347
Show file tree
Hide file tree
Showing 7 changed files with 50 additions and 52 deletions.
4 changes: 2 additions & 2 deletions examples/knapsack/main.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -164,7 +164,7 @@ fn solve_optional(pb: &Pb) -> Sol {
prez,
format!("{}_weight", pb.items[i].name),
)
.or_zero()
.with_lit(prez)
})
.collect();
let value_vars: Vec<_> = presence_vars
Expand All @@ -179,7 +179,7 @@ fn solve_optional(pb: &Pb) -> Sol {
prez,
format!("{}_value", pb.items[i].name),
)
.or_zero()
.with_lit(prez)
})
.collect();

Expand Down
4 changes: 2 additions & 2 deletions planning/planners/src/encode.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -438,7 +438,7 @@ pub fn add_metric(pb: &FiniteProblem, model: &mut Model, metric: Metric) -> IAto
.map(|(ch_id, p)| {
model
.new_optional_ivar(1, 1, *p, Container::Instance(*ch_id).var(VarType::Cost))
.or_zero()
.with_lit(*p)
})
.collect();
let action_costs = LinearSum::of(action_costs);
Expand Down Expand Up @@ -466,7 +466,7 @@ pub fn add_metric(pb: &FiniteProblem, model: &mut Model, metric: Metric) -> IAto
.map(|&(ch_id, p, cost)| {
model
.new_optional_ivar(cost, cost, p, Container::Instance(ch_id).var(VarType::Cost))
.or_zero()
.with_lit(p)
})
.collect();
let action_costs = LinearSum::of(action_costs);
Expand Down
2 changes: 1 addition & 1 deletion planning/planning/src/chronicles/concrete.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ pub trait Substitution {
}

fn sub_linear_term(&self, term: &LinearTerm) -> LinearTerm {
LinearTerm::new(term.factor(), self.sub_ivar(term.var()), term.is_or_zero())
LinearTerm::new(term.factor(), self.sub_ivar(term.var()), term.lit())
}

fn sub_linear_sum(&self, sum: &LinearSum) -> LinearSum {
Expand Down
6 changes: 3 additions & 3 deletions solver/src/model/lang/int.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,8 +37,8 @@ impl IVar {
Lit::gt(self, i)
}

pub fn or_zero(self) -> LinearTerm {
LinearTerm::new(1, self, true)
pub fn with_lit(self, lit: Lit) -> LinearTerm {
LinearTerm::new(1, self, lit)
}
}

Expand Down Expand Up @@ -197,6 +197,6 @@ impl std::ops::Mul<IntCst> for IVar {
type Output = LinearTerm;

fn mul(self, rhs: IntCst) -> Self::Output {
LinearTerm::new(rhs, self, false)
LinearTerm::new(rhs, self, Lit::TRUE)
}
}
56 changes: 28 additions & 28 deletions solver/src/model/lang/linear.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,26 +10,26 @@ use std::collections::BTreeMap;
pub struct LinearTerm {
factor: IntCst,
var: IVar,
/// If true, then this term should be interpreted as zero if the variable is absent.
or_zero: bool,
/// If true, then the variable should be present. Otherwise, the term is ignored.
lit: Lit,
denom: IntCst,
}

impl LinearTerm {
pub const fn new(factor: IntCst, var: IVar, or_zero: bool) -> LinearTerm {
pub const fn new(factor: IntCst, var: IVar, lit: Lit) -> LinearTerm {
LinearTerm {
factor,
var,
or_zero,
lit,
denom: 1,
}
}

pub fn or_zero(self) -> Self {
pub fn with_lit(&self, lit: Lit) -> Self {
LinearTerm {
factor: self.factor,
var: self.var,
or_zero: true,
lit,
denom: self.denom,
}
}
Expand All @@ -42,8 +42,8 @@ impl LinearTerm {
self.factor
}

pub fn is_or_zero(&self) -> bool {
self.or_zero
pub fn lit(&self) -> Lit {
self.lit
}

pub fn var(&self) -> IVar {
Expand All @@ -53,7 +53,7 @@ impl LinearTerm {

impl From<IVar> for LinearTerm {
fn from(var: IVar) -> Self {
LinearTerm::new(1, var, false)
LinearTerm::new(1, var, Lit::TRUE)
}
}

Expand All @@ -64,7 +64,7 @@ impl std::ops::Neg for LinearTerm {
LinearTerm {
factor: -self.factor,
var: self.var,
or_zero: self.or_zero,
lit: self.lit,
denom: self.denom,
}
}
Expand Down Expand Up @@ -175,7 +175,7 @@ impl From<FAtom> for LinearSum {
terms: vec![LinearTerm {
factor: 1,
var: value.num.var,
or_zero: false,
lit: Lit::TRUE,
denom: value.denom,
}],
constant: value.num.shift,
Expand All @@ -190,7 +190,7 @@ impl From<IAtom> for LinearSum {
terms: vec![LinearTerm {
factor: 1,
var: value.var,
or_zero: false,
lit: Lit::TRUE,
denom: 1,
}],
constant: value.shift,
Expand Down Expand Up @@ -265,15 +265,15 @@ impl From<LinearLeq> for ReifExpr {
let mut vars = BTreeMap::new();
for e in &value.sum.terms {
let var = VarRef::from(e.var);
let key = (var, e.or_zero);
let key = (var, e.lit);
vars.entry(key)
.and_modify(|factor| *factor += e.factor)
.or_insert(e.factor);
}
ReifExpr::Linear(NFLinearLeq {
sum: vars
.iter()
.map(|(&(var, or_zero), &factor)| NFLinearSumItem { var, factor, or_zero })
.map(|(&(var, lit), &factor)| NFLinearSumItem { var, factor, lit })
.collect(),
upper_bound: value.ub - value.sum.constant,
})
Expand All @@ -284,8 +284,8 @@ impl From<LinearLeq> for ReifExpr {
pub struct NFLinearSumItem {
pub var: VarRef,
pub factor: IntCst,
/// If true, the this term should be interpreted as zero if the variable is absent.
pub or_zero: bool,
/// If true, then the variable should be present. Otherwise, the term is ignored.
pub lit: Lit,
}

impl std::ops::Neg for NFLinearSumItem {
Expand All @@ -295,7 +295,7 @@ impl std::ops::Neg for NFLinearSumItem {
NFLinearSumItem {
var: self.var,
factor: -self.factor,
or_zero: self.or_zero,
lit: self.lit,
}
}
}
Expand All @@ -312,19 +312,19 @@ impl NFLinearLeq {
let required_presence: Vec<Lit> = self
.sum
.iter()
.filter(|item| !item.or_zero)
.filter(|item| item.lit == Lit::TRUE)
.map(|item| presence(item.var))
.collect();
ValidityScope::new(required_presence, [])
}

/// Returns a new `NFLinearLeq` without the items of the sum with a null `factor` or the `variable` ZERO.
pub(crate) fn simplify(&self) -> NFLinearLeq {
// Group the terms by their `variable` and `or_zero` attribute
// Group the terms by their `variable` and `lit` attribute
let mut sum_map = BTreeMap::new();
for term in &self.sum {
sum_map
.entry((term.or_zero, term.var))
.entry((term.lit, term.var))
.and_modify(|f| *f += term.factor)
.or_insert(term.factor);
}
Expand All @@ -336,7 +336,7 @@ impl NFLinearLeq {
.map(|((z, v), f)| NFLinearSumItem {
var: v,
factor: f,
or_zero: z,
lit: z,
})
.collect(),
upper_bound: self.upper_bound,
Expand Down Expand Up @@ -471,32 +471,32 @@ mod tests {
NFLinearSumItem {
var: VarRef::ZERO,
factor: 1,
or_zero: false,
lit: Lit::TRUE,
},
NFLinearSumItem {
var: var1,
factor: 0,
or_zero: false,
lit: Lit::TRUE,
},
NFLinearSumItem {
var: var1,
factor: 1,
or_zero: false,
lit: Lit::TRUE,
},
NFLinearSumItem {
var: var1,
factor: -1,
or_zero: false,
lit: Lit::TRUE,
},
NFLinearSumItem {
var: var2,
factor: 1,
or_zero: false,
lit: Lit::TRUE,
},
NFLinearSumItem {
var: var2,
factor: -2,
or_zero: false,
lit: Lit::TRUE,
},
],
upper_bound: 5,
Expand All @@ -505,7 +505,7 @@ mod tests {
sum: vec![NFLinearSumItem {
var: var2,
factor: -1,
or_zero: false,
lit: Lit::TRUE,
}],
upper_bound: 5,
};
Expand Down
28 changes: 13 additions & 15 deletions solver/src/reasoners/cp/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,8 @@ use std::collections::HashMap;
struct SumElem {
factor: IntCst,
var: VarRef,
// if true, this element should be evaluated to zero if the variable is empty.
or_zero: bool,
/// If true, then the variable should be present. Otherwise, the term is ignored.
lit: Lit,
}

#[derive(Clone, Debug)]
Expand All @@ -31,7 +31,7 @@ struct LinearSumLeq {

impl LinearSumLeq {
fn get_lower_bound(&self, elem: SumElem, domains: &Domains) -> IntCst {
debug_assert!(elem.or_zero || domains.present(elem.var) == Some(true));
debug_assert!(!domains.entails(elem.lit) || domains.present(elem.var) == Some(true));
let int_part = match elem.factor.cmp(&0) {
Ordering::Less => domains
.ub(elem.var)
Expand All @@ -50,7 +50,7 @@ impl LinearSumLeq {
}
}
fn get_upper_bound(&self, elem: SumElem, domains: &Domains) -> IntCst {
debug_assert!(elem.or_zero || domains.present(elem.var) == Some(true));
debug_assert!(!domains.entails(elem.lit) || domains.present(elem.var) == Some(true));
let int_part = match elem.factor.cmp(&0) {
Ordering::Less => domains
.lb(elem.var)
Expand All @@ -69,7 +69,7 @@ impl LinearSumLeq {
}
}
fn set_ub(&self, elem: SumElem, ub: IntCst, domains: &mut Domains, cause: Cause) -> Result<bool, InvalidUpdate> {
debug_assert!(elem.or_zero || domains.present(elem.var) == Some(true));
debug_assert!(!domains.entails(elem.lit) || domains.present(elem.var) == Some(true));
// println!(
// " {:?} : [{}, {}] ub: {ub} -> {}",
// elem.var,
Expand Down Expand Up @@ -111,9 +111,9 @@ impl Propagator for LinearSumLeq {
Ordering::Equal => {}
Ordering::Greater => context.add_watch(SignedVar::minus(e.var), id),
}
if e.or_zero {
// TODO: watch presence
}
// if e.or_zero {
// TODO: watch presence
// }
}
}
fn propagate(&self, domains: &mut Domains, cause: Cause) -> Result<(), Contradiction> {
Expand Down Expand Up @@ -166,12 +166,10 @@ impl Propagator for LinearSumLeq {
Ordering::Greater => out_explanation.push(Lit::geq(e.var, domains.lb(e.var))),
}
}
if e.or_zero {
let prez = domains.presence(e.var);
// println!("{prez:?}, {:?}", domains.value(prez));
match domains.value(prez) {
Some(true) => out_explanation.push(prez),
Some(false) => out_explanation.push(!prez),
if e.lit != Lit::TRUE {
match domains.value(e.lit) {
Some(true) => out_explanation.push(e.lit),
Some(false) => out_explanation.push(!e.lit),
_ => {}
}
}
Expand Down Expand Up @@ -277,7 +275,7 @@ impl Cp {
.map(|e| SumElem {
factor: e.factor,
var: e.var,
or_zero: e.or_zero,
lit: e.lit,
})
.collect();
let propagator = LinearSumLeq {
Expand Down
2 changes: 1 addition & 1 deletion solver/src/reif/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ impl ReifExpr {
for term in &lin.sum {
if prez(term.var) {
sum += value(term.var) * term.factor
} else if !term.or_zero {
} else if term.lit == Lit::TRUE {
return None;
}
}
Expand Down

0 comments on commit 730e347

Please sign in to comment.