Since CaDiCaL 3.x allows the solver to introduce extension variables that the user can't use, we should combine variable management and collecting clauses into one trait along the lines of pindakaas' ClausesDatabase.
Additionally, building non-incremental encodings should probably cause a typestate transition of sorts.
Since CaDiCaL 3.x allows the solver to introduce extension variables that the user can't use, we should combine variable management and collecting clauses into one trait along the lines of
pindakaas'ClausesDatabase.Additionally, building non-incremental encodings should probably cause a typestate transition of sorts.