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.

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a186c052ec3531f841a93f5b3dacf5053fe5fb72..bc9f2a06f4cd0a6918b8e36222bf068ffa6eb128 100644 (file)
--- 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 d8f675af156ec936b91a19fa7fc18f268ff91753..a297cee815d75de960a1bf33b5f874e398ee0216 100644 (file)
--- 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 (file)
index 0000000..96baab7
--- /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 f1f1c134281c8dd64e4423c264759839e1887394..ed875523675665f2ed3a502f23ff0265cc213a4b 100644 (file)
--- 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 (file)
index 0000000..5858af9
--- /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)