The problem is that the compiler reacts with the error message "Invalid argument type 'Formula' to unary expression" for the return statements in AndFormula's and OrFormula's operator! functions. It doesn't seem logical to me since the base class is abstract and thus cannot be instantiated, so each Formula is either an AndFormula or an OrFormula, and the recursion means that negating a Formula should always eventually land in the base case, which is the negation of a VariableFormula. Why is this happening? How can I fix it?
You're right. But it causes problems for me with this setup. I cannot define a Formula-type !operator function in Formula because I cannot return a Formula (cannot be instantiated because it's an abstract type). The fact that each subclass has a different return type for the (same) operator! function means that in C++ they're not true subclasses to Formula. So taking away the abstractness of the base class is not enough.
UPDATE: Actually, I take it back, the solution I thought I had is not a complete solution. The inverse (!) of formulas just returns a bool and not the actual inverse of the formula. JLBorges's solution is so far the only one I've found to work. The only downside to this solution is that it dynamically allocates the actual formulas, but I don't know how to solve it otherwise.
I've finally got a working solution. It's inspired by JLBorges answer, but doesn't use a pointer/reference variable in the abstract class. Instead, in the base class I defined and implemented the bool not and general operators and && and || operators for generating AndFormulas and OrFormulas and then used these two operators in the isTrue functions for these two types of Formula's to make the comparisons. I even managed to keep the abstractness of the base class.