sygusComp2018: add regressions (#2191)

9 files changed, 311 insertions, 1 deletions

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index aa896258f..cef27bc72 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -814,6 +814,7 @@ REG0_TESTS = \
 	regress0/strings/type001.smt2 \
 	regress0/strings/unsound-0908.smt2 \
 	regress0/sygus/General_plus10.sy \
+	regress0/sygus/aig-si.sy \
 	regress0/sygus/c100.sy \
 	regress0/sygus/ccp16.lus.sy \
 	regress0/sygus/check-generic-red.sy \
@@ -1502,6 +1503,8 @@ REG1_TESTS = \
 	regress1/sygus/constant.sy \
 	regress1/sygus/constant-ite-bv.sy \
 	regress1/sygus/crci-ssb-unk.sy \
+	regress1/sygus/crcy-si-rcons.sy \
+	regress1/sygus/crcy-si.sy \
 	regress1/sygus/dt-test-ns.sy \
 	regress1/sygus/dup-op.sy \
 	regress1/sygus/fg_polynomial3.sy \
@@ -1526,6 +1529,7 @@ REG1_TESTS = \
 	regress1/sygus/nia-max-square-ns.sy \
 	regress1/sygus/no-flat-simp.sy \
 	regress1/sygus/no-mention.sy \
+	regress1/sygus/parity-si-rcons.sy \
 	regress1/sygus/pbe_multi.sy \
 	regress1/sygus/planning-unif.sy \
 	regress1/sygus/process-10-vars.sy \
@@ -1541,6 +1545,8 @@ REG1_TESTS = \
 	regress1/sygus/strings-trivial-two-type.sy \
 	regress1/sygus/strings-trivial.sy \
 	regress1/sygus/sygus-dt.sy \
+	regress1/sygus/sygus-uf-ex.sy \
+	regress1/sygus/t8.sy \
 	regress1/sygus/tl-type-0.sy \
 	regress1/sygus/tl-type-4x.sy \
 	regress1/sygus/tl-type.sy \
@@ -1549,6 +1555,7 @@ REG1_TESTS = \
 	regress1/sygus/twolets2-orig.sy \
 	regress1/sygus/unbdd_inv_gen_ex7.sy \
 	regress1/sygus/unbdd_inv_gen_winf1.sy \
+	regress1/sygus/univ_2-long-repeat.sy \
 	regress1/sym/sym1.smt2 \
 	regress1/sym/sym2.smt2 \
 	regress1/sym/sym3.smt2 \
diff --git a/test/regress/regress0/sygus/aig-si.sy b/test/regress/regress0/sygus/aig-si.sy
new file mode 100644
index 000000000..ef12e3c0e
--- /dev/null
+++ b/test/regress/regress0/sygus/aig-si.sy
@@ -0,0 +1,30 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi --cbqi-prereg-inst --sygus-out=status
+(set-logic BV)
+
+(define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+  (xor (not (xor a b)) (not (xor c d))))
+
+(synth-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+           ((Start Bool ((and Start Start) (not Start) a b c d))))
+
+(declare-var a Bool)
+(declare-var b Bool)
+(declare-var c Bool)
+(declare-var d Bool)
+
+(constraint
+ (= (parity a b c d) 
+    (and (AIG a b c d)
+        (not (and (and (not (and a b)) (not (and (not a) (not b))))
+               (and (not (and (not c) (not d))) (not (and c d))))))))
+
+
+(check-synth)
+
+; Solution:
+;(define-fun AIG ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+;(not
+;  (and
+;   (and (not (and (not a) b)) (not (and d (not c))))
+;   (and (not (and (not b) a)) (not (and (not d) c)))))) 
diff --git a/test/regress/regress1/sygus/crcy-si-rcons.sy b/test/regress/regress1/sygus/crcy-si-rcons.sy
new file mode 100644
index 000000000..6e2f54c31
--- /dev/null
+++ b/test/regress/regress1/sygus/crcy-si-rcons.sy
@@ -0,0 +1,78 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=all --cegqi-si-abort --decision=internal --cegqi-si-rcons=try --sygus-out=status
+
+(set-logic BV)
+
+
+(define-fun origCir ( (LN24 Bool) (k3 Bool) (LN129 Bool) (LN141 Bool)  )  Bool    
+          (not (not (not (xor (not (xor (not (and  LN24 k3 ) ) LN129 ) ) LN141 ) ) ) )
+)
+
+
+(synth-fun skel ( (LN24 Bool) (k3 Bool) (LN129 Bool) (LN141 Bool)  )  Bool    
+          ((Start Bool (
+		                                  (and depth1 depth1)
+		                                  (not depth1)
+		                                  (or depth1 depth1)
+		                                  (xor depth1 depth1)
+          ))
+          (depth1 Bool (
+		                                  (and depth2 depth2)
+		                                  (not depth2)
+		                                  (or depth2 depth2)
+		                                  (xor depth2 depth2)
+          ))
+          (depth2 Bool (
+		                                  (and depth3 depth3)
+		                                  (not depth3)
+		                                  (or depth3 depth3)
+		                                  (xor depth3 depth3)
+          ))
+          (depth3 Bool (
+		                                  (and depth4 depth4)
+		                                  (not depth4)
+		                                  (or depth4 depth4)
+		                                  (xor depth4 depth4)
+          ))
+          (depth4 Bool (
+		                                  (and depth5 depth5)
+		                                  (not depth5)
+		                                  (or depth5 depth5)
+		                                  (xor depth5 depth5)
+		                                  LN141
+          ))
+          (depth5 Bool (
+		                                  (and depth6 depth6)
+		                                  (not depth6)
+		                                  (or depth6 depth6)
+		                                  (xor depth6 depth6)
+          ))
+          (depth6 Bool (
+		                                  (and depth7 depth7)
+		                                  (not depth7)
+		                                  (or depth7 depth7)
+		                                  (xor depth7 depth7)
+		                                  LN129
+          ))
+          (depth7 Bool (
+		                                  (and depth8 depth8)
+		                                  (not depth8)
+		                                  (or depth8 depth8)
+		                                  (xor depth8 depth8)
+		                                  LN24
+          ))
+          (depth8 Bool (
+		                                  k3
+          )))
+)
+
+
+(declare-var LN24 Bool)
+(declare-var k3 Bool)
+(declare-var LN129 Bool)
+(declare-var LN141 Bool)
+
+(constraint (= (origCir LN24 k3 LN129 LN141 ) (skel LN24 k3 LN129 LN141 )))
+
+
+(check-synth)
diff --git a/test/regress/regress1/sygus/crcy-si.sy b/test/regress/regress1/sygus/crcy-si.sy
new file mode 100644
index 000000000..46500ee4d
--- /dev/null
+++ b/test/regress/regress1/sygus/crcy-si.sy
@@ -0,0 +1,21 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic BV)
+
+(define-fun Spec ((k1 Bool) (k2 Bool) (k3 Bool) ) Bool
+  (xor k1 (and k3 (not k2)))
+)
+ 
+(synth-fun Imp ((k1 Bool) (k2 Bool) (k3 Bool)) Bool
+ ((Start Bool ( (and d1 d1) (or d1 d1) (xor d1 d1) (not d1) ) )
+ (d1 Bool ( (and d2 d2) (or d2 d2) (xor d2 d2) (not d2) ) )
+ (d2 Bool ( k1 k2 k3) ) )
+)
+ 
+(declare-var k1 Bool)
+(declare-var k2 Bool)
+(declare-var k3 Bool)
+
+(constraint (= (Spec k1 k2 k3) (Imp k1 k2 k3)))
+(check-synth)
diff --git a/test/regress/regress1/sygus/parity-si-rcons.sy b/test/regress/regress1/sygus/parity-si-rcons.sy
new file mode 100644
index 000000000..a836c9726
--- /dev/null
+++ b/test/regress/regress1/sygus/parity-si-rcons.sy
@@ -0,0 +1,36 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi-prereg-inst --cegqi-si-rcons=try --sygus-out=status
+
+(set-logic BV)
+
+(define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+  (xor (not (xor a b)) (not (xor c d))))
+
+(synth-fun NAND ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+ ((Start Bool ((not StartAnd) Vars Constants))
+  (StartAnd Bool ((and Start Start)))
+  (Vars Bool (a b c d))
+  (Constants Bool (true false))))
+
+(declare-var a Bool)
+(declare-var b Bool)
+(declare-var c Bool)
+(declare-var d Bool)
+
+(constraint
+ (= (parity a b c d) 
+    (not (and (NAND a b c d)
+              (not
+               (and
+                (not (and (not (and d (not (and d a)))) (not (and a (not (and d a))))))
+                (not (and (not (and (not (and true c)) (not (and true b)))) (not (and b c))))))))))
+
+
+(check-synth)
+
+; Solution:
+;(define-fun NAND ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
+;(not
+;  (and
+;   (not (and (not (and (not (and c true)) b)) (not (and (not (and b c)) c))))
+;   (not (and (not (and a d)) (not (and (not (and a true)) (not (and true d)))))))))
diff --git a/test/regress/regress1/sygus/sygus-uf-ex.sy b/test/regress/regress1/sygus/sygus-uf-ex.sy
new file mode 100644
index 000000000..b9731de0f
--- /dev/null
+++ b/test/regress/regress1/sygus/sygus-uf-ex.sy
@@ -0,0 +1,18 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic LIA)
+(declare-fun uf ( Int ) Int)
+(synth-fun f ((x Int) (y Int)) Bool
+((Start Bool (true false
+  (<= IntExpr IntExpr )
+  (= IntExpr IntExpr )
+  (and Start Start )
+  (or Start Start )
+  (not Start )))
+(IntExpr Int (0 1 x y
+  (+ IntExpr IntExpr )
+  (- IntExpr IntExpr )))))
+(declare-var x Int)
+(constraint (f (uf x) (uf x)))
+(constraint (not (f 3 4)))
+(check-synth)
diff --git a/test/regress/regress1/sygus/t8.sy b/test/regress/regress1/sygus/t8.sy
new file mode 100644
index 000000000..4dd726875
--- /dev/null
+++ b/test/regress/regress1/sygus/t8.sy
@@ -0,0 +1,31 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic  LIA)
+(
+synth-fun f_143-17-143-55 ( (x2 Int) (x1 Int) (parentNode Int) (EMPTY_PARENT Int)) Bool
+	((Start Bool (
+(< IntExpr IntExpr)
+(and Start Start)
+(= IntExpr IntExpr)
+(not Start )
+(<= IntExpr IntExpr)
+(or Start Start)
+
+
+
+))
+(IntExpr Int (
+x2 x1 parentNode EMPTY_PARENT 
+0 1
+))
+
+	)
+)
+(declare-var x2_143-17-143-55 Int)
+(declare-var x1_143-17-143-55 Int)
+(declare-var parentNode_143-17-143-55 Int)
+(declare-var EMPTY_PARENT_143-17-143-55 Int)
+
+(constraint  (=>  (and (= parentNode_143-17-143-55 0)  (and (= EMPTY_PARENT_143-17-143-55 -1)  (and (= x2_143-17-143-55 1) (= x1_143-17-143-55 1)) ) )  (= (f_143-17-143-55 x2_143-17-143-55 x1_143-17-143-55 parentNode_143-17-143-55 EMPTY_PARENT_143-17-143-55 ) true)))
+
+(check-synth)
diff --git a/test/regress/regress1/sygus/univ_2-long-repeat.sy b/test/regress/regress1/sygus/univ_2-long-repeat.sy
new file mode 100644
index 000000000..ac9493b2d
--- /dev/null
+++ b/test/regress/regress1/sygus/univ_2-long-repeat.sy
@@ -0,0 +1,89 @@
+; EXPECT: unsat

