pumpkin-core 0.4.0

use super::outputs::Satisfiable;
use super::outputs::SolutionReference;
use super::results::OptimisationResult;
use super::results::SatisfactionResult;
use super::results::SatisfactionResultUnderAssumptions;
use crate::basic_types::CSPSolverExecutionFlag;
use crate::basic_types::ConstraintOperationError;
use crate::branching::Brancher;
use crate::branching::branchers::autonomous_search::AutonomousSearch;
use crate::branching::branchers::independent_variable_value_brancher::IndependentVariableValueBrancher;
use crate::branching::value_selection::RandomSplitter;
#[cfg(doc)]
use crate::branching::value_selection::ValueSelector;
use crate::branching::variable_selection::RandomSelector;
#[cfg(doc)]
use crate::branching::variable_selection::VariableSelector;
use crate::conflict_resolving::ConflictAnalysisContext;
use crate::conflict_resolving::ConflictResolver;
use crate::constraints::ConstraintPoster;
use crate::containers::HashSet;
use crate::engine::ConstraintSatisfactionSolver;
use crate::engine::predicates::predicate::Predicate;
use crate::engine::termination::TerminationCondition;
use crate::engine::variables::DomainId;
use crate::engine::variables::IntegerVariable;
use crate::engine::variables::Literal;
use crate::optimisation::OptimisationProcedure;
#[cfg(doc)]
use crate::optimisation::linear_sat_unsat::LinearSatUnsat;
#[cfg(doc)]
use crate::optimisation::linear_unsat_sat::LinearUnsatSat;
use crate::optimisation::solution_callback::SolutionCallback;
use crate::options::SolverOptions;
#[cfg(doc)]
use crate::predicates;
use crate::proof::ConstraintTag;
use crate::propagation::PropagatorConstructor;
pub use crate::propagation::store::PropagatorHandle;
use crate::results::solution_iterator::SolutionIterator;
use crate::results::unsatisfiable::UnsatisfiableUnderAssumptions;
use crate::statistics::StatisticLogger;
use crate::statistics::log_statistic;
use crate::statistics::log_statistic_postfix;

/// The main interaction point which allows the creation of variables, the addition of constraints,
/// and solving problems.
///
///
/// # Creating Variables
/// As stated in [`crate::variables`], we can create two types of variables: propositional variables
/// and integer variables.
///
/// ```rust
/// # use pumpkin_core::Solver;
/// # use pumpkin_core::variables::TransformableVariable;
/// let mut solver = Solver::default();
///
/// // Integer Variables
///
/// // We can create an integer variable with a domain in the range [0, 10]
/// let integer_between_bounds = solver.new_bounded_integer(0, 10);
///
/// // We can also create such a variable with a name
/// let named_integer_between_bounds = solver.new_named_bounded_integer(0, 10, "x");
///
/// // We can also create an integer variable with a non-continuous domain in the follow way
/// let mut sparse_integer = solver.new_sparse_integer(vec![0, 3, 5]);
///
/// // We can also create such a variable with a name
/// let named_sparse_integer = solver.new_named_sparse_integer(vec![0, 3, 5], "y");
///
/// // Additionally, we can also create an affine view over a variable with both a scale and an offset (or either)
/// let view_over_integer = integer_between_bounds.scaled(-1).offset(15);
///
///
/// // Propositional Variable
///
/// // We can create a literal
/// let literal = solver.new_literal();
///
/// // We can also create such a variable with a name
/// let named_literal = solver.new_named_literal("z");
///
/// // 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<_>>();
/// assert_eq!(list_of_5_literals.len(), 5);
/// ```
///
/// # Using the Solver
/// For examples on how to use the solver, see the [root-level crate documentation](crate) or [one of these examples](https://github.com/ConSol-Lab/Pumpkin/tree/master/pumpkin-lib/examples).
#[derive(Debug)]
pub struct Solver {
    /// The internal [`ConstraintSatisfactionSolver`] which is used to solve the problems.
    pub(crate) satisfaction_solver: ConstraintSatisfactionSolver,
    true_literal: Literal,
}

