Skip to main content Crate pumpkin_core Copy item path Source pub use convert_case ;pub use rand ;branching Contains structures and traits to define the decision making procedure of the Solver conflict_resolving Contains algorithms for conflict analysis, core extraction, and clause minimisation.
The algorithms use resolution and implement the 1uip and all decision literal learning schemes constraints Defines the main building blocks of constraints. containers Contains containers which are used by the solver. optimisation Contains structures related to optimissation. options Contains the options which can be passed to the Solver predicates Contains structures which represent certain predicates . proof Pumpkin supports proof logging for SAT and CP problems. During search, the solver produces a
ProofLog propagation Contains the main building blocks for propagators. propagators results Contains the outputs of solving using the Solver state Contains structures for the state containing the propagators and variables. statistics Contains structures related to the statistic logging of the Solver termination Contains the conditions which are used to determine when the Solver variables Contains the variables which are used by the Solver conjunction A macro which allows for the creation of a PropositionalConjunction create_statistics_struct A macro for generating a struct for storing statistics. declare_inference_label Conveniently creates InferenceLabel predicate A macro which allows for the creation of a Predicate Duration A Duration type to represent a span of time, typically used for system
timeouts. Function A struct which represents a linear function over weighted Literal Instant A measurement of a monotonically nondecreasing clock.
Opaque and useful only with Duration Solver The main interaction point which allows the creation of variables, the addition of constraints,
and solving problems. SolverStatistics Structure responsible for storing several statistics of the solving process of the solver. TestSolver A container for CP variables, which can be used to test propagators. ConstraintOperationError Errors related to adding constraints to the Solver Random Abstraction for randomness, in order to swap out different source of randomness. DefaultBrancher A brancher which makes use of VSIDS [1] and solution-based phase saving (both adapted for CP).