From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 14 May 2018 16:33:14 +0000 (-0500)
Subject: Add regressions, change defaults. (#1911)
X-Git-Tag: cvc5-1.0.0~5057
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c308c094548bcd9bee59e33334d147a9afe97018;p=cvc5.git

Add regressions, change defaults. (#1911)
---

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 10000bbb1..715b0c286 100644
--- 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 5cb24d072..7784a6825 100644
--- 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
index 000000000..31f660b2a
--- /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
index 000000000..61b08a838
--- /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)