Merge pull request #4015 from allredj/smt2_strings_tests

SMT2 strings tests

Author: tautschnig

regression/CMakeLists.txt

@@ -32,6 +32,7 @@ add_subdirectory(cpp)
 add_subdirectory(cbmc-cover)
 add_subdirectory(goto-instrument-typedef)
 add_subdirectory(smt2_solver)
+add_subdirectory(smt2_strings)
 add_subdirectory(strings)
 add_subdirectory(invariants)
 add_subdirectory(goto-diff)

regression/Makefile

@@ -10,6 +10,7 @@ DIRS = cbmc \
        cbmc-cover \
        goto-instrument-typedef \
        smt2_solver \
+       smt2_strings \
        strings \
        invariants \
        goto-diff \

regression/smt2_strings/.gitignore

@@ -0,0 +1 @@
+!*.smt2

regression/smt2_strings/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:smt2_solver>"
+)

regression/smt2_strings/Makefile

@@ -0,0 +1,18 @@
+default: tests.log
+
+test:
+	@../test.pl -p -c ../../../src/solvers/smt2_solver
+
+tests.log: ../test.pl
+	@../test.pl -p -c ../../../src/solvers/smt2_solver
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/smt2_strings/README.md

@@ -0,0 +1,8 @@
+FUTURE
+concat_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/concat_const_sat/concat_const_sat.desc

@@ -0,0 +1,2 @@
+(assert (= (str.++ "abc" "def" "" "gh") "abcdefgh"))
+(check-sat)

regression/smt2_strings/concat_const_sat/concat_const_sat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+concat_const_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/concat_const_unsat/concat_const_unsat.desc

@@ -0,0 +1,2 @@
+(assert (= (str.++ "abc" "cdef") "abcde"))
+(check-sat)

regression/smt2_strings/concat_const_unsat/concat_const_unsat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+contains_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/contains_const_sat/contains_const_sat.desc

@@ -0,0 +1,2 @@
+(assert (str.contains "abcdef" "bcd"))
+(check-sat)

regression/smt2_strings/contains_const_sat/contains_const_sat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+contains_const_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/contains_const_unsat/contains_const_unsat.desc

@@ -0,0 +1,2 @@
+(assert (str.contains "abcdef" "dc"))
+(check-sat)

regression/smt2_strings/contains_const_unsat/contains_const_unsat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+indexof_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/indexof_const_sat/indexof_const_sat.desc

@@ -0,0 +1,2 @@
+(assert (= (str.indexof "abcdef" "cde" 1) 2))
+(check-sat)

regression/smt2_strings/indexof_const_sat/indexof_const_sat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+indexof_const_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/indexof_const_unsat/indexof_const_unsat.desc

@@ -0,0 +1,2 @@
+(assert (= (str.indexof "abcdef" "cde" 1) 1))
+(check-sat)

regression/smt2_strings/indexof_const_unsat/indexof_const_unsat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+int_to_str_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/int_to_str_const_sat/int_to_str_const_sat.desc

@@ -0,0 +1,2 @@
+(assert (= (int.to.str 1234567890) "1234567890"))
+(check-sat)

regression/smt2_strings/int_to_str_const_sat/int_to_str_const_sat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+int_to_str_const_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/int_to_str_const_unsat/int_to_str_const_unsat.desc

@@ -0,0 +1,2 @@
+(assert (= (int.to.str 1234567890) "1234467890"))
+(check-sat)

regression/smt2_strings/int_to_str_const_unsat/int_to_str_const_unsat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+length_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/length_const_sat/length_const_sat.desc

@@ -0,0 +1,2 @@
+(assert (= (str.len "abc") 3))
+(check-sat)

regression/smt2_strings/length_const_sat/length_const_sat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+length_const_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/length_const_unsat/length_const_unsat.desc

@@ -0,0 +1,2 @@
+(assert (= (str.len "abc") 4))
+(check-sat)

regression/smt2_strings/length_const_unsat/length_const_unsat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+lex_order_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/lex_order_const_sat/lex_order_const_sat.desc

@@ -0,0 +1,2 @@
+(assert (str.< "abc" "acc"))
+(check-sat)

regression/smt2_strings/lex_order_const_sat/lex_order_const_sat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+lex_order_const_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/lex_order_const_unsat/lex_order_const_unsat.desc

@@ -0,0 +1,2 @@
+(assert (str.< "abc" "aac"))
+(check-sat)

regression/smt2_strings/lex_order_const_unsat/lex_order_const_unsat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+prefixof_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/prefixof_const_sat/prefixof_const_sat.desc

@@ -0,0 +1,2 @@
+(assert (str.prefixof "abc" "abcdef"))
+(check-sat)

regression/smt2_strings/prefixof_const_sat/prefixof_const_sat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+prefixof_const_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/prefixof_const_unsat/prefixof_const_unsat.desc

@@ -0,0 +1,2 @@
+(assert (str.prefixof "bc" "abcdef"))
+(check-sat)