impl Default for Solver {
    fn default() -> Self {
        let satisfaction_solver = ConstraintSatisfactionSolver::default();
        let true_literal = Literal::new(Predicate::trivially_true().get_domain());
        Self {
            satisfaction_solver,
            true_literal,
        }
    }
}

impl Solver {
    /// Creates a solver with the provided [`SolverOptions`].
    pub fn with_options(solver_options: SolverOptions) -> Self {
        let satisfaction_solver = ConstraintSatisfactionSolver::new(solver_options);
        let true_literal = Literal::new(Predicate::trivially_true().get_domain());
        Self {
            satisfaction_solver,
            true_literal,
        }
    }

    /// Logs the statistics currently present in the solver with the provided objective value.
    pub fn log_statistics_with_objective(
        &self,
        brancher: &impl Brancher,
        resolver: &impl ConflictResolver,
        objective_value: i64,
        verbose: bool,
    ) {
        log_statistic("objective", objective_value);
        self.log_statistics(brancher, resolver, verbose);
    }

    /// Logs the statistics currently present in the solver.
    pub fn log_statistics(
        &self,
        brancher: &impl Brancher,
        resolver: &impl ConflictResolver,
        verbose: bool,
    ) {
        self.satisfaction_solver.log_statistics(verbose);
        resolver.log_statistics(StatisticLogger::default());
        if verbose {
            brancher.log_statistics(StatisticLogger::default());
        }
        log_statistic_postfix();
    }

    pub fn get_solution_reference(&self) -> SolutionReference<'_> {
        self.satisfaction_solver.get_solution_reference()
    }

    pub fn is_logging_proof(&self) -> bool {
        self.satisfaction_solver.is_logging_proof()
    }
}

/// Methods to retrieve information about variables
impl Solver {
    /// Get the value of the given [`Literal`] at the root level (after propagation), which could be
    /// unassigned.
    pub fn get_literal_value(&self, literal: Literal) -> Option<bool> {
        self.satisfaction_solver.get_literal_value(literal)
    }

    /// Get the lower-bound of the given [`IntegerVariable`] at the root level (after propagation).
    pub fn lower_bound(&self, variable: &impl IntegerVariable) -> i32 {
        self.satisfaction_solver.get_lower_bound(variable)
    }

    /// Get the upper-bound of the given [`IntegerVariable`] at the root level (after propagation).
    pub fn upper_bound(&self, variable: &impl IntegerVariable) -> i32 {
        self.satisfaction_solver.get_upper_bound(variable)
    }

    /// Returns whether the solver is in an inconsistent state.
    pub fn is_inconsistent(&self) -> bool {
        self.satisfaction_solver.get_state().is_inconsistent()
    }
}

