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, 49 insertions, 27 deletions

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index ecebd27c9..05f8c7a9f 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -39,7 +39,7 @@ LogicInfo::LogicInfo()
       d_linear(false),
       d_differenceLogic(false),
       d_cardinalityConstraints(false),
-      d_higherOrder(true),
+      d_higherOrder(false),
       d_locked(false)
 {
   for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id)
@@ -117,13 +117,25 @@ bool LogicInfo::isHigherOrder() const
   return d_higherOrder;
 }
 
-/** Is this the all-inclusive logic? */
-bool LogicInfo::hasEverything() const {
-  PrettyCheckArgument(d_locked, *this,
+bool LogicInfo::hasEverything() const
+{
+  PrettyCheckArgument(d_locked,
+                      *this,
                       "This LogicInfo isn't locked yet, and cannot be queried");
-  LogicInfo everything;
-  everything.lock();
-  return *this == everything;
+  // A logic has everything if all theories are enabled as well as quantifiers
+  bool doesNotHaveEverything = !isQuantified();
+  for (TheoryId id = THEORY_FIRST; !doesNotHaveEverything && id < THEORY_LAST;
+       ++id)
+  {
+    // if not configured with symfpu, we allow THEORY_FP to be disabled and
+    // still *this to contain the ALL logic
+    if (!this->d_theories[id]
+        && (id != THEORY_FP || Configuration::isBuiltWithSymFPU()))
+    {
+      doesNotHaveEverything = true;
+    }
+  }
+  return !doesNotHaveEverything;
 }
 
 /** Is this the all-exclusive logic?  (Here, that means propositional logic) */
@@ -275,17 +287,22 @@ std::string LogicInfo::getLogicString() const {
     LogicInfo qf_all_supported;
     qf_all_supported.disableQuantifiers();
     qf_all_supported.lock();
-    if(hasEverything()) {
-      d_logicString = "ALL";
-    } else if(*this == qf_all_supported) {
-      d_logicString = "QF_ALL";
-    } else {
+    stringstream ss;
+    if (isHigherOrder())
+    {
+      ss << "HO_";
+    }
+    if (!isQuantified())
+    {
+      ss << "QF_";
+    }
+    if (*this == qf_all_supported || hasEverything())
+    {
+      ss << "ALL";
+    }
+    else
+    {
       size_t seen = 0; // make sure we support all the active theories
-
-      stringstream ss;
-      if(!isQuantified()) {
-        ss << "QF_";
-      }
       if (d_theories[THEORY_SEP])
       {
         ss << "SEP_";
@@ -309,7 +326,7 @@ std::string LogicInfo::getLogicString() const {
       if(d_theories[THEORY_FP]) {
         ss << "FP";
         ++seen;
-      } 
+      }
       if(d_theories[THEORY_DATATYPES]) {
         ss << "DT";
         ++seen;
@@ -350,9 +367,8 @@ std::string LogicInfo::getLogicString() const {
       if(seen == 0) {
         ss << "SAT";
       }
-
-      d_logicString = ss.str();
     }
+    d_logicString = ss.str();
   }
   return d_logicString;
 }
@@ -374,6 +390,11 @@ void LogicInfo::setLogicString(std::string logicString)
   enableTheory(THEORY_BOOL);
 
   const char* p = logicString.c_str();
+  if (!strncmp(p, "HO_", 3))
+  {
+    enableHigherOrder();
+    p += 3;
+  }
   if(*p == '\0') {
     // propositional logic only; we're done.
   } else if(!strcmp(p, "QF_SAT")) {
@@ -384,14 +405,14 @@ void LogicInfo::setLogicString(std::string logicString)
     enableQuantifiers();
     p += 3;
   } else if(!strcmp(p, "QF_ALL")) {
-    // the "all theories included" logic, no quantifiers
-    enableEverything();
+    // the "all theories included" logic, no quantifiers.
+    enableEverything(d_higherOrder);
     disableQuantifiers();
     arithNonLinear();
     p += 6;
   } else if(!strcmp(p, "ALL")) {
-    // the "all theories included" logic, with quantifiers
-    enableEverything();
+    // the "all theories included" logic, with quantifiers.
+    enableEverything(d_higherOrder);
     enableQuantifiers();
     arithNonLinear();
     p += 3;
@@ -399,7 +420,7 @@ void LogicInfo::setLogicString(std::string logicString)
   else if (!strcmp(p, "HORN"))
   {
     // the HORN logic
-    enableEverything();
+    enableEverything(d_higherOrder);
     enableQuantifiers();
     arithNonLinear();
     p += 4;
@@ -541,9 +562,11 @@ void LogicInfo::setLogicString(std::string logicString)
   d_logicString = logicString;
 }
 
-void LogicInfo::enableEverything() {
+void LogicInfo::enableEverything(bool enableHigherOrder)
+{
   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   *this = LogicInfo();
+  this->d_higherOrder = enableHigherOrder;
 }
 
 void LogicInfo::disableEverything() {
@@ -584,7 +607,6 @@ void LogicInfo::enableSygus()
   enableTheory(THEORY_UF);
   enableTheory(THEORY_DATATYPES);
   enableIntegers();
-  enableHigherOrder();
 }
 
 void LogicInfo::enableSeparationLogic()