+; COMMAND-LINE: --sygus-fair=direct --sygus-out=status

+(set-logic SLIA)

+ 

+(synth-fun f ((col1 String) (col2 String)) String

+    ((Start String (ntString))

+     (ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY"

+                       (str.++ ntString ntString)

+                       (str.replace ntString ntString ntString)

+                       (str.at ntString ntInt)

+                       (int.to.str ntInt)

+                       (ite ntBool ntString ntString)

+                       (str.substr ntString ntInt ntInt)))

+      (ntInt Int (0 1 2

+                  (+ ntInt ntInt)

+                  (- ntInt ntInt)

+                  (str.len ntString)

+                  (str.to.int ntString)

+                  (str.indexof ntString ntString ntInt)))

+      (ntBool Bool (true false

+                    (str.prefixof ntString ntString)

+                    (str.suffixof ntString ntString)

+                    (str.contains ntString ntString)))))

+

+

+(declare-var col1 String)

+(declare-var col2 String)

+(constraint (= (f "UC Berkeley" "Berkeley, CA") 

+                  "UC Berkeley, Berkeley, CA, USA"))

+(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA") 

+                  "University of Pennsylvania, Phialdelphia, PA, USA"))

+(constraint (= (f "UCLA" "Los Angeles, CA") 

+                    "UCLA, Los Angeles, CA, USA"))

