the method responsible for making various calls to the underlying
decision procedure with different Constraints
Parameters: lightWeight - true iff only quantifier free formulas shall beconsidered.
Invokes the actual decision procedure. This method is responsible for
translating to the syntax of the external tool, as well as passing this
as input to the tool and capturing its.