From ebd9c958a0c20e37cc0e1a79be26afd525dd8fb9 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 12 Oct 2017 13:00:12 -0500
Subject: [PATCH] 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.
---
 src/parser/smt2/smt2.cpp                      | 38 ++++++++-----------
 test/regress/regress0/sygus/Makefile.am       |  3 +-
 .../regress0/sygus/nia-max-square-ns.sy       | 13 +++++++
 test/regress/regress1/sygus/Makefile.am       |  3 +-
 test/regress/regress1/sygus/nia-max-square.sy | 21 ++++++++++
 5 files changed, 54 insertions(+), 24 deletions(-)
 create mode 100644 test/regress/regress0/sygus/nia-max-square-ns.sy
 create mode 100644 test/regress/regress1/sygus/nia-max-square.sy

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);
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am
index d8f675af1..a297cee81 100644
--- a/test/regress/regress0/sygus/Makefile.am
+++ b/test/regress/regress0/sygus/Makefile.am
@@ -64,7 +64,8 @@ TESTS = commutative.sy \
         cggmp.sy \
         parse-bv-let.sy \
         cegar1.sy \
-        triv-type-mismatch-si.sy
+        triv-type-mismatch-si.sy \
+        nia-max-square-ns.sy
 
 
 # sygus tests currently taking too long for make regress
diff --git a/test/regress/regress0/sygus/nia-max-square-ns.sy b/test/regress/regress0/sygus/nia-max-square-ns.sy
new file mode 100644
index 000000000..96baab7fe
--- /dev/null
+++ b/test/regress/regress0/sygus/nia-max-square-ns.sy
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth --nl-ext-tplanes
+(set-logic NIA)
+
+(synth-fun max ((x Int) (y Int)) Int)
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (>= (max x y) (* x x)))
+(constraint (>= (max x y) (* y y)))
+
+(check-synth)
diff --git a/test/regress/regress1/sygus/Makefile.am b/test/regress/regress1/sygus/Makefile.am
index f1f1c1342..ed8755236 100644
--- a/test/regress/regress1/sygus/Makefile.am
+++ b/test/regress/regress1/sygus/Makefile.am
@@ -25,7 +25,8 @@ TESTS =	\
 	inv_gen_n_c11.sy \
 	unbdd_inv_gen_ex7.sy \
 	icfp_easy_mt_ite.sy \
-  three.sy
+	three.sy \
+	nia-max-square.sy
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress1/sygus/nia-max-square.sy b/test/regress/regress1/sygus/nia-max-square.sy
new file mode 100644
index 000000000..5858af98a
--- /dev/null
+++ b/test/regress/regress1/sygus/nia-max-square.sy
@@ -0,0 +1,21 @@
+; EXPECT: unsat
+; COMMAND-LINE: --no-dump-synth --nl-ext-tplanes
+(set-logic NIA)
+
+(synth-fun max ((x Int) (y Int)) Int
+  ((Start Int (0 1 x y
+               (+ Start Start)
+               (- Start Start)
+               (* Start Start)
+               (ite StartBool Start Start)))
+   (StartBool Bool ((and StartBool StartBool)
+                    (not StartBool)
+                    (<= Start Start)))))
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (>= (max x y) (* x x)))
+(constraint (>= (max x y) (* y y)))
+
+(check-synth)
-- 
2.30.2