Sygus logics (#1226)

* Allow any smt2 logic to be a sygus logic. Add non-linear SyGuS regressions.

* Minor

* Add case for reals, comment.

* Fix regress1.

1 files changed, 16 insertions, 22 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a186c052e..bc9f2a06f 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -365,30 +365,13 @@ void Smt2::resetAssertions() {
 }
 
 void Smt2::setLogic(std::string name) {
+
   if(sygus()) {
-    // sygus by default requires UF, datatypes, and LIA
+    // non-smt2-standard sygus logic names go here (http://sygus.seas.upenn.edu/files/sygus.pdf Section 3.2)
     if(name == "Arrays") {
-      name = "AUFDTLIA";
-    } else if(name == "Reals") {
-      name = "UFDTLIRA";
-    } else if(name == "LIA") {
-      name = "UFDTLIA";
-    } else if(name == "LRA") {
-      name = "UFDTLIRA";
-    } else if(name == "LIRA") {
-      name = "UFDTLIRA";
-    } else if(name == "BV") {
-      name = "UFDTBVLIA";
-    } else if(name == "SLIA") {
-      name = "UFDTSLIA";
-    } else if(name == "SAT") {
-      name = "UFDTLIA";
-    } else if(name == "ALL" || name == "ALL_SUPPORTED") {
-      //no change
-    } else {
-      std::stringstream ss;
-      ss << "Unknown SyGuS background logic `" << name << "'";
-      parseError(ss.str());
+      name = "A";
+    }else if(name == "Reals") {
+      name = "LRA";
     }
   }
 
@@ -398,6 +381,17 @@ void Smt2::setLogic(std::string name) {
   } else {
     d_logic = name;
   }
+  
+  // if sygus is enabled, we must enable UF, datatypes and integer arithmetic
+  if(sygus()) {
+    // get unlocked copy, modify, copy and relock
+    LogicInfo log(d_logic.getUnlockedCopy());
+    log.enableTheory(theory::THEORY_UF);
+    log.enableTheory(theory::THEORY_DATATYPES);
+    log.enableIntegers();
+    d_logic = log;
+    d_logic.lock();
+  }
 
   // Core theory belongs to every logic
   addTheory(THEORY_CORE);