From c3a959b3112af83492694b8f0919381b1c467fb8 Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 11 Sep 2013 11:23:19 -0400
Subject: Theory of strings.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
---
 test/regress/regress0/Makefile.am              |  4 +--
 test/regress/regress0/strings/Makefile         |  8 +++++
 test/regress/regress0/strings/Makefile.am      | 47 ++++++++++++++++++++++++++
 test/regress/regress0/strings/cardinality.smt2 | 23 +++++++++++++
 test/regress/regress0/strings/loop001.smt2     | 13 +++++++
 test/regress/regress0/strings/loop002.smt2     | 17 ++++++++++
 test/regress/regress0/strings/loop003.smt2     | 17 ++++++++++
 test/regress/regress0/strings/loop004.smt2     | 17 ++++++++++
 test/regress/regress0/strings/loop005.smt2     | 20 +++++++++++
 test/regress/regress0/strings/loop006.smt2     | 17 ++++++++++
 test/regress/regress0/strings/str001.smt2      | 16 +++++++++
 test/regress/regress0/strings/str002.smt2      | 18 ++++++++++
 test/regress/regress0/strings/str003.smt2      | 15 ++++++++
 test/regress/regress0/strings/str004.smt2      | 15 ++++++++
 test/regress/regress0/strings/str005.smt2      | 18 ++++++++++
 15 files changed, 263 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress0/strings/Makefile
 create mode 100644 test/regress/regress0/strings/Makefile.am
 create mode 100644 test/regress/regress0/strings/cardinality.smt2
 create mode 100644 test/regress/regress0/strings/loop001.smt2
 create mode 100644 test/regress/regress0/strings/loop002.smt2
 create mode 100644 test/regress/regress0/strings/loop003.smt2
 create mode 100644 test/regress/regress0/strings/loop004.smt2
 create mode 100644 test/regress/regress0/strings/loop005.smt2
 create mode 100644 test/regress/regress0/strings/loop006.smt2
 create mode 100644 test/regress/regress0/strings/str001.smt2
 create mode 100644 test/regress/regress0/strings/str002.smt2
 create mode 100644 test/regress/regress0/strings/str003.smt2
 create mode 100644 test/regress/regress0/strings/str004.smt2
 create mode 100644 test/regress/regress0/strings/str005.smt2

(limited to 'test/regress/regress0')

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 082662a1e..80c377972 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,5 +1,5 @@
-SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf
-DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf
+SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings
+DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings
 
 BINARY = cvc4
 LOG_COMPILER = @srcdir@/../run_regression
