Support HORN logic string (#1849)

diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index c3365eb132bf88a2cc932a64f49a367e9af519c2..04737343690dda3bbdee19a7b694ca105080eda1 100644 (file)
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -61,6 +61,7 @@ std::unordered_map<std::string, Smt1::Logic> Smt1::newLogicMap() {
   logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED;
   logicMap["QF_ALL"] = QF_ALL_SUPPORTED;
   logicMap["ALL"] = ALL_SUPPORTED;
+  logicMap["HORN"] = ALL_SUPPORTED;
   return logicMap;
 }
 

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 9fe3b713f027a0df75543262dd7438ebd4a4d602..41d74b4a0f79b358dbd0b6fbee749125bdc1a213 100644 (file)
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -377,6 +377,14 @@ void LogicInfo::setLogicString(std::string logicString)
     enableQuantifiers();
     arithNonLinear();
     p += 3;
+  }
+  else if (!strcmp(p, "HORN"))
+  {
+    // the HORN logic
+    enableEverything();
+    enableQuantifiers();
+    arithNonLinear();
+    p += 4;
   } else {
     if(!strncmp(p, "QF_", 3)) {
       disableQuantifiers();