Expand description
Contains the outputs of solving using the [Solver].
We differentiate between 3 different types of results:
- For a satisfaction problem (
SatisfactionResult) - For a satisfaction problem using assumptions
(
SatisfactionResultUnderAssumptions) - For an optimisation problem (
OptimisationResult)
On these results, different methods can be called which ensure that the solver is in the
right state for these operations. For example,
SatisfactionResultUnderAssumptions::UnsatisfiableUnderAssumptions allows you to extract
a core consisting of the assumptions using [UnsatisfiableUnderAssumptions::extract_core].
Modules§
- solution_
iterator - Contains the structures corresponding to solution iterations.
- unsatisfiable
- Contains the representation of a unsatisfiable solution.
Structs§
- Satisfiable
- Solution
- A solution which takes ownership of its inner structures.
- Solution
Reference - A solution which keeps reference to its inner structures.
Enums§
- Optimisation
Result - The result of a call to
Solver::optimise. - Satisfaction
Result - The result of a call to
Solver::satisfy. - Satisfaction
Result Under Assumptions - The result of a call to
Solver::satisfy_under_assumptions.
Traits§
- Problem
Solution - A trait which specifies the common behaviours of
SolutionandSolutionReference.