Adding a generic option manager for the dolmen state

[Stevendeo]

No description provided.

[bclement-ocp]

While I agree that sharing the boilerplate for these is nice, I am worried that the silent fall-back to the Options module could lead to some surprising behavior if we ever use this for options that incorporate mutable state. I would prefer keeping the reset function and either exposing the key directly (as DO.ProduceAssignment.key etc. which would be my preferred approach) or making get a pass-through to State.get to avoid the possibility of such issues entirely.

[bclement-ocp]

I think we should either go through first-class module or through a Make functor, but not both. I believe this could be:

(module struct
    type nonrec k = k
    type nonrec t = t
    let key = State.create_key ~pipe:"" key
    let set opt st = (* .. as in Make *)
    let reset = set (get ())
    let get st = (* .. as in Make *)
end : S with type k = k and type t = t)

which would get rid of both the Make functor and the Input signature.

[bclement-ocp]

This one seems unused?

[Stevendeo]

It is used in set and, while there is no option setting on_update yet, it will be useful for other options (like the steps limit that has to check a few things before setting the option).

[bclement-ocp]

I am not sure how a function with type k -> unit can be very meaningfully used to perform checks. Is the idea to have it raise an exception? I worry this would start to make the control flow for setting options quite a bit more convoluted than it needs to be.

[Stevendeo]

I am worried that the silent fall-back to the Options module could lead to some surprising behavior if we ever use this for options that incorporate mutable state

I am not sure what kind of behavior you are mentioning, do you have examples in mind?

[bclement-ocp]

I am not sure what kind of behavior you are mentioning, do you have examples in mind?

If the value returned by map is mutable (say a reference) then then each time get is called on a State that doesn't have the key a new reference is created from the value in Options, which is different from the behavior if the Staet does have the key (where the same reference would be returned).

[Stevendeo]

Okay I get your point, but I would really prefer to abstract the accesses to the Dolmen state regarding the options. By exporting the key, you would have to manually handle the options and initialize all the options on the Dolmen state, which is what I wanted to avoid because we may rely on Dolmen state for a lot of options in the future. I would rather add as a documentation of create_opt (which would have been better in a module sig) that the type t must not be mutable.

[bclement-ocp]

Besides issues with mutability there can be a performance concern if the option is accessed often (e.g. if map is doing some expensive computation). Instanciating a new SAT functor each time we call check-sat feels weird.

Maybe we could be storing the list of Dolmen options in a global reference (at module initialisation) and doing DolmenOptions.init st in the solving loop, where DolmenOptions.init iterates over the list? This way, the option will always be set on the Dolmen state without duplications. And if (when!) we get rid of the global Options module, DolmenOptions.init can take an additional argument which will be local to that function instead of being kept alive forever. What do you think of that option?

[Stevendeo]

Maybe we could be storing the list of Dolmen options in a global reference (at module initialisation) and doing DolmenOptions.init st in the solving loop

That was my first plan actually, but I wanted to not initialize the dolmen state with options that were not used at all. I'm starting to think this map function was an error, as it complicates everything and is error prone for the only purpose of the sat option. I can use the on_update function (with a slight type change) to separate the two keys actually, I think it is a better design.

[Stevendeo]

Here's another solution: there is now a list of options (known at compile time) that must be initialized at the beginning. Also, this option cannot be set and depends on SatSolver to be updated.

[bclement-ocp]

If we have the list, why not just add to it automatically when create_opt is called and get rid of the fallback in get entirely?

[Stevendeo]

For two reasons:

• the list would not be known at compile time;
• I do not want all the options to be stored in the dolmen state.

Besides, I will need the on_update for a future option.

[bclement-ocp]

I don't understand what knowing the list at compile time brings, and I also don't understand why options shouldn't be stored on the dolmen state, I thought that was the whole point.

I am also not proposing to get rid of on_update.

[Stevendeo]

I don't understand what knowing the list at compile time brings

Not much, but it is one less reference in a codebase that has too many

I also don't understand why options shouldn't be stored on the dolmen state

Because we don't need to store most of them, they already are set somewhere else (in the Options module). When it is removed we can think about saving them somewhere else, but at the moment we just don't need to.

[bclement-ocp]

Ah but having all the options initialized will mean that options that depend on other options through on_update will be initialized twice. Urgh. OK, I am still not really convinced (and actually quite worried about us messing up using on_update now), but it's also probably not worth quibbling on about, so let's merge as is. We can always change the design if it turns out to become problematic, the surface is tiny.

[bclement-ocp]

I have already state I am ok merging as is but:

Not much, but it is one less reference in a codebase that has too many

I understand but I don't think that is very fair; a local reference that is only modified during module initialization is the tamest form of reference except perhaps for a reference inside a function! It is not the same as a reference being used a as a global variable and modified during execution.

Because we don't need to store most of them, they already are set somewhere else (in the Options module). When it is removed we can think about saving them somewhere else, but at the moment we just don't need to.

On the other hand, the reason I would want them even with the Options is that now if someone calls Option.set_XXX it will suddenly change the value of the option for all the existing Dolmen states implicitly. IOW, currently, the following behavior is possible and I don't think that's very clean or intuitive:

let pa = ProduceAssignments.get st in
Options.set_produce_assignment (not pa);
let pa' = ProduceAssignment.get st in
assert (pa <> pa') (* ?? *)

[Stevendeo]

I understand but I don't think that is very fair...

I'm not saying references are bad, I use references when I need to. Here it is just not the case, especially considering I did not plan on registering all the options in the dolmen state. If I did, as I told you, I would have initialized a list ref at module creation.

IOW, currently, the following behavior is possible and I don't think that's very clean or intuitive:

I clearly documented the behavior of the get function. What does seem not clean is the fact that it looks like a fully functional interface while it is not because it depends on some reference. The thing is, these references should not be updated by something else than the command line parser. It is not the case yet because all the options are not handled by the dolmen state, but it will be in a near future ( depending on the merge of such a PR ;) )

[bclement-ocp]

What does seem not clean is the fact that it looks like a fully functional interface while it is not because it depends on some reference.

I guess we agree here since this is exactly why I have been arguing in favor of actually making it a functional interface :)

The thing is, these references should not be updated by something else than the command line parser.

I don't think that is true in the library use case.