Theory of strings.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

17 files changed, 265 insertions, 2 deletions

diff --git a/test/Makefile.am b/test/Makefile.am
index 1ac00eb82..104d40ab1 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -55,6 +55,7 @@ subdirs_to_check = \
 	regress/regress0/unconstrained \
 	regress/regress0/decision \
 	regress/regress0/fmf \
+	regress/regress0/strings \
 	regress/regress1 \
 	regress/regress2 \
 	regress/regress3
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)
+
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 39d8aadb1..8f9417966 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -511,6 +511,7 @@ public:
 
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );
+    info.disableTheory(THEORY_STRINGS);
     info.arithOnlyLinear();
     info.disableIntegers();
     info.lock();