Support default sygus grammar for strings (#3148)

3 files changed, 28 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 99b464d09..19e5fa899 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1696,6 +1696,7 @@ set(regress_1_tests
   regress1/sygus/real-grammar.sy
   regress1/sygus/simple-regexp.sy
   regress1/sygus/stopwatch-bt.sy
+  regress1/sygus/strings-no-syntax.sy
   regress1/sygus/strings-concat-3-args.sy
   regress1/sygus/strings-double-rec.sy
   regress1/sygus/strings-small.sy
@@ -1833,6 +1834,7 @@ 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/strings-no-syntax-len.sy
   regress2/sygus/three.sy
   regress2/sygus/vcb.sy
   regress2/typed_v1l50016-simp.cvc
diff --git a/test/regress/regress1/sygus/strings-no-syntax.sy b/test/regress/regress1/sygus/strings-no-syntax.sy
new file mode 100644
index 000000000..4959d6fe1
--- /dev/null
+++ b/test/regress/regress1/sygus/strings-no-syntax.sy
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+
+(synth-fun f ((x String) (y String)) String)
+
+(declare-var x String)
+(declare-var y String)
+
+(constraint (>= (str.len (f x y)) (str.len x)))
+(constraint (>= (str.len (f x y)) (str.len y)))
+
+(check-synth)
diff --git a/test/regress/regress2/sygus/strings-no-syntax-len.sy b/test/regress/regress2/sygus/strings-no-syntax-len.sy
new file mode 100644
index 000000000..22048f1ec
--- /dev/null
+++ b/test/regress/regress2/sygus/strings-no-syntax-len.sy
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+
+(synth-fun f ((x String)) Int)
+
+(declare-var x String)
+(constraint (>= (f (str.++ "A" x)) (f x)))
+(constraint (= (f "A") 2))
+(constraint (= (f "BB") 4))
+(constraint (= (f "BCB") 6))
+
+(check-synth)