function to add a literal

[c-cube]

would be nice to have add_lit: lit -> unit that forces the solver to decide on this literal, even if there is no constraint on it yet.

[Gbury]

Would it be enough to have such a fonction in the signature of the solver, or do you need it in the slice ? Also note that such a function would add literals to the set of literals on which to decide, so that they will be decided on at some time later in the algorithm, but not right away.

[c-cube]

I'm aware they will not be decided just yet, sure. It can be in the signature directly, I guess?

[c-cube]

Also:

val reset : unit -> unit to go back to level 0 without solving again immediately. Should backtrack the theory as well, but not forget the learnt clauses.

[Gbury]

About the reset function, two things:

• it wouldn't be possible to call it from within a slice
• it wouldn't backtrack to level 0, but rather base_level (i.e. level 0 plus the local/temp assumptions)

Would that be sufficient ? If not, what exactly would be your use case of reset ?

[c-cube]

bah, should be fine anyway.

[Gbury]

Closed with 928622b5115e3c2247de196a6b8ab9c715ccd047