Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/post conditions. Dump synth by default in sygus, update regressions. Set better defaults for induction. Fix bug in related to IFF and EQUAL in sygus grammar.

26 files changed, 73 insertions, 73 deletions

diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy
index 5d8cd8752..56a30b210 100644
--- a/test/regress/regress0/sygus/array_search_2.sy
+++ b/test/regress/regress0/sygus/array_search_2.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)
diff --git a/test/regress/regress0/sygus/array_sum_2_5.sy b/test/regress/regress0/sygus/array_sum_2_5.sy
index 48b5c8a4d..f6c0320e2 100644
--- a/test/regress/regress0/sygus/array_sum_2_5.sy
+++ b/test/regress/regress0/sygus/array_sum_2_5.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start)    (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)
diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy
index 15567b0a8..46dbd2981 100644
--- a/test/regress/regress0/sygus/commutative.sy
+++ b/test/regress/regress0/sygus/commutative.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy
index 0d753bdf1..428cb2adc 100644
--- a/test/regress/regress0/sygus/const-var-test.sy
+++ b/test/regress/regress0/sygus/const-var-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy
index ddc12a6a9..0059f6947 100644
--- a/test/regress/regress0/sygus/constant.sy
+++ b/test/regress/regress0/sygus/constant.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy
index dbf415986..e5448d626 100644
--- a/test/regress/regress0/sygus/dup-op.sy
+++ b/test/regress/regress0/sygus/dup-op.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-cegqi-si
+; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Con Con) (+ Start Start) x))
diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy
index 52a72c07d..cd129385e 100644
--- a/test/regress/regress0/sygus/enum-test.sy
+++ b/test/regress/regress0/sygus/enum-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (define-sort D (Enum (a b)))
 (define-fun f ((x D)) Int (ite (= x D::a) 3 7))
diff --git a/test/regress/regress0/sygus/hd-01-d1-prog.sy b/test/regress/regress0/sygus/hd-01-d1-prog.sy
index a58bc2f64..2e6c6ef81 100644
--- a/test/regress/regress0/sygus/hd-01-d1-prog.sy
+++ b/test/regress/regress0/sygus/hd-01-d1-prog.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 
 (set-logic BV)
 
@@ -8,12 +8,12 @@
 (synth-fun f ((x (BitVec 32))) (BitVec 32)
     ((Start (BitVec 32) ((bvand Start Start)
                          (bvsub Start Start)
-						 (bvor Start Start)
-						 (bvadd Start Start)
-						 (bvxor Start Start)
+             (bvor Start Start)
+             (bvadd Start Start)
+             (bvxor Start Start)
                          x
-						 #x00000000
-						 #xFFFFFFFF
+             #x00000000
+             #xFFFFFFFF
                          #x00000001))))
 
 (declare-var x (BitVec 32))
diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy
index 6e1610337..b07be0e98 100644
--- a/test/regress/regress0/sygus/icfp_28_10.sy
+++ b/test/regress/regress0/sygus/icfp_28_10.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 
 (set-logic BV)
 
@@ -14,14 +14,14 @@
 
 (Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
                     (shl1 Start)
- 		    (shr1 Start)
-		    (shr4 Start)
-		    (shr16 Start)
-		    (bvand Start Start)
-		    (bvor Start Start)
-		    (bvxor Start Start)
-		    (bvadd Start Start)
-		    (if0 Start Start Start)
+        (shr1 Start)
+        (shr4 Start)
+        (shr16 Start)
+        (bvand Start Start)
+        (bvor Start Start)
+        (bvxor Start Start)
+        (bvadd Start Start)
+        (if0 Start Start Start)
  ))
 )
 )
diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy
index dda8e0ed5..aafbbd987 100644
--- a/test/regress/regress0/sygus/inv-example.sy
+++ b/test/regress/regress0/sygus/inv-example.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-inv inv-f ((x Int) (y Int) (b Bool)))
 (declare-primed-var x Int)
diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy
index 046d074d9..4bae90b00 100644
--- a/test/regress/regress0/sygus/let-ringer.sy
+++ b/test/regress/regress0/sygus/let-ringer.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (define-fun g ((x Int)) Int (ite (= x 1) 15 19))
 (synth-fun f ((x Int)) Int
diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy
index daca906a2..71cd27e8f 100644
--- a/test/regress/regress0/sygus/let-simp.sy
+++ b/test/regress/regress0/sygus/let-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int) (y Int)) Int
     ((Start Int (x
diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy
index 4fc515353..dec4594d7 100644
--- a/test/regress/regress0/sygus/max.sy
+++ b/test/regress/regress0/sygus/max.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 
 (synth-fun max ((x Int) (y Int)) Int
diff --git a/test/regress/regress0/sygus/multi-fun-polynomial2.sy b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
index 24d49ee4e..6d185ba3f 100644
--- a/test/regress/regress0/sygus/multi-fun-polynomial2.sy
+++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
@@ -1,13 +1,13 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 
 (set-logic LIA)
 
 (synth-fun addExpr1 ((x Int) (y Int)) Int
     ((Start Int (x
                  y
-		 0
-		 1
+     0
+     1
                  (+ Start Start)
                  (- Start Start)
                  ))
@@ -16,8 +16,8 @@
 (synth-fun addExpr2 ((x Int) (y Int)) Int
     ((Start Int (x
                  y
-		 0
-		 1
+     0
+     1
                  (+ Start Start)
                  (- Start Start)
                  ))
diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy
index bd7c79e3e..9065a1025 100644
--- a/test/regress/regress0/sygus/nflat-fwd-3.sy
+++ b/test/regress/regress0/sygus/nflat-fwd-3.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ (+ Con Con) Con) x))
diff --git a/test/regress/regress0/sygus/nflat-fwd.sy b/test/regress/regress0/sygus/nflat-fwd.sy
index 0f9d46215..d211d475b 100644
--- a/test/regress/regress0/sygus/nflat-fwd.sy
+++ b/test/regress/regress0/sygus/nflat-fwd.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x))
diff --git a/test/regress/regress0/sygus/no-flat-simp.sy b/test/regress/regress0/sygus/no-flat-simp.sy
index 81f90e2aa..cb284b180 100755
--- a/test/regress/regress0/sygus/no-flat-simp.sy
+++ b/test/regress/regress0/sygus/no-flat-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy
index cc3855ad1..4b3fa22e6 100644
--- a/test/regress/regress0/sygus/no-syntax-test-bool.sy
+++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/no-syntax-test-no-si.sy b/test/regress/regress0/sygus/no-syntax-test-no-si.sy
index 21788426c..86b60638b 100644
--- a/test/regress/regress0/sygus/no-syntax-test-no-si.sy
+++ b/test/regress/regress0/sygus/no-syntax-test-no-si.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/no-syntax-test.sy b/test/regress/regress0/sygus/no-syntax-test.sy
index 95f9b7c11..b95f31aa7 100644
--- a/test/regress/regress0/sygus/no-syntax-test.sy
+++ b/test/regress/regress0/sygus/no-syntax-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy
index c4fbd1c17..03d180634 100644
--- a/test/regress/regress0/sygus/parity-AIG-d0.sy
+++ b/test/regress/regress0/sygus/parity-AIG-d0.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic BV)
 
 (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
diff --git a/test/regress/regress0/sygus/tl-type.sy b/test/regress/regress0/sygus/tl-type.sy
index a8da13742..1545f86cd 100644
--- a/test/regress/regress0/sygus/tl-type.sy
+++ b/test/regress/regress0/sygus/tl-type.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-cegqi-si
+; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int (Term (+ Start Start)))
diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy
index 24b0f2c09..7f84ce06c 100644
--- a/test/regress/regress0/sygus/twolets1.sy
+++ b/test/regress/regress0/sygus/twolets1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 
 ;; f1 is x plus 2 ;; f2 is 2x plus 5
@@ -7,27 +7,27 @@
 (define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z))
 
 (synth-fun f1 ((x Int)) Int
-	   (
-	   (Start Int (
-	   	      (let0 Intx CInt CInt)
-	   	      )
- 	   )
- 	   (Intx Int (x))
-	   (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
-
-	   )
+     (
+     (Start Int (
+            (let0 Intx CInt CInt)
+            )
+     )
+     (Intx Int (x))
+     (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+
+     )
 )
 
 (synth-fun f2 ((x Int)) Int
-	   (
-	   (Start Int (x
-	   	      (let0 Intx Start CInt)
-	   	      )
- 	   )
+     (
+     (Start Int (x
+            (let0 Intx Start CInt)
+            )
+     )
      (Intx Int (x))
-	   (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+     (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
 
-	   )
+     )
 )
 
 
diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy
index c1066277e..91bab5ece 100644
--- a/test/regress/regress0/sygus/twolets2-orig.sy
+++ b/test/regress/regress0/sygus/twolets2-orig.sy
@@ -1,25 +1,25 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si
+; COMMAND-LINE: --cegqi-si --no-dump-synth
 (set-logic LIA)
 (synth-fun f1 ((x Int)) Int
-	   (
-	   (Start Int (
-	   	      (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z))
-	   	      )
- 	   )
-	   (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+     (
+     (Start Int (
+            (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z))
+            )
+     )
+     (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
 
-	   )
+     )
 )
 (synth-fun f2 ((x Int)) Int
-	   (
-	   (Start Int (x
-	   	      (let ((y Int Start) (z Int CInt)) (+ (+ y x) z))
-	   	      )
- 	   )
-	   (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
+     (
+     (Start Int (x
+            (let ((y Int Start) (z Int CInt)) (+ (+ y x) z))
+            )
+     )
+     (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
 
-	   )
+     )
 )
 (declare-var x1 Int)
 (declare-var x2 Int)
diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy
index b020c0bee..9886f6a7b 100644
--- a/test/regress/regress0/sygus/uminus_one.sy
+++ b/test/regress/regress0/sygus/uminus_one.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int ((Start Int ((- 1)))))
 (declare-var x Int)
diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
index dc39efd84..7c9d6c601 100644
--- a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
+++ b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi --no-dump-synth
 
 (set-logic LIA)
 (synth-fun inv ((x Int)) Bool