design clean API for theories

Gbury / mSAT

A modular sat/smt solver with proof output.

https://gbury.github.io/mSAT/

Apache License 2.0

97 stars 8 forks source link

design clean API for theories #13

Closed c-cube closed 5 years ago

c-cube commented 6 years ago

instead of exposing dirty St:

simplify the internals by removing Solver_types.mli
have a submodule for each type in Solver_types.ml
expose only a carefully chosen part of each module outside of Msat

Gbury commented 6 years ago

Good idea, but I have at least one case where I manually instantiate all the functors so that I can use functions from St when defining the theory, which is useful. More precisely, using add_atom and peeking at the is_true/neg.is_true fields allows the theory to fetch the current truth value of a literal without having to maintain a separate backtrackable truth table.

c-cube commented 5 years ago

fixed in #11