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).

1 files changed, 13 insertions, 10 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 8add1c698..4b04c77b7 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -303,9 +303,10 @@ public:
   virtual api::Term getExpressionForName(const std::string& name);
 
   /**
-   * Returns the expression that name should be interpreted as, based on the current binding.
+   * Returns the expression that name should be interpreted as, based on the
+   * current binding.
    *
-   * This is the same as above but where the name has been type cast to t. 
+   * This is the same as above but where the name has been type cast to t.
    */
   virtual api::Term getExpressionForNameAndType(const std::string& name,
                                                 api::Sort t);
@@ -331,9 +332,9 @@ public:
    * This is a generalization of ExprManager::operatorToKind that also
    * handles variables whose types are "function-like", i.e. where
    * checkFunctionLike(fun) returns true.
-   * 
+   *
    * For examples of the latter, this function returns
-   *   APPLY_UF if fun has function type, 
+   *   APPLY_UF if fun has function type,
    *   APPLY_CONSTRUCTOR if fun has constructor type.
    */
   api::Kind getKindForFunction(api::Term fun);
@@ -379,7 +380,7 @@ public:
 
   /**
    * Checks whether the given expression is function-like, i.e.
-   * it expects arguments. This is checked by looking at the type 
+   * it expects arguments. This is checked by looking at the type
    * of fun. Examples of function types are function, constructor,
    * selector, tester.
    * @param fun the expression to check
@@ -443,11 +444,12 @@ public:
   std::vector<api::Term> bindBoundVars(const std::vector<std::string> names,
                                        const api::Sort& type);
 
-  /** Create a new variable definition (e.g., from a let binding). 
+  /** Create a new variable definition (e.g., from a let binding).
    * levelZero is set if the binding must be done at level 0.
    * If a symbol with name already exists,
    *  then if doOverload is true, we create overloaded operators.
-   *  else if doOverload is false, the existing expression is shadowed by the new expression.
+   *  else if doOverload is false, the existing expression is shadowed by the
+   * new expression.
    */
   void defineVar(const std::string& name,
                  const api::Term& val,
@@ -648,9 +650,10 @@ public:
   /** Is the symbol bound to a boolean variable? */
   bool isBoolean(const std::string& name);
 
-  /** Is fun a function (or function-like thing)? 
-  * Currently this means its type is either a function, constructor, tester, or selector.
-  */
+  /** Is fun a function (or function-like thing)?
+   * Currently this means its type is either a function, constructor, tester, or
+   * selector.
+   */
   bool isFunctionLike(api::Term fun);
 
   /** Is the symbol bound to a predicate? */