Struct RpEngine

pub struct RpEngine { /* private fields */ }

An API for performing backwards reverse propagation of a clausal proof. The API allows the reasons for all propagations that are used to derive the RP clause to be accessed.

To use the RpEngine, one can do the following:

1. Initialise it with a base model against which the individual reverse propagating clauses will be checked.
2. Add reverse propagating clauses through RpEngine::add_rp_clause. The order in which this happens matters.
3. Check whether a propagation can derive a conflict under certain assumptions (probably the negation of a reverse propagating clause which is no-longer in the engine).
4. Remove the reverse propagating clauses with RpEngine::remove_last_rp_clause in reverse order in which they were added.

Implementations

impl RpEngine

pub fn new(solver: Solver) -> Self

Create a new reverse propagating engine based on a Solver initialized with the model of the problem.

pub fn add_rp_clause( &mut self, clause: impl IntoIterator<Item = Literal>, ) -> Result<RpClauseHandle, ReversePropagationConflict>

Add a new reverse propagating clause to the engine. The clause should not be empty, and the engine should not be in an conflicting state.

If the new clause causes a conflict under propagation, the engine will be in a conflicting state. A call to RpEngine::remove_last_rp_clause will remove the newly added clause and reset the engine to a useable state.

pub fn remove_last_rp_clause(&mut self) -> Option<Vec<Literal>>

Remove the last clause in the proof from consideration and return the literals it contains.

pub fn propagate_under_assumptions( &mut self, assumptions: impl IntoIterator<Item = Literal>, ) -> Result<(), Vec<ConflictReason>>

Perform unit propagation under assumptions.

In case the engine discovers a conflict, the engine will be in a conflicting state. At this point, no new clauses can be added before a call to RpEngine::remove_last_rp_clause.

Trait Implementations

impl Debug for RpEngine

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.