docs: fix documentation test cases

pumpkin-solver/src/api/outputs/unsatisfiable.rs

@@ -66,13 +66,13 @@ impl<'solver, 'brancher, B: Brancher> UnsatisfiableUnderAssumptions<'solver, 'br
     /// // We create a termination condition which allows the solver to run indefinitely
     /// let mut termination = Indefinite;
     /// // And we create a search strategy (in this case, simply the default)
-    /// let mut brancher = solver.default_brancher_over_all_propositional_variables();
+    /// let mut brancher = solver.default_brancher();
     ///
     /// // Then we solve to satisfaction
     /// let assumptions = vec![
-    ///     solver.get_literal(predicate!(x == 1)),
-    ///     solver.get_literal(predicate!(y <= 1)),
-    ///     solver.get_literal(predicate!(y != 0)),
+    ///     predicate!(x == 1),
+    ///     predicate!(y <= 1),
+    ///     predicate!(y != 0),
     /// ];
     /// let result =
     ///     solver.satisfy_under_assumptions(&mut brancher, &mut termination, &assumptions);
@@ -84,10 +84,8 @@ impl<'solver, 'brancher, B: Brancher> UnsatisfiableUnderAssumptions<'solver, 'br
     ///     {
     ///         let core = unsatisfiable.extract_core();
     ///
-    ///         // In this case, the core should be equal to all assumption literals
-    ///         assert!(assumptions
-    ///             .into_iter()
-    ///             .all(|literal| core.contains(&literal)));
+    ///         // In this case, the core should be equal to all assumption predicates
+    ///         assert_eq!(core, vec![predicate!(y == 1), predicate!(x == 1)].into());
     ///     }
     /// }
     ///  ```

pumpkin-solver/src/api/solver.rs

@@ -72,8 +72,8 @@ use crate::statistics::log_statistic_postfix;
 /// // We can also create such a variable with a name
 /// let named_literal = solver.new_named_literal("z");
 ///
-/// // We can also get the propositional variable from the literal
-/// let propositional_variable = literal.get_propositional_variable();
+/// // We can also get the predicate from the literal
+/// let true_predicate = literal.get_true_predicate();
 ///
 /// // We can also create an iterator of new literals and get a number of them at once
 /// let list_of_5_literals = solver.new_literals().take(5).collect::<Vec<_>>();

pumpkin-solver/src/branching/mod.rs

@@ -15,28 +15,21 @@
 //! [`Solver::minimise`]:
 //! ```rust
 //! # use pumpkin_solver::Solver;
-//! # use pumpkin_solver::variables::PropositionalVariable;
-//! # use pumpkin_solver::branching::variable_selection::Vsids;
-//! # use pumpkin_solver::branching::value_selection::PhaseSaving;
-//! # use pumpkin_solver::branching::branchers::independent_variable_value_brancher::IndependentVariableValueBrancher;
 //! # use pumpkin_solver::variables::Literal;
 //! # use pumpkin_solver::termination::Indefinite;
 //! # use pumpkin_solver::results::SatisfactionResult;
 //! # use crate::pumpkin_solver::results::ProblemSolution;
 //! let mut solver = Solver::default();
 //!
-//! let variables = vec![solver.new_literal().get_propositional_variable()];
+//! let variables = vec![solver.new_literal()];
 //!
 //! let mut termination = Indefinite;
-//! let mut brancher = IndependentVariableValueBrancher::new(
-//!     Vsids::new(&variables),
-//!     PhaseSaving::new(&variables),
-//! );
+//! let mut brancher = solver.default_brancher();
 //! let result = solver.satisfy(&mut brancher, &mut termination);
 //! if let SatisfactionResult::Satisfiable(solution) = result {
 //!     // Getting the value of the literal in the solution should not panic
 //!     variables.into_iter().for_each(|variable| {
