Extend assertions to check for theory symbols

[nrueh]

Extend the assertions Contains and SupersetOf (and SubsetOf?) with an option to check for theory symbols:

This would include adding an argument check_theory: bool = False

And something like the following code in the respective holds_for function:

Contains

if self.__check_theory:
            return self.__symbol in model.symbols(shown=True, theory=True)
return model.contains(self.__symbol)

SupersetOf

return set(model.symbols(shown=True, theory=self.__check_theory)).issuperset(self.__symbols)

[daveraja]

+1 for this feature... but I think it would be really useful to generalise this feature request beyond being able to check theory atoms.

Sometimes you might want theory atoms but other times you might want to check all atoms and not just shown atoms. We also have some cases where we need to post-process the model and then perform the check on the post-processed facts. So something that could accommodate all these use-cases would be really useful.

Maybe this could be implemented with a wrapper around the model object that allows the user to override what action is performed for the different checks.