This PR implements very rudimentary support for is_relevant for the datatypes logic. This avoids enabling the datatype mutators on SMTLIB instances that do not use datatypes (e.g., pure QF_BV instances).
After reading SMTLIB 2.6 (2021-05-12), it doesn't appear that you can declare a datatype const/function without having the datatype sort "forward declared" (i.e., there are no built-in datatype sorts). This makes the relevancy check very easy, as you can "just" check for the use of declare-datatype and declare-datatypes (and you don't need to "look inside" const/function declarations).
This PR implements very rudimentary support for
is_relevantfor the datatypes logic. This avoids enabling the datatype mutators on SMTLIB instances that do not use datatypes (e.g., pure QF_BV instances).After reading SMTLIB 2.6 (2021-05-12), it doesn't appear that you can declare a datatype const/function without having the datatype sort "forward declared" (i.e., there are no built-in datatype sorts). This makes the relevancy check very easy, as you can "just" check for the use of
declare-datatypeanddeclare-datatypes(and you don't need to "look inside" const/function declarations).Signed-off-by: Andrew V. Jones andrewvaughanj@gmail.com