-//!         solver.get_literal_value(Literal::new(variable, true));
+//!         solver.get_literal_value(variable);
 //!     });
 //! } else {
 //!     panic!("Solving should have returned satsifiable")
@@ -49,8 +42,6 @@
 //! [`Solver::default_brancher`].
 //! ```rust
 //! # use pumpkin_solver::Solver;
-//! # use pumpkin_solver::variables::PropositionalVariable;
-//! # use pumpkin_solver::branching::branchers::independent_variable_value_brancher::IndependentVariableValueBrancher;
 //! # use pumpkin_solver::variables::Literal;
 //! # use pumpkin_solver::termination::Indefinite;
 //! # use pumpkin_solver::results::SatisfactionResult;
@@ -60,7 +51,7 @@
 //! let literals = vec![solver.new_literal()];
 //!
 //! let mut termination = Indefinite;
-//! let mut brancher = solver.default_brancher_over_all_propositional_variables();
+//! let mut brancher = solver.default_brancher();
 //! let result = solver.satisfy(&mut brancher, &mut termination);
 //! if let SatisfactionResult::Satisfiable(solution) = result {
 //!     // Getting the value of the literal in the solution should not panic

pumpkin-solver/src/constraints/cumulative.rs

@@ -67,7 +67,7 @@ use crate::Solver;
 ///     .post();
 ///
 /// let mut termination = Indefinite;
-/// let mut brancher = solver.default_brancher_over_all_propositional_variables();
+/// let mut brancher = solver.default_brancher();
 ///
 /// let result = solver.satisfy(&mut brancher, &mut termination);
 ///

pumpkin-solver/src/engine/constraint_satisfaction_solver.rs

@@ -66,60 +66,22 @@ use crate::Solver;
 /// a Lazy Clause Generation (LCG [\[1\]](https://people.eng.unimelb.edu.au/pstuckey/papers/cp09-lc.pdf))
 /// approach.
 ///
-/// The solver maintains two views of the problem, a Constraint Programming (CP) view and a SAT
-/// view. It requires that all of the propagators which are added, are able to explain the
+/// It requires that all of the propagators which are added, are able to explain the
 /// propagations and conflicts they have made/found. It then uses standard SAT concepts such as
 /// 1UIP (see \[2\]) to learn clauses (also called nogoods in the CP field, see \[3\]) to avoid
 /// unnecessary exploration of the search space while utilizing the search procedure benefits from
 /// constraint programming (e.g. by preventing the exponential blow-up of problem encodings).
 ///
 /// # Practical
 /// The [`ConstraintSatisfactionSolver`] makes use of certain options which allow the user to
-/// influence the behaviour of the solver; see the [`SatisfactionSolverOptions`].
+/// influence the behaviour of the solver; see for example the [`SatisfactionSolverOptions`].
 ///
 /// The solver switches between making decisions using implementations of the [`Brancher`] (which
 /// are passed to the [`ConstraintSatisfactionSolver::solve`] method) and propagation (use
 /// [`ConstraintSatisfactionSolver::add_propagator`] to add a propagator). If a conflict is found by
-/// any of the propagators (including the clausal one) then the solver will analyse the conflict
+/// any of the propagators then the solver will analyse the conflict
 /// using 1UIP reasoning and backtrack if possible.
 ///