+(constraint (= (f "Cornell University" "Ithaca, New York, USA") 

+                  "Cornell University, Ithaca, New York, USA"))

+(constraint (= (f "Penn" "Philadelphia, PA, USA") 

+                  "Penn, Philadelphia, PA, USA"))

+(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA") 

+                  "University of Michigan, Ann Arbor, MI, USA"))

+(constraint (= (f "UC Berkeley" "Berkeley, CA") 

+                  "UC Berkeley, Berkeley, CA, USA"))

+(constraint (= (f "MIT" "Cambridge, MA") 

+                  "MIT, Cambridge, MA, USA"))

+(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA") 

+                  "University of Pennsylvania, Phialdelphia, PA, USA"))

+(constraint (= (f "UCLA" "Los Angeles, CA") 

+                    "UCLA, Los Angeles, CA, USA"))                  

+(constraint (= (f "University of Maryland College Park" "College Park, MD")   

+                  "University of Maryland College Park, College Park, MD, USA"))

+(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA") 

+                  "University of Michigan, Ann Arbor, MI, USA"))

+(constraint (= (f "UC Berkeley" "Berkeley, CA") 

+                  "UC Berkeley, Berkeley, CA, USA"))

+(constraint (= (f "MIT" "Cambridge, MA") 

+                  "MIT, Cambridge, MA, USA"))