/// Functions to create and retrieve integer and propositional variables.
impl Solver {
    /// Returns an infinite iterator of positive literals of new variables. The new variables will
    /// be unnamed.
    ///
    /// # Example
    /// ```
    /// # use pumpkin_core::Solver;
    /// # use pumpkin_core::variables::Literal;
    /// let mut solver = Solver::default();
    /// let literals: Vec<Literal> = solver.new_literals().take(5).collect();
    ///
    /// // `literals` contains 5 positive literals of newly created propositional variables.
    /// assert_eq!(literals.len(), 5);
    /// ```
    ///
    /// Note that this method captures the lifetime of the immutable reference to `self`.
    pub fn new_literals(&mut self) -> impl Iterator<Item = Literal> + '_ {
        std::iter::from_fn(|| Some(self.new_literal()))
    }

    /// Create a fresh propositional variable and return the literal with positive polarity.
    ///
    /// # Example
    /// ```rust
    /// # use pumpkin_core::Solver;
    /// let mut solver = Solver::default();
    ///
    /// // We can create a literal
    /// let literal = solver.new_literal();
    /// ```
    pub fn new_literal(&mut self) -> Literal {
        self.satisfaction_solver.create_new_literal(None)
    }

    pub fn new_literal_for_predicate(
        &mut self,
        predicate: Predicate,
        constraint_tag: ConstraintTag,
    ) -> Literal {
        self.satisfaction_solver
            .create_new_literal_for_predicate(predicate, None, constraint_tag)
    }

    pub fn new_named_literal_for_predicate(
        &mut self,
        predicate: Predicate,
        constraint_tag: ConstraintTag,
        name: impl Into<String>,
    ) -> Literal {
        self.satisfaction_solver.create_new_literal_for_predicate(
            predicate,
            Some(name.into().into()),
            constraint_tag,
        )
    }

    /// Create a fresh propositional variable with a given name and return the literal with positive
    /// polarity.
    ///
    /// # Example
    /// ```rust
    /// # use pumpkin_core::Solver;
    /// let mut solver = Solver::default();
    ///
    /// // We can also create such a variable with a name
    /// let named_literal = solver.new_named_literal("z");
    /// ```
    pub fn new_named_literal(&mut self, name: impl Into<String>) -> Literal {
        let name = name.into();
        self.satisfaction_solver
            .create_new_literal(Some(name.into()))
    }

    /// Get a literal which is always true.
    pub fn get_true_literal(&self) -> Literal {
        self.true_literal
    }

    /// Get a literal which is always false.
    pub fn get_false_literal(&self) -> Literal {
        !self.true_literal
    }

    /// Create a new integer variable with the given bounds.
    ///
    /// # Example
    /// ```rust
    /// # use pumpkin_core::Solver;
    /// let mut solver = Solver::default();
    ///
    /// // We can create an integer variable with a domain in the range [0, 10]
    /// let integer_between_bounds = solver.new_bounded_integer(0, 10);
    /// ```
    pub fn new_bounded_integer(&mut self, lower_bound: i32, upper_bound: i32) -> DomainId {
        self.satisfaction_solver
            .create_new_integer_variable(lower_bound, upper_bound, None)
    }

    /// Create a new named integer variable with the given bounds.
    ///
    /// # Example
    /// ```rust
    /// # use pumpkin_core::Solver;
    /// let mut solver = Solver::default();
    ///
    /// // We can also create such a variable with a name
    /// let named_integer_between_bounds = solver.new_named_bounded_integer(0, 10, "x");
    /// ```
    pub fn new_named_bounded_integer(
        &mut self,
        lower_bound: i32,
        upper_bound: i32,
        name: impl Into<String>,
    ) -> DomainId {
        let name = name.into();
        self.satisfaction_solver.create_new_integer_variable(
            lower_bound,
            upper_bound,
            Some(name.into()),
        )
    }

    /// Create a new integer variable which has a domain of predefined values. We remove duplicates
    /// by converting to a hash set
    ///
    /// # Example
    /// ```rust
    /// # use pumpkin_core::Solver;
    /// let mut solver = Solver::default();
    ///
    /// // We can also create an integer variable with a non-continuous domain in the follow way
    /// let mut sparse_integer = solver.new_sparse_integer(vec![0, 3, 5]);
    /// ```
    pub fn new_sparse_integer(&mut self, values: impl Into<Vec<i32>>) -> DomainId {
        let values: HashSet<i32> = values.into().into_iter().collect();

        self.satisfaction_solver
            .create_new_integer_variable_sparse(values.into_iter().collect(), None)
    }

    /// Create a new named integer variable which has a domain of predefined values.
    ///
    /// # Example
    /// ```rust
    /// # use pumpkin_core::Solver;
    /// let mut solver = Solver::default();
    ///
    /// // We can also create such a variable with a name
    /// let named_sparse_integer = solver.new_named_sparse_integer(vec![0, 3, 5], "y");
    /// ```
    pub fn new_named_sparse_integer(
        &mut self,
        values: impl Into<Vec<i32>>,
        name: impl Into<String>,
    ) -> DomainId {
        self.satisfaction_solver
            .create_new_integer_variable_sparse(values.into(), Some(name.into()))
    }
}

