From 5ed0a1b8dd73e339189df1556fa4bdbf95767245 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 May 2018 21:27:53 -0500
Subject: [PATCH] Support HORN logic string (#1849)

---
 src/parser/smt1/smt1.cpp  | 1 +
 src/theory/logic_info.cpp | 8 ++++++++
 2 files changed, 9 insertions(+)

diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index c3365eb13..047373436 100644
--- 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 9fe3b713f..41d74b4a0 100644
--- 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();
-- 
2.30.2