Skip to content

Commit

Permalink
Merge pull request #159 from plaans/assumptions
Browse files Browse the repository at this point in the history 
Assumption solving
  • Loading branch information
@arbimo
arbimo authored Jan 9, 2025
2 parents b1b7af3 + c0efeaa commit e38372d
Show file tree
Hide file tree
Showing 11 changed files with 595 additions and 93 deletions.
28 changes: 15 additions & 13 deletions examples/smt/tests/smt.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,7 @@ fn minimize() {

let mut solver = Solver::new(model);
assert!(solver.solve().unwrap().is_some());
solver.reset();
match solver.minimize(c).unwrap() {
None => panic!(),
Some((val, _)) => assert_eq!(val, 7),
Expand All @@ -80,6 +81,7 @@ fn minimize_small() {

let mut solver = Solver::new(model);
assert!(solver.solve().unwrap().is_some());
solver.reset();
match solver.minimize(a).unwrap() {
None => panic!(),
Some((val, _)) => assert_eq!(val, 6),
Expand Down Expand Up @@ -120,7 +122,7 @@ fn int_bounds() {

let mut solver = Solver::new(model);
solver.enforce_all(constraints, []);
assert!(solver.propagate_and_backtrack_to_consistent());
assert!(solver.propagate_and_backtrack_to_consistent().is_ok());
let check_dom = |v, lb, ub| {
assert_eq!(solver.model.domain_of(v), (lb, ub));
};
Expand Down Expand Up @@ -148,7 +150,7 @@ fn bools_as_ints() {

let mut solver = Solver::new(model);

assert!(solver.propagate_and_backtrack_to_consistent());
assert!(solver.propagate_and_backtrack_to_consistent().is_ok());
assert_eq!(solver.model.boolean_value_of(a), None);
assert_eq!(solver.model.domain_of(ia), (0, 1));
assert_eq!(solver.model.boolean_value_of(a), None);
Expand Down Expand Up @@ -183,25 +185,25 @@ fn ints_and_bools() {

let mut solver = Solver::new(model);

assert!(solver.propagate_and_backtrack_to_consistent());
assert!(solver.propagate_and_backtrack_to_consistent().is_ok());
assert_eq!(solver.model.domain_of(i), (-10, 10));
assert_eq!(solver.model.domain_of(ia), (0, 1));
assert_eq!(solver.model.boolean_value_of(a), None);

solver.enforce(leq(i, ia), []);
assert!(solver.propagate_and_backtrack_to_consistent());
assert!(solver.propagate_and_backtrack_to_consistent().is_ok());
assert_eq!(solver.model.domain_of(i), (-10, 1));
assert_eq!(solver.model.domain_of(ia), (0, 1));
assert_eq!(solver.model.boolean_value_of(a), None);

solver.enforce(gt(ia, i), []);
assert!(solver.propagate_and_backtrack_to_consistent());
assert!(solver.propagate_and_backtrack_to_consistent().is_ok());
assert_eq!(solver.model.domain_of(i), (-10, 0));
assert_eq!(solver.model.domain_of(ia), (0, 1));
assert_eq!(solver.model.boolean_value_of(a), None);

solver.enforce(geq(i, 0), []);
assert!(solver.propagate_and_backtrack_to_consistent());
assert!(solver.propagate_and_backtrack_to_consistent().is_ok());
assert_eq!(solver.model.domain_of(i), (0, 0));
assert_eq!(solver.model.domain_of(ia), (1, 1));
assert_eq!(solver.model.boolean_value_of(a), Some(true));
Expand Down Expand Up @@ -237,7 +239,7 @@ fn optional_hierarchy() {

// solver.model.print_state();

assert!(solver.propagate_and_backtrack_to_consistent());
assert!(solver.propagate_and_backtrack_to_consistent().is_ok());

// solver.model.print_state();

Expand All @@ -247,7 +249,7 @@ fn optional_hierarchy() {
assert_eq!(solver.model.opt_domain_of(vars[2]), Unknown(5, 10));

solver.decide(Lit::leq(i, 9));
assert!(solver.propagate_and_backtrack_to_consistent());
assert!(solver.propagate_and_backtrack_to_consistent().is_ok());

assert_eq!(solver.model.opt_domain_of(i), Unknown(-10, 9));
assert_eq!(solver.model.opt_domain_of(vars[0]), Unknown(0, 8));
Expand All @@ -258,7 +260,7 @@ fn optional_hierarchy() {
// solver.model.state.print();

solver.decide(Lit::leq(i, 4));
assert!(solver.propagate_and_backtrack_to_consistent());
assert!(solver.propagate_and_backtrack_to_consistent().is_ok());

// println!();
// solver.model.state.print();
Expand All @@ -271,7 +273,7 @@ fn optional_hierarchy() {

solver.save_state();
solver.decide(p);
assert!(solver.propagate_and_backtrack_to_consistent());
assert!(solver.propagate_and_backtrack_to_consistent().is_ok());
assert_eq!(solver.model.opt_domain_of(i), Present(-10, 4));
assert_eq!(solver.model.opt_domain_of(vars[0]), Unknown(0, 4));
assert_eq!(solver.model.opt_domain_of(vars[1]), Unknown(-10, -5));
Expand All @@ -280,21 +282,21 @@ fn optional_hierarchy() {
println!("======================");

solver.decide(Lit::leq(i, -1));
assert!(solver.propagate_and_backtrack_to_consistent());
assert!(solver.propagate_and_backtrack_to_consistent().is_ok());
assert_eq!(solver.model.opt_domain_of(i), Present(-10, -1));
assert_eq!(solver.model.opt_domain_of(vars[0]), Absent);
assert_eq!(solver.model.opt_domain_of(vars[1]), Unknown(-10, -5));
assert_eq!(solver.model.opt_domain_of(vars[2]), Absent);

solver.decide(scopes[1]);
assert!(solver.propagate_and_backtrack_to_consistent());
assert!(solver.propagate_and_backtrack_to_consistent().is_ok());
assert_eq!(solver.model.opt_domain_of(i), Present(-10, -5));
assert_eq!(solver.model.opt_domain_of(vars[0]), Absent);
assert_eq!(solver.model.opt_domain_of(vars[1]), Present(-10, -5));
assert_eq!(solver.model.opt_domain_of(vars[2]), Absent);

// solver.decide(!p);
// assert!(matches!(solver.propagate_and_backtrack_to_consistent(), Ok(true));
// assert!(matches!(solver.propagate_and_backtrack_to_consistent().is_ok(), Ok(true));
// solver.model.discrete.print();

// assert_eq!(solver.model.opt_domain_of(i), Absent);
Expand Down
8 changes: 4 additions & 4 deletions planning/planners/src/encode.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -381,7 +381,7 @@ fn enforce_refinement(t: TaskRef, supporters: Vec<TaskRef>, model: &mut Model) {
/// Multiply an integer atom with a literal.
/// The result is a linear sum evaluated to the atom if the literal is true, and to 0 otherwise.
fn iatom_mul_lit(model: &mut Model, atom: IAtom, lit: Lit) -> LinearSum {
debug_assert!(model.state.implies(lit, model.presence_literal(atom.var.into())));
debug_assert!(model.state.implies(lit, model.presence_literal(atom.var)));
if atom.var == IVar::ZERO {
// Constant variable
if atom.shift == 0 {
Expand Down Expand Up @@ -892,7 +892,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
}
// each term of the increase value is present
for term in inc_val.terms() {
let p = solver.model.presence_literal(term.var().into());
let p = solver.model.presence_literal(term.var());
active_inc_conjunction.push(p);
}
// compute wether the increase is active in the condition value
Expand All @@ -903,7 +903,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
inc_support.entry(inc_id).or_default().push(active_inc);
for term in inc_val.terms() {
// compute some static implication for better propagation
let p = solver.model.presence_literal(term.var().into());
let p = solver.model.presence_literal(term.var());
if !solver.model.entails(p) {
solver.model.state.add_implication(active_inc, p);
}
Expand All @@ -914,7 +914,7 @@ pub fn encode(pb: &FiniteProblem, metric: Option<Metric>) -> std::result::Result
// enforce the condition value to be the sum of the assignment values and the increase values
for term in cond_val_sum.terms() {
// compute some static implication for better propagation
let p = solver.model.presence_literal(term.var().into());
let p = solver.model.presence_literal(term.var());
if !solver.model.entails(p) {
solver.model.state.add_implication(supported_by, p);
}
Expand Down
6 changes: 6 additions & 0 deletions solver/src/core/state/cause.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,8 @@ use crate::reasoners::ReasonerId;
pub enum Cause {
/// Event caused by a decision.
Decision,
/// Event caused by an assumption.
Assumption,
/// Event that resulted from the encoding of a constraint.
/// This should only occur at the root decision level.
Encoding,
Expand All @@ -32,6 +34,7 @@ impl From<Cause> for DirectOrigin {
fn from(c: Cause) -> Self {
match c {
Cause::Decision => DirectOrigin::Decision,
Cause::Assumption => DirectOrigin::Assumption,
Cause::Encoding => DirectOrigin::Encoding,
Cause::Inference(i) => DirectOrigin::ExternalInference(i),
}
Expand All @@ -42,6 +45,7 @@ impl From<Cause> for Origin {
fn from(c: Cause) -> Self {
match c {
Cause::Decision => Origin::Direct(DirectOrigin::Decision),
Cause::Assumption => Origin::Direct(DirectOrigin::Assumption),
Cause::Encoding => Origin::Direct(DirectOrigin::Encoding),
Cause::Inference(i) => Origin::Direct(DirectOrigin::ExternalInference(i)),
}
Expand Down Expand Up @@ -75,6 +79,7 @@ pub enum Origin {
}
impl Origin {
pub const DECISION: Origin = Origin::Direct(DirectOrigin::Decision);
pub const ASSUMPTION: Origin = Origin::Direct(DirectOrigin::Assumption);

pub const fn implication_propagation(lit: Lit) -> Origin {
Origin::Direct(DirectOrigin::ImplicationPropagation(lit))
Expand All @@ -91,6 +96,7 @@ impl Origin {
#[derive(Copy, Clone, Debug, Eq, PartialEq)]
pub enum DirectOrigin {
Decision,
Assumption,
/// Result of encoding a constraint at the root decision level.
Encoding,
/// The event is due to an inference.
Expand Down
Loading

0 comments on commit e38372d

Please sign in to comment.