regression/smt2_strings/prefixof_const_unsat/prefixof_const_unsat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+reflexive_lex_order_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat.desc

@@ -0,0 +1,2 @@
+(assert (str.<= "abc" "acc"))
+(check-sat)

regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+reflexive_lex_order_const_sat2.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat2.desc

@@ -0,0 +1,2 @@
+(assert (str.<= "abc" "abc"))
+(check-sat)

regression/smt2_strings/reflexive_lex_order_const_sat/reflexive_lex_order_const_sat2.smt2

@@ -0,0 +1,8 @@
+FUTURE
+reflexive_lex_order_const_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/reflexive_lex_order_const_unsat/reflexive_lex_order_const_unsat.desc

@@ -0,0 +1,2 @@
+(assert (str.<= "acc" "abc"))
+(check-sat)

regression/smt2_strings/reflexive_lex_order_const_unsat/reflexive_lex_order_const_unsat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+regexp_all_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/regexp_all_const_sat/regexp_all_const_sat.desc

@@ -0,0 +1,2 @@
+(assert (str.in.re "abc" (re.* re.all)))
+(check-sat)

regression/smt2_strings/regexp_all_const_sat/regexp_all_const_sat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+regexp_allchar_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/regexp_allchar_const_sat/regexp_allchar_const_sat.desc

@@ -0,0 +1,2 @@
+(assert (str.in.re "aaabbb" (re.++ (re.* (str.to.re "a")) (re.* re.allchar))))
+(check-sat)

regression/smt2_strings/regexp_allchar_const_sat/regexp_allchar_const_sat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+regexp_allchar_const_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/regexp_allchar_const_unsat/regexp_allchar_const_unsat.desc

@@ -0,0 +1,2 @@
+(assert (str.in.re "a" (re.++ (re.+ (str.to.re "a")) (re.+ re.allchar))))
+(check-sat)

regression/smt2_strings/regexp_allchar_const_unsat/regexp_allchar_const_unsat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+regexp_concat_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/regexp_concat_const_sat/regexp_concat_const_sat.desc

@@ -0,0 +1,2 @@
+(assert (str.in.re "aaabbb" (re.++ (re.* (str.to.re "a")) (re.* (str.to.re "b")))))
+(check-sat)

regression/smt2_strings/regexp_concat_const_sat/regexp_concat_const_sat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+regexp_concat_const_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/regexp_concat_const_unsat/regexp_concat_const_unsat.desc

@@ -0,0 +1,2 @@
+(assert (str.in.re "aaabbbc" (re.++ (re.* (str.to.re "a")) (re.* (str.to.re "b")))))
+(check-sat)

regression/smt2_strings/regexp_concat_const_unsat/regexp_concat_const_unsat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+regexp_inter_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/regexp_inter_const_sat/regexp_inter_const_sat.desc

@@ -0,0 +1,2 @@
+(assert (str.in.re "e" (re.inter (re.range "a" "h") (re.range "d" "w"))))
+(check-sat)

regression/smt2_strings/regexp_inter_const_sat/regexp_inter_const_sat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+regexp_inter_const_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/regexp_inter_const_unsat/regexp_inter_const_unsat.desc

@@ -0,0 +1,2 @@
+(assert (str.in.re "e" (re.inter (re.range "a" "b") (re.range "b" "w"))))
+(check-sat)

regression/smt2_strings/regexp_inter_const_unsat/regexp_inter_const_unsat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+regexp_loop_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/regexp_loop_const_sat/regexp_loop_const_sat.desc

@@ -0,0 +1,2 @@
+(assert (str.in.re "aaa" ((_ re.loop 3 3) (str.to.re "a"))))
+(check-sat)

regression/smt2_strings/regexp_loop_const_sat/regexp_loop_const_sat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+regexp_loop_const_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/regexp_loop_const_unsat/regexp_loop_const_unsat.desc

@@ -0,0 +1,2 @@
+(assert (str.in.re "aaa" ((_ re.loop 1 2) (str.to.re "a"))))
+(check-sat)

regression/smt2_strings/regexp_loop_const_unsat/regexp_loop_const_unsat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+regexp_nostr_const_unsat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+error

regression/smt2_strings/regexp_nostr_const_unsat/regexp_nostr_const_unsat.desc

@@ -0,0 +1,2 @@
+(assert (str.in.re "a" re.nostr))
+(check-sat)

regression/smt2_strings/regexp_nostr_const_unsat/regexp_nostr_const_unsat.smt2

@@ -0,0 +1,8 @@
+FUTURE
+regexp_opt_const_sat.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--
+error

regression/smt2_strings/regexp_opt_const_sat/regexp_opt_const_sat.desc

@@ -0,0 +1,2 @@
+(assert (str.in.re "aaab" (re.++ (re.+ (str.to.re "a")) (re.opt (str.to.re "b")))))
+(check-sat)