/// Functions for solving with the constraints that have been added to the [`Solver`].
impl Solver {
    /// Solves the current model in the [`Solver`] until it finds a solution (or is indicated to
    /// terminate by the provided [`TerminationCondition`]) and returns a [`SatisfactionResult`]
    /// which can be used to obtain the found solution or find other solutions.
    pub fn satisfy<
        'this,
        'brancher,
        'resolver,
        B: Brancher,
        T: TerminationCondition,
        R: ConflictResolver,
    >(
        &'this mut self,
        brancher: &'brancher mut B,
        termination: &mut T,
        resolver: &'resolver mut R,
    ) -> SatisfactionResult<'this, 'brancher, 'resolver, B, R> {
        match self
            .satisfaction_solver
            .solve(termination, brancher, resolver)
        {
            CSPSolverExecutionFlag::Feasible => {
                brancher.on_solution(self.satisfaction_solver.get_solution_reference());

                SatisfactionResult::Satisfiable(Satisfiable::new(self, brancher, resolver))
            }
            CSPSolverExecutionFlag::Infeasible => {
                // Reset the state whenever we return a result
                self.satisfaction_solver.restore_state_at_root(brancher);
                let _ = self.satisfaction_solver.conclude_proof_unsat();

                SatisfactionResult::Unsatisfiable(self, brancher, resolver)
            }
            CSPSolverExecutionFlag::Timeout => {
                // Reset the state whenever we return a result
                self.satisfaction_solver.restore_state_at_root(brancher);
                SatisfactionResult::Unknown(self, brancher, resolver)
            }
        }
    }

    /// Returns a [`SolutionIterator`] which can be used to generate multiple solutions for a
    /// satisfaction problem.
    pub fn get_solution_iterator<
        'this,
        'brancher,
        'termination,
        'resolver,
        B: Brancher,
        T: TerminationCondition,
        R: ConflictResolver,
    >(
        &'this mut self,
        brancher: &'brancher mut B,
        termination: &'termination mut T,
        resolver: &'resolver mut R,
    ) -> SolutionIterator<'this, 'brancher, 'termination, 'resolver, B, T, R> {
        SolutionIterator::new(self, brancher, termination, resolver)
    }

    /// Solves the current model in the [`Solver`] until it finds a solution (or is indicated to
    /// terminate by the provided [`TerminationCondition`]) and returns a [`SatisfactionResult`]
    /// which can be used to obtain the found solution or find other solutions.
    ///
    /// This method takes as input a list of [`Predicate`]s which represent so-called assumptions
    /// (see \[1\] for a more detailed explanation). See the [`predicates`] documentation for how
    /// to construct these predicates.
    ///
    /// # Bibliography
    /// \[1\] N. Eén and N. Sörensson, ‘Temporal induction by incremental SAT solving’, Electronic
    /// Notes in Theoretical Computer Science, vol. 89, no. 4, pp. 543–560, 2003.
    pub fn satisfy_under_assumptions<
        'this,
        'brancher,
        'resolver,
        B: Brancher,
        R: ConflictResolver,
    >(
        &'this mut self,
        brancher: &'brancher mut B,
        termination: &mut impl TerminationCondition,
        resolver: &'resolver mut R,
        assumptions: &[Predicate],
    ) -> SatisfactionResultUnderAssumptions<'this, 'brancher, 'resolver, B, R> {
        match self.satisfaction_solver.solve_under_assumptions(
            assumptions,
            termination,
            brancher,
            resolver,
        ) {
            CSPSolverExecutionFlag::Feasible => {
                // Reset the state whenever we return a result
                brancher.on_solution(self.satisfaction_solver.get_solution_reference());
                SatisfactionResultUnderAssumptions::Satisfiable(Satisfiable::new(
                    self, brancher, resolver,
                ))
            }
            CSPSolverExecutionFlag::Infeasible => {
                if self
                    .satisfaction_solver
                    .solver_state
                    .is_infeasible_under_assumptions()
                {
                    // The state is automatically reset when we return this result
                    SatisfactionResultUnderAssumptions::UnsatisfiableUnderAssumptions(
                        UnsatisfiableUnderAssumptions::new(&mut self.satisfaction_solver, brancher),
                    )
                } else {
                    // Reset the state whenever we return a result
                    self.satisfaction_solver.restore_state_at_root(brancher);
                    SatisfactionResultUnderAssumptions::Unsatisfiable(self)
                }
            }
            CSPSolverExecutionFlag::Timeout => {
                // Reset the state whenever we return a result
                self.satisfaction_solver.restore_state_at_root(brancher);
                SatisfactionResultUnderAssumptions::Unknown(self)
            }
        }
    }

    /// Solves the model currently in the [`Solver`] to optimality where the provided
    /// `objective_variable` is optimised as indicated by the `direction` (or is indicated to
    /// terminate by the provided [`TerminationCondition`]). Uses a search strategy based on the
    /// provided [`OptimisationProcedure`], currently [`LinearSatUnsat`] and
    /// [`LinearUnsatSat`] are supported.
    ///
    /// It returns an [`OptimisationResult`] which can be used to retrieve the optimal solution if
    /// it exists.
    pub fn optimise<B, R, Callback>(
        &mut self,
        brancher: &mut B,
        termination: &mut impl TerminationCondition,
        resolver: &mut R,
        mut optimisation_procedure: impl OptimisationProcedure<B, R, Callback>,
    ) -> OptimisationResult<Callback::Stop>
    where
        B: Brancher,
        R: ConflictResolver,
        Callback: SolutionCallback<B, R>,
    {
        optimisation_procedure.optimise(brancher, termination, resolver, self)
    }
}

