From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 3 May 2018 02:27:53 +0000 (-0500)
Subject: Support HORN logic string (#1849)
X-Git-Tag: cvc5-1.0.0~5102
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5ed0a1b8dd73e339189df1556fa4bdbf95767245;p=cvc5.git

Support HORN logic string (#1849)
---

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();