Merge pull request #207 from plaans/feat/views

feat(solver): Provide variable views

Author: arbimo

aries_fzn/src/aries/constraint/abs.rs

@@ -32,7 +32,7 @@ impl Abs {
 
 impl<Lbl: Label> Post<Lbl> for Abs {
     fn post(&self, model: &mut Model<Lbl>) {
-        let (lb, ub) = model.state.bounds(self.a.into());
+        let (lb, ub) = model.state.bounds(self.a);
 
         let minus_a = model.state.new_var(-ub, -lb);
         let minus_a = IVar::new(minus_a);

examples/knapsack/main.rs

@@ -1,7 +1,7 @@
 #![allow(clippy::needless_range_loop)]
 
 use aries::core::{IntCst, Lit, INT_CST_MAX};
-use aries::model::extensions::AssignmentExt;
+use aries::model::extensions::DomainsExt;
 use aries::model::lang::linear::LinearSum;
 use aries::model::lang::{IVar, Rational};
 use aries::solver::search::combinators::WithGeomRestart;

examples/scheduling/src/main.rs

@@ -5,7 +5,7 @@ mod search;
 use crate::problem::{Encoding, OperationId, Problem, ProblemKind};
 use crate::search::{SearchStrategy, Solver, Var};
 use anyhow::*;
-use aries::model::extensions::AssignmentExt;
+use aries::model::extensions::DomainsExt;
 use aries::model::lang::IVar;
 use aries::solver::parallel::{Solution, SolverResult};
 use std::fmt::Write;
@@ -92,7 +92,7 @@ fn solve(kind: ProblemKind, instance: &str, opt: &Opt) {
 
     let result = solver.minimize_with(
         makespan,
-        |s| println!("New solution with makespan: {}", s.domain_of(makespan).0),
+        |s| println!("New solution with makespan: {}", s.bounds(makespan).0),
         None,
         deadline,
     );

examples/scheduling/src/search/greedy.rs

@@ -6,7 +6,7 @@ use crate::Var;
 use aries::backtrack::{Backtrack, DecLvl, DecisionLevelTracker};
 use aries::core::state::{OptDomain, Term};
 use aries::core::{IntCst, Lit, VarRef};
-use aries::model::extensions::AssignmentExt;
+use aries::model::extensions::DomainsExt;
 use aries::solver::search::{Decision, SearchControl};
 use aries::solver::stats::Stats;
 

examples/smt/tests/smt.rs

@@ -1,7 +1,7 @@
 use aries::backtrack::Backtrack;
 use aries::core::state::{OptDomain, Term};
 use aries::core::Lit;
-use aries::model::extensions::AssignmentExt;
+use aries::model::extensions::DomainsExt;
 use aries::model::lang::alternative::Alternative;
 use aries::model::lang::expr::*;
 use aries::model::lang::max::{EqMax, EqMin};
@@ -124,7 +124,7 @@ fn int_bounds() {
     solver.enforce_all(constraints, []);
     assert!(solver.propagate_and_backtrack_to_consistent().is_ok());
     let check_dom = |v, lb, ub| {
-        assert_eq!(solver.model.domain_of(v), (lb, ub));
+        assert_eq!(solver.model.bounds(v), (lb, ub));
     };
     check_dom(a, 2, 8);
     check_dom(b, 2, 8);
@@ -152,13 +152,13 @@ fn bools_as_ints() {
 
     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.bounds(ia), (0, 1));
     assert_eq!(solver.model.boolean_value_of(a), None);
-    assert_eq!(solver.model.domain_of(ia), (0, 1));
+    assert_eq!(solver.model.bounds(ia), (0, 1));
     assert_eq!(solver.model.boolean_value_of(a), None);
-    assert_eq!(solver.model.domain_of(ia), (0, 1));
+    assert_eq!(solver.model.bounds(ia), (0, 1));
     assert_eq!(solver.model.boolean_value_of(a), None);
-    assert_eq!(solver.model.domain_of(ia), (0, 1));
+    assert_eq!(solver.model.bounds(ia), (0, 1));
 
     solver.enforce(a.true_lit(), []);
     solver.enforce(b.false_lit(), []);
@@ -167,13 +167,13 @@ fn bools_as_ints() {
 
     solver.propagate().unwrap();
     assert_eq!(solver.model.boolean_value_of(a), Some(true));
-    assert_eq!(solver.model.domain_of(ia), (1, 1));
+    assert_eq!(solver.model.bounds(ia), (1, 1));
     assert_eq!(solver.model.boolean_value_of(b), Some(false));
-    assert_eq!(solver.model.domain_of(ib), (0, 0));
+    assert_eq!(solver.model.bounds(ib), (0, 0));
     assert_eq!(solver.model.boolean_value_of(c), Some(true));
-    assert_eq!(solver.model.domain_of(ic), (1, 1));
+    assert_eq!(solver.model.bounds(ic), (1, 1));
     assert_eq!(solver.model.boolean_value_of(d), Some(false));
-    assert_eq!(solver.model.domain_of(id), (0, 0));
+    assert_eq!(solver.model.bounds(id), (0, 0));
 }
 
 #[test]
@@ -186,26 +186,26 @@ fn ints_and_bools() {
     let mut solver = Solver::new(model);
 
     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.bounds(i), (-10, 10));
+    assert_eq!(solver.model.bounds(ia), (0, 1));
     assert_eq!(solver.model.boolean_value_of(a), None);
 
     solver.enforce(leq(i, ia), []);
     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.bounds(i), (-10, 1));
+    assert_eq!(solver.model.bounds(ia), (0, 1));
     assert_eq!(solver.model.boolean_value_of(a), None);
 
     solver.enforce(gt(ia, i), []);
     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.bounds(i), (-10, 0));
+    assert_eq!(solver.model.bounds(ia), (0, 1));
     assert_eq!(solver.model.boolean_value_of(a), None);
 
     solver.enforce(geq(i, 0), []);
     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.bounds(i), (0, 0));
+    assert_eq!(solver.model.bounds(ia), (1, 1));
     assert_eq!(solver.model.boolean_value_of(a), Some(true));
 }
 

planning/engine/src/repair.rs

@@ -12,7 +12,7 @@ use std::{
 use aries::{
     core::{INT_CST_MAX, Lit, literals::ConjunctionBuilder},
     model::{
-        extensions::AssignmentExt,
+        extensions::DomainsExt,
         lang::{
             FAtom, IAtom,
             expr::{and, eq, neq},

planning/grpc/server/src/bin/server.rs

@@ -1,5 +1,6 @@
 use anyhow::{bail, ensure, Context, Error};
-use aries::model::extensions::SavedAssignment;
+
+use aries::core::state::Domains;
 use aries_grpc_server::chronicles::problem_to_chronicles;
 use aries_grpc_server::serialize::{engine, serialize_plan};
 use aries_grpc_server::warm_up::plan_from_option_upf;
@@ -196,7 +197,7 @@ fn solve_blocking(
     let warm_up_plan = plan_from_option_upf(warm_up_plan, &base_problem)?;
 
     // callback that will be invoked each time an intermediate solution is found
-    let on_new_solution = |pb: &FiniteProblem, ass: Arc<SavedAssignment>| {
+    let on_new_solution = |pb: &FiniteProblem, ass: Arc<Domains>| {
         let plan = serialize_plan(&problem, pb, &ass);
         match plan {
             Ok(plan) => on_new_sol(plan),

planning/grpc/server/src/serialize.rs

@@ -1,6 +1,6 @@
 use anyhow::{ensure, Context, Result};
 use aries::core::state::Domains;
-use aries::model::extensions::AssignmentExt;
+use aries::model::extensions::DomainsExt;
 use aries::model::lang::{Atom, FAtom};
 use aries_planners::encoding::ChronicleId;
 use aries_planners::fmt::{extract_plan_actions, format_atom};

planning/planners/src/encode.rs

@@ -11,7 +11,7 @@ use crate::Model;
 use anyhow::{Context, Result};
 use aries::core::state::Conflict;
 use aries::core::*;
-use aries::model::extensions::{AssignmentExt, Shaped};
+use aries::model::extensions::{DomainsExt, Shaped};
 use aries::model::lang::linear::LinearSum;
 use aries::model::lang::mul::EqVarMulLit;
 use aries::model::lang::{expr::*, IVar};

planning/planners/src/encode/numeric.rs

@@ -7,7 +7,7 @@ use aries::backtrack::Backtrack;
 use aries::backtrack::DecLvl;
 use aries::core::state::Conflict;
 use aries::core::*;
-use aries::model::extensions::AssignmentExt;
+use aries::model::extensions::DomainsExt;
 use aries::model::lang::FAtom;
 use aries::model::lang::{expr::*, Atom, Type};
 use aries_planning::chronicles::*;
@@ -100,7 +100,7 @@ fn lit_to_ivar(model: &mut Model, lit: Lit) -> IVar {
         IVar::ONE
     } else if model.entails(!lit) {
         IVar::ZERO
-    } else if model.domain_of(lit.variable()) == (0, 1) {
+    } else if model.bounds(lit.variable()) == (0, 1) {
         IVar::new(lit.variable())
     } else {
         let lbl = model
@@ -130,8 +130,8 @@ pub fn iatom_mul_lit(model: &mut Model, atom: IAtom, lit: Lit) -> LinearSum {
         }
     } else {
         // Real variable
-        let lb = model.lower_bound(atom.var);
-        let ub = model.upper_bound(atom.var);
+        let lb = model.lb(atom.var);
+        let ub = model.ub(atom.var);
         let lbl = model
             .get_label(atom.var)
             .unwrap_or(&(Container::Base / VarType::Reification))