From fc85af349b05e996ca98be5b955f1b23228d2d80 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Sat, 3 Feb 2024 22:51:06 +0000 Subject: [PATCH 1/7] add feature flag for unstable-solver-interface --- conjure_oxide/Cargo.toml | 4 ++++ conjure_oxide/src/lib.rs | 6 ++++++ conjure_oxide/src/unstable/solver_interface/mod.rs | 0 3 files changed, 10 insertions(+) create mode 100644 conjure_oxide/src/unstable/solver_interface/mod.rs diff --git a/conjure_oxide/Cargo.toml b/conjure_oxide/Cargo.toml index 2bb063da1f..31a2ce75bf 100644 --- a/conjure_oxide/Cargo.toml +++ b/conjure_oxide/Cargo.toml @@ -24,5 +24,9 @@ strum = "0.26.1" versions = "6.1.0" linkme = "0.3.22" +[features] + +unstable-solver-interface = [] + [lints] workspace = true diff --git a/conjure_oxide/src/lib.rs b/conjure_oxide/src/lib.rs index 35aecb7bd6..fe40784ece 100644 --- a/conjure_oxide/src/lib.rs +++ b/conjure_oxide/src/lib.rs @@ -11,3 +11,9 @@ pub use conjure_core::ast::Model; // rexport core::ast::Model as conjure_oxide:: pub use conjure_core::solvers::Solver; pub use error::Error; + + +#[cfg(feature = "unstable-solver-interface")] +mod unstable { + mod solver_interface; +} diff --git a/conjure_oxide/src/unstable/solver_interface/mod.rs b/conjure_oxide/src/unstable/solver_interface/mod.rs new file mode 100644 index 0000000000..e69de29bb2 From 1976d924719ae7692b087d21cbd75524bbadcb37 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Sat, 3 Feb 2024 23:38:28 +0000 Subject: [PATCH 2/7] types for new solver interface --- .../src/unstable/solver_interface/mod.rs | 67 +++++++++++++++++++ 1 file changed, 67 insertions(+) diff --git a/conjure_oxide/src/unstable/solver_interface/mod.rs b/conjure_oxide/src/unstable/solver_interface/mod.rs index e69de29bb2..1320b6d85c 100644 --- a/conjure_oxide/src/unstable/solver_interface/mod.rs +++ b/conjure_oxide/src/unstable/solver_interface/mod.rs @@ -0,0 +1,67 @@ +use std::fmt::Debug; + +use conjure_core::ast::Model; + +struct Init; +struct HasModel; +struct HasRun; +struct ExecutionSuccess; +struct ExecutionFailure; + +// TODO: seal trait. +trait SolverState {} +impl SolverState for Init {} +impl SolverState for HasModel {} +impl SolverState for ExecutionSuccess {} +impl SolverState for ExecutionFailure {} + +type SolverError = String; + +// TODO: seal trait? +trait SolverAdaptor { + type Model: Clone; + type Solution; + type ExecutionError; + type TranslationError: Debug; + + // TODO: this should be able to go to multiple states. + fn run_solver(&mut self, model: Self::Model) -> Result; + fn load_model(&mut self, model: Model) -> Result; + fn init_solver(&mut self) {} +} + + +struct Solver { + state: std::marker::PhantomData, + adaptor: A, + model: Option, +} + +impl Solver { + pub fn load_model(mut self,model: Model) -> Result,SolverError> { + let solver_model = &mut self.adaptor.load_model(model).unwrap(); + Ok(Solver { + state: std::marker::PhantomData::, + adaptor: self.adaptor, + model: Some(solver_model.clone()), + }) + } +} + +impl Solver { + + pub fn solve(mut self, callback: ()) -> Result { + // TODO: how do we actually handle callbacks? + self.adaptor.run_solver(self.model.unwrap()) + } +} + +impl Solver { + pub fn new(solver_adaptor: T) -> Solver { + Solver { + state: std::marker::PhantomData::, + adaptor: solver_adaptor, + model: todo!(), + } + } +} From 5b41f7202bc8465b5ba5c3f752396228c37b6fca Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Sat, 3 Feb 2024 23:51:43 +0000 Subject: [PATCH 3/7] add callbacks to solver interface --- .../src/unstable/solver_interface/mod.rs | 22 +++++++++++++------ 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/conjure_oxide/src/unstable/solver_interface/mod.rs b/conjure_oxide/src/unstable/solver_interface/mod.rs index 1320b6d85c..dc5198a60c 100644 --- a/conjure_oxide/src/unstable/solver_interface/mod.rs +++ b/conjure_oxide/src/unstable/solver_interface/mod.rs @@ -1,3 +1,4 @@ +use std::collections::HashMap; use std::fmt::Debug; use conjure_core::ast::Model; @@ -17,6 +18,9 @@ impl SolverState for ExecutionFailure {} type SolverError = String; +// TODO: this will use constant when it exists +type Callback = fn(bindings: HashMap) -> bool; + // TODO: seal trait? trait SolverAdaptor { type Model: Clone; @@ -25,7 +29,8 @@ trait SolverAdaptor { type TranslationError: Debug; // TODO: this should be able to go to multiple states. - fn run_solver(&mut self, model: Self::Model) -> Result; + // Adaptor implementers must call the user provided callback whenever a solution is found. + fn run_solver(&mut self, model: Self::Model, callback: Callback) -> Result; fn load_model(&mut self, model: Model) -> Result; fn init_solver(&mut self) {} } @@ -50,18 +55,21 @@ impl Solver { impl Solver { - pub fn solve(mut self, callback: ()) -> Result { - // TODO: how do we actually handle callbacks? - self.adaptor.run_solver(self.model.unwrap()) + pub fn solve(mut self, callback: Callback) -> Result { + #[allow(clippy::unwrap_used)] + self.adaptor.run_solver(self.model.unwrap(),callback) } } impl Solver { pub fn new(solver_adaptor: T) -> Solver { - Solver { + let mut solver = Solver { state: std::marker::PhantomData::, adaptor: solver_adaptor, - model: todo!(), - } + model: None, + }; + + solver.adaptor.init_solver(); + solver } } From ac5572b250db91f58619566d5f898091d545d56e Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Sun, 4 Feb 2024 15:15:55 +0000 Subject: [PATCH 4/7] solver-interface: basic type structure for mutating a model in the middle of solving. --- conjure_oxide/src/lib.rs | 1 - .../src/unstable/solver_interface/mod.rs | 124 +++++++++++++++--- 2 files changed, 105 insertions(+), 20 deletions(-) diff --git a/conjure_oxide/src/lib.rs b/conjure_oxide/src/lib.rs index fe40784ece..b75719a7fd 100644 --- a/conjure_oxide/src/lib.rs +++ b/conjure_oxide/src/lib.rs @@ -12,7 +12,6 @@ pub use conjure_core::solvers::Solver; pub use error::Error; - #[cfg(feature = "unstable-solver-interface")] mod unstable { mod solver_interface; diff --git a/conjure_oxide/src/unstable/solver_interface/mod.rs b/conjure_oxide/src/unstable/solver_interface/mod.rs index dc5198a60c..2417ebdbf1 100644 --- a/conjure_oxide/src/unstable/solver_interface/mod.rs +++ b/conjure_oxide/src/unstable/solver_interface/mod.rs @@ -1,13 +1,24 @@ +#![allow(dead_code)] +#![allow(unused)] + +use anyhow::anyhow; use std::collections::HashMap; -use std::fmt::Debug; +use std::error::Error; +use std::fmt::{Debug, Display}; -use conjure_core::ast::Model; +use conjure_core::ast::{Domain, Expression, Model, Name}; struct Init; struct HasModel; struct HasRun; struct ExecutionSuccess; -struct ExecutionFailure; + +enum ExecutionFailure { + NotImplemented, + Timeout, + // What type here?? + Error(String), +} // TODO: seal trait. trait SolverState {} @@ -16,35 +27,103 @@ impl SolverState for HasModel {} impl SolverState for ExecutionSuccess {} impl SolverState for ExecutionFailure {} -type SolverError = String; - // TODO: this will use constant when it exists -type Callback = fn(bindings: HashMap) -> bool; +type Callback = fn(bindings: HashMap) -> bool; + +enum ModificationFailure { + OperationNotSupported, + OperationNotImplementedYet, + ArgsNotSupported(String), + Error(E), +} + +/// A `ModelModifier` allows the modification of 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: [`SolverAdaptor::solve_mut`]. +trait ModelModifier { + type Error: Error; + fn add_constraint(constraint: Expression) -> Result<(), ModificationFailure> { + Err(ModificationFailure::OperationNotSupported) + } + + fn add_variable(name: Name, domain: Domain) -> Result<(), ModificationFailure> { + Err(ModificationFailure::OperationNotSupported) + } +} + +/// A [`ModelModifier`] for a solver that does not support incremental solving. Returns +/// [`OperationNotSupported`](`ModificationFailure::OperationNotSupported`) for all operations. +struct NotModifiable; + +#[derive(thiserror::Error, Debug)] +enum NotModifiableError {} + +impl ModelModifier for NotModifiable { + type Error = NotModifiableError; +} // TODO: seal trait? trait SolverAdaptor { type Model: Clone; - type Solution; - type ExecutionError; - type TranslationError: Debug; + type Solution; + type ExecutionError: Error; + type TranslationError<'a>: Error + Display + Send + Sync + where + Self: 'a; + + /// The [`ModelModifier`] to use during incremental search. + /// + /// If incremental solving is not supported, set this to [`NotModifiable`] . + type Modifier: ModelModifier; // TODO: this should be able to go to multiple states. // Adaptor implementers must call the user provided callback whenever a solution is found. - fn run_solver(&mut self, model: Self::Model, callback: Callback) -> Result; - fn load_model(&mut self, model: Model) -> Result; + + /// Run the solver on the given model. + /// + /// 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( + &mut self, + model: Self::Model, + callback: Callback, + ) -> Result; + + /// Run the solver on the given model, allowing modification of the model through a + /// [`ModelModifier`]. + /// + /// Implementations of this function MUST return [`OperationNotSupported`](`ModificationFailure::OperationNotSupported`) + /// 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 + /// function whenever a solution is found. + fn solve_mut( + &mut self, + model: Self::Model, + callback: fn(HashMap, Self::Modifier) -> bool, + ) -> Result; + fn load_model(&mut self, model: Model) -> Result>; fn init_solver(&mut self) {} } - -struct Solver { +struct Solver { state: std::marker::PhantomData, adaptor: A, model: Option, } -impl Solver { - pub fn load_model(mut self,model: Model) -> Result,SolverError> { - let solver_model = &mut self.adaptor.load_model(model).unwrap(); +impl Solver { + // TODO: decent error handling + pub fn load_model(mut self, model: Model) -> Result, ()> { + let solver_model = &mut self.adaptor.load_model(model).map_err(|_| ())?; Ok(Solver { state: std::marker::PhantomData::, adaptor: self.adaptor, @@ -53,11 +132,18 @@ impl Solver { } } -impl Solver { +impl Solver { + pub fn solve(mut self, callback: Callback) -> Result { + #[allow(clippy::unwrap_used)] + self.adaptor.solve(self.model.unwrap(), callback) + } - pub fn solve(mut self, callback: Callback) -> Result { + pub fn solve_mut( + mut self, + callback: fn(HashMap, A::Modifier) -> bool, + ) -> Result { #[allow(clippy::unwrap_used)] - self.adaptor.run_solver(self.model.unwrap(),callback) + self.adaptor.solve_mut(self.model.unwrap(), callback) } } From 186d92738e370bcab93cf47fae460008d049bc87 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Sun, 4 Feb 2024 16:03:38 +0000 Subject: [PATCH 5/7] solver-interface: try to seal things off / make them private --- .../src/unstable/solver_interface/mod.rs | 54 +++++++++++++------ 1 file changed, 38 insertions(+), 16 deletions(-) diff --git a/conjure_oxide/src/unstable/solver_interface/mod.rs b/conjure_oxide/src/unstable/solver_interface/mod.rs index 2417ebdbf1..74e4a74415 100644 --- a/conjure_oxide/src/unstable/solver_interface/mod.rs +++ b/conjure_oxide/src/unstable/solver_interface/mod.rs @@ -11,26 +11,36 @@ use conjure_core::ast::{Domain, Expression, Model, Name}; struct Init; struct HasModel; struct HasRun; -struct ExecutionSuccess; -enum ExecutionFailure { +#[doc(hidden)] +mod private { + /// Make some methods uncallable from outside of this module. + pub struct Internal; + + // https://predr.ag/blog/definitive-guide-to-sealed-traits-in-rust/#the-trick-for-sealing-traits + /// Make some traits unimplementable from outside of this module. + pub trait Sealed {} +} + +pub struct ExecutionSuccess; +pub enum ExecutionFailure { NotImplemented, Timeout, // What type here?? Error(String), } -// TODO: seal trait. trait SolverState {} + impl SolverState for Init {} impl SolverState for HasModel {} impl SolverState for ExecutionSuccess {} impl SolverState for ExecutionFailure {} // TODO: this will use constant when it exists -type Callback = fn(bindings: HashMap) -> bool; +pub type Callback = fn(bindings: HashMap) -> bool; -enum ModificationFailure { +pub enum ModificationFailure { OperationNotSupported, OperationNotImplementedYet, ArgsNotSupported(String), @@ -46,7 +56,7 @@ enum ModificationFailure { /// through the rewriter, or only low-level solver constraints are supported. /// /// See also: [`SolverAdaptor::solve_mut`]. -trait ModelModifier { +pub trait ModelModifier: private::Sealed { type Error: Error; fn add_constraint(constraint: Expression) -> Result<(), ModificationFailure> { Err(ModificationFailure::OperationNotSupported) @@ -59,17 +69,18 @@ trait ModelModifier { /// A [`ModelModifier`] for a solver that does not support incremental solving. Returns /// [`OperationNotSupported`](`ModificationFailure::OperationNotSupported`) for all operations. -struct NotModifiable; +pub struct NotModifiable; +#[doc(hidden)] #[derive(thiserror::Error, Debug)] -enum NotModifiableError {} +pub enum NotModifiableError {} +impl private::Sealed for NotModifiable {} impl ModelModifier for NotModifiable { type Error = NotModifiableError; } -// TODO: seal trait? -trait SolverAdaptor { +pub trait SolverAdaptor: private::Sealed { type Model: Clone; type Solution; type ExecutionError: Error; @@ -94,6 +105,7 @@ trait SolverAdaptor { &mut self, model: Self::Model, callback: Callback, + _: private::Internal, ) -> Result; /// Run the solver on the given model, allowing modification of the model through a @@ -109,9 +121,14 @@ trait SolverAdaptor { &mut self, model: Self::Model, callback: fn(HashMap, Self::Modifier) -> bool, + _: private::Internal, ) -> Result; - fn load_model(&mut self, model: Model) -> Result>; - fn init_solver(&mut self) {} + fn load_model( + &mut self, + model: Model, + _: private::Internal, + ) -> Result>; + fn init_solver(&mut self, _: private::Internal) {} } struct Solver { @@ -123,7 +140,10 @@ struct 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).map_err(|_| ())?; + let solver_model = &mut self + .adaptor + .load_model(model, private::Internal) + .map_err(|_| ())?; Ok(Solver { state: std::marker::PhantomData::, adaptor: self.adaptor, @@ -135,7 +155,8 @@ impl Solver { impl Solver { pub fn solve(mut self, callback: Callback) -> Result { #[allow(clippy::unwrap_used)] - self.adaptor.solve(self.model.unwrap(), callback) + self.adaptor + .solve(self.model.unwrap(), callback, private::Internal) } pub fn solve_mut( @@ -143,7 +164,8 @@ impl Solver { callback: fn(HashMap, A::Modifier) -> bool, ) -> Result { #[allow(clippy::unwrap_used)] - self.adaptor.solve_mut(self.model.unwrap(), callback) + self.adaptor + .solve_mut(self.model.unwrap(), callback, private::Internal) } } @@ -155,7 +177,7 @@ impl Solver { model: None, }; - solver.adaptor.init_solver(); + solver.adaptor.init_solver(private::Internal); solver } } From a78899d4247dea0f09082f3be3eb814d96ec896f Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Tue, 6 Feb 2024 15:12:50 +0000 Subject: [PATCH 6/7] CI: generate docs for all features --- .gitignore | 4 +++- tools/gen_docs.sh | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/.gitignore b/.gitignore index bbc4295af7..be5454681e 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,6 @@ *.log +*.json +*.serialised.json coverage conjure_oxide/tests/**/*.generated.* @@ -163,4 +165,4 @@ fabric.properties .idea/misc.xml .idea/inspectionProfiles .idea/.gitignore -.idea/conjure-oxide.iml \ No newline at end of file +.idea/conjure-oxide.iml diff --git a/tools/gen_docs.sh b/tools/gen_docs.sh index 5dae7f727e..b64a0ad013 100755 --- a/tools/gen_docs.sh +++ b/tools/gen_docs.sh @@ -26,4 +26,4 @@ TARGET_DIR=$(cargo metadata 2> /dev/null | jq -r .target_directory 2>/dev/null) cd "$PROJECT_ROOT" rm -rf "$TARGET_DIR/doc" -RUSTDOCFLAGS="-Zunstable-options --markdown-no-toc --index-page ${PROJECT_ROOT}/doc/index.md" cargo +nightly doc --no-deps -p conjure_oxide -p conjure_core -p minion_rs -p chuffed_rs -p conjure_rules +RUSTDOCFLAGS="-Zunstable-options --markdown-no-toc --index-page ${PROJECT_ROOT}/doc/index.md" cargo +nightly doc --no-deps --all-features -p conjure_oxide -p conjure_core -p minion_rs -p chuffed_rs -p conjure_rules $@ From 4e32afd12702ca6c359da75070761dec081ff1d8 Mon Sep 17 00:00:00 2001 From: Niklas Dewally Date: Tue, 6 Feb 2024 17:28:05 +0000 Subject: [PATCH 7/7] solver-interface: some docs --- conjure_oxide/Cargo.toml | 3 +- conjure_oxide/src/lib.rs | 8 +- conjure_oxide/src/unstable/mod.rs | 6 + .../src/unstable/solver_interface/mod.rs | 238 +++++++++++------- 4 files changed, 161 insertions(+), 94 deletions(-) create mode 100644 conjure_oxide/src/unstable/mod.rs diff --git a/conjure_oxide/Cargo.toml b/conjure_oxide/Cargo.toml index 15f160c43f..ff7eb89fec 100644 --- a/conjure_oxide/Cargo.toml +++ b/conjure_oxide/Cargo.toml @@ -26,7 +26,8 @@ linkme = "0.3.22" [features] -unstable-solver-interface = [] +unstable = [] +unstable-solver-interface = ["unstable"] [lints] workspace = true diff --git a/conjure_oxide/src/lib.rs b/conjure_oxide/src/lib.rs index 28290a1eec..7d799be154 100644 --- a/conjure_oxide/src/lib.rs +++ b/conjure_oxide/src/lib.rs @@ -1,3 +1,6 @@ + +// #![feature(doc_auto_cfg)] + pub mod error; pub mod find_conjure; pub mod parse; @@ -12,7 +15,4 @@ pub use conjure_core::solvers::Solver; pub use error::Error; -#[cfg(feature = "unstable-solver-interface")] -mod unstable { - mod solver_interface; -} +pub mod unstable; diff --git a/conjure_oxide/src/unstable/mod.rs b/conjure_oxide/src/unstable/mod.rs new file mode 100644 index 0000000000..7f45f32813 --- /dev/null +++ b/conjure_oxide/src/unstable/mod.rs @@ -0,0 +1,6 @@ +//! 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 74e4a74415..e846e38809 100644 --- a/conjure_oxide/src/unstable/solver_interface/mod.rs +++ b/conjure_oxide/src/unstable/solver_interface/mod.rs @@ -1,100 +1,60 @@ +#![cfg(feature = "unstable-solver-interface")] + +//! A new interface for interacting with solvers. +//! +//! # Example +//! +//! TODO + +// # Implementing Solver interfaces +// +// Solver interfaces can only be implemented inside this module, due to the SolverAdaptor crate +// being sealed. +// +// To add support for a solver, implement the `SolverAdaptor` trait in a submodule. +// +// If incremental solving support is required, also implement `ModelModifier`. If this is not +// required, all `ModelModifier` instances required by the SolverAdaptor trait can be replaced with +// NotModifiable. +// +// For more details, see the docstrings for SolverAdaptor, ModelModifier, and NotModifiable. + #![allow(dead_code)] #![allow(unused)] - -use anyhow::anyhow; -use std::collections::HashMap; -use std::error::Error; -use std::fmt::{Debug, Display}; - -use conjure_core::ast::{Domain, Expression, Model, Name}; - -struct Init; -struct HasModel; -struct HasRun; +#![warn(clippy::exhaustive_enums)] #[doc(hidden)] mod private { - /// Make some methods uncallable from outside of this module. + // 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 some traits unimplementable from outside of this module. + // Make traits unimplementable from outside of this module. + #[doc(hidden)] pub trait Sealed {} } -pub struct ExecutionSuccess; -pub enum ExecutionFailure { - NotImplemented, - Timeout, - // What type here?? - Error(String), -} - -trait SolverState {} - -impl SolverState for Init {} -impl SolverState for HasModel {} -impl SolverState for ExecutionSuccess {} -impl SolverState for ExecutionFailure {} - -// TODO: this will use constant when it exists -pub type Callback = fn(bindings: HashMap) -> bool; - -pub enum ModificationFailure { - OperationNotSupported, - OperationNotImplementedYet, - ArgsNotSupported(String), - Error(E), -} - -/// A `ModelModifier` allows the modification of 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: [`SolverAdaptor::solve_mut`]. -pub trait ModelModifier: private::Sealed { - type Error: Error; - fn add_constraint(constraint: Expression) -> Result<(), ModificationFailure> { - Err(ModificationFailure::OperationNotSupported) - } - - fn add_variable(name: Name, domain: Domain) -> Result<(), ModificationFailure> { - Err(ModificationFailure::OperationNotSupported) - } -} - -/// A [`ModelModifier`] for a solver that does not support incremental solving. Returns -/// [`OperationNotSupported`](`ModificationFailure::OperationNotSupported`) for all operations. -pub struct NotModifiable; - -#[doc(hidden)] -#[derive(thiserror::Error, Debug)] -pub enum NotModifiableError {} - -impl private::Sealed for NotModifiable {} -impl ModelModifier for NotModifiable { - type Error = NotModifiableError; -} +use self::incremental::*; +use self::solver_states::*; +use anyhow::anyhow; +use conjure_core::ast::{Domain, Expression, Model, Name}; +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`]. pub trait SolverAdaptor: private::Sealed { + /// The native model type of the underlying solver. type Model: Clone; - type Solution; - type ExecutionError: Error; - type TranslationError<'a>: Error + Display + Send + Sync - where - Self: 'a; - /// The [`ModelModifier`] to use during incremental search. - /// - /// If incremental solving is not supported, set this to [`NotModifiable`] . - type Modifier: ModelModifier; + /// The native solution type of the underlying solver. + type Solution: Clone; - // TODO: this should be able to go to multiple states. - // Adaptor implementers must call the user provided callback whenever a solution is found. + /// The [`ModelModifier`](incremental::ModelModifier) used during incremental search. + /// + /// If incremental solving is not supported, this SHOULD be set to [NotModifiable](`incremental::NotModifiable`) . + type Modifier: incremental::ModelModifier; /// Run the solver on the given model. /// @@ -104,14 +64,14 @@ pub trait SolverAdaptor: private::Sealed { fn solve( &mut self, model: Self::Model, - callback: Callback, + callback: fn(HashMap) -> bool, _: private::Internal, ) -> Result; /// Run the solver on the given model, allowing modification of the model through a /// [`ModelModifier`]. /// - /// Implementations of this function MUST return [`OperationNotSupported`](`ModificationFailure::OperationNotSupported`) + /// 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. /// @@ -127,11 +87,12 @@ pub trait SolverAdaptor: private::Sealed { &mut self, model: Model, _: private::Internal, - ) -> Result>; + ) -> Result; fn init_solver(&mut self, _: private::Internal) {} } -struct Solver { +/// A Solver executes of a Conjure-Oxide model usign a specified solver. +pub struct Solver { state: std::marker::PhantomData, adaptor: A, model: Option, @@ -139,21 +100,24 @@ struct Solver { impl Solver { // TODO: decent error handling - pub fn load_model(mut self, model: Model) -> Result, ()> { + pub fn load_model(mut self, model: Model) -> Result, ()> { let solver_model = &mut self .adaptor .load_model(model, private::Internal) .map_err(|_| ())?; Ok(Solver { - state: std::marker::PhantomData::, + state: std::marker::PhantomData::, adaptor: self.adaptor, model: Some(solver_model.clone()), }) } } -impl Solver { - pub fn solve(mut self, callback: Callback) -> Result { +impl Solver { + pub fn solve( + mut self, + callback: fn(HashMap) -> bool, + ) -> Result { #[allow(clippy::unwrap_used)] self.adaptor .solve(self.model.unwrap(), callback, private::Internal) @@ -181,3 +145,99 @@ impl Solver { solver } } + +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), + } +} + +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), + } +}