diff options
Diffstat (limited to 'src/theory/logic_info.h')
| -rw-r--r-- | src/theory/logic_info.h | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index 107093a5c..c6aa71ad0 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -120,7 +120,11 @@ public: /** Is this a quantified logic? */ bool isQuantified() const; - /** Is this the all-inclusive logic? */ + /** Is this a logic that includes the all-inclusive logic? + * + * @return Yields true if the logic corresponds to "ALL" or its super + * set including , such as "HO_ALL". + */ bool hasEverything() const; /** Is this the all-exclusive logic? (Here, that means propositional logic) */ @@ -168,8 +172,11 @@ public: /** * Enable all functionality. All theories, plus quantifiers, will be * enabled. + * + * @param enableHigherOrder Whether HOL should be enable together with the + * above. */ - void enableEverything(); + void enableEverything(bool enableHigherOrder = false); /** * Disable all functionality. The result will be a LogicInfo with |