From f8e5ea1ff0457f1a8d5a7b4416d8076c20c8d081 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Tue, 27 Feb 2024 13:59:50 +0000 Subject: [PATCH 01/10] Change error type of get_example functions from Box to anyhow::Error --- conjure_oxide/src/generate_custom.rs | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/conjure_oxide/src/generate_custom.rs b/conjure_oxide/src/generate_custom.rs index d8adbcf09..b8ba38405 100644 --- a/conjure_oxide/src/generate_custom.rs +++ b/conjure_oxide/src/generate_custom.rs @@ -4,13 +4,11 @@ use crate::parse::model_from_json; use conjure_core::ast::Model; -use std::error::Error; - use std::path::PathBuf; use walkdir::WalkDir; -/// Searches recursively in `../tests/integration` folder for an `.essence` file matching the given filename, -/// then uses conjure to process it into astjson, and returns the parsed model. +/// Searches recursively in `../tests/integration` folder for an `.essence` file matching the given +/// filename, then uses conjure to process it into astjson, and returns the parsed model. /// /// # Arguments /// @@ -18,8 +16,8 @@ use walkdir::WalkDir; /// /// # Returns /// -/// Function returns a `Result>`, where `Value` is the parsed model -pub fn get_example_model(filename: &str) -> Result> { +/// Function returns a `Result`, where `Value` is the parsed model. +pub fn get_example_model(filename: &str) -> Result { // define relative path -> integration tests dir let base_dir = "tests/integration"; let mut essence_path = PathBuf::new(); @@ -36,11 +34,11 @@ pub fn get_example_model(filename: &str) -> Result> { } } - println!("PATH TO FILE: {}", essence_path.display()); + //println!("PATH TO FILE: {}", essence_path.display()); // return error if file not found if essence_path.as_os_str().is_empty() { - return Err(Box::new(std::io::Error::new( + return Err(anyhow::Error::new(std::io::Error::new( std::io::ErrorKind::NotFound, "ERROR: File not found in any subdirectory", ))); @@ -57,7 +55,7 @@ pub fn get_example_model(filename: &str) -> Result> { // convert Conjure's stdout from bytes to string let astjson = String::from_utf8(output.stdout)?; - println!("ASTJSON: {}", astjson); + //println!("ASTJSON: {}", astjson); // parse AST JSON from desired Model format let generated_mdl = model_from_json(&astjson)?; @@ -74,19 +72,19 @@ pub fn get_example_model(filename: &str) -> Result> { /// /// # Returns /// -/// Function returns a `Result>`, where `Value` is the parsed model -pub fn get_example_model_by_path(filepath: &str) -> Result> { +/// Function returns a `Result`, where `Value` is the parsed model +pub fn get_example_model_by_path(filepath: &str) -> Result { let essence_path = PathBuf::from(filepath); // return error if file not found if essence_path.as_os_str().is_empty() { - return Err(Box::new(std::io::Error::new( + return Err(anyhow::Error::new(std::io::Error::new( std::io::ErrorKind::NotFound, "ERROR: File not found in any subdirectory", ))); } - println!("PATH TO FILE: {}", essence_path.display()); + // println!("PATH TO FILE: {}", essence_path.display()); // Command execution using 'conjure' CLI tool with provided path let mut cmd = std::process::Command::new("conjure"); @@ -99,7 +97,7 @@ pub fn get_example_model_by_path(filepath: &str) -> Result // convert Conjure's stdout from bytes to string let astjson = String::from_utf8(output.stdout)?; - println!("ASTJSON: {}", astjson); + // println!("ASTJSON: {}", astjson); // parse AST JSON into the desired Model format let generated_model = model_from_json(&astjson)?; From 18a9f07b99a3785fe4fd79e6a4c4b23eabc186be Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Mon, 26 Feb 2024 12:10:57 +0000 Subject: [PATCH 02/10] solver-interface: remove feature flag from definition --- conjure_oxide/src/unstable/mod.rs | 3 --- conjure_oxide/src/unstable/solver_interface/mod.rs | 2 -- 2 files changed, 5 deletions(-) diff --git a/conjure_oxide/src/unstable/mod.rs b/conjure_oxide/src/unstable/mod.rs index 7f45f3281..c31642288 100644 --- a/conjure_oxide/src/unstable/mod.rs +++ b/conjure_oxide/src/unstable/mod.rs @@ -1,6 +1,3 @@ //! Unstable and in-development features of Conjure-Oxide. -//! -//! Enabling these may introduce breaking changes that affect code compilation. -#![cfg(feature = "unstable-solver-interface")] pub mod solver_interface; diff --git a/conjure_oxide/src/unstable/solver_interface/mod.rs b/conjure_oxide/src/unstable/solver_interface/mod.rs index e846e3880..e66573089 100644 --- a/conjure_oxide/src/unstable/solver_interface/mod.rs +++ b/conjure_oxide/src/unstable/solver_interface/mod.rs @@ -1,5 +1,3 @@ -#![cfg(feature = "unstable-solver-interface")] - //! A new interface for interacting with solvers. //! //! # Example From e7b649f88ae424010f1e95f8cf0211b632544474 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Mon, 26 Feb 2024 13:29:15 +0000 Subject: [PATCH 03/10] solver-interface: refactor --- Cargo.lock | 1 + conjure_oxide/Cargo.toml | 1 + .../src/unstable/solver_interface/mod.rs | 196 ++++++------------ .../solver_interface/model_modifier.rs | 53 +++++ .../src/unstable/solver_interface/private.rs | 8 + .../solver_interface/solver_states.rs | 51 +++++ .../src/unstable/solver_interface/stats.rs | 8 + 7 files changed, 191 insertions(+), 127 deletions(-) create mode 100644 conjure_oxide/src/unstable/solver_interface/model_modifier.rs create mode 100644 conjure_oxide/src/unstable/solver_interface/private.rs create mode 100644 conjure_oxide/src/unstable/solver_interface/solver_states.rs create mode 100644 conjure_oxide/src/unstable/solver_interface/stats.rs diff --git a/Cargo.lock b/Cargo.lock index b40a5ae1d..030deacb3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -278,6 +278,7 @@ dependencies = [ "clap", "conjure_core", "conjure_rules", + "itertools", "linkme", "minion_rs", "serde", diff --git a/conjure_oxide/Cargo.toml b/conjure_oxide/Cargo.toml index c10315ede..69abdb69a 100644 --- a/conjure_oxide/Cargo.toml +++ b/conjure_oxide/Cargo.toml @@ -24,6 +24,7 @@ strum = "0.26.1" versions = "6.1.0" linkme = "0.3.22" walkdir = "2.4.0" +itertools = "0.12.1" [features] diff --git a/conjure_oxide/src/unstable/solver_interface/mod.rs b/conjure_oxide/src/unstable/solver_interface/mod.rs index e66573089..4d5151599 100644 --- a/conjure_oxide/src/unstable/solver_interface/mod.rs +++ b/conjure_oxide/src/unstable/solver_interface/mod.rs @@ -21,27 +21,24 @@ #![allow(unused)] #![warn(clippy::exhaustive_enums)] +pub mod model_modifier; +pub mod stats; + #[doc(hidden)] -mod private { - // Used to limit calling trait functions outside this module. - #[doc(hidden)] - pub struct Internal; - - // https://predr.ag/blog/definitive-guide-to-sealed-traits-in-rust/#the-trick-for-sealing-traits - // Make traits unimplementable from outside of this module. - #[doc(hidden)] - pub trait Sealed {} -} +mod private; +mod solver_states; -use self::incremental::*; +use self::model_modifier::*; use self::solver_states::*; +use self::stats::Stats; use anyhow::anyhow; use conjure_core::ast::{Domain, Expression, Model, Name}; +use itertools::Either; use std::collections::HashMap; use std::error::Error; use std::fmt::{Debug, Display}; -/// A [`SolverAdaptor`] provide an interface to an underlying solver. Used by [`Solver`]. +/// A [`SolverAdaptor`] provide an interface to an underlying solver, used by [Solver]. pub trait SolverAdaptor: private::Sealed { /// The native model type of the underlying solver. type Model: Clone; @@ -49,10 +46,10 @@ pub trait SolverAdaptor: private::Sealed { /// The native solution type of the underlying solver. type Solution: Clone; - /// The [`ModelModifier`](incremental::ModelModifier) used during incremental search. + /// The [`ModelModifier`](model_modifier::ModelModifier) used during incremental search. /// - /// If incremental solving is not supported, this SHOULD be set to [NotModifiable](`incremental::NotModifiable`) . - type Modifier: incremental::ModelModifier; + /// If incremental solving is not supported, this SHOULD be set to [NotModifiable](model_modifier::NotModifiable) . + type Modifier: model_modifier::ModelModifier; /// Run the solver on the given model. /// @@ -89,13 +86,27 @@ pub trait SolverAdaptor: private::Sealed { fn init_solver(&mut self, _: private::Internal) {} } -/// A Solver executes of a Conjure-Oxide model usign a specified solver. +/// A Solver executes a Conjure-Oxide model using a given [SolverAdaptor]. +#[derive(Clone)] pub struct Solver { - state: std::marker::PhantomData, + state: State, adaptor: A, model: Option, } +impl Solver { + pub fn new(solver_adaptor: Adaptor) -> Solver { + let mut solver = Solver { + state: Init, + adaptor: solver_adaptor, + model: None, + }; + + solver.adaptor.init_solver(private::Internal); + solver + } +} + impl Solver { // TODO: decent error handling pub fn load_model(mut self, model: Model) -> Result, ()> { @@ -104,7 +115,7 @@ impl Solver { .load_model(model, private::Internal) .map_err(|_| ())?; Ok(Solver { - state: std::marker::PhantomData::, + state: ModelLoaded, adaptor: self.adaptor, model: Some(solver_model.clone()), }) @@ -115,127 +126,58 @@ impl Solver { pub fn solve( mut self, callback: fn(HashMap) -> bool, - ) -> Result { + ) -> Either, Solver> { #[allow(clippy::unwrap_used)] - self.adaptor - .solve(self.model.unwrap(), callback, private::Internal) + let result = self + .adaptor + .solve(self.model.clone().unwrap(), callback, private::Internal); + + match result { + Ok(x) => Either::Left(Solver { + adaptor: self.adaptor, + model: self.model, + state: x, + }), + Err(x) => Either::Right(Solver { + adaptor: self.adaptor, + model: self.model, + state: x, + }), + } } pub fn solve_mut( mut self, callback: fn(HashMap, A::Modifier) -> bool, - ) -> Result { + ) -> Either, Solver> { #[allow(clippy::unwrap_used)] - self.adaptor - .solve_mut(self.model.unwrap(), callback, private::Internal) - } -} - -impl Solver { - pub fn new(solver_adaptor: T) -> Solver { - let mut solver = Solver { - state: std::marker::PhantomData::, - adaptor: solver_adaptor, - model: None, - }; - - solver.adaptor.init_solver(private::Internal); - solver + let result = + self.adaptor + .solve_mut(self.model.clone().unwrap(), callback, private::Internal); + + match result { + Ok(x) => Either::Left(Solver { + adaptor: self.adaptor, + model: self.model, + state: x, + }), + Err(x) => Either::Right(Solver { + adaptor: self.adaptor, + model: self.model, + state: x, + }), + } } } -pub mod solver_states { - //! States of a [`Solver`]. - - use super::private::Sealed; - use super::Solver; - - pub trait SolverState: Sealed {} - - impl Sealed for Init {} - impl Sealed for ModelLoaded {} - impl Sealed for ExecutionSuccess {} - impl Sealed for ExecutionFailure {} - - impl SolverState for Init {} - impl SolverState for ModelLoaded {} - impl SolverState for ExecutionSuccess {} - impl SolverState for ExecutionFailure {} - - pub struct Init; - pub struct ModelLoaded; - - /// The state returned by [`Solver`] if solving has been successful. - pub struct ExecutionSuccess; - - /// The state returned by [`Solver`] if solving has not been successful. - #[non_exhaustive] - pub enum ExecutionFailure { - /// The desired function or solver is not implemented yet. - OpNotImplemented, - - /// The solver does not support this operation. - OpNotSupported, - - /// Solving timed-out. - TimedOut, - - /// An unspecified error has occurred. - Error(anyhow::Error), +impl Solver { + pub fn stats(self) -> Box { + self.state.stats } } -pub mod incremental { - //! Incremental / mutable solving (changing the model during search). - //! - //! Incremental solving can be triggered for a solverthrough the - //! [`Solver::solve_mut`] method. - //! - //! This gives access to a [`ModelModifier`] in the solution retrieval callback. - use super::private; - use super::Solver; - use conjure_core::ast::{Domain, Expression, Model, Name}; - - /// A ModelModifier provides an interface to modify a model during solving. - /// - /// Modifications are defined in terms of Conjure AST nodes, so must be translated to a solver - /// specfic form before use. - /// - /// It is implementation defined whether these constraints can be given at high level and passed - /// through the rewriter, or only low-level solver constraints are supported. - /// - /// See also: [`Solver::solve_mut`]. - pub trait ModelModifier: private::Sealed { - fn add_constraint(constraint: Expression) -> Result<(), ModificationFailure> { - Err(ModificationFailure::OpNotSupported) - } - - fn add_variable(name: Name, domain: Domain) -> Result<(), ModificationFailure> { - Err(ModificationFailure::OpNotSupported) - } - } - - /// A [`ModelModifier`] for a solver that does not support incremental solving. Returns - /// [`OperationNotSupported`](`ModificationFailure::OperationNotSupported`) for all operations. - pub struct NotModifiable; - - impl private::Sealed for NotModifiable {} - impl ModelModifier for NotModifiable {} - - /// The requested modification to the model has failed. - #[non_exhaustive] - pub enum ModificationFailure { - /// The desired operation is not supported for this solver adaptor. - OpNotSupported, - - /// The desired operation is supported by this solver adaptor, but has not been - /// implemented yet. - OpNotImplemented, - - // The arguments given to the operation are invalid. - ArgsInvalid(anyhow::Error), - - /// An unspecified error has occurred. - Error(anyhow::Error), +impl Solver { + pub fn why(self) -> ExecutionFailure { + self.state } } diff --git a/conjure_oxide/src/unstable/solver_interface/model_modifier.rs b/conjure_oxide/src/unstable/solver_interface/model_modifier.rs new file mode 100644 index 000000000..c0cd880bf --- /dev/null +++ b/conjure_oxide/src/unstable/solver_interface/model_modifier.rs @@ -0,0 +1,53 @@ +//! Modifying a model during search. +//! +//! Incremental solving can be triggered for a solverthrough the +//! [`Solver::solve_mut`] method. +//! +//! This gives access to a [`ModelModifier`] in the solution retrieval callback. + +use super::private; +use super::Solver; +use conjure_core::ast::{Domain, Expression, Model, Name}; + +/// A ModelModifier provides an interface to modify a model during solving. +/// +/// Modifications are defined in terms of Conjure AST nodes, so must be translated to a solver +/// specfic form before use. +/// +/// It is implementation defined whether these constraints can be given at high level and passed +/// through the rewriter, or only low-level solver constraints are supported. +/// +/// See also: [`Solver::solve_mut`]. +pub trait ModelModifier: private::Sealed { + fn add_constraint(constraint: Expression) -> Result<(), ModificationFailure> { + Err(ModificationFailure::OpNotSupported) + } + + fn add_variable(name: Name, domain: Domain) -> Result<(), ModificationFailure> { + Err(ModificationFailure::OpNotSupported) + } +} + +/// A [`ModelModifier`] for a solver that does not support incremental solving. Returns +/// [`OperationNotSupported`](`ModificationFailure::OperationNotSupported`) for all operations. +pub struct NotModifiable; + +impl private::Sealed for NotModifiable {} +impl ModelModifier for NotModifiable {} + +/// The requested modification to the model has failed. +#[non_exhaustive] +pub enum ModificationFailure { + /// The desired operation is not supported for this solver adaptor. + OpNotSupported, + + /// The desired operation is supported by this solver adaptor, but has not been + /// implemented yet. + OpNotImplemented, + + // The arguments given to the operation are invalid. + ArgsInvalid(anyhow::Error), + + /// An unspecified error has occurred. + Error(anyhow::Error), +} diff --git a/conjure_oxide/src/unstable/solver_interface/private.rs b/conjure_oxide/src/unstable/solver_interface/private.rs new file mode 100644 index 000000000..67f87b89c --- /dev/null +++ b/conjure_oxide/src/unstable/solver_interface/private.rs @@ -0,0 +1,8 @@ +// Used to limit calling trait functions outside this module. +#[doc(hidden)] +pub struct Internal; + +// https://predr.ag/blog/definitive-guide-to-sealed-traits-in-rust/#the-trick-for-sealing-traits +// Make traits unimplementable from outside of this module. +#[doc(hidden)] +pub trait Sealed {} diff --git a/conjure_oxide/src/unstable/solver_interface/solver_states.rs b/conjure_oxide/src/unstable/solver_interface/solver_states.rs new file mode 100644 index 000000000..65733130f --- /dev/null +++ b/conjure_oxide/src/unstable/solver_interface/solver_states.rs @@ -0,0 +1,51 @@ +//! States of a [`Solver`]. +use std::fmt::Display; + +use thiserror::Error; + +use super::private::Internal; +use super::private::Sealed; +use super::stats::*; +use super::Solver; + +pub trait SolverState: Sealed {} + +impl Sealed for Init {} +impl Sealed for ModelLoaded {} +impl Sealed for ExecutionSuccess {} +impl Sealed for ExecutionFailure {} + +impl SolverState for Init {} +impl SolverState for ModelLoaded {} +impl SolverState for ExecutionSuccess {} +impl SolverState for ExecutionFailure {} + +pub struct Init; +pub struct ModelLoaded; + +/// The state returned by [`Solver`] if solving has been successful. +pub struct ExecutionSuccess { + /// Execution statistics. + pub stats: Box, + + // make this struct unconstructable outside of this module + #[doc(hidden)] + _private: Internal, +} + +/// The state returned by [`Solver`] if solving has not been successful. +#[non_exhaustive] +#[derive(Debug, Error)] +pub enum ExecutionFailure { + #[error("operation not implemented yet")] + OpNotImplemented, + + #[error("operation is not supported by this solver")] + OpNotSupported, + + #[error("time out")] + TimedOut, + + #[error(transparent)] + Other(#[from] anyhow::Error), +} diff --git a/conjure_oxide/src/unstable/solver_interface/stats.rs b/conjure_oxide/src/unstable/solver_interface/stats.rs new file mode 100644 index 000000000..0af598039 --- /dev/null +++ b/conjure_oxide/src/unstable/solver_interface/stats.rs @@ -0,0 +1,8 @@ +//! Statistics about a solver run. +use super::private::Sealed; + +pub trait Stats: Sealed {} + +struct NoStats; +impl Sealed for NoStats {} +impl Stats for NoStats {} From 3584af22ac05e192d2b2ed49db6a96492a59f128 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Tue, 27 Feb 2024 11:00:38 +0000 Subject: [PATCH 04/10] solver-interface: more docs --- .../unstable/solver_interface/adaptors/mod.rs | 1 + .../src/unstable/solver_interface/mod.rs | 65 +++++++++++++++---- 2 files changed, 55 insertions(+), 11 deletions(-) create mode 100644 conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs diff --git a/conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs b/conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs new file mode 100644 index 000000000..fcc9a8e4a --- /dev/null +++ b/conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs @@ -0,0 +1 @@ +//! Solver adaptors. diff --git a/conjure_oxide/src/unstable/solver_interface/mod.rs b/conjure_oxide/src/unstable/solver_interface/mod.rs index 4d5151599..728887575 100644 --- a/conjure_oxide/src/unstable/solver_interface/mod.rs +++ b/conjure_oxide/src/unstable/solver_interface/mod.rs @@ -1,8 +1,39 @@ -//! A new interface for interacting with solvers. +//! A high-level API for interacting with constraints solvers. +//! +//! This module provides a consistent, solver-independent API for interacting with constraints +//! solvers. It also provides incremental solving support, and the returning of run stats from +//! solvers. +//! +//! ----- +//! +//! - [Solver] provides the API for interacting with constraints solvers. +//! +//! - The [SolverAdaptor] trait controls how solving actually occurs and handles translation +//! between the [Solver] type and a specific solver. +//! +//! - [adaptors] contains all implemented solver adaptors. +//! +//! - The [model_modifier] submodule defines types to help with incremental solving / changing a +//! model during search. The entrypoint for incremental solving is the [Solver::solve_mut] +//! function. +//! +//! # Examples +//! +//! ## A Successful Minion Model +//! +//! ``` +//! # use conjure_oxide::generate_custom::get_example_model; +//! # use conjure_oxide::rule_engine::rewrite::rewrite_model; +//! # use conjure_oxide::rule_engine::resolve_rules::resolve_rule_sets; +//! +//! // Let's solve a simple model with Minion. +//! let model = get_example_model("bool-03").unwrap(); +//! let rule_sets = resolve_rule_sets(vec!["Minion", "Constant"]).unwrap(); +//! let model = rewrite_model(&model,&rule_sets); +//! todo!() +//! ``` //! -//! # Example //! -//! TODO // # Implementing Solver interfaces // @@ -21,6 +52,7 @@ #![allow(unused)] #![warn(clippy::exhaustive_enums)] +pub mod adaptors; pub mod model_modifier; pub mod stats; @@ -38,7 +70,7 @@ use std::collections::HashMap; use std::error::Error; use std::fmt::{Debug, Display}; -/// A [`SolverAdaptor`] provide an interface to an underlying solver, used by [Solver]. +/// A common interface for calling underlying solver APIs inside a [Solver]. pub trait SolverAdaptor: private::Sealed { /// The native model type of the underlying solver. type Model: Clone; @@ -48,12 +80,12 @@ pub trait SolverAdaptor: private::Sealed { /// The [`ModelModifier`](model_modifier::ModelModifier) used during incremental search. /// - /// If incremental solving is not supported, this SHOULD be set to [NotModifiable](model_modifier::NotModifiable) . + /// If incremental solving is not supported, this **should** be set to [NotModifiable](model_modifier::NotModifiable) . type Modifier: model_modifier::ModelModifier; - /// Run the solver on the given model. + /// Runs the solver on the given model. /// - /// Implementations of this function MUST call the user provided callback whenever a solution + /// Implementations of this function *must** call the user provided callback whenever a solution /// is found. If the user callback returns `true`, search should continue, if the user callback /// returns `false`, search should terminate. fn solve( @@ -63,14 +95,14 @@ pub trait SolverAdaptor: private::Sealed { _: private::Internal, ) -> Result; - /// Run the solver on the given model, allowing modification of the model through a + /// Runs the solver on the given model, allowing modification of the model through a /// [`ModelModifier`]. /// - /// Implementations of this function MUST return [`OpNotSupported`](`ModificationFailure::OpNotSupported`) + /// Implementations of this function **must** return [`OpNotSupported`](`ModificationFailure::OpNotSupported`) /// if modifying the model mid-search is not supported. These implementations may also find the /// [`NotModifiable`] modifier useful. /// - /// As with [`solve`](SolverAdaptor::solve), this function MUST call the user provided callback + /// As with [`solve`](SolverAdaptor::solve), this function **must** call the user provided callback /// function whenever a solution is found. fn solve_mut( &mut self, @@ -86,7 +118,18 @@ pub trait SolverAdaptor: private::Sealed { fn init_solver(&mut self, _: private::Internal) {} } -/// A Solver executes a Conjure-Oxide model using a given [SolverAdaptor]. +/// An abstract representation of a constraints solver. +/// +/// [Solver] provides a common interface for interacting with a constraint solver. It also +/// abstracts over solver-specific datatypes, handling the translation to/from [conjure_core::ast] +/// types for a model and its solutions. +/// +/// Details of how a model is solved is specified by the [SolverAdaptor]. This includes: the +/// underlying solver used, the translation of the model to a solver compatible form, how solutions +/// are translated back to [conjure_core::ast] types, and how incremental solving is implemented. +/// As such, there may be multiple [SolverAdaptor] implementations for a single underlying solver: +/// eg. one adaptor may give solutions in a representation close to the solvers, while another may +/// attempt to rewrite it back into Essence. #[derive(Clone)] pub struct Solver { state: State, From 44045db1c0492cbfef2cd0c9849851d869bf4a87 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Tue, 27 Feb 2024 12:11:53 +0000 Subject: [PATCH 05/10] solver-interface: load a minion model --- .../solver_interface/adaptors/minion.rs | 237 ++++++++++++++++++ .../unstable/solver_interface/adaptors/mod.rs | 3 + .../src/unstable/solver_interface/mod.rs | 92 +++++-- .../{solver_states.rs => states.rs} | 25 +- 4 files changed, 317 insertions(+), 40 deletions(-) create mode 100644 conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs rename conjure_oxide/src/unstable/solver_interface/{solver_states.rs => states.rs} (61%) diff --git a/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs b/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs new file mode 100644 index 000000000..a455c7a26 --- /dev/null +++ b/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs @@ -0,0 +1,237 @@ +use crate::unstable::solver_interface::states; + +use super::super::model_modifier::NotModifiable; +use super::super::private; +use super::super::SolveSuccess; +use super::super::SolverAdaptor; +use super::super::SolverError; +use super::super::SolverError::*; + +use crate::ast as conjureast; +use minion_rs::ast as minionast; + +/// A [SolverAdaptor] for interacting with Minion. +/// +/// This adaptor uses the `minion_rs` crate to talk to Minion over FFI. +pub struct Minion; + +impl private::Sealed for Minion {} +impl SolverAdaptor for Minion { + type Model = minionast::Model; + type Solution = minionast::Constant; + type Modifier = NotModifiable; + + fn solve( + &mut self, + model: Self::Model, + callback: fn(std::collections::HashMap) -> bool, + _: private::Internal, + ) -> Result { + Err(OpNotImplemented("solve".into())) + } + + fn solve_mut( + &mut self, + model: Self::Model, + callback: fn(std::collections::HashMap, Self::Modifier) -> bool, + _: private::Internal, + ) -> Result { + Err(OpNotImplemented("solve_mut".into())) + } + + fn load_model( + &mut self, + model: conjure_core::ast::Model, + _: private::Internal, + ) -> Result { + let mut minion_model = minionast::Model::new(); + parse_vars(&model, &mut minion_model)?; + parse_exprs(&model, &mut minion_model)?; + Ok(minion_model) + } +} + +fn parse_vars( + conjure_model: &conjureast::Model, + minion_model: &mut minionast::Model, +) -> Result<(), SolverError> { + // TODO (nd60): remove unused vars? + // TODO (nd60): ensure all vars references are used. + + for (name, variable) in conjure_model.variables.iter() { + parse_var(name, variable, minion_model)?; + } + Ok(()) +} + +fn parse_var( + name: &conjureast::Name, + var: &conjureast::DecisionVariable, + minion_model: &mut minionast::Model, +) -> Result<(), SolverError> { + match &var.domain { + conjureast::Domain::IntDomain(ranges) => _parse_intdomain_var(name, ranges, minion_model), + conjureast::Domain::BoolDomain => _parse_booldomain_var(name, minion_model), + x => Err(ModelFeatureNotSupported(format!("{:?}", x))), + } +} + +fn _parse_intdomain_var( + name: &conjureast::Name, + ranges: &Vec>, + minion_model: &mut minionast::Model, +) -> Result<(), SolverError> { + let str_name = _name_to_string(name.to_owned()); + + if ranges.len() != 1 { + return Err(ModelFeatureNotImplemented(format!( + "variable {:?} has {:?} ranges. Multiple ranges / SparseBound is not yet supported.", + str_name, + ranges.len() + ))); + } + + let range = ranges.first().ok_or(ModelInvalid(format!( + "variable {:?} has no range", + str_name + )))?; + + let (low, high) = match range { + conjureast::Range::Bounded(x, y) => Ok((x.to_owned(), y.to_owned())), + conjureast::Range::Single(x) => Ok((x.to_owned(), x.to_owned())), + #[allow(unreachable_patterns)] + x => Err(ModelFeatureNotSupported(format!("{:?}", x))), + }?; + + _try_add_var( + str_name.to_owned(), + minionast::VarDomain::Bound(low, high), + minion_model, + ) +} + +fn _parse_booldomain_var( + name: &conjureast::Name, + minion_model: &mut minionast::Model, +) -> Result<(), SolverError> { + let str_name = _name_to_string(name.to_owned()); + _try_add_var( + str_name.to_owned(), + minionast::VarDomain::Bool, + minion_model, + ) +} + +fn _try_add_var( + name: minionast::VarName, + domain: minionast::VarDomain, + minion_model: &mut minionast::Model, +) -> Result<(), SolverError> { + minion_model + .named_variables + .add_var(name.clone(), domain) + .ok_or(ModelInvalid(format!( + "variable {:?} is defined twice", + name + ))) +} + +fn parse_exprs( + conjure_model: &conjureast::Model, + minion_model: &mut minionast::Model, +) -> Result<(), SolverError> { + for expr in conjure_model.get_constraints_vec().iter() { + parse_expr(expr.to_owned(), minion_model)?; + } + Ok(()) +} + +fn parse_expr( + expr: conjureast::Expression, + minion_model: &mut minionast::Model, +) -> Result<(), SolverError> { + match expr { + conjureast::Expression::SumLeq(_metadata, lhs, rhs) => { + minion_model.constraints.push(minionast::Constraint::SumLeq( + read_vars(lhs)?, + read_var(*rhs)?, + )); + Ok(()) + } + conjureast::Expression::SumGeq(_metadata, lhs, rhs) => { + minion_model.constraints.push(minionast::Constraint::SumGeq( + read_vars(lhs)?, + read_var(*rhs)?, + )); + Ok(()) + } + conjureast::Expression::Ineq(_metadata, a, b, c) => { + minion_model.constraints.push(minionast::Constraint::Ineq( + read_var(*a)?, + read_var(*b)?, + minionast::Constant::Integer(read_const(*c)?), + )); + Ok(()) + } + conjureast::Expression::Neq(_metadata, a, b) => { + minion_model + .constraints + .push(minionast::Constraint::WatchNeq( + read_var(*a)?, + read_var(*b)?, + )); + Ok(()) + } + x => Err(ModelFeatureNotSupported(format!("{:?}", x))), + } +} + +fn read_vars(exprs: Vec) -> Result, SolverError> { + let mut minion_vars: Vec = vec![]; + for expr in exprs { + let minion_var = read_var(expr)?; + minion_vars.push(minion_var); + } + Ok(minion_vars) +} + +fn read_var(e: conjureast::Expression) -> Result { + // a minion var is either a reference or a "var as const" + match _read_ref(e.clone()) { + Ok(name) => Ok(minionast::Var::NameRef(name)), + Err(_) => match read_const(e) { + Ok(n) => Ok(minionast::Var::ConstantAsVar(n)), + Err(x) => Err(x), + }, + } +} + +fn _read_ref(e: conjureast::Expression) -> Result { + let name = match e { + conjureast::Expression::Reference(_metdata, n) => Ok(n), + x => Err(ModelInvalid(format!( + "expected a reference, but got `{0:?}`", + x + ))), + }?; + + let str_name = _name_to_string(name); + Ok(str_name) +} + +fn read_const(e: conjureast::Expression) -> Result { + match e { + conjureast::Expression::Constant(_, conjureast::Constant::Int(n)) => Ok(n), + x => Err(ModelInvalid(format!( + "expected a constant, but got `{0:?}`", + x + ))), + } +} + +fn _name_to_string(name: conjureast::Name) -> String { + match name { + conjureast::Name::UserName(x) => x, + conjureast::Name::MachineName(x) => x.to_string(), + } +} diff --git a/conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs b/conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs index fcc9a8e4a..346ffcfee 100644 --- a/conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs +++ b/conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs @@ -1 +1,4 @@ //! Solver adaptors. + +pub mod minion; +pub use minion::Minion; diff --git a/conjure_oxide/src/unstable/solver_interface/mod.rs b/conjure_oxide/src/unstable/solver_interface/mod.rs index 728887575..48a613590 100644 --- a/conjure_oxide/src/unstable/solver_interface/mod.rs +++ b/conjure_oxide/src/unstable/solver_interface/mod.rs @@ -23,13 +23,20 @@ //! //! ``` //! # use conjure_oxide::generate_custom::get_example_model; -//! # use conjure_oxide::rule_engine::rewrite::rewrite_model; -//! # use conjure_oxide::rule_engine::resolve_rules::resolve_rule_sets; +//! use conjure_oxide::rule_engine::rewrite::rewrite_model; +//! use conjure_oxide::rule_engine::resolve_rules::resolve_rule_sets; +//! use conjure_oxide::unstable::solver_interface::{Solver,adaptors}; +//! use conjure_oxide::unstable::solver_interface::states::*; //! -//! // Let's solve a simple model with Minion. +//! // Define and rewrite a model for minion. //! let model = get_example_model("bool-03").unwrap(); //! let rule_sets = resolve_rule_sets(vec!["Minion", "Constant"]).unwrap(); -//! let model = rewrite_model(&model,&rule_sets); +//! let model = rewrite_model(&model,&rule_sets).unwrap(); +//! +//! +//! // Solve using Minion. +//! let solver = Solver::using(adaptors::Minion); +//! let solver: Solver = solver.load_model(model).unwrap(); //! todo!() //! ``` //! @@ -58,10 +65,11 @@ pub mod stats; #[doc(hidden)] mod private; -mod solver_states; + +pub mod states; use self::model_modifier::*; -use self::solver_states::*; +use self::states::*; use self::stats::Stats; use anyhow::anyhow; use conjure_core::ast::{Domain, Expression, Model, Name}; @@ -69,6 +77,7 @@ use itertools::Either; use std::collections::HashMap; use std::error::Error; use std::fmt::{Debug, Display}; +use thiserror::Error; /// A common interface for calling underlying solver APIs inside a [Solver]. pub trait SolverAdaptor: private::Sealed { @@ -93,7 +102,7 @@ pub trait SolverAdaptor: private::Sealed { model: Self::Model, callback: fn(HashMap) -> bool, _: private::Internal, - ) -> Result; + ) -> Result; /// Runs the solver on the given model, allowing modification of the model through a /// [`ModelModifier`]. @@ -109,12 +118,12 @@ pub trait SolverAdaptor: private::Sealed { model: Self::Model, callback: fn(HashMap, Self::Modifier) -> bool, _: private::Internal, - ) -> Result; + ) -> Result; fn load_model( &mut self, model: Model, _: private::Internal, - ) -> Result; + ) -> Result; fn init_solver(&mut self, _: private::Internal) {} } @@ -138,7 +147,7 @@ pub struct Solver { } impl Solver { - pub fn new(solver_adaptor: Adaptor) -> Solver { + pub fn using(solver_adaptor: Adaptor) -> Solver { let mut solver = Solver { state: Init, adaptor: solver_adaptor, @@ -151,12 +160,8 @@ impl Solver { } impl Solver { - // TODO: decent error handling - pub fn load_model(mut self, model: Model) -> Result, ()> { - let solver_model = &mut self - .adaptor - .load_model(model, private::Internal) - .map_err(|_| ())?; + pub fn load_model(mut self, model: Model) -> Result, SolverError> { + let solver_model = &mut self.adaptor.load_model(model, private::Internal)?; Ok(Solver { state: ModelLoaded, adaptor: self.adaptor, @@ -179,12 +184,18 @@ impl Solver { Ok(x) => Either::Left(Solver { adaptor: self.adaptor, model: self.model, - state: x, + state: ExecutionSuccess { + stats: x.stats, + _sealed: private::Internal, + }, }), Err(x) => Either::Right(Solver { adaptor: self.adaptor, model: self.model, - state: x, + state: ExecutionFailure { + why: x, + _sealed: private::Internal, + }, }), } } @@ -202,25 +213,60 @@ impl Solver { Ok(x) => Either::Left(Solver { adaptor: self.adaptor, model: self.model, - state: x, + state: ExecutionSuccess { + stats: x.stats, + _sealed: private::Internal, + }, }), Err(x) => Either::Right(Solver { adaptor: self.adaptor, model: self.model, - state: x, + state: ExecutionFailure { + why: x, + _sealed: private::Internal, + }, }), } } } impl Solver { - pub fn stats(self) -> Box { + pub fn stats(self) -> Option> { self.state.stats } } impl Solver { - pub fn why(self) -> ExecutionFailure { - self.state + pub fn why(&self) -> SolverError { + self.state.why.clone() } } + +/// Errors returned by [Solver] on failure. +#[non_exhaustive] +#[derive(Debug, Error, Clone)] +pub enum SolverError { + #[error("operation not implemented yet: {0}")] + OpNotImplemented(String), + + #[error("operation not supported: {0}")] + OpNotSupported(String), + + #[error("model feature not supported: {0}")] + ModelFeatureNotSupported(String), + + #[error("model feature not implemented yet: {0}")] + ModelFeatureNotImplemented(String), + + // use for semantics / type errors, use the above for syntax + #[error("model invalid: {0}")] + ModelInvalid(String), + + #[error("time out")] + TimeOut, +} + +/// Returned from [SolverAdaptor] when solving is successful. +pub struct SolveSuccess { + stats: Option>, +} diff --git a/conjure_oxide/src/unstable/solver_interface/solver_states.rs b/conjure_oxide/src/unstable/solver_interface/states.rs similarity index 61% rename from conjure_oxide/src/unstable/solver_interface/solver_states.rs rename to conjure_oxide/src/unstable/solver_interface/states.rs index 65733130f..a1eeab7d2 100644 --- a/conjure_oxide/src/unstable/solver_interface/solver_states.rs +++ b/conjure_oxide/src/unstable/solver_interface/states.rs @@ -7,6 +7,7 @@ use super::private::Internal; use super::private::Sealed; use super::stats::*; use super::Solver; +use super::SolverError; pub trait SolverState: Sealed {} @@ -26,26 +27,16 @@ pub struct ModelLoaded; /// The state returned by [`Solver`] if solving has been successful. pub struct ExecutionSuccess { /// Execution statistics. - pub stats: Box, + pub stats: Option>, - // make this struct unconstructable outside of this module - #[doc(hidden)] - _private: Internal, + /// Cannot construct this from outside this module. + pub _sealed: Internal, } /// The state returned by [`Solver`] if solving has not been successful. -#[non_exhaustive] -#[derive(Debug, Error)] -pub enum ExecutionFailure { - #[error("operation not implemented yet")] - OpNotImplemented, +pub struct ExecutionFailure { + pub why: SolverError, - #[error("operation is not supported by this solver")] - OpNotSupported, - - #[error("time out")] - TimedOut, - - #[error(transparent)] - Other(#[from] anyhow::Error), + /// Cannot construct this from outside this module. + pub _sealed: Internal, } From d256aea3860b125959a3f21dab0f3a7c54edb527 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Thu, 29 Feb 2024 10:50:10 +0000 Subject: [PATCH 06/10] solver-interface: use closures not function pointers to get results out --- .../unstable/solver_interface/adaptors/minion.rs | 7 ++++--- conjure_oxide/src/unstable/solver_interface/mod.rs | 14 ++++++++++---- 2 files changed, 14 insertions(+), 7 deletions(-) diff --git a/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs b/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs index a455c7a26..80e70f5be 100644 --- a/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs +++ b/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs @@ -1,4 +1,5 @@ -use crate::unstable::solver_interface::states; +use crate::unstable::solver_interface::SolverMutCallback; +use crate::unstable::solver_interface::{states, SolverCallback}; use super::super::model_modifier::NotModifiable; use super::super::private; @@ -24,7 +25,7 @@ impl SolverAdaptor for Minion { fn solve( &mut self, model: Self::Model, - callback: fn(std::collections::HashMap) -> bool, + callback: SolverCallback, _: private::Internal, ) -> Result { Err(OpNotImplemented("solve".into())) @@ -33,7 +34,7 @@ impl SolverAdaptor for Minion { fn solve_mut( &mut self, model: Self::Model, - callback: fn(std::collections::HashMap, Self::Modifier) -> bool, + callback: SolverMutCallback, _: private::Internal, ) -> Result { Err(OpNotImplemented("solve_mut".into())) diff --git a/conjure_oxide/src/unstable/solver_interface/mod.rs b/conjure_oxide/src/unstable/solver_interface/mod.rs index 48a613590..b90edb0f0 100644 --- a/conjure_oxide/src/unstable/solver_interface/mod.rs +++ b/conjure_oxide/src/unstable/solver_interface/mod.rs @@ -72,6 +72,8 @@ use self::model_modifier::*; use self::states::*; use self::stats::Stats; use anyhow::anyhow; +use conjure_core::ast::Constant; +use conjure_core::ast::DecisionVariable; use conjure_core::ast::{Domain, Expression, Model, Name}; use itertools::Either; use std::collections::HashMap; @@ -79,6 +81,10 @@ use std::error::Error; use std::fmt::{Debug, Display}; use thiserror::Error; +pub type SolverCallback = Box) -> bool + Send>; +pub type SolverMutCallback = + Box, ::Modifier) -> bool + Send>; + /// A common interface for calling underlying solver APIs inside a [Solver]. pub trait SolverAdaptor: private::Sealed { /// The native model type of the underlying solver. @@ -100,7 +106,7 @@ pub trait SolverAdaptor: private::Sealed { fn solve( &mut self, model: Self::Model, - callback: fn(HashMap) -> bool, + callback: SolverCallback, _: private::Internal, ) -> Result; @@ -116,7 +122,7 @@ pub trait SolverAdaptor: private::Sealed { fn solve_mut( &mut self, model: Self::Model, - callback: fn(HashMap, Self::Modifier) -> bool, + callback: SolverMutCallback, _: private::Internal, ) -> Result; fn load_model( @@ -173,7 +179,7 @@ impl Solver { impl Solver { pub fn solve( mut self, - callback: fn(HashMap) -> bool, + callback: SolverCallback, ) -> Either, Solver> { #[allow(clippy::unwrap_used)] let result = self @@ -202,7 +208,7 @@ impl Solver { pub fn solve_mut( mut self, - callback: fn(HashMap, A::Modifier) -> bool, + callback: SolverMutCallback, ) -> Either, Solver> { #[allow(clippy::unwrap_used)] let result = From f7613065d906b3e5fbd67244fa549c8b3cf31c53 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Sun, 3 Mar 2024 20:52:34 +0000 Subject: [PATCH 07/10] solver-interface: solver.solve() with minion --- .../solver_interface/adaptors/minion.rs | 74 ++++++++++++++++++- .../src/unstable/solver_interface/mod.rs | 32 +++++++- .../src/unstable/solver_interface/stats.rs | 2 +- 3 files changed, 103 insertions(+), 5 deletions(-) diff --git a/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs b/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs index 80e70f5be..7b1e84512 100644 --- a/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs +++ b/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs @@ -1,13 +1,19 @@ +use std::collections::HashMap; +use std::sync::{Condvar, Mutex, OnceLock}; + use crate::unstable::solver_interface::SolverMutCallback; use crate::unstable::solver_interface::{states, SolverCallback}; use super::super::model_modifier::NotModifiable; use super::super::private; +use super::super::stats::NoStats; use super::super::SolveSuccess; use super::super::SolverAdaptor; use super::super::SolverError; use super::super::SolverError::*; +use minion_rs::run_minion; + use crate::ast as conjureast; use minion_rs::ast as minionast; @@ -16,19 +22,81 @@ use minion_rs::ast as minionast; /// This adaptor uses the `minion_rs` crate to talk to Minion over FFI. pub struct Minion; +static MINION_LOCKED: Mutex = Mutex::new(false); +static MINION_CONDVAR: Condvar = Condvar::new(); +static USER_CALLBACK: OnceLock> = OnceLock::new(); + +fn minion_rs_callback(solutions: HashMap) -> bool { + #[allow(clippy::unwrap_used)] + let callback = USER_CALLBACK + .get_or_init(|| Mutex::new(Box::new(|x| true))) + .lock() + .unwrap(); + + let mut conjure_solutions: HashMap = HashMap::new(); + for (minion_name, minion_const) in solutions.into_iter() { + let conjure_const = match minion_const { + minionast::Constant::Bool(x) => conjureast::Constant::Bool(x), + minionast::Constant::Integer(x) => conjureast::Constant::Int(x), + _ => todo!(), + }; + + //FIXME (niklasdewally): what about machine names? + let conjure_name = conjureast::Name::UserName(minion_name); + conjure_solutions.insert(conjure_name, conjure_const); + } + + (**callback)(conjure_solutions) +} + impl private::Sealed for Minion {} impl SolverAdaptor for Minion { type Model = minionast::Model; type Solution = minionast::Constant; type Modifier = NotModifiable; + #[allow(clippy::unwrap_used)] fn solve( &mut self, model: Self::Model, callback: SolverCallback, _: private::Internal, ) -> Result { - Err(OpNotImplemented("solve".into())) + // our minion callback is global state, so single threading the adaptor as a whole is + // probably a good move... + #[allow(clippy::unwrap_used)] + let mut locked = MINION_LOCKED.lock().unwrap(); + + #[allow(clippy::unwrap_used)] + while *locked { + locked = MINION_CONDVAR.wait(locked).unwrap(); + } + *locked = true; + + let mut user_callback = USER_CALLBACK + .get_or_init(|| Mutex::new(Box::new(|x| true))) + .lock() + .unwrap(); + *user_callback = callback; + std::mem::drop(user_callback); // release mutex. REQUIRED so that run_minion can use the + // user callback and not deadlock. + + minion_rs::run_minion(model, minion_rs_callback).map_err(|err| match err { + minion_rs::error::MinionError::RuntimeError(x) => { + SolverError::Runtime(format!("{:#?}", x)) + } + minion_rs::error::MinionError::Other(x) => SolverError::Runtime(format!("{:#?}", x)), + minion_rs::error::MinionError::NotImplemented(x) => { + SolverError::RuntimeNotImplemented(x) + } + x => SolverError::Runtime(format!("unknown minion_rs error: {:#?}", x)), + })?; + + *locked = false; + std::mem::drop(locked); // unlock mutex + MINION_CONDVAR.notify_one(); // wake up waiting threads + + Ok(SolveSuccess { stats: None }) } fn solve_mut( @@ -56,8 +124,8 @@ fn parse_vars( conjure_model: &conjureast::Model, minion_model: &mut minionast::Model, ) -> Result<(), SolverError> { - // TODO (nd60): remove unused vars? - // TODO (nd60): ensure all vars references are used. + // TODO (niklasdewally): remove unused vars? + // TODO (niklasdewally): ensure all vars references are used. for (name, variable) in conjure_model.variables.iter() { parse_var(name, variable, minion_model)?; diff --git a/conjure_oxide/src/unstable/solver_interface/mod.rs b/conjure_oxide/src/unstable/solver_interface/mod.rs index b90edb0f0..e79ddca1f 100644 --- a/conjure_oxide/src/unstable/solver_interface/mod.rs +++ b/conjure_oxide/src/unstable/solver_interface/mod.rs @@ -27,6 +27,7 @@ //! use conjure_oxide::rule_engine::resolve_rules::resolve_rule_sets; //! use conjure_oxide::unstable::solver_interface::{Solver,adaptors}; //! use conjure_oxide::unstable::solver_interface::states::*; +//! use std::sync::{Arc,Mutex}; //! //! // Define and rewrite a model for minion. //! let model = get_example_model("bool-03").unwrap(); @@ -37,7 +38,30 @@ //! // Solve using Minion. //! let solver = Solver::using(adaptors::Minion); //! let solver: Solver = solver.load_model(model).unwrap(); -//! todo!() +//! +//! // In this example, we will count solutions. +//! // +//! // The solver interface is designed to allow adaptors to use multiple-threads / processes if +//! // necessary. Therefore, the callback type requires all variables inside it to have a static +//! // lifetime and to implement Send (i.e. the variable can be safely shared between theads). +//! // +//! // We use Arc> to create multiple references to a threadsafe mutable +//! // variable of type T. +//! // +//! // Using the move |x| ... closure syntax, we move one of these references into the closure. +//! // Note that a normal closure borrow variables from the parent so is not +//! // thread-safe. +//! +//! let counter_ref = Arc::new(Mutex::new(0)); +//! let counter_ref_2 = counter_ref.clone(); +//! solver.solve(Box::new(move |_| { +//! let mut counter = (*counter_ref_2).lock().unwrap(); +//! *counter += 1; +//! true +//! })); +//! +//! let mut counter = (*counter_ref).lock().unwrap(); +//! assert_eq!(*counter,2); //! ``` //! //! @@ -270,6 +294,12 @@ pub enum SolverError { #[error("time out")] TimeOut, + + #[error("error during solver execution: not implemented: {0}")] + RuntimeNotImplemented(String), + + #[error("error during solver execution: {0}")] + Runtime(String), } /// Returned from [SolverAdaptor] when solving is successful. diff --git a/conjure_oxide/src/unstable/solver_interface/stats.rs b/conjure_oxide/src/unstable/solver_interface/stats.rs index 0af598039..6aa14db07 100644 --- a/conjure_oxide/src/unstable/solver_interface/stats.rs +++ b/conjure_oxide/src/unstable/solver_interface/stats.rs @@ -3,6 +3,6 @@ use super::private::Sealed; pub trait Stats: Sealed {} -struct NoStats; +pub struct NoStats; impl Sealed for NoStats {} impl Stats for NoStats {} From e1c65393890f9acb726f813a81132665cc00fd15 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Sun, 3 Mar 2024 21:13:04 +0000 Subject: [PATCH 08/10] migrate integration text suite to new solver interface --- conjure_oxide/src/utils/conjure.rs | 89 +++++-------------- conjure_oxide/src/utils/testing.rs | 13 +-- .../01/bool-01.expected-minion.solutions.json | 4 +- .../02/bool-02.expected-minion.solutions.json | 16 ++-- .../03/bool-03.expected-minion.solutions.json | 8 +- .../xyz/input.expected-minion.solutions.json | 12 +-- 6 files changed, 51 insertions(+), 91 deletions(-) diff --git a/conjure_oxide/src/utils/conjure.rs b/conjure_oxide/src/utils/conjure.rs index b0c903482..6ece30c56 100644 --- a/conjure_oxide/src/utils/conjure.rs +++ b/conjure_oxide/src/utils/conjure.rs @@ -1,19 +1,15 @@ use crate::parse::model_from_json; -use crate::solvers::minion::MinionModel; -use crate::solvers::FromConjureModel; use crate::utils::json::sort_json_object; use crate::Error as ParseErr; -use conjure_core::ast::Model; -use minion_rs::ast::{Constant, VarName}; -use minion_rs::run_minion; +use conjure_core::ast::{Constant, Model, Name}; +use itertools::Either::{Left, Right}; use serde_json::{Map, Value as JsonValue}; use std::collections::HashMap; -use std::ops::Deref; -use std::sync::{Condvar, Mutex}; +use std::sync::{Arc, Mutex}; use thiserror::Error as ThisError; -static ALL_SOLUTIONS: Mutex>> = Mutex::new(vec![]); -static LOCK: (Mutex, Condvar) = (Mutex::new(false), Condvar::new()); +use crate::unstable::solver_interface::adaptors::Minion; +use crate::unstable::solver_interface::Solver; #[derive(Debug, ThisError)] pub enum EssenceParseError { @@ -61,75 +57,38 @@ pub fn parse_essence_file(path: &str, filename: &str) -> Result Result>, anyhow::Error> { - fn callback(solutions: HashMap) -> bool { - match ALL_SOLUTIONS.lock() { - Ok(mut guard) => { - guard.push(solutions); - true - } - Err(e) => { - eprintln!("Error getting lock on ALL_SOLUTIONS: {}", e); - false - } - } - } +pub fn get_minion_solutions(model: Model) -> Result>, anyhow::Error> { + let solver = Solver::using(Minion); println!("Building Minion model..."); - let minion_model = MinionModel::from_conjure(model)?; - - // @niklasdewally would be able to explain this better - // We use a condvar to keep a lock on the ALL_SOLUTIONS mutex until it goes out of scope - // So, no other threads can mutate ALL_SOLUTIONS while we're running Minion, only our callback can - let (lock, condvar) = &LOCK; - #[allow(clippy::unwrap_used)] // If the mutex is poisoned, we want to panic anyway - let mut _lock_guard = condvar - .wait_while(lock.lock().unwrap(), |locked| *locked) - .unwrap(); - - *_lock_guard = true; + let solver = solver.load_model(model)?; println!("Running Minion..."); - match run_minion(minion_model, callback) { - Ok(res) => res, - Err(e) => { - eprintln!("Error running Minion: {}", e); - return Err(anyhow::anyhow!("Error running Minion: {}", e)); - } - }; - let ans = match ALL_SOLUTIONS.lock() { - Ok(mut guard) => { - let ans = guard.deref().clone(); - guard.clear(); // Clear the solutions for the next test - ans + let all_solutions_ref = Arc::new(Mutex::>>::new(vec![])); + let all_solutions_ref_2 = all_solutions_ref.clone(); + let solver_state = solver.solve(Box::new(move |sols| { + let mut all_solutions = (*all_solutions_ref_2).lock().unwrap(); + (*all_solutions).push(sols); + true + })); + + match solver_state { + Left(x) => { + let all_solutions = (*all_solutions_ref).lock().unwrap(); + Ok(all_solutions.clone()) } - Err(e) => { - eprintln!("Error getting lock on ALL_SOLUTIONS: {}", e); - return Err(anyhow::anyhow!( - "Error getting lock on ALL_SOLUTIONS: {}", - e - )); - } - }; - - // Release the lock and wake the next waiting thread - *_lock_guard = false; - std::mem::drop(_lock_guard); - condvar.notify_one(); - - Ok(ans) + Right(x) => Err(anyhow::Error::from(x.why())), + } } -pub fn minion_solutions_to_json(solutions: &Vec>) -> JsonValue { +pub fn minion_solutions_to_json(solutions: &Vec>) -> JsonValue { let mut json_solutions = Vec::new(); for solution in solutions { let mut json_solution = Map::new(); for (var_name, constant) in solution { let serialized_constant = match constant { - Constant::Integer(i) => JsonValue::Number((*i).into()), + Constant::Int(i) => JsonValue::Number((*i).into()), Constant::Bool(b) => JsonValue::Bool(*b), x => unimplemented!("{:#?}", x), }; diff --git a/conjure_oxide/src/utils/testing.rs b/conjure_oxide/src/utils/testing.rs index 3b3884613..6b9b72241 100644 --- a/conjure_oxide/src/utils/testing.rs +++ b/conjure_oxide/src/utils/testing.rs @@ -2,7 +2,8 @@ use crate::utils::conjure::minion_solutions_to_json; use crate::utils::json::sort_json_object; use crate::utils::misc::to_set; use crate::Error; -use conjure_core::ast::Model as ConjureModel; +use conjure_core::ast::Name::UserName; +use conjure_core::ast::{Constant, Model as ConjureModel, Name}; use minion_rs::ast::{Constant as MinionConstant, VarName as MinionVarName}; use serde_json::{Error as JsonError, Value as JsonValue}; use std::collections::{HashMap, HashSet}; @@ -85,7 +86,7 @@ pub fn read_model_json( pub fn minion_solutions_from_json( serialized: &str, -) -> Result>, anyhow::Error> { +) -> Result>, anyhow::Error> { let json: JsonValue = serde_json::from_str(serialized)?; let json_array = json @@ -106,13 +107,13 @@ pub fn minion_solutions_from_json( let n = n .as_i64() .ok_or(Error::Parse("Invalid integer".to_owned()))?; - MinionConstant::Integer(n as i32) + Constant::Int(n as i32) } - JsonValue::Bool(b) => MinionConstant::Bool(*b), + JsonValue::Bool(b) => Constant::Bool(*b), _ => return Err(Error::Parse("Invalid constant".to_owned()).into()), }; - sol.insert(MinionVarName::from(var_name), constant); + sol.insert(UserName(var_name.into()), constant); } solutions.push(sol); @@ -122,7 +123,7 @@ pub fn minion_solutions_from_json( } pub fn save_minion_solutions_json( - solutions: &Vec>, + solutions: &Vec>, path: &str, test_name: &str, accept: bool, diff --git a/conjure_oxide/tests/integration/basic/bool/01/bool-01.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/bool/01/bool-01.expected-minion.solutions.json index 991d98a76..293ab86db 100644 --- a/conjure_oxide/tests/integration/basic/bool/01/bool-01.expected-minion.solutions.json +++ b/conjure_oxide/tests/integration/basic/bool/01/bool-01.expected-minion.solutions.json @@ -1,8 +1,8 @@ [ { - "x": 0 + "UserName(x)": 0 }, { - "x": 1 + "UserName(x)": 1 } ] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/bool/02/bool-02.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/bool/02/bool-02.expected-minion.solutions.json index a35964e6c..261073022 100644 --- a/conjure_oxide/tests/integration/basic/bool/02/bool-02.expected-minion.solutions.json +++ b/conjure_oxide/tests/integration/basic/bool/02/bool-02.expected-minion.solutions.json @@ -1,18 +1,18 @@ [ { - "x": 0, - "y": 0 + "UserName(x)": 0, + "UserName(y)": 0 }, { - "x": 0, - "y": 1 + "UserName(x)": 0, + "UserName(y)": 1 }, { - "x": 1, - "y": 0 + "UserName(x)": 1, + "UserName(y)": 0 }, { - "x": 1, - "y": 1 + "UserName(x)": 1, + "UserName(y)": 1 } ] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/bool/03/bool-03.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/bool/03/bool-03.expected-minion.solutions.json index 04c3691bb..41f27f106 100644 --- a/conjure_oxide/tests/integration/basic/bool/03/bool-03.expected-minion.solutions.json +++ b/conjure_oxide/tests/integration/basic/bool/03/bool-03.expected-minion.solutions.json @@ -1,10 +1,10 @@ [ { - "x": 0, - "y": 1 + "UserName(x)": 0, + "UserName(y)": 1 }, { - "x": 1, - "y": 0 + "UserName(x)": 1, + "UserName(y)": 0 } ] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/xyz/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/xyz/input.expected-minion.solutions.json index 24874137f..1cc649f7c 100644 --- a/conjure_oxide/tests/integration/xyz/input.expected-minion.solutions.json +++ b/conjure_oxide/tests/integration/xyz/input.expected-minion.solutions.json @@ -1,12 +1,12 @@ [ { - "a": 1, - "b": 1, - "c": 2 + "UserName(a)": 1, + "UserName(b)": 1, + "UserName(c)": 2 }, { - "a": 2, - "b": 1, - "c": 1 + "UserName(a)": 2, + "UserName(b)": 1, + "UserName(c)": 1 } ] \ No newline at end of file From 64baea45e92f36fb0be7ad7fb5da78387a9b4578 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Fri, 8 Mar 2024 20:56:43 +0000 Subject: [PATCH 09/10] solver-interface: Refactor return values to solve, add wall time, docs --- Cargo.lock | 5 +- conjure_oxide/Cargo.toml | 1 + .../solver_interface/adaptors/minion.rs | 50 ++++-- .../unstable/solver_interface/adaptors/mod.rs | 3 +- .../src/unstable/solver_interface/mod.rs | 146 +++++++++++++----- .../src/unstable/solver_interface/states.rs | 7 + conjure_oxide/src/utils/conjure.rs | 19 +-- 7 files changed, 164 insertions(+), 67 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 030deacb3..719a9f390 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -279,6 +279,7 @@ dependencies = [ "conjure_core", "conjure_rules", "itertools", + "libc", "linkme", "minion_rs", "serde", @@ -563,9 +564,9 @@ checksum = "830d08ce1d1d941e6b30645f1a0eb5643013d835ce3779a5fc208261dbe10f55" [[package]] name = "libc" -version = "0.2.150" +version = "0.2.153" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "89d92a4743f9a61002fae18374ed11e7973f530cb3a3255fb354818118b2203c" +checksum = "9c198f91728a82281a64e1f4f9eeb25d82cb32a5de251c6bd1b5154d63a8e7bd" [[package]] name = "libloading" diff --git a/conjure_oxide/Cargo.toml b/conjure_oxide/Cargo.toml index 69abdb69a..8def9c9cf 100644 --- a/conjure_oxide/Cargo.toml +++ b/conjure_oxide/Cargo.toml @@ -25,6 +25,7 @@ versions = "6.1.0" linkme = "0.3.22" walkdir = "2.4.0" itertools = "0.12.1" +libc = "0.2.153" [features] diff --git a/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs b/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs index 7b1e84512..1ff640a29 100644 --- a/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs +++ b/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs @@ -7,6 +7,9 @@ use crate::unstable::solver_interface::{states, SolverCallback}; use super::super::model_modifier::NotModifiable; use super::super::private; use super::super::stats::NoStats; +use super::super::SearchComplete::*; +use super::super::SearchIncomplete::*; +use super::super::SearchStatus::*; use super::super::SolveSuccess; use super::super::SolverAdaptor; use super::super::SolverError; @@ -20,14 +23,18 @@ use minion_rs::ast as minionast; /// A [SolverAdaptor] for interacting with Minion. /// /// This adaptor uses the `minion_rs` crate to talk to Minion over FFI. -pub struct Minion; +pub struct Minion { + __non_constructable: private::Internal, +} -static MINION_LOCKED: Mutex = Mutex::new(false); -static MINION_CONDVAR: Condvar = Condvar::new(); +static MINION_LOCK: Mutex<()> = Mutex::new(()); static USER_CALLBACK: OnceLock> = OnceLock::new(); +static ANY_SOLUTIONS: Mutex = Mutex::new(false); +static USER_TERIMINATED: Mutex = Mutex::new(false); +#[allow(clippy::unwrap_used)] fn minion_rs_callback(solutions: HashMap) -> bool { - #[allow(clippy::unwrap_used)] + *(ANY_SOLUTIONS.lock().unwrap()) = true; let callback = USER_CALLBACK .get_or_init(|| Mutex::new(Box::new(|x| true))) .lock() @@ -46,7 +53,12 @@ fn minion_rs_callback(solutions: HashMap Minion { + Minion { + __non_constructable: private::Internal, + } + } + #[allow(clippy::unwrap_used)] fn solve( &mut self, @@ -65,14 +83,9 @@ impl SolverAdaptor for Minion { // our minion callback is global state, so single threading the adaptor as a whole is // probably a good move... #[allow(clippy::unwrap_used)] - let mut locked = MINION_LOCKED.lock().unwrap(); + let mut minion_lock = MINION_LOCK.lock().unwrap(); #[allow(clippy::unwrap_used)] - while *locked { - locked = MINION_CONDVAR.wait(locked).unwrap(); - } - *locked = true; - let mut user_callback = USER_CALLBACK .get_or_init(|| Mutex::new(Box::new(|x| true))) .lock() @@ -92,11 +105,16 @@ impl SolverAdaptor for Minion { x => SolverError::Runtime(format!("unknown minion_rs error: {:#?}", x)), })?; - *locked = false; - std::mem::drop(locked); // unlock mutex - MINION_CONDVAR.notify_one(); // wake up waiting threads - - Ok(SolveSuccess { stats: None }) + let mut status = Complete(HasSolutions); + if *(USER_TERIMINATED.lock()).unwrap() { + status = Incomplete(UserTerminated); + } else if *(ANY_SOLUTIONS.lock()).unwrap() { + status = Complete(NoSolutions); + } + Ok(SolveSuccess { + stats: None, + status, + }) } fn solve_mut( diff --git a/conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs b/conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs index 346ffcfee..04eb63e72 100644 --- a/conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs +++ b/conjure_oxide/src/unstable/solver_interface/adaptors/mod.rs @@ -1,4 +1,5 @@ //! Solver adaptors. -pub mod minion; +mod minion; +#[doc(inline)] pub use minion::Minion; diff --git a/conjure_oxide/src/unstable/solver_interface/mod.rs b/conjure_oxide/src/unstable/solver_interface/mod.rs index e79ddca1f..d7f19b15b 100644 --- a/conjure_oxide/src/unstable/solver_interface/mod.rs +++ b/conjure_oxide/src/unstable/solver_interface/mod.rs @@ -21,11 +21,11 @@ //! //! ## A Successful Minion Model //! -//! ``` +//! ```rust //! # use conjure_oxide::generate_custom::get_example_model; //! use conjure_oxide::rule_engine::rewrite::rewrite_model; //! use conjure_oxide::rule_engine::resolve_rules::resolve_rule_sets; -//! use conjure_oxide::unstable::solver_interface::{Solver,adaptors}; +//! use conjure_oxide::unstable::solver_interface::{Solver,adaptors,SolverAdaptor}; //! use conjure_oxide::unstable::solver_interface::states::*; //! use std::sync::{Arc,Mutex}; //! @@ -36,7 +36,7 @@ //! //! //! // Solve using Minion. -//! let solver = Solver::using(adaptors::Minion); +//! let solver = Solver::new(adaptors::Minion::new()); //! let solver: Solver = solver.load_model(model).unwrap(); //! //! // In this example, we will count solutions. @@ -103,13 +103,50 @@ use itertools::Either; use std::collections::HashMap; use std::error::Error; use std::fmt::{Debug, Display}; +use std::time::Instant; use thiserror::Error; +/// The type for user-defined callbacks for use with [Solver]. +/// +/// Note that this enforces threadsafetyb pub type SolverCallback = Box) -> bool + Send>; pub type SolverMutCallback = Box, ::Modifier) -> bool + Send>; -/// A common interface for calling underlying solver APIs inside a [Solver]. +/// A common interface for calling underlying solver APIs inside a [`Solver`]. +/// +/// Implementations of this trait arn't directly callable and should be used through [`Solver`] . +/// +/// The below documentation lists the formal requirements that all implementations of +/// [`SolverAdaptor`] should follow - **see the top level module documentation and [`Solver`] for +/// usage details.** +/// +/// # Encapsulation +/// +/// The [`SolverAdaptor`] trait **must** only be implemented inside a submodule of this one, +/// and **should** only be called through [`Solver`]. +/// +/// The `private::Sealed` trait and `private::Internal` type enforce these requirements by only +/// allowing trait implementations and calling of methods of SolverAdaptor to occur inside this +/// module. +/// +/// # Thread Safety +/// +/// Multiple instances of [`Solver`] can be run in parallel across multiple threads. +/// +/// [`Solver`] provides no concurrency control or thread-safety; therefore, adaptors **must** +/// ensure that multiple instances of themselves can be ran in parallel. This applies to all +/// stages of solving including having two active `solve()` calls happening at a time, loading +/// a model while another is mid-solve, loading two models at once, etc. +/// +/// A [SolverAdaptor] **may** use whatever threading or process model it likes underneath the hood, +/// as long as it obeys the above. +/// +/// Method calls **should** block instead of erroring where possible. +/// +/// Underlying solvers that only have one instance per process (such as Minion) **should** block +/// (eg. using a [`Mutex<()>`](`std::sync::Mutex`)) to run calls to +/// [`Solver::solve()`] and [`Solver::solve_mut()`] sequentially. pub trait SolverAdaptor: private::Sealed { /// The native model type of the underlying solver. type Model: Clone; @@ -122,11 +159,26 @@ pub trait SolverAdaptor: private::Sealed { /// If incremental solving is not supported, this **should** be set to [NotModifiable](model_modifier::NotModifiable) . type Modifier: model_modifier::ModelModifier; + fn new() -> Self; + /// Runs the solver on the given model. /// - /// Implementations of this function *must** call the user provided callback whenever a solution + /// Implementations of this function **must** call the user provided callback whenever a solution /// is found. If the user callback returns `true`, search should continue, if the user callback /// returns `false`, search should terminate. + /// + /// # Returns + /// + /// If the solver terminates without crashing a [SolveSuccess] struct **must** returned. The + /// value of [SearchStatus] can be used to denote whether the underlying solver completed its + /// search or not. The latter case covers most non-crashing "failure" cases including user + /// termination, timeouts, etc. + /// + /// To help populate [SearchStatus], it may be helpful to implement counters that track if the + /// user callback has been called yet, and its return value. This information makes it is + /// possible to distinguish between the most common search statuses: + /// [SearchComplete::HasSolutions], [SearchComplete::NoSolutions], and + /// [SearchIncomplete::UserTerminated]. fn solve( &mut self, model: Self::Model, @@ -138,11 +190,9 @@ pub trait SolverAdaptor: private::Sealed { /// [`ModelModifier`]. /// /// Implementations of this function **must** return [`OpNotSupported`](`ModificationFailure::OpNotSupported`) - /// if modifying the model mid-search is not supported. These implementations may also find the - /// [`NotModifiable`] modifier useful. + /// if modifying the model mid-search is not supported. /// - /// As with [`solve`](SolverAdaptor::solve), this function **must** call the user provided callback - /// function whenever a solution is found. + /// Otherwise, this should work in the same way as [`solve`](SolverAdaptor::solve). fn solve_mut( &mut self, model: Self::Model, @@ -169,6 +219,7 @@ pub trait SolverAdaptor: private::Sealed { /// As such, there may be multiple [SolverAdaptor] implementations for a single underlying solver: /// eg. one adaptor may give solutions in a representation close to the solvers, while another may /// attempt to rewrite it back into Essence. +/// #[derive(Clone)] pub struct Solver { state: State, @@ -177,7 +228,7 @@ pub struct Solver { } impl Solver { - pub fn using(solver_adaptor: Adaptor) -> Solver { + pub fn new(solver_adaptor: Adaptor) -> Solver { let mut solver = Solver { state: Init, adaptor: solver_adaptor, @@ -204,58 +255,58 @@ impl Solver { pub fn solve( mut self, callback: SolverCallback, - ) -> Either, Solver> { + ) -> Result, SolverError> { + #[allow(clippy::unwrap_used)] + let start_time = Instant::now(); + #[allow(clippy::unwrap_used)] let result = self .adaptor .solve(self.model.clone().unwrap(), callback, private::Internal); + let duration = start_time.elapsed(); + match result { - Ok(x) => Either::Left(Solver { + Ok(x) => Ok(Solver { adaptor: self.adaptor, model: self.model, state: ExecutionSuccess { stats: x.stats, + status: x.status, _sealed: private::Internal, + wall_time_s: duration.as_secs_f64(), }, }), - Err(x) => Either::Right(Solver { - adaptor: self.adaptor, - model: self.model, - state: ExecutionFailure { - why: x, - _sealed: private::Internal, - }, - }), + Err(x) => Err(x), } } pub fn solve_mut( mut self, callback: SolverMutCallback, - ) -> Either, Solver> { + ) -> Result, SolverError> { + #[allow(clippy::unwrap_used)] + let start_time = Instant::now(); + #[allow(clippy::unwrap_used)] let result = self.adaptor .solve_mut(self.model.clone().unwrap(), callback, private::Internal); + let duration = start_time.elapsed(); + match result { - Ok(x) => Either::Left(Solver { + Ok(x) => Ok(Solver { adaptor: self.adaptor, model: self.model, state: ExecutionSuccess { stats: x.stats, + status: x.status, _sealed: private::Internal, + wall_time_s: duration.as_secs_f64(), }, }), - Err(x) => Either::Right(Solver { - adaptor: self.adaptor, - model: self.model, - state: ExecutionFailure { - why: x, - _sealed: private::Internal, - }, - }), + Err(x) => Err(x), } } } @@ -264,11 +315,9 @@ impl Solver { pub fn stats(self) -> Option> { self.state.stats } -} -impl Solver { - pub fn why(&self) -> SolverError { - self.state.why.clone() + pub fn wall_time_s(&self) -> f64 { + self.state.wall_time_s } } @@ -292,9 +341,6 @@ pub enum SolverError { #[error("model invalid: {0}")] ModelInvalid(String), - #[error("time out")] - TimeOut, - #[error("error during solver execution: not implemented: {0}")] RuntimeNotImplemented(String), @@ -305,4 +351,30 @@ pub enum SolverError { /// Returned from [SolverAdaptor] when solving is successful. pub struct SolveSuccess { stats: Option>, + status: SearchStatus, +} + +pub enum SearchStatus { + /// The search was complete (i.e. the solver found all possible solutions) + Complete(SearchComplete), + /// The search was incomplete (i.e. it was terminated before all solutions were found) + Incomplete(SearchIncomplete), +} + +#[non_exhaustive] +pub enum SearchIncomplete { + Timeout, + UserTerminated, + #[doc(hidden)] + /// This variant should not be matched - it exists to simulate non-exhaustiveness of this enum. + __NonExhaustive, +} + +#[non_exhaustive] +pub enum SearchComplete { + HasSolutions, + NoSolutions, + #[doc(hidden)] + /// This variant should not be matched - it exists to simulate non-exhaustiveness of this enum. + __NonExhaustive, } diff --git a/conjure_oxide/src/unstable/solver_interface/states.rs b/conjure_oxide/src/unstable/solver_interface/states.rs index a1eeab7d2..b0f4f9e97 100644 --- a/conjure_oxide/src/unstable/solver_interface/states.rs +++ b/conjure_oxide/src/unstable/solver_interface/states.rs @@ -6,6 +6,7 @@ use thiserror::Error; use super::private::Internal; use super::private::Sealed; use super::stats::*; +use super::SearchStatus; use super::Solver; use super::SolverError; @@ -29,6 +30,12 @@ pub struct ExecutionSuccess { /// Execution statistics. pub stats: Option>, + /// The status of the search + pub status: SearchStatus, + + // Wall time elapsed in seconds. + pub wall_time_s: f64, + /// Cannot construct this from outside this module. pub _sealed: Internal, } diff --git a/conjure_oxide/src/utils/conjure.rs b/conjure_oxide/src/utils/conjure.rs index 6ece30c56..58b12e718 100644 --- a/conjure_oxide/src/utils/conjure.rs +++ b/conjure_oxide/src/utils/conjure.rs @@ -9,7 +9,7 @@ use std::sync::{Arc, Mutex}; use thiserror::Error as ThisError; use crate::unstable::solver_interface::adaptors::Minion; -use crate::unstable::solver_interface::Solver; +use crate::unstable::solver_interface::{Solver, SolverAdaptor}; #[derive(Debug, ThisError)] pub enum EssenceParseError { @@ -58,7 +58,7 @@ pub fn parse_essence_file(path: &str, filename: &str) -> Result Result>, anyhow::Error> { - let solver = Solver::using(Minion); + let solver = Solver::new(Minion::new()); println!("Building Minion model..."); let solver = solver.load_model(model)?; @@ -67,19 +67,16 @@ pub fn get_minion_solutions(model: Model) -> Result> let all_solutions_ref = Arc::new(Mutex::>>::new(vec![])); let all_solutions_ref_2 = all_solutions_ref.clone(); - let solver_state = solver.solve(Box::new(move |sols| { + #[allow(clippy::unwrap_used)] + solver.solve(Box::new(move |sols| { let mut all_solutions = (*all_solutions_ref_2).lock().unwrap(); (*all_solutions).push(sols); true - })); + }))?; - match solver_state { - Left(x) => { - let all_solutions = (*all_solutions_ref).lock().unwrap(); - Ok(all_solutions.clone()) - } - Right(x) => Err(anyhow::Error::from(x.why())), - } + #[allow(clippy::unwrap_used)] + let sols = (*all_solutions_ref).lock().unwrap(); + Ok((*sols).clone()) } pub fn minion_solutions_to_json(solutions: &Vec>) -> JsonValue { From f5f4b4c46c888a24d057dfb7453141ca55352ef7 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Sat, 9 Mar 2024 16:25:07 +0000 Subject: [PATCH 10/10] port minion changes from #230 to new solver interface --- Cargo.lock | 2 +- conjure_oxide/Cargo.toml | 1 + .../solver_interface/adaptors/minion.rs | 80 +++++++++++-------- .../01/input.expected-minion.solutions.json | 6 +- .../02/input.expected-minion.solutions.json | 48 +++++------ .../03/input.expected-minion.solutions.json | 42 +++++----- .../05/input.expected-minion.solutions.json | 54 ++++++------- 7 files changed, 123 insertions(+), 110 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index e71e06588..aa282d5ca 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -281,9 +281,9 @@ dependencies = [ "conjure_core", "conjure_rules", "itertools", - "libc", "linkme", "minion_rs", + "regex", "serde", "serde_json", "serde_with", diff --git a/conjure_oxide/Cargo.toml b/conjure_oxide/Cargo.toml index 2e09d7c96..f7560e34a 100644 --- a/conjure_oxide/Cargo.toml +++ b/conjure_oxide/Cargo.toml @@ -25,6 +25,7 @@ versions = "6.1.0" linkme = "0.3.22" walkdir = "2.5.0" itertools = "0.12.1" +regex = "1.10.3" [features] diff --git a/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs b/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs index 1ff640a29..859fc0e74 100644 --- a/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs +++ b/conjure_oxide/src/unstable/solver_interface/adaptors/minion.rs @@ -16,6 +16,7 @@ use super::super::SolverError; use super::super::SolverError::*; use minion_rs::run_minion; +use regex::Regex; use crate::ast as conjureast; use minion_rs::ast as minionast; @@ -48,8 +49,13 @@ fn minion_rs_callback(solutions: HashMap todo!(), }; - //FIXME (niklasdewally): what about machine names? - let conjure_name = conjureast::Name::UserName(minion_name); + let machine_name_re = Regex::new(r"__conjure_machine_name_([0-9]+)").unwrap(); + let conjure_name = if let Some(caps) = machine_name_re.captures(&minion_name) { + conjureast::Name::MachineName(caps[1].parse::().unwrap()) + } else { + conjureast::Name::UserName(minion_name) + }; + conjure_solutions.insert(conjure_name, conjure_const); } @@ -237,42 +243,48 @@ fn parse_expr( expr: conjureast::Expression, minion_model: &mut minionast::Model, ) -> Result<(), SolverError> { + minion_model.constraints.push(read_expr(expr)?); + Ok(()) +} + +fn read_expr(expr: conjureast::Expression) -> Result { match expr { - conjureast::Expression::SumLeq(_metadata, lhs, rhs) => { - minion_model.constraints.push(minionast::Constraint::SumLeq( - read_vars(lhs)?, - read_var(*rhs)?, - )); - Ok(()) - } - conjureast::Expression::SumGeq(_metadata, lhs, rhs) => { - minion_model.constraints.push(minionast::Constraint::SumGeq( - read_vars(lhs)?, - read_var(*rhs)?, - )); - Ok(()) - } - conjureast::Expression::Ineq(_metadata, a, b, c) => { - minion_model.constraints.push(minionast::Constraint::Ineq( - read_var(*a)?, - read_var(*b)?, - minionast::Constant::Integer(read_const(*c)?), - )); - Ok(()) - } - conjureast::Expression::Neq(_metadata, a, b) => { - minion_model - .constraints - .push(minionast::Constraint::WatchNeq( - read_var(*a)?, - read_var(*b)?, - )); - Ok(()) + conjureast::Expression::SumLeq(_metadata, lhs, rhs) => Ok(minionast::Constraint::SumLeq( + read_vars(lhs)?, + read_var(*rhs)?, + )), + conjureast::Expression::SumGeq(_metadata, lhs, rhs) => Ok(minionast::Constraint::SumGeq( + read_vars(lhs)?, + read_var(*rhs)?, + )), + conjureast::Expression::Ineq(_metadata, a, b, c) => Ok(minionast::Constraint::Ineq( + read_var(*a)?, + read_var(*b)?, + minionast::Constant::Integer(read_const(*c)?), + )), + conjureast::Expression::Neq(_metadata, a, b) => Ok(minionast::Constraint::AllDiff(vec![ + read_var(*a)?, + read_var(*b)?, + ])), + // conjureast::Expression::DivEq(_metadata, a, b, c) => { + // minion_model.constraints.push(minionast::Constraint::Div( + // (read_var(*a)?, read_var(*b)?), + // read_var(*c)?, + // )); + // Ok(()) + // } + conjureast::Expression::AllDiff(_metadata, vars) => { + Ok(minionast::Constraint::AllDiff(read_vars(vars)?)) } + conjureast::Expression::Or(_metadata, exprs) => Ok(minionast::Constraint::WatchedOr( + exprs + .iter() + .map(|x| read_expr(x.to_owned())) + .collect::, SolverError>>()?, + )), x => Err(ModelFeatureNotSupported(format!("{:?}", x))), } } - fn read_vars(exprs: Vec) -> Result, SolverError> { let mut minion_vars: Vec = vec![]; for expr in exprs { @@ -319,6 +331,6 @@ fn read_const(e: conjureast::Expression) -> Result { fn _name_to_string(name: conjureast::Name) -> String { match name { conjureast::Name::UserName(x) => x, - conjureast::Name::MachineName(x) => x.to_string(), + conjureast::Name::MachineName(x) => format!("__conjure_machine_name_{}", x), } } diff --git a/conjure_oxide/tests/integration/basic/min/01/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/min/01/input.expected-minion.solutions.json index 16e182aab..ed1979f9f 100644 --- a/conjure_oxide/tests/integration/basic/min/01/input.expected-minion.solutions.json +++ b/conjure_oxide/tests/integration/basic/min/01/input.expected-minion.solutions.json @@ -1,7 +1,7 @@ [ { - "0": 3, - "a": 3, - "b": 3 + "MachineName(0)": 3, + "UserName(a)": 3, + "UserName(b)": 3 } ] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/min/02/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/min/02/input.expected-minion.solutions.json index fb8e40563..82b2c192c 100644 --- a/conjure_oxide/tests/integration/basic/min/02/input.expected-minion.solutions.json +++ b/conjure_oxide/tests/integration/basic/min/02/input.expected-minion.solutions.json @@ -1,42 +1,42 @@ [ { - "0": 1, - "a": 1, - "b": 1 + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 1 }, { - "0": 1, - "a": 1, - "b": 2 + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 2 }, { - "0": 1, - "a": 1, - "b": 3 + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 3 }, { - "0": 1, - "a": 2, - "b": 1 + "MachineName(0)": 1, + "UserName(a)": 2, + "UserName(b)": 1 }, { - "0": 1, - "a": 3, - "b": 1 + "MachineName(0)": 1, + "UserName(a)": 3, + "UserName(b)": 1 }, { - "0": 2, - "a": 2, - "b": 2 + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 2 }, { - "0": 2, - "a": 2, - "b": 3 + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 3 }, { - "0": 2, - "a": 3, - "b": 2 + "MachineName(0)": 2, + "UserName(a)": 3, + "UserName(b)": 2 } ] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/min/03/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/min/03/input.expected-minion.solutions.json index 9f4798a80..13d32026b 100644 --- a/conjure_oxide/tests/integration/basic/min/03/input.expected-minion.solutions.json +++ b/conjure_oxide/tests/integration/basic/min/03/input.expected-minion.solutions.json @@ -1,37 +1,37 @@ [ { - "0": 1, - "a": 1, - "b": 2 + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 2 }, { - "0": 1, - "a": 1, - "b": 3 + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 3 }, { - "0": 1, - "a": 1, - "b": 4 + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 4 }, { - "0": 2, - "a": 2, - "b": 2 + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 2 }, { - "0": 2, - "a": 2, - "b": 3 + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 3 }, { - "0": 2, - "a": 2, - "b": 4 + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 4 }, { - "0": 2, - "a": 3, - "b": 2 + "MachineName(0)": 2, + "UserName(a)": 3, + "UserName(b)": 2 } ] \ No newline at end of file diff --git a/conjure_oxide/tests/integration/basic/min/05/input.expected-minion.solutions.json b/conjure_oxide/tests/integration/basic/min/05/input.expected-minion.solutions.json index c326a64db..b3ae27c7a 100644 --- a/conjure_oxide/tests/integration/basic/min/05/input.expected-minion.solutions.json +++ b/conjure_oxide/tests/integration/basic/min/05/input.expected-minion.solutions.json @@ -1,47 +1,47 @@ [ { - "0": 1, - "a": 1, - "b": 2 + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 2 }, { - "0": 1, - "a": 1, - "b": 3 + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 3 }, { - "0": 1, - "a": 1, - "b": 4 + "MachineName(0)": 1, + "UserName(a)": 1, + "UserName(b)": 4 }, { - "0": 2, - "a": 2, - "b": 2 + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 2 }, { - "0": 2, - "a": 2, - "b": 3 + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 3 }, { - "0": 2, - "a": 2, - "b": 4 + "MachineName(0)": 2, + "UserName(a)": 2, + "UserName(b)": 4 }, { - "0": 2, - "a": 3, - "b": 2 + "MachineName(0)": 2, + "UserName(a)": 3, + "UserName(b)": 2 }, { - "0": 2, - "a": 4, - "b": 2 + "MachineName(0)": 2, + "UserName(a)": 4, + "UserName(b)": 2 }, { - "0": 2, - "a": 5, - "b": 2 + "MachineName(0)": 2, + "UserName(a)": 5, + "UserName(b)": 2 } ] \ No newline at end of file