Merge branch 'linear-expl' into knapsack

ci/sat.py

@@ -9,7 +9,7 @@
 import time
 
 os.system("cargo build --profile ci --bin aries-sat")
-solver = "target/ci/aries-sat --threads 1"
+solver = "target/ci/aries-sat"
 
 solver_cmd = solver + " {params} --source {archive} {instance}"
 
@@ -42,4 +42,3 @@ def run_all(archive, sat):
 
 run_all("examples/sat/instances/test-sat.zip", sat=True)
 run_all("examples/sat/instances/test-unsat.zip", sat=False)
-

examples/knapsack/main.rs

@@ -1,6 +1,6 @@
 #![allow(clippy::needless_range_loop)]
 
-use aries::core::{IntCst, Lit, INT_CST_MAX};
+use aries::core::{IntCst, INT_CST_MAX};
 use aries::model::extensions::AssignmentExt;
 use aries::model::lang::linear::LinearSum;
 use aries::model::lang::IVar;

examples/sat/main.rs

@@ -104,12 +104,12 @@ fn solve_multi_threads(model: Model, opt: &Opt, deadline: Option<Instant>) -> Re
     let choices: Vec<_> = model.state.variables().map(|v| Lit::geq(v, 1)).collect();
     let solver = Box::new(Solver::new(model));
 
-    let search_params: Vec<_> = opt.search.split(",").collect();
+    let search_params: Vec<_> = opt.search.split(',').collect();
     let num_threads = search_params.len();
 
     let conflict_params = |conf: &str| {
         let mut params = Params::default();
-        for opt in conf.split(":") {
+        for opt in conf.split(':') {
             let handled = params.configure(opt);
             if !handled {
                 panic!("UNSUPPORTED OPTION: {opt}")
@@ -119,8 +119,8 @@ fn solve_multi_threads(model: Model, opt: &Opt, deadline: Option<Instant>) -> Re
     };
 
     let mut par_solver = ParSolver::new(solver, num_threads, |id, solver| {
-        let search_params: Vec<_> = search_params[id].split("/").collect();
-        let stable_params = if search_params.len() > 0 {
+        let search_params: Vec<_> = search_params[id].split('/').collect();
+        let stable_params = if !search_params.is_empty() {
             search_params[0]
         } else {
             "+lrb:+p+l:-neg"

examples/scheduling/src/search.rs

@@ -82,12 +82,14 @@ struct Strat {
 pub fn get_solver(base: Solver, strategy: &SearchStrategy, pb: &Encoding, num_threads: usize) -> ParSolver {
     let mut base_solver = Box::new(base);
 
-    let mut load_conf = |conf: &str| -> Strat {
+    let load_conf = |conf: &str| -> Strat {
         let mut mode = Mode::Stable;
-        let mut params = conflicts::Params::default();
-        params.heuristic = conflicts::Heuristic::LearningRate;
-        params.active = conflicts::ActiveLiterals::Reasoned;
-        params.impact_measure = ImpactMeasure::LBD;
+        let mut params = conflicts::Params {
+            heuristic: conflicts::Heuristic::LearningRate,
+            active: conflicts::ActiveLiterals::Reasoned,
+            impact_measure: ImpactMeasure::LBD,
+            ..Default::default()
+        };
         for opt in conf.split(':') {
             if params.configure(opt) {
                 // handled
@@ -111,7 +113,7 @@ pub fn get_solver(base: Solver, strategy: &SearchStrategy, pb: &Encoding, num_th
         SearchStrategy::Default => "stable:+sol",
         SearchStrategy::Custom(conf) => conf.as_str(),
     };
-    let all_strats = conf.split("/").map(|s| load_conf(s)).collect_vec();
+    let all_strats = conf.split('/').map(load_conf).collect_vec();
 
     let decision_lits: Vec<Lit> = base_solver
         .model
@@ -131,8 +133,7 @@ pub fn get_solver(base: Solver, strategy: &SearchStrategy, pb: &Encoding, num_th
             Mode::Stable => (2000, 1.2), // stable: few restarts
             Mode::Focused => (800, 1.0), // focused: always aggressive restarts
         };
-        let brancher = brancher.with_restarts(restart_period, restart_update);
-        brancher
+        brancher.with_restarts(restart_period, restart_update)
     };
 
     // build a brancher that alternates between the proposed strategies
@@ -160,7 +161,7 @@ pub fn get_solver(base: Solver, strategy: &SearchStrategy, pb: &Encoding, num_th
             .collect_vec();
 
         // conflict based search, possibly alternating between several strategies
-        let branchers = strats.into_iter().map(|strat| build_brancher(strat)).collect_vec();
+        let branchers = strats.into_iter().map(build_brancher).collect_vec();
         let brancher = round_robin(branchers);
 
         // search strategy. For the first one simply add a greedy EST strategy to bootstrap the search

planning/planners/src/bin/lcp.rs

@@ -65,6 +65,15 @@ pub struct Opt {
 }
 
 fn main() -> Result<()> {
+    // Terminate the process if a thread panics.
+    // take_hook() returns the default hook in case when a custom one is not set
+    let orig_hook = std::panic::take_hook();
+    std::panic::set_hook(Box::new(move |panic_info| {
+        // invoke the default handler and exit the process
+        orig_hook(panic_info);
+        std::process::exit(1);
+    }));
+
     let opt: Opt = Opt::from_args();
 
     // set up logger