/// Functions for adding new constraints to the solver.
impl Solver {
    /// Creates a new [`ConstraintTag`] that can be used to add constraints to the solver.
    ///
    /// See the [`ConstraintTag`] documentation for information on how the tags are used.
    pub fn new_constraint_tag(&mut self) -> ConstraintTag {
        self.satisfaction_solver.new_constraint_tag()
    }

    /// Add a constraint to the solver. This returns a [`ConstraintPoster`] which enables control
    /// on whether to add the constraint as-is, or whether to (half) reify it.
    ///
    /// All constraints require a [`ConstraintTag`] to be supplied. See its documentation for more
    /// information.
    ///
    /// If none of the methods on [`ConstraintPoster`] are used, the constraint _is not_ actually
    /// added to the solver. In this case, a warning is emitted.
    ///
    /// # Example
    /// ```ignore
    /// # use pumpkin_core::Solver;
    /// let mut solver = Solver::default();
    ///
    /// let a = solver.new_bounded_integer(0, 3);
    /// let b = solver.new_bounded_integer(0, 3);
    ///
    /// let constraint_tag = solver.new_constraint_tag();
    ///
    /// solver
    ///     .add_constraint(pumpkin_constraints::equals([a, b], 0, constraint_tag))
    ///     .post();
    /// ```
    pub fn add_constraint<Constraint>(
        &mut self,
        constraint: Constraint,
    ) -> ConstraintPoster<'_, Constraint> {
        ConstraintPoster::new(self, constraint)
    }

    /// Creates a clause from `literals` and adds it to the current formula.
    ///
    /// If the formula becomes trivially unsatisfiable, a [`ConstraintOperationError`] will be
    /// returned. Subsequent calls to this method will always return an error, and no
    /// modification of the solver will take place.
    pub fn add_clause(
        &mut self,
        clause: impl IntoIterator<Item = Predicate>,
        constraint_tag: ConstraintTag,
    ) -> Result<(), ConstraintOperationError> {
        self.satisfaction_solver.add_clause(clause, constraint_tag)
    }

    /// Post a new propagator to the solver. If unsatisfiability can be immediately determined
    /// through propagation, this will return a [`ConstraintOperationError`].
    ///
    /// A propagator is provided through an implementation of [`PropagatorConstructor`]. The
    /// propagator that will be added is [`PropagatorConstructor::PropagatorImpl`].
    ///
    /// If the solver is already in a conflicting state, i.e. a previous call to this method
    /// already returned `false`, calling this again will not alter the solver in any way, and
    /// `false` will be returned again.
    pub fn add_propagator<Constructor>(
        &mut self,
        constructor: Constructor,
    ) -> Result<PropagatorHandle<Constructor::PropagatorImpl>, ConstraintOperationError>
    where
        Constructor: PropagatorConstructor,
        Constructor::PropagatorImpl: 'static,
    {
        self.satisfaction_solver.add_propagator(constructor)
    }
}