diff --git a/test/regress/regress0/strings/Makefile b/test/regress/regress0/strings/Makefile
new file mode 100644
index 000000000..1c399b3e4
--- /dev/null
+++ b/test/regress/regress0/strings/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/strings
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
new file mode 100644
index 000000000..37da1091e
--- /dev/null
+++ b/test/regress/regress0/strings/Makefile.am
@@ -0,0 +1,47 @@
+SUBDIRS = .
+
+BINARY = cvc4
+LOG_COMPILER = @srcdir@/../../run_regression
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
+
+if AUTOMAKE_1_11
+# old-style (pre-automake 1.12) test harness
+TESTS_ENVIRONMENT = \
+	$(TESTS_ENVIRONMENT) $(LOG_COMPILER) \
+	$(AM_LOG_FLAGS) $(LOG_FLAGS)
+endif
+
+MAKEFLAGS = -k
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	\
+  cardinality.smt2 \
+  str001.smt2 \
+  str002.smt2 \
+  str003.smt2 \
+  str004.smt2 \
+  str005.smt2 \
+  loop001.smt2
+# loop002.smt2 \
+# loop003.smt2 \
+# loop004.smt2 \
+# loop005.smt2 \
+# loop006.smt2
+
+FAILING_TESTS =
+
+EXTRA_DIST = $(TESTS)
+
+
+# and make sure to distribute it
+EXTRA_DIST +=
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
diff --git a/test/regress/regress0/strings/cardinality.smt2 b/test/regress/regress0/strings/cardinality.smt2
new file mode 100644
index 000000000..5c4771d71
--- /dev/null
+++ b/test/regress/regress0/strings/cardinality.smt2
@@ -0,0 +1,23 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(set-option :str-cardinality 2)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+(declare-fun i () Int)
+
+(assert (= i 1))
+(assert (= (str.len x) i))
+(assert (= (str.len y) i))
+(assert (= (str.len z) i))
+(assert (= (str.len w) 2))
+
+(assert (not (=  x y)))
+(assert (not (=  x z)))
+(assert (not (=  z y)))
+
+
+(check-sat)
diff --git a/test/regress/regress0/strings/loop001.smt2 b/test/regress/regress0/strings/loop001.smt2
new file mode 100644
index 000000000..11460b335
--- /dev/null
+++ b/test/regress/regress0/strings/loop001.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+(declare-fun w1 () String)
+(declare-fun w2 () String)
+
+(assert (= (str.++ x "a") (str.++ "b" x)))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/loop002.smt2 b/test/regress/regress0/strings/loop002.smt2
new file mode 100644
index 000000000..a47b959f5
--- /dev/null
+++ b/test/regress/regress0/strings/loop002.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+; EXIT: 10
+;
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+(declare-fun w1 () String)
+(declare-fun w2 () String)
+
+(assert (= (str.++ x "ba") (str.++ "ab" x)))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/loop003.smt2 b/test/regress/regress0/strings/loop003.smt2
new file mode 100644
index 000000000..a535f7583
--- /dev/null
+++ b/test/regress/regress0/strings/loop003.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+; EXIT: 10
+;
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+(declare-fun w1 () String)
+(declare-fun w2 () String)
+
+(assert (= (str.++ x "aaaae") (str.++ "eaaaa" x)))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/loop004.smt2 b/test/regress/regress0/strings/loop004.smt2
new file mode 100644
index 000000000..7b39bf2d3
--- /dev/null
+++ b/test/regress/regress0/strings/loop004.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+; EXIT: 10
+;
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+(declare-fun w1 () String)
+(declare-fun w2 () String)
+
+(assert (= (str.++ x y z) (str.++ y z x)))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/loop005.smt2 b/test/regress/regress0/strings/loop005.smt2
new file mode 100644
index 000000000..ec294b9bb
--- /dev/null
+++ b/test/regress/regress0/strings/loop005.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+; EXIT: 10
+;
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+(declare-fun w1 () String)
+(declare-fun w2 () String)
+
+(assert (= (str.++ x y z) (str.++ x z y)))
+(assert (= (str.++ x w z) (str.++ x z w)))
+(assert (not (= y w)))
+(assert (> (str.len z) 0))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/loop006.smt2 b/test/regress/regress0/strings/loop006.smt2
new file mode 100644
index 000000000..8c3690c61
--- /dev/null
+++ b/test/regress/regress0/strings/loop006.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+; EXIT: 10
+;
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+(declare-fun w1 () String)
+(declare-fun w2 () String)
+
+(assert (= (str.++ x y z) (str.++ x z y)))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/str001.smt2 b/test/regress/regress0/strings/str001.smt2
new file mode 100644
index 000000000..8ae10edbe
--- /dev/null
+++ b/test/regress/regress0/strings/str001.smt2
@@ -0,0 +1,16 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-fun xx () String)
+(declare-fun yy () String)
+(declare-fun zz () String)
+(declare-fun ww () String)
+(declare-fun pp () String)
+(declare-fun qq () String)
+
+(assert (= (str.++ xx yy zz) (str.++ ww qq)))
+(assert (= ww (str.++ xx pp)))
+(assert (= yy pp))
+(assert (not (= zz qq)))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/str002.smt2 b/test/regress/regress0/strings/str002.smt2
new file mode 100644
index 000000000..98b3e1e00
--- /dev/null
+++ b/test/regress/regress0/strings/str002.smt2
@@ -0,0 +1,18 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-fun xx () String)
+(declare-fun yy () String)
+(declare-fun zz () String)
+(declare-fun ww () String)
+(declare-fun pp () String)
+(declare-fun qq () String)
+
+; assoc
+(assert (or (= xx (str.++ yy "aa")) (= zz (str.++ yy "aa"))
+))
+(assert (and (not (= (str.++ xx "bb") (str.++ yy "aa" "bb")))
+		    (not (= (str.++ zz "bb") (str.++ yy "aa" "bb")))
+))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/str003.smt2 b/test/regress/regress0/strings/str003.smt2
new file mode 100644
index 000000000..c88e1233e
--- /dev/null
+++ b/test/regress/regress0/strings/str003.smt2
@@ -0,0 +1,15 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-fun xx () String)
+(declare-fun yy () String)
+(declare-fun zz () String)
+(declare-fun ww () String)
+(declare-fun pp () String)
+(declare-fun qq () String)
+
+(assert (= "ab" (str.++ "a" xx)))
+(assert (not (= xx yy)))
+(assert (= "b" yy))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/str004.smt2 b/test/regress/regress0/strings/str004.smt2
new file mode 100644
index 000000000..d4763adee
--- /dev/null
+++ b/test/regress/regress0/strings/str004.smt2
@@ -0,0 +1,15 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-fun xx () String)
+(declare-fun yy () String)
+(declare-fun zz () String)
+(declare-fun ww () String)
+(declare-fun pp () String)
+(declare-fun qq () String)
+
+; Morgan says it needs length bound
+(assert (> (str.len yy) (str.len xx)))
+(assert (= xx (str.++ xx yy)))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/str005.smt2 b/test/regress/regress0/strings/str005.smt2
new file mode 100644
index 000000000..4916b1df4
--- /dev/null
+++ b/test/regress/regress0/strings/str005.smt2
@@ -0,0 +1,18 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-fun xx () String)
+(declare-fun yy () String)
+(declare-fun zz () String)
+(declare-fun ww () String)
+(declare-fun pp () String)
+(declare-fun qq () String)
+
+; common postfix
+;(assert (= (str.++ xx "aa") (str.++ xx "bb")))
+
+(assert (= (str.len yy) 0))
+(assert (not (= yy "")))
+
+(check-sat)
+
-- 
cgit v1.2.3