conjure_oxide

Module solver

Source
Expand description

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<A,ModelLoaded>::solve_mut function.

§Examples

§A Successful Minion Model

use std::sync::{Arc,Mutex};
use conjure_core::parse::get_example_model;
use conjure_core::rule_engine::resolve_rule_sets;
use conjure_core::rule_engine::rewrite_model;
use conjure_core::solver::{adaptors, Solver, SolverAdaptor};
use conjure_core::solver::states::ModelLoaded;
use conjure_core::solver::SolverFamily;

// Define and rewrite a model for minion.
let model = get_example_model("bool-03").unwrap();
let rule_sets = resolve_rule_sets(SolverFamily::Minion, &vec!["Constant".to_string()]).unwrap();
let model = rewrite_model(&model,&rule_sets).unwrap();


// Solve using Minion.
let solver = Solver::new(adaptors::Minion::new());
let solver: Solver<adaptors::Minion,ModelLoaded> = solver.load_model(model).unwrap();

// 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<Mutex<T>> 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);

§The Solver callback function

The callback function given to solve is called whenever a solution is found by the solver.

Its return value can be used to control how many solutions the solver finds:

  • If the callback function returns true, solver execution continues.
  • If the callback function returns false, the solver is terminated.

Modules§

Structs§

Enums§

Traits§

Type Aliases§