/// Default brancher implementation
impl Solver {
    /// Creates an instance of the [`DefaultBrancher`].
    pub fn default_brancher(&self) -> DefaultBrancher {
        DefaultBrancher::default_over_all_variables(self.satisfaction_solver.assignments())
    }
}

/// Proof logging methods
impl Solver {
    #[doc(hidden)]
    /// Conclude the proof with the unsatisfiable claim.
    ///
    /// This method will finish the proof. Any new operation will not be logged to the proof.
    pub fn conclude_proof_unsat(&mut self) {
        let _ = self.satisfaction_solver.conclude_proof_unsat();
    }

    /// Conclude the proof with the optimality claim.
    ///
    /// This method will finish the proof. Any new operation will not be logged to the proof.
    pub fn conclude_proof_dual_bound(&mut self, bound: Predicate) {
        let _ = self.satisfaction_solver.conclude_proof_optimal(bound);
    }
}

impl Solver {
    #[deprecated(note = "Should only be used for testing")]
    pub fn conflict_analysis_context<'a>(
        &'a mut self,
        brancher: &'a mut impl Brancher,
    ) -> ConflictAnalysisContext<'a> {
        ConflictAnalysisContext {
            solver_state: &mut self.satisfaction_solver.solver_state,
            brancher,
            proof_log: &mut self.satisfaction_solver.internal_parameters.proof_log,
            unit_nogood_inference_codes: &mut self.satisfaction_solver.unit_nogood_inference_codes,
            restart_strategy: &mut self.satisfaction_solver.restart_strategy,
            state: &mut self.satisfaction_solver.state,
            nogood_propagator_handle: self.satisfaction_solver.nogood_propagator_handle,
            rng: &mut self
                .satisfaction_solver
                .internal_parameters
                .random_generator,
        }
    }
}

/// A brancher which makes use of VSIDS \[1\] and solution-based phase saving (both adapted for CP).
///
/// If VSIDS does not contain any (unfixed) predicates then it will default to the
/// [`IndependentVariableValueBrancher`] using [`RandomSelector`] for variable selection
/// (over the variables in the order in which they were defined) and [`RandomSplitter`] for
/// value selection.
///
/// # Bibliography
/// \[1\] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, ‘Chaff: Engineering an
/// efficient SAT solver’, in Proceedings of the 38th annual Design Automation Conference, 2001.
///
/// \[2\] E. Demirović, G. Chu, and P. J. Stuckey, ‘Solution-based phase saving for CP: A
/// value-selection heuristic to simulate local search behavior in complete solvers’, in the
/// proceedings of the Principles and Practice of Constraint Programming (CP 2018).
pub type DefaultBrancher =
    AutonomousSearch<IndependentVariableValueBrancher<DomainId, RandomSelector, RandomSplitter>>;