Basic incremental solving

[soonho-tri]

• When a solver-status is unsat with the current assertions {φ₁, ..., φₙ}, adding further assertions {φₙ₊₁, ...} should return unsat immediately.

• When an assertion φᵢ is added to a solver, we need to run the contractor to reduce its search space (but without branching). This should be the first step toward more interesting techniques (i.e. learning).

/cc @AndreaCallia