From: Andrew Reynolds Date: Wed, 8 Dec 2021 19:25:37 +0000 (-0600) Subject: Make several regressions faster (#7769) X-Git-Tag: cvc5-1.0.0~701 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d6d3f74ebff704675aa941ac9eeafa97bad662db;p=cvc5.git Make several regressions faster (#7769) This makes several slow regressions faster, mostly by changing options. It changes a strings regression to be faster by making it smaller. This should avoid timeouts on https://cvc5-buildbot.stanford.edu/. --- diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b565895ba..3881a142a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2688,7 +2688,7 @@ set(regress_2_tests regress2/strings/replaceall-diffrange.smt2 regress2/strings/replaceall-len-c.smt2 regress2/strings/small-1.smt2 - regress2/strings/strings-alpha-card-129.smt2 + regress2/strings/strings-alpha-card-65.smt2 regress2/strings/update-ex3.smt2 regress2/strings/update-ex4-seq.smt2 regress2/sygus/MPwL_d1s3.sy diff --git a/test/regress/regress2/strings/strings-alpha-card-129.smt2 b/test/regress/regress2/strings/strings-alpha-card-129.smt2 deleted file mode 100644 index c0b4ae0a2..000000000 --- a/test/regress/regress2/strings/strings-alpha-card-129.smt2 +++ /dev/null @@ -1,393 +0,0 @@ -; COMMAND-LINE: --strings-alpha-card=128 --simplification=none -; EXPECT: unsat -(set-logic QF_SLIA) -(declare-fun s1 () String) -(assert (= (str.len s1) 1)) -(declare-fun s2 () String) -(assert (= (str.len s2) 1)) -(declare-fun s3 () String) -(assert (= (str.len s3) 1)) -(declare-fun s4 () String) -(assert (= (str.len s4) 1)) -(declare-fun s5 () String) -(assert (= (str.len s5) 1)) -(declare-fun s6 () String) -(assert (= (str.len s6) 1)) -(declare-fun s7 () String) -(assert (= (str.len s7) 1)) -(declare-fun s8 () String) -(assert (= (str.len s8) 1)) -(declare-fun s9 () String) -(assert (= (str.len s9) 1)) -(declare-fun s10 () String) -(assert (= (str.len s10) 1)) -(declare-fun s11 () String) -(assert (= (str.len s11) 1)) -(declare-fun s12 () String) -(assert (= (str.len s12) 1)) -(declare-fun s13 () String) -(assert (= (str.len s13) 1)) -(declare-fun s14 () String) -(assert (= (str.len s14) 1)) -(declare-fun s15 () String) -(assert (= (str.len s15) 1)) -(declare-fun s16 () String) -(assert (= (str.len s16) 1)) -(declare-fun s17 () String) -(assert (= (str.len s17) 1)) -(declare-fun s18 () String) -(assert (= (str.len s18) 1)) -(declare-fun s19 () String) -(assert (= (str.len s19) 1)) -(declare-fun s20 () String) -(assert (= (str.len s20) 1)) -(declare-fun s21 () String) -(assert (= (str.len s21) 1)) -(declare-fun s22 () String) -(assert (= (str.len s22) 1)) -(declare-fun s23 () String) -(assert (= (str.len s23) 1)) -(declare-fun s24 () String) -(assert (= (str.len s24) 1)) -(declare-fun s25 () String) -(assert (= (str.len s25) 1)) -(declare-fun s26 () String) -(assert (= (str.len s26) 1)) -(declare-fun s27 () String) -(assert (= (str.len s27) 1)) -(declare-fun s28 () String) -(assert (= (str.len s28) 1)) -(declare-fun s29 () String) -(assert (= (str.len s29) 1)) -(declare-fun s30 () String) -(assert (= (str.len s30) 1)) -(declare-fun s31 () String) -(assert (= (str.len s31) 1)) -(declare-fun s32 () String) -(assert (= (str.len s32) 1)) -(declare-fun s33 () String) -(assert (= (str.len s33) 1)) -(declare-fun s34 () String) -(assert (= (str.len s34) 1)) -(declare-fun s35 () String) -(assert (= (str.len s35) 1)) -(declare-fun s36 () String) -(assert (= (str.len s36) 1)) -(declare-fun s37 () String) -(assert (= (str.len s37) 1)) -(declare-fun s38 () String) -(assert (= (str.len s38) 1)) -(declare-fun s39 () String) -(assert (= (str.len s39) 1)) -(declare-fun s40 () String) -(assert (= (str.len s40) 1)) -(declare-fun s41 () String) -(assert (= (str.len s41) 1)) -(declare-fun s42 () String) -(assert (= (str.len s42) 1)) -(declare-fun s43 () String) -(assert (= (str.len s43) 1)) -(declare-fun s44 () String) -(assert (= (str.len s44) 1)) -(declare-fun s45 () String) -(assert (= (str.len s45) 1)) -(declare-fun s46 () String) -(assert (= (str.len s46) 1)) -(declare-fun s47 () String) -(assert (= (str.len s47) 1)) -(declare-fun s48 () String) -(assert (= (str.len s48) 1)) -(declare-fun s49 () String) -(assert (= (str.len s49) 1)) -(declare-fun s50 () String) -(assert (= (str.len s50) 1)) -(declare-fun s51 () String) -(assert (= (str.len s51) 1)) -(declare-fun s52 () String) -(assert (= (str.len s52) 1)) -(declare-fun s53 () String) -(assert (= (str.len s53) 1)) -(declare-fun s54 () String) -(assert (= (str.len s54) 1)) -(declare-fun s55 () String) -(assert (= (str.len s55) 1)) -(declare-fun s56 () String) -(assert (= (str.len s56) 1)) -(declare-fun s57 () String) -(assert (= (str.len s57) 1)) -(declare-fun s58 () String) -(assert (= (str.len s58) 1)) -(declare-fun s59 () String) -(assert (= (str.len s59) 1)) -(declare-fun s60 () String) -(assert (= (str.len s60) 1)) -(declare-fun s61 () String) -(assert (= (str.len s61) 1)) -(declare-fun s62 () String) -(assert (= (str.len s62) 1)) -(declare-fun s63 () String) -(assert (= (str.len s63) 1)) -(declare-fun s64 () String) -(assert (= (str.len s64) 1)) -(declare-fun s65 () String) -(assert (= (str.len s65) 1)) -(declare-fun s66 () String) -(assert (= (str.len s66) 1)) -(declare-fun s67 () String) -(assert (= (str.len s67) 1)) -(declare-fun s68 () String) -(assert (= (str.len s68) 1)) -(declare-fun s69 () String) -(assert (= (str.len s69) 1)) -(declare-fun s70 () String) -(assert (= (str.len s70) 1)) -(declare-fun s71 () String) -(assert (= (str.len s71) 1)) -(declare-fun s72 () String) -(assert (= (str.len s72) 1)) -(declare-fun s73 () String) -(assert (= (str.len s73) 1)) -(declare-fun s74 () String) -(assert (= (str.len s74) 1)) -(declare-fun s75 () String) -(assert (= (str.len s75) 1)) -(declare-fun s76 () String) -(assert (= (str.len s76) 1)) -(declare-fun s77 () String) -(assert (= (str.len s77) 1)) -(declare-fun s78 () String) -(assert (= (str.len s78) 1)) -(declare-fun s79 () String) -(assert (= (str.len s79) 1)) -(declare-fun s80 () String) -(assert (= (str.len s80) 1)) -(declare-fun s81 () String) -(assert (= (str.len s81) 1)) -(declare-fun s82 () String) -(assert (= (str.len s82) 1)) -(declare-fun s83 () String) -(assert (= (str.len s83) 1)) -(declare-fun s84 () String) -(assert (= (str.len s84) 1)) -(declare-fun s85 () String) -(assert (= (str.len s85) 1)) -(declare-fun s86 () String) -(assert (= (str.len s86) 1)) -(declare-fun s87 () String) -(assert (= (str.len s87) 1)) -(declare-fun s88 () String) -(assert (= (str.len s88) 1)) -(declare-fun s89 () String) -(assert (= (str.len s89) 1)) -(declare-fun s90 () String) -(assert (= (str.len s90) 1)) -(declare-fun s91 () String) -(assert (= (str.len s91) 1)) -(declare-fun s92 () String) -(assert (= (str.len s92) 1)) -(declare-fun s93 () String) -(assert (= (str.len s93) 1)) -(declare-fun s94 () String) -(assert (= (str.len s94) 1)) -(declare-fun s95 () String) -(assert (= (str.len s95) 1)) -(declare-fun s96 () String) -(assert (= (str.len s96) 1)) -(declare-fun s97 () String) -(assert (= (str.len s97) 1)) -(declare-fun s98 () String) -(assert (= (str.len s98) 1)) -(declare-fun s99 () String) -(assert (= (str.len s99) 1)) -(declare-fun s100 () String) -(assert (= (str.len s100) 1)) -(declare-fun s101 () String) -(assert (= (str.len s101) 1)) -(declare-fun s102 () String) -(assert (= (str.len s102) 1)) -(declare-fun s103 () String) -(assert (= (str.len s103) 1)) -(declare-fun s104 () String) -(assert (= (str.len s104) 1)) -(declare-fun s105 () String) -(assert (= (str.len s105) 1)) -(declare-fun s106 () String) -(assert (= (str.len s106) 1)) -(declare-fun s107 () String) -(assert (= (str.len s107) 1)) -(declare-fun s108 () String) -(assert (= (str.len s108) 1)) -(declare-fun s109 () String) -(assert (= (str.len s109) 1)) -(declare-fun s110 () String) -(assert (= (str.len s110) 1)) -(declare-fun s111 () String) -(assert (= (str.len s111) 1)) -(declare-fun s112 () String) -(assert (= (str.len s112) 1)) -(declare-fun s113 () String) -(assert (= (str.len s113) 1)) -(declare-fun s114 () String) -(assert (= (str.len s114) 1)) -(declare-fun s115 () String) -(assert (= (str.len s115) 1)) -(declare-fun s116 () String) -(assert (= (str.len s116) 1)) -(declare-fun s117 () String) -(assert (= (str.len s117) 1)) -(declare-fun s118 () String) -(assert (= (str.len s118) 1)) -(declare-fun s119 () String) -(assert (= (str.len s119) 1)) -(declare-fun s120 () String) -(assert (= (str.len s120) 1)) -(declare-fun s121 () String) -(assert (= (str.len s121) 1)) -(declare-fun s122 () String) -(assert (= (str.len s122) 1)) -(declare-fun s123 () String) -(assert (= (str.len s123) 1)) -(declare-fun s124 () String) -(assert (= (str.len s124) 1)) -(declare-fun s125 () String) -(assert (= (str.len s125) 1)) -(declare-fun s126 () String) -(assert (= (str.len s126) 1)) -(declare-fun s127 () String) -(assert (= (str.len s127) 1)) -(declare-fun s128 () String) -(assert (= (str.len s128) 1)) -(declare-fun s129 () String) -(assert (= (str.len s129) 1)) -(assert (distinct -s1 -s2 -s3 -s4 -s5 -s6 -s7 -s8 -s9 -s10 -s11 -s12 -s13 -s14 -s15 -s16 -s17 -s18 -s19 -s20 -s21 -s22 -s23 -s24 -s25 -s26 -s27 -s28 -s29 -s30 -s31 -s32 -s33 -s34 -s35 -s36 -s37 -s38 -s39 -s40 -s41 -s42 -s43 -s44 -s45 -s46 -s47 -s48 -s49 -s50 -s51 -s52 -s53 -s54 -s55 -s56 -s57 -s58 -s59 -s60 -s61 -s62 -s63 -s64 -s65 -s66 -s67 -s68 -s69 -s70 -s71 -s72 -s73 -s74 -s75 -s76 -s77 -s78 -s79 -s80 -s81 -s82 -s83 -s84 -s85 -s86 -s87 -s88 -s89 -s90 -s91 -s92 -s93 -s94 -s95 -s96 -s97 -s98 -s99 -s100 -s101 -s102 -s103 -s104 -s105 -s106 -s107 -s108 -s109 -s110 -s111 -s112 -s113 -s114 -s115 -s116 -s117 -s118 -s119 -s120 -s121 -s122 -s123 -s124 -s125 -s126 -s127 -s128 -s129 -)) -(check-sat) diff --git a/test/regress/regress2/strings/strings-alpha-card-65.smt2 b/test/regress/regress2/strings/strings-alpha-card-65.smt2 new file mode 100644 index 000000000..82ab06ea9 --- /dev/null +++ b/test/regress/regress2/strings/strings-alpha-card-65.smt2 @@ -0,0 +1,201 @@ +; COMMAND-LINE: --strings-alpha-card=64 --simplification=none +; EXPECT: unsat +(set-logic QF_SLIA) +(declare-fun s1 () String) +(assert (= (str.len s1) 1)) +(declare-fun s2 () String) +(assert (= (str.len s2) 1)) +(declare-fun s3 () String) +(assert (= (str.len s3) 1)) +(declare-fun s4 () String) +(assert (= (str.len s4) 1)) +(declare-fun s5 () String) +(assert (= (str.len s5) 1)) +(declare-fun s6 () String) +(assert (= (str.len s6) 1)) +(declare-fun s7 () String) +(assert (= (str.len s7) 1)) +(declare-fun s8 () String) +(assert (= (str.len s8) 1)) +(declare-fun s9 () String) +(assert (= (str.len s9) 1)) +(declare-fun s10 () String) +(assert (= (str.len s10) 1)) +(declare-fun s11 () String) +(assert (= (str.len s11) 1)) +(declare-fun s12 () String) +(assert (= (str.len s12) 1)) +(declare-fun s13 () String) +(assert (= (str.len s13) 1)) +(declare-fun s14 () String) +(assert (= (str.len s14) 1)) +(declare-fun s15 () String) +(assert (= (str.len s15) 1)) +(declare-fun s16 () String) +(assert (= (str.len s16) 1)) +(declare-fun s17 () String) +(assert (= (str.len s17) 1)) +(declare-fun s18 () String) +(assert (= (str.len s18) 1)) +(declare-fun s19 () String) +(assert (= (str.len s19) 1)) +(declare-fun s20 () String) +(assert (= (str.len s20) 1)) +(declare-fun s21 () String) +(assert (= (str.len s21) 1)) +(declare-fun s22 () String) +(assert (= (str.len s22) 1)) +(declare-fun s23 () String) +(assert (= (str.len s23) 1)) +(declare-fun s24 () String) +(assert (= (str.len s24) 1)) +(declare-fun s25 () String) +(assert (= (str.len s25) 1)) +(declare-fun s26 () String) +(assert (= (str.len s26) 1)) +(declare-fun s27 () String) +(assert (= (str.len s27) 1)) +(declare-fun s28 () String) +(assert (= (str.len s28) 1)) +(declare-fun s29 () String) +(assert (= (str.len s29) 1)) +(declare-fun s30 () String) +(assert (= (str.len s30) 1)) +(declare-fun s31 () String) +(assert (= (str.len s31) 1)) +(declare-fun s32 () String) +(assert (= (str.len s32) 1)) +(declare-fun s33 () String) +(assert (= (str.len s33) 1)) +(declare-fun s34 () String) +(assert (= (str.len s34) 1)) +(declare-fun s35 () String) +(assert (= (str.len s35) 1)) +(declare-fun s36 () String) +(assert (= (str.len s36) 1)) +(declare-fun s37 () String) +(assert (= (str.len s37) 1)) +(declare-fun s38 () String) +(assert (= (str.len s38) 1)) +(declare-fun s39 () String) +(assert (= (str.len s39) 1)) +(declare-fun s40 () String) +(assert (= (str.len s40) 1)) +(declare-fun s41 () String) +(assert (= (str.len s41) 1)) +(declare-fun s42 () String) +(assert (= (str.len s42) 1)) +(declare-fun s43 () String) +(assert (= (str.len s43) 1)) +(declare-fun s44 () String) +(assert (= (str.len s44) 1)) +(declare-fun s45 () String) +(assert (= (str.len s45) 1)) +(declare-fun s46 () String) +(assert (= (str.len s46) 1)) +(declare-fun s47 () String) +(assert (= (str.len s47) 1)) +(declare-fun s48 () String) +(assert (= (str.len s48) 1)) +(declare-fun s49 () String) +(assert (= (str.len s49) 1)) +(declare-fun s50 () String) +(assert (= (str.len s50) 1)) +(declare-fun s51 () String) +(assert (= (str.len s51) 1)) +(declare-fun s52 () String) +(assert (= (str.len s52) 1)) +(declare-fun s53 () String) +(assert (= (str.len s53) 1)) +(declare-fun s54 () String) +(assert (= (str.len s54) 1)) +(declare-fun s55 () String) +(assert (= (str.len s55) 1)) +(declare-fun s56 () String) +(assert (= (str.len s56) 1)) +(declare-fun s57 () String) +(assert (= (str.len s57) 1)) +(declare-fun s58 () String) +(assert (= (str.len s58) 1)) +(declare-fun s59 () String) +(assert (= (str.len s59) 1)) +(declare-fun s60 () String) +(assert (= (str.len s60) 1)) +(declare-fun s61 () String) +(assert (= (str.len s61) 1)) +(declare-fun s62 () String) +(assert (= (str.len s62) 1)) +(declare-fun s63 () String) +(assert (= (str.len s63) 1)) +(declare-fun s64 () String) +(assert (= (str.len s64) 1)) +(declare-fun s65 () String) +(assert (= (str.len s65) 1)) +(assert (distinct +s1 +s2 +s3 +s4 +s5 +s6 +s7 +s8 +s9 +s10 +s11 +s12 +s13 +s14 +s15 +s16 +s17 +s18 +s19 +s20 +s21 +s22 +s23 +s24 +s25 +s26 +s27 +s28 +s29 +s30 +s31 +s32 +s33 +s34 +s35 +s36 +s37 +s38 +s39 +s40 +s41 +s42 +s43 +s44 +s45 +s46 +s47 +s48 +s49 +s50 +s51 +s52 +s53 +s54 +s55 +s56 +s57 +s58 +s59 +s60 +s61 +s62 +s63 +s64 +s65 +)) +(check-sat) diff --git a/test/regress/regress2/sygus/multi-udiv.sy b/test/regress/regress2/sygus/multi-udiv.sy index d9deb28a3..65e5d428f 100644 --- a/test/regress/regress2/sygus/multi-udiv.sy +++ b/test/regress/regress2/sygus/multi-udiv.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-active-gen=enum (set-logic BV) (define-fun hd05 ((x (_ BitVec 32))) (_ BitVec 32) (bvor x (bvsub x #x00000001))) diff --git a/test/regress/regress2/sygus/sets-fun-test.sy b/test/regress/regress2/sygus/sets-fun-test.sy index 43a8b36a9..23abc5c7e 100644 --- a/test/regress/regress2/sygus/sets-fun-test.sy +++ b/test/regress/regress2/sygus/sets-fun-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-active-gen=enum (set-logic ALL) (synth-fun f ((x Int)) (Set Int)) diff --git a/test/regress/regress2/sygus/three.sy b/test/regress/regress2/sygus/three.sy index 239f7f498..9bed1e667 100644 --- a/test/regress/regress2/sygus/three.sy +++ b/test/regress/regress2/sygus/three.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-active-gen=enum (set-logic NIA)