search

elliottt / easy-smt

Easy SMT solver interaction
Apache License 2.0
24 stars 4 forks source link

Deprecate `Context::declare` or `Context::declare_const` #15

Closed rachitnigam closed 1 year ago

rachitnigam commented 1 year ago

The Context has both a declare method, which dispatches to declare_fun, and a declare_const method, which uses the SMTLIB declare-const construct. However, declare-const in SMTLIB is defined to be a macro for define-fun in the same way that declare is implemented (See Z3 reference). Because of this, we should probably only expose one of these methods on the context and deprecate the other.

fitzgen commented 1 year ago

After digging in some more, I now realize that Context::declare doesn't directly correspond to any SMTLIB form, while Context::declare_const corresponds to the SMTLIB declare-const. Since Context::declare and Context::declare_const are the same, as you pointed out, I think it makes sense to remove/deprecate Context::declare and only keep Context::declare_const.

Would you like to send a PR doing the above?

Thanks for filing this issue.

rachitnigam commented 1 year ago

Sure, I can do that!