-/// ## Example
-/// This example will show how to set-up the [`ConstraintSatisfactionSolver`] to solve a simple not
-/// equals problem between two variables. Note that any constraint is added in the form of
-/// propagators.
-/// ```
-/// # use pumpkin_lib::engine::ConstraintSatisfactionSolver;
-/// # use pumpkin_lib::propagators::arithmetic::linear_not_equal::LinearNotEqualConstructor;
-/// # use pumpkin_lib::branching::branchers::independent_variable_value_brancher::IndependentVariableValueBrancher;
-/// # use pumpkin_lib::basic_types::CSPSolverExecutionFlag;
-/// # use pumpkin_lib::engine::variables::IntegerVariable;
-/// # use pumpkin_lib::engine::variables::TransformableVariable;
-/// # use pumpkin_lib::engine::termination::indefinite::Indefinite;
-/// // We create a solver with default options (note that this is only possible in a testing environment)
-/// let mut solver = ConstraintSatisfactionSolver::default();
-///
-/// // Now we create the two variables for which we want to define the propagator
-/// let x = solver.create_new_integer_variable(0, 10, None);
-/// let y = solver.create_new_integer_variable(0, 10, None);
-///
-/// // We add the propagator to the solver and check that adding the propagator did not cause a conflict
-/// //  'x != y' is represented using the propagator for 'x - y != 0'
-/// let no_root_level_conflict = solver.add_propagator(LinearNotEqualConstructor::new([x.into(), y.scaled(-1)].into(), 0));
-/// assert!(no_root_level_conflict);
-///
-/// // We create a branching strategy, in our case we will simply use the default one
-/// let mut brancher = IndependentVariableValueBrancher::default_over_all_variables(&solver);
-///
-/// // Then we solve the problem given a time-limit and a branching strategy
-/// let result = solver.solve(&mut Indefinite, &mut brancher);
-///
-/// // Now we check that the result is feasible and that the chosen values for the two variables are different
-/// assert_eq!(result, CSPSolverExecutionFlag::Feasible);
-/// assert!(
-///     solver.get_assigned_integer_value(&x).unwrap() != solver.get_assigned_integer_value(&y).unwrap()
-/// );
-/// ```
-///
 /// # Bibliography
 /// \[1\] T. Feydy and P. J. Stuckey, ‘Lazy clause generation reengineered’, in International
 /// Conference on Principles and Practice of Constraint Programming, 2009, pp. 352–366.
