solver3: Remove Push() and refactor Solve()

This method is no longer needed technically speaking, we should
use Assume() instead. It turns out that there is a slight bug in
the propagation and some clauses that are unit end up on the heap
rather than having been propagated away, so we temporarily need
to keep an if for that around.

To accomodate the switch from Push() to Assume() we need to make
sure that the work item is pushed to our trail *after* we
have assumed it, such that reverting pushes it back to the work
heap.

Refactor the code to consistently use Assume() rather than supporting
Enqueue(), this vastly simplifies things. This is not fully accurate
in the current model and leads to unnecessary decision levels, since
sometimes we seem to be reaching unit clauses here.

This preserves traversal order by first removing the item from the
heap and then adding it back if we need to solve it again.

1 files changed, 0 insertions, 2 deletions

diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h
index f66b3cf62..facba4d39 100644
--- a/apt-pkg/solver3.h
+++ b/apt-pkg/solver3.h
@@ -370,8 +370,6 @@ class Solver
    inline LiftedBool value(Lit lit) const;
 
    public:
-   // \brief Create a new decision level.
-   void Push(Var var, Work work);
    // \brief Revert to the previous decision level.
    [[nodiscard]] bool Pop();
    // \brief Undo a single assignment / trail work item