conjure_core/solver/adaptors/minion/
adaptor.rs

Help
1use regex::Regex;
2use std::collections::HashMap;
3use std::sync::{LazyLock, 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::{self as conjure_ast, Name};
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
42fn parse_name(minion_name: &str) -> Name {
43    static MACHINE_NAME_RE: LazyLock<Regex> =
44        LazyLock::new(|| Regex::new(r"__conjure_machine_name_([0-9]+)").unwrap());
45    static REPRESENTED_NAME_RE: LazyLock<Regex> =
46        LazyLock::new(|| Regex::new(r"__conjure_represented_name##(.*)##(.*)___(.*)").unwrap());
47
48    if let Some(caps) = MACHINE_NAME_RE.captures(minion_name) {
49        conjure_ast::Name::MachineName(caps[1].parse::<i32>().unwrap())
50    } else if let Some(caps) = REPRESENTED_NAME_RE.captures(minion_name) {
51        conjure_ast::Name::RepresentedName(
52            Box::new(parse_name(&caps[1])),
53            caps[2].to_string(),
54            caps[3].to_string(),
55        )
56    } else {
57        conjure_ast::Name::UserName(minion_name.to_string())
58    }
59}
60
61#[allow(clippy::unwrap_used)]
62fn minion_rs_callback(solutions: HashMap<minion_ast::VarName, minion_ast::Constant>) -> bool {
63    *(ANY_SOLUTIONS.lock().unwrap()) = true;
64    let callback = USER_CALLBACK
65        .get_or_init(|| Mutex::new(Box::new(|x| true)))
66        .lock()
67        .unwrap();
68
69    let mut conjure_solutions: HashMap<conjure_ast::Name, conjure_ast::Literal> = HashMap::new();
70    for (minion_name, minion_const) in solutions.into_iter() {
71        let conjure_const = match minion_const {
72            minion_ast::Constant::Bool(x) => conjure_ast::Literal::Bool(x),
73            minion_ast::Constant::Integer(x) => conjure_ast::Literal::Int(x),
74            _ => todo!(),
75        };
76
77        let conjure_name = parse_name(&minion_name);
78        conjure_solutions.insert(conjure_name, conjure_const);
79    }
80
81    let continue_search = (**callback)(conjure_solutions);
82    if !continue_search {
83        *(USER_TERMINATED.lock().unwrap()) = true;
84    }
85
86    continue_search
87}
88
89impl private::Sealed for Minion {}
90
91impl Minion {
92    pub fn new() -> Minion {
93        Minion {
94            __non_constructable: private::Internal,
95            model: None,
96        }
97    }
98}
99
100impl Default for Minion {
101    fn default() -> Self {
102        Minion::new()
103    }
104}
105
106impl SolverAdaptor for Minion {
107    #[allow(clippy::unwrap_used)]
108    fn solve(
109        &mut self,
110        callback: SolverCallback,
111        _: private::Internal,
112    ) -> Result<SolveSuccess, SolverError> {
113        // our minion callback is global state, so single threading the adaptor as a whole is
114        // probably a good move...
115        #[allow(clippy::unwrap_used)]
116        let mut minion_lock = MINION_LOCK.lock().unwrap();
117
118        #[allow(clippy::unwrap_used)]
119        let mut user_callback = USER_CALLBACK
120            .get_or_init(|| Mutex::new(Box::new(|x| true)))
121            .lock()
122            .unwrap();
123        *user_callback = callback;
124        drop(user_callback); // release mutex. REQUIRED so that run_minion can use the
125                             // user callback and not deadlock.
126
127        run_minion(
128            self.model.clone().expect("STATE MACHINE ERR"),
129            minion_rs_callback,
130        )
131        .map_err(|err| match err {
132            MinionError::RuntimeError(x) => Runtime(format!("{:#?}", x)),
133            MinionError::Other(x) => Runtime(format!("{:#?}", x)),
134            MinionError::NotImplemented(x) => RuntimeNotImplemented(x),
135            x => Runtime(format!("unknown minion_rs error: {:#?}", x)),
136        })?;
137
138        let mut status = Complete(HasSolutions);
139        if *(USER_TERMINATED.lock()).unwrap() {
140            status = Incomplete(UserTerminated);
141        } else if *(ANY_SOLUTIONS.lock()).unwrap() {
142            status = Complete(NoSolutions);
143        }
144        Ok(SolveSuccess {
145            stats: get_solver_stats(),
146            status,
147        })
148    }
149
150    fn solve_mut(
151        &mut self,
152        callback: SolverMutCallback,
153        _: private::Internal,
154    ) -> Result<SolveSuccess, SolverError> {
155        Err(OpNotImplemented("solve_mut".into()))
156    }
157
158    fn load_model(&mut self, model: ConjureModel, _: private::Internal) -> Result<(), SolverError> {
159        self.model = Some(model_to_minion(model)?);
160        Ok(())
161    }
162
163    fn get_family(&self) -> SolverFamily {
164        SolverFamily::Minion
165    }
166
167    fn get_name(&self) -> Option<String> {
168        Some("Minion".to_owned())
169    }
170}
171
172#[allow(clippy::unwrap_used)]
173fn get_solver_stats() -> SolverStats {
174    SolverStats {
175        nodes: get_from_table("Nodes".into()).map(|x| x.parse::<u64>().unwrap()),
176        ..Default::default()
177    }
178}
conjure_core/solver/adaptors/minion/adaptor.rs

conjure_core/solver/adaptors/minion/
adaptor.rs
