Add regressions, change defaults. (#1911)

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 10000bbb1846952bbb826ed90bdc40d972f6b28b..715b0c28688903620071a98f9646464551746ff0 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -981,7 +981,7 @@ header = "options/quantifiers_options.h"
   category   = "regular"
   long       = "sygus-repair-const"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   help       = "use approach to repair constants in sygus candidate solutions"
 
 [[option]]
@@ -998,7 +998,7 @@ header = "options/quantifiers_options.h"
   category   = "regular"
   long       = "sygus-add-const-grammar"
   type       = "bool"
-  default    = "true"
+  default    = "false"
   read_only  = true
   help       = "statically add constants appearing in conjecture to grammars"
 

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 5cb24d072a9a923e2520a4128c7b11b5095dc343..7784a68258b192ae569d59e24d177fc01bfb9386 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1488,6 +1488,7 @@ REG1_TESTS = \
        regress1/sygus/icfp_easy-ite.sy \
        regress1/sygus/inv-example.sy \
        regress1/sygus/inv-unused.sy \
+       regress1/sygus/large-const-simp.sy \
        regress1/sygus/list-head-x.sy \
        regress1/sygus/max.sy \
        regress1/sygus/multi-fun-polynomial2.sy \
@@ -1589,6 +1590,7 @@ REG2_TESTS = \
        regress2/strings/norn-dis-0707-3.smt2 \
        regress2/sygus/MPwL_d1s3.sy \
        regress2/sygus/array_sum_dd.sy \
+       regress2/sygus/ex23.sy \
        regress2/sygus/icfp_easy_mt_ite.sy \
        regress2/sygus/inv_gen_n_c11.sy \
        regress2/sygus/lustre-real.sy \

diff --git a/test/regress/regress1/sygus/large-const-simp.sy b/test/regress/regress1/sygus/large-const-simp.sy
new file mode 100644 (file)
index 0000000..31f660b
--- /dev/null
+++ b/test/regress/regress1/sygus/large-const-simp.sy
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status --sygus-add-const-grammar
+(set-logic LIA)
+
+(synth-fun lc ((x Int)) Int)
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (> (lc x) 1500))
+(constraint (< (lc x) 1600))
+
+(check-synth)

diff --git a/test/regress/regress2/sygus/ex23.sy b/test/regress/regress2/sygus/ex23.sy
new file mode 100644 (file)
index 0000000..61b08a8
--- /dev/null
+++ b/test/regress/regress2/sygus/ex23.sy
@@ -0,0 +1,23 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic LIA)
+
+(synth-inv inv-f ((y Int) (z Int) (c Int)))
+
+(declare-primed-var y Int)
+(declare-primed-var z Int)
+(declare-primed-var c Int)
+
+(define-fun pre-f ((y Int) (z Int) (c Int)) Bool
+(and (and (= c 0) (>= y 0)) (and (>= 127 y) (= z (* 36 y)))))
+
+
+(define-fun trans-f ((y Int) (z Int) (c Int) (y! Int) (z! Int) (c! Int)) Bool
+(and (and (and (< c 36) (= z! (+ z 1))) (= c! (+ c 1))) (= y! y)))
+
+(define-fun post-f ((y Int) (z Int) (c Int)) Bool
+(not (and (< c 36) (or (< z 0) (>= z 4608)))))
+
+(inv-constraint inv-f pre-f trans-f post-f)
+
+(check-synth)