+(constraint (= (f "Rice University" "Houston, TX") 

+                  "Rice University, Houston, TX, USA"))

+(constraint (= (f "Yale University" "New Haven, CT, USA") 

+                  "Yale University, New Haven, CT, USA"))

+(constraint (= (f "Columbia University" "New York, NY, USA") 

+                  "Columbia University, New York, NY, USA"))

+(constraint (= (f "NYU" "New York, New York, USA") 

+                  "NYU, New York, New York, USA"))

+(constraint (= (f "Drexel University" "Philadelphia, PA") 

+                  "Drexel University, Philadelphia, PA, USA"))                  

+(constraint (= (f "UC Berkeley" "Berkeley, CA") 

+                  "UC Berkeley, Berkeley, CA, USA"))

+(constraint (= (f "UIUC" "Urbana, IL") 

+                  "UIUC, Urbana, IL, USA"))

+(constraint (= (f "Temple University" "Philadelphia, PA") 

+                  "Temple University, Philadelphia, PA, USA"))

+(constraint (= (f "Harvard University" "Cambridge, MA, USA") 

+                  "Harvard University, Cambridge, MA, USA"))

+(constraint (= (f "University of Connecticut" "Storrs, CT, USA") 

+                  "University of Connecticut, Storrs, CT, USA"))

+(constraint (= (f "Drexel University" "Philadelphia, PA") 

+                  "Drexel University, Philadelphia, PA, USA"))

+(constraint (= (f "NYU" "New York, New York, USA") 

+                  "NYU, New York, New York, USA"))  

+(constraint (= (f "UIUC" "Urbana, IL") 

+                  "UIUC, Urbana, IL, USA"))                                  

+(constraint (= (f "New Haven University" "New Haven, CT, USA") 

+                  "New Haven University, New Haven, CT, USA"))

+(constraint (= (f "University of California, Santa Barbara" "Santa Barbara, CA, USA") 

+                  "University of California, Santa Barbara, Santa Barbara, CA, USA"))

+(constraint (= (f "University of Connecticut" "Storrs, CT, USA") 

+                  "University of Connecticut, Storrs, CT, USA"))                  

+ 

+(check-synth)

diff --git a/test/regress/regress2/sygus/process-10-vars-2fun.sy b/test/regress/regress2/sygus/process-10-vars-2fun.sy
index 00340030f..a107fd88b 100644
--- a/test/regress/regress2/sygus/process-10-vars-2fun.sy
+++ b/test/regress/regress2/sygus/process-10-vars-2fun.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status --no-sygus-repair-const
 ; EXPECT: unsat
 (set-logic LIA)