From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 8 Oct 2018 23:28:30 +0000 (-0500)
Subject: Address slow sygus regressions (#2598)
X-Git-Tag: cvc5-1.0.0~4450
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bd5f6d16dc88624a1dbf463f5d080bdc5af50494;p=cvc5.git

Address slow sygus regressions (#2598)
---

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 19513ada3..a7b7532f1 100644
--- 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 5bd187e8f..523650926 100644
--- 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
index fc4d7e5be..000000000
--- 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 d8d4ff9bb..e6f43fc21 100644
--- 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
index 000000000..0acdcf25e
--- /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
+