diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-06-11 18:29:19 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-11 21:29:19 +0000 |
| commit | 8ddd5e82c8e896977d5573b639524264c7207d85 (patch) | |
| tree | ee6a94468288397e290cb3db60db76dbdf69e978 /src/theory/logic_info.h | |
| parent | f10087c3b347da6ef625a2ad92846551ad324d73 (diff) | |
Better support for HOL parsing and set up (#6697)
This commit adds a new parser option, --hol, which marks that HOL is being used. This option has the effect of prepending the problem's logic with "HO_", which teels the solver that the logic is higher order. The parser builder, base parser, and SMT2 and TPTP parsers are all updated to work with this new setting, as is the logic info class.
For now this parser option is enabling the --uf-ho option for internal use, since for now higher-order solving relies it. In a future PR this dependency will be removed (since this information is already given to the SMT solver via the logic).
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 |