conjure_core/solver/adaptors/minion/
adaptor.rs

1use regex::Regex;
2use std::collections::HashMap;
3use std::sync::{Mutex, OnceLock};
4
5use minion_ast::Model as MinionModel;
6use minion_rs::ast as minion_ast;
7use minion_rs::error::MinionError;
8use minion_rs::{get_from_table, run_minion};
9
10use crate::ast as conjure_ast;
11use crate::solver::SolverCallback;
12use crate::solver::SolverFamily;
13use crate::solver::SolverMutCallback;
14use crate::stats::SolverStats;
15use crate::Model as ConjureModel;
16
17use crate::solver::model_modifier::NotModifiable;
18use crate::solver::private;
19use crate::solver::SearchComplete::*;
20use crate::solver::SearchIncomplete::*;
21use crate::solver::SearchStatus::*;
22use crate::solver::SolveSuccess;
23use crate::solver::SolverAdaptor;
24use crate::solver::SolverError;
25use crate::solver::SolverError::*;
26
27use super::parse_model::model_to_minion;
28
29/// A [SolverAdaptor] for interacting with Minion.
30///
31/// This adaptor uses the `minion_rs` crate to talk to Minion over FFI.
32pub struct Minion {
33    __non_constructable: private::Internal,
34    model: Option<MinionModel>,
35}
36
37static MINION_LOCK: Mutex<()> = Mutex::new(());
38static USER_CALLBACK: OnceLock<Mutex<SolverCallback>> = OnceLock::new();
39static ANY_SOLUTIONS: Mutex<bool> = Mutex::new(false);
40static USER_TERMINATED: Mutex<bool> = Mutex::new(false);
41
42#[allow(clippy::unwrap_used)]
43fn minion_rs_callback(solutions: HashMap<minion_ast::VarName, minion_ast::Constant>) -> bool {
44    *(ANY_SOLUTIONS.lock().unwrap()) = true;
45    let callback = USER_CALLBACK
46        .get_or_init(|| Mutex::new(Box::new(|x| true)))
47        .lock()
48        .unwrap();
49
50    let mut conjure_solutions: HashMap<conjure_ast::Name, conjure_ast::Literal> = HashMap::new();
51    let machine_name_re = Regex::new(r"__conjure_machine_name_([0-9]+)").unwrap();
52    for (minion_name, minion_const) in solutions.into_iter() {
53        let conjure_const = match minion_const {
54            minion_ast::Constant::Bool(x) => conjure_ast::Literal::Bool(x),
55            minion_ast::Constant::Integer(x) => conjure_ast::Literal::Int(x),
56            _ => todo!(),
57        };
58
59        let conjure_name = if let Some(caps) = machine_name_re.captures(&minion_name) {
60            conjure_ast::Name::MachineName(caps[1].parse::<i32>().unwrap())
61        } else {
62            conjure_ast::Name::UserName(minion_name)
63        };
64
65        conjure_solutions.insert(conjure_name, conjure_const);
66    }
67
68    let continue_search = (**callback)(conjure_solutions);
69    if !continue_search {
70        *(USER_TERMINATED.lock().unwrap()) = true;
71    }
72
73    continue_search
74}
75
76impl private::Sealed for Minion {}
77
78impl Minion {
79    pub fn new() -> Minion {
80        Minion {
81            __non_constructable: private::Internal,
82            model: None,
83        }
84    }
85}
86
87impl Default for Minion {
88    fn default() -> Self {
89        Minion::new()
90    }
91}
92
93impl SolverAdaptor for Minion {
94    #[allow(clippy::unwrap_used)]
95    fn solve(
96        &mut self,
97        callback: SolverCallback,
98        _: private::Internal,
99    ) -> Result<SolveSuccess, SolverError> {
100        // our minion callback is global state, so single threading the adaptor as a whole is
101        // probably a good move...
102        #[allow(clippy::unwrap_used)]
103        let mut minion_lock = MINION_LOCK.lock().unwrap();
104
105        #[allow(clippy::unwrap_used)]
106        let mut user_callback = USER_CALLBACK
107            .get_or_init(|| Mutex::new(Box::new(|x| true)))
108            .lock()
109            .unwrap();
110        *user_callback = callback;
111        drop(user_callback); // release mutex. REQUIRED so that run_minion can use the
112                             // user callback and not deadlock.
113
114        run_minion(
115            self.model.clone().expect("STATE MACHINE ERR"),
116            minion_rs_callback,
117        )
118        .map_err(|err| match err {
119            MinionError::RuntimeError(x) => Runtime(format!("{:#?}", x)),
120            MinionError::Other(x) => Runtime(format!("{:#?}", x)),
121            MinionError::NotImplemented(x) => RuntimeNotImplemented(x),
122            x => Runtime(format!("unknown minion_rs error: {:#?}", x)),
123        })?;
124
125        let mut status = Complete(HasSolutions);
126        if *(USER_TERMINATED.lock()).unwrap() {
127            status = Incomplete(UserTerminated);
128        } else if *(ANY_SOLUTIONS.lock()).unwrap() {
129            status = Complete(NoSolutions);
130        }
131        Ok(SolveSuccess {
132            stats: get_solver_stats(),
133            status,
134        })
135    }
136
137    fn solve_mut(
138        &mut self,
139        callback: SolverMutCallback,
140        _: private::Internal,
141    ) -> Result<SolveSuccess, SolverError> {
142        Err(OpNotImplemented("solve_mut".into()))
143    }
144
145    fn load_model(&mut self, model: ConjureModel, _: private::Internal) -> Result<(), SolverError> {
146        self.model = Some(model_to_minion(model)?);
147        Ok(())
148    }
149
150    fn get_family(&self) -> SolverFamily {
151        SolverFamily::Minion
152    }
153
154    fn get_name(&self) -> Option<String> {
155        Some("Minion".to_owned())
156    }
157}
158
159#[allow(clippy::unwrap_used)]
160fn get_solver_stats() -> SolverStats {
161    SolverStats {
162        nodes: get_from_table("Nodes".into()).map(|x| x.parse::<u64>().unwrap()),
163        ..Default::default()
164    }
165}
conjure_core/solver/adaptors/minion/adaptor.rs

conjure_core/solver/adaptors/minion/
adaptor.rs
