Address slow sygus regressions (#2598)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 19513ada33b5f68e4eff8fb9f9c03d1aea577372..a7b7532f10112e04264ead2488546b2ea8fabea9 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1727,7 +1727,6 @@ set(regress_2_tests
   regress2/sygus/process-10-vars-2fun.sy
   regress2/sygus/process-arg-invariance.sy
   regress2/sygus/real-grammar-neg.sy
-  regress2/sygus/sixfuncs.sy
   regress2/sygus/three.sy
   regress2/sygus/vcb.sy
   regress2/typed_v1l50016-simp.cvc
@@ -1752,6 +1751,7 @@ set(regress_3_tests
   regress3/issue2429.smt2
   regress3/pp-regfile.smt
   regress3/qwh.35.405.shuffled-as.sat03-1651.smt
+  regress3/sixfuncs.sy
 )
 
 #-----------------------------------------------------------------------------#

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 5bd187e8fe3ab3888ae9d4d404212ec1117aa906..5236509262270d7de5dd016f33d906ba334b9c8d 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1720,7 +1720,6 @@ REG2_TESTS = \
        regress2/sygus/process-10-vars-2fun.sy \
        regress2/sygus/process-arg-invariance.sy \
        regress2/sygus/real-grammar-neg.sy \
-       regress2/sygus/sixfuncs.sy \
        regress2/sygus/three.sy \
        regress2/sygus/vcb.sy \
        regress2/typed_v1l50016-simp.cvc \
@@ -1740,7 +1739,8 @@ REG3_TESTS = \
        regress3/incorrect2.smt \
        regress3/issue2429.smt2 \
        regress3/pp-regfile.smt \
-       regress3/qwh.35.405.shuffled-as.sat03-1651.smt
+       regress3/qwh.35.405.shuffled-as.sat03-1651.smt \
+       regress3/sixfuncs.sy
 
 REG4_TESTS = \
        regress4/C880mul.miter.shuffled-as.sat03-348.smt \

diff --git a/test/regress/regress2/sygus/sixfuncs.sy b/test/regress/regress2/sygus/sixfuncs.sy
deleted file mode 100644 (file)
index fc4d7e5..0000000
--- a/test/regress/regress2/sygus/sixfuncs.sy
+++ /dev/null
@@ -1,83 +0,0 @@
-; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
-(set-logic LIA)
-
-(synth-fun f1 ((p1 Int) (P1 Int)) Int
-          ((Start Int (
-                       p1
-                       P1
-                       (- Start Start)
-                       (+ Start Start)
-                     )
-           )))
-
-(synth-fun f2 ((p1 Int) (P1 Int)) Int
-          ((Start Int (
-                       p1
-                       P1
-                       (+ Start Start)
-                     )
-           )))
-
-(synth-fun f3 ((p1 Int) (P1 Int)) Int
-          ((Start Int (
-                       p1
-                       P1
-                       (- Start Start)
-                       (+ Start Start)
-                     )
-           )))
-
-(synth-fun f4 ((p1 Int) (P1 Int)) Int
-          ((Start Int (
-                       p1
-                       P1
-                       (- Start Start)
-                       (+ Start Start)
-                     )
-           )))
-
-(synth-fun f5 ((p1 Int) (P1 Int)) Int
-          ((Start Int (
-                       p1
-                       P1
-                       (- Start Start)
-                       (+ Start Start)
-                     )
-           )))
-
-(synth-fun g1 ((p1 Int) (P1 Int)) Int
-          ((Start Int (
-                       p1
-                       P1
-                       (- Start Start)
-                       (+ Start Start)
-                     )
-           )))
-
-
-(declare-var x Int)
-(declare-var y Int)
-
-(constraint (= (+ (f1 x y) (f1 x y)) (f2 x y)))
-(constraint (= (- (+ (f1 x y) (f2 x y)) y) (f3 x y)))
-(constraint (= (+ (f2 x y) (f2 x y)) (f4 x y))) 
-(constraint (= (+ (f4 x y) (f1 x y)) (f5 x y))) 
-
-(constraint (= (- (f1 x y) y) (g1 x y)))
-
-
-(check-synth)
-
-;; possible solution
-;; f1: y+x+1
-;; f2: y+2x+2
-;; f3: y+3x+3
-;; f4: 4y+4x+4
-;; f5: 5y+5x+5
-;; g1: x+1
-;; g2: y+2
-;; g3: y+3
-;; g4: 2y+6
-;; g5: 3y+x+7
-

diff --git a/test/regress/regress2/sygus/vcb.sy b/test/regress/regress2/sygus/vcb.sy
index d8d4ff9bb7d3d4a19bdf9791182d638c1cf53fc8..e6f43fc21b045beb13688b4ef782727786773e5a 100644 (file)
--- a/test/regress/regress2/sygus/vcb.sy
+++ b/test/regress/regress2/sygus/vcb.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --no-sygus-repair-const
+; COMMAND-LINE: --sygus-out=status --no-sygus-repair-const --decision=justification
 (set-logic LIA)
 
 (synth-fun f1 ((x1 Int) (x2 Int)) Int)

diff --git a/test/regress/regress3/sixfuncs.sy b/test/regress/regress3/sixfuncs.sy
new file mode 100644 (file)
index 0000000..0acdcf2
--- /dev/null
+++ b/test/regress/regress3/sixfuncs.sy
@@ -0,0 +1,83 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --decision=justification
+(set-logic LIA)
+
+(synth-fun f1 ((p1 Int) (P1 Int)) Int
+          ((Start Int (
+                       p1
+                       P1
+                       (- Start Start)
+                       (+ Start Start)
+                     )
+           )))
+
+(synth-fun f2 ((p1 Int) (P1 Int)) Int
+          ((Start Int (
+                       p1
+                       P1
+                       (+ Start Start)
+                     )
+           )))
+
+(synth-fun f3 ((p1 Int) (P1 Int)) Int
+          ((Start Int (
+                       p1
+                       P1
+                       (- Start Start)
+                       (+ Start Start)
+                     )
+           )))
+
+(synth-fun f4 ((p1 Int) (P1 Int)) Int
+          ((Start Int (
+                       p1
+                       P1
+                       (- Start Start)
+                       (+ Start Start)
+                     )
+           )))
+
+(synth-fun f5 ((p1 Int) (P1 Int)) Int
+          ((Start Int (
+                       p1
+                       P1
+                       (- Start Start)
+                       (+ Start Start)
+                     )
+           )))
+
+(synth-fun g1 ((p1 Int) (P1 Int)) Int
+          ((Start Int (
+                       p1
+                       P1
+                       (- Start Start)
+                       (+ Start Start)
+                     )
+           )))
+
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (+ (f1 x y) (f1 x y)) (f2 x y)))
+(constraint (= (- (+ (f1 x y) (f2 x y)) y) (f3 x y)))
+(constraint (= (+ (f2 x y) (f2 x y)) (f4 x y))) 
+(constraint (= (+ (f4 x y) (f1 x y)) (f5 x y))) 
+
+(constraint (= (- (f1 x y) y) (g1 x y)))
+
+
+(check-synth)
+
+;; possible solution
+;; f1: y+x+1
+;; f2: y+2x+2
+;; f3: y+3x+3
+;; f4: 4y+4x+4
+;; f5: 5y+5x+5
+;; g1: x+1
+;; g2: y+2
+;; g3: y+3
+;; g4: 2y+6
+;; g5: 3y+x+7
+