@@ -608,30 +570,25 @@ impl ConstraintSatisfactionSolver {
     /// // And solve under the assumptions:
     /// //   !x0 /\ x1 /\ !x2
     /// # use pumpkin_solver::Solver;
-    /// # use pumpkin_solver::variables::PropositionalVariable;
-    /// # use pumpkin_solver::variables::Literal;
     /// # use pumpkin_solver::termination::Indefinite;
-    /// # use pumpkin_solver::branching::branchers::independent_variable_value_brancher::IndependentVariableValueBrancher;
     /// # use pumpkin_solver::results::SatisfactionResultUnderAssumptions;
     /// let mut solver = Solver::default();
     /// let x = vec![
-    ///     solver.new_literal(),
-    ///     solver.new_literal(),
-    ///     solver.new_literal(),
+    ///     solver.new_literal().get_true_predicate(),
+    ///     solver.new_literal().get_true_predicate(),
+    ///     solver.new_literal().get_true_predicate(),
     /// ];
     ///
     /// solver.add_clause([x[0], x[1], x[2]]);
     /// solver.add_clause([x[0], !x[1], x[2]]);
     ///
     /// let assumptions = [!x[0], x[1], !x[2]];
     /// let mut termination = Indefinite;
-    /// let mut brancher = solver.default_brancher_over_all_propositional_variables();
-    /// let result =
-    ///     solver.satisfy_under_assumptions(&mut brancher, &mut termination, &assumptions);
+    /// let mut brancher = solver.default_brancher();
+    /// let result = solver.satisfy_under_assumptions(&mut brancher, &mut termination, &assumptions);
     ///
-    /// if let SatisfactionResultUnderAssumptions::UnsatisfiableUnderAssumptions(
-    ///     mut unsatisfiable,
-    /// ) = result
+    /// if let SatisfactionResultUnderAssumptions::UnsatisfiableUnderAssumptions(mut unsatisfiable) =
+    ///     result
     /// {
     ///     {
     ///         let core = unsatisfiable.extract_core();

pumpkin-solver/src/engine/predicates/predicate_constructor.rs

@@ -57,7 +57,7 @@ impl PredicateConstructor for DomainId {
 /// ```rust
 /// # use pumpkin_solver::Solver;
 /// # use pumpkin_solver::predicate;
-/// # use pumpkin_solver::predicates::IntegerPredicate;
+/// # use pumpkin_solver::predicates::Predicate;
 /// let mut solver = Solver::default();
 /// let x = solver.new_bounded_integer(0, 10);
 ///

pumpkin-solver/src/lib.rs

@@ -68,7 +68,7 @@
 //! // We create a termination condition which allows the solver to run indefinitely
 //! let mut termination = Indefinite;
 //! // And we create a search strategy (in this case, simply the default)
-//! let mut brancher = solver.default_brancher_over_all_propositional_variables();
+//! let mut brancher = solver.default_brancher();
 //! ```
 //!
 //!
@@ -87,7 +87,7 @@
 //! # let z = solver.new_bounded_integer(7, 25);
 //! # solver.add_constraint(constraints::equals(vec![x, y, z], 17)).post();
 //! # let mut termination = Indefinite;
-//! # let mut brancher = solver.default_brancher_over_all_propositional_variables();
+//! # let mut brancher = solver.default_brancher();
 //! // Then we find a solution to the problem
 //! let result = solver.satisfy(&mut brancher, &mut termination);
 //!
@@ -139,7 +139,7 @@
 //! # solver.add_constraint(constraints::equals(vec![x, y, z], 17)).post();
 //! # solver.add_constraint(constraints::maximum(vec![x, y, z], objective)).post();
 //! # let mut termination = Indefinite;
-//! # let mut brancher = solver.default_brancher_over_all_propositional_variables();
+//! # let mut brancher = solver.default_brancher();
 //! // Then we solve to optimality
 //! let result = solver.minimise(&mut brancher, &mut termination, objective);
 //!
@@ -190,7 +190,7 @@
 //! // We create a termination condition which allows the solver to run indefinitely
 //! let mut termination = Indefinite;
 //! // And we create a search strategy (in this case, simply the default)
-//! let mut brancher = solver.default_brancher_over_all_propositional_variables();
+//! let mut brancher = solver.default_brancher();
 //!
 //! // Then we solve to satisfaction
 //! let mut solution_iterator = solver.get_solution_iterator(&mut brancher, &mut termination);
@@ -255,13 +255,13 @@
 //! // We create a termination condition which allows the solver to run indefinitely
 //! let mut termination = Indefinite;
 //! // And we create a search strategy (in this case, simply the default)
-//! let mut brancher = solver.default_brancher_over_all_propositional_variables();
+//! let mut brancher = solver.default_brancher();
 //!
 //! // Then we solve to satisfaction
 //! let assumptions = vec![
-//!     solver.get_literal(predicate!(x == 1)),
-//!     solver.get_literal(predicate!(y <= 1)),
-//!     solver.get_literal(predicate!(y != 0)),
+//!     predicate!(x == 1),
+//!     predicate!(y <= 1),
+//!     predicate!(y != 0),
 //! ];
 //! let result =
 //!     solver.satisfy_under_assumptions(&mut brancher, &mut termination, &assumptions);
@@ -274,9 +274,7 @@
 //!         let core = unsatisfiable.extract_core();
 //!
 //!         // In this case, the core should be equal to all of the assumption literals
-//!         assert!(assumptions
-//!             .into_iter()
-//!             .all(|literal| core.contains(&literal)));
+//!         assert_eq!(core, vec![predicate!(y == 1), predicate!(x == 1)].into());
 //!     }
 //! }
 //!  ```

pumpkin-solver/src/propagators/cumulative/mod.rs

@@ -65,7 +65,7 @@
 //!     .post();
 //!
 //! let mut termination = Indefinite;
-//! let mut brancher = solver.default_brancher_over_all_propositional_variables();
+//! let mut brancher = solver.default_brancher();
 //!
 //! let result = solver.satisfy(&mut brancher, &mut termination);
 //!