literals in theory atoms

[jorgefandinno]

Would it be possible to extend theory atoms so literals can occur inside them, like in

&k{ not p(2,X) }

Thanks

[rkaminsk]

If it is simple enough to implement, I will put it in the next release.

Note that a theory will never know what a literal is. It just knows about terms. But it should be possible to extend the theory specification so that unary operators composed of letters are accepted; it will probably be limited to identifier syntax.