100x speedup when using smt.string_solver=z3str3

[OrenGitHub]

Hi, Regarding issue #1614, we ran the following query with and without smt.string_solver=z3str3. The speedup in favor of smt.string_solver=z3str3 was the biggest we've seen so far (100x) We wanted to know if there are known heuristics for choosing z3str3? Is this related to #1672? Here is the query:

(declare-fun AB_serial_1_version_0 () String)
(declare-fun AB_serial_1_version_1 () String)
(declare-fun AB_serial_2_version_0 () String)
(declare-fun AB_serial_2_version_1 () String)
(declare-fun AB_serial_3_version_0 () String)
(declare-fun AB_serial_3_version_1 () String)
(declare-fun pre800 () String)
(declare-fun pre_tag801 () String)
(declare-fun pre803 () String)
(declare-fun pre_tag804 () String)
(declare-fun pre806 () String)
(declare-fun pre_tag807 () String)
(assert (= (str.len AB_serial_1_version_0) 32))
(assert (= (str.len AB_serial_1_version_1) (str.len AB_serial_1_version_0)))
(assert (= (str.at AB_serial_1_version_1 31) (seq.unit #x00)))
(assert (= (str.len AB_serial_2_version_0) 32))
(assert (= (str.len AB_serial_2_version_1) (str.len AB_serial_2_version_0)))
(assert (= (str.at AB_serial_2_version_1 31) (seq.unit #x00)))
(assert (= (str.len AB_serial_3_version_0) 32))
(assert (= (str.len AB_serial_3_version_1) (str.len AB_serial_3_version_0)))
(assert (= (str.at AB_serial_3_version_1 31) (seq.unit #x00)))
(assert (not (str.contains pre800 "M")))
(assert (not (str.contains pre800 "T")))
(assert (not (str.contains pre800 "\x00")))
(assert (or (str.contains pre_tag801 "M")
    (str.contains pre_tag801 "T")
    (str.contains pre_tag801 "\x00")))

(assert (str.prefixof pre800 (str.substr AB_serial_1_version_1 0 (- 32 0))))

(assert (str.prefixof pre_tag801 (str.substr AB_serial_1_version_1 0 (- 32 0))))
(assert (= (+ 1 (str.len pre800)) (str.len pre_tag801)))
(assert (< 27 (- (+ 93948521521952 (str.len pre800)) 93948521521952)))
(assert (not (str.contains pre803 "M")))
(assert (not (str.contains pre803 "T")))
(assert (not (str.contains pre803 "\x00")))
(assert (or (str.contains pre_tag804 "M")
    (str.contains pre_tag804 "T")
    (str.contains pre_tag804 "\x00")))

(assert (str.prefixof pre803 (str.substr AB_serial_2_version_1 0 (- 32 0))))

(assert (str.prefixof pre_tag804 (str.substr AB_serial_2_version_1 0 (- 32 0))))
(assert (= (+ 1 (str.len pre803)) (str.len pre_tag804)))
(assert (< 27 (- (+ 93948521522800 (str.len pre803)) 93948521522800)))
(assert (not (str.contains pre806 "M")))
(assert (not (str.contains pre806 "T")))
(assert (not (str.contains pre806 "\x00")))
(assert (or (str.contains pre_tag807 "M")
    (str.contains pre_tag807 "T")
    (str.contains pre_tag807 "\x00")))

(assert (str.prefixof pre806 (str.substr AB_serial_3_version_1 0 (- 32 0))))

(assert (str.prefixof pre_tag807 (str.substr AB_serial_3_version_1 0 (- 32 0))))
(assert (= (+ 1 (str.len pre806)) (str.len pre_tag807)))
(assert (let ((a!1 (< 27 (- (+ 93948521524832 (str.len pre806)) 93948521524832))))
  (not (not a!1))))
(check-sat)
(get-value (pre800 pre_tag801 AB_serial_1_version_1))

Here are the responses: with smt.string_solver=z3str3, 1 sec.

sat
((pre800 "aaaaaaaaaaaaaaaaaaaaaaaaaaaad")
 (pre_tag801 "aaaaaaaaaaaaaaaaaaaaaaaaaaaad\x00")
 (AB_serial_1_version_1 "aaaaaaaaaaaaaaaaaaaaaaaaaaaad\x00s\x00"))

without it, 120 sec.

sat
((pre800 "\x04� @@\x08\x01\x01\x10\x08\x10\x01\x10 (�@\x01\x10\x01\x01\x04\x04\x10\x10� @")
 (pre_tag801 "\x04� @@\x08\x01\x01\x10\x08\x10\x01\x10 (�@\x01\x10\x01\x01\x04\x04\x10\x10� @\x00")
 (AB_serial_1_version_1 "\x04� @@\x08\x01\x01\x10\x08\x10\x01\x10 (�@\x01\x10\x01\x01\x04\x04\x10\x10� @\x00\x04\x00\x00"))

[NikolajBjorner]

this is great for z3str3. It is a longer standing issue that the seq solver is very poor on negated contains constraints. I will have to reconsider how to handle this from scratch (or take clues from what others do). So far z3str3 was not the default solver until it could handle quantified formulas and other arbitrary formulas users throw at it. This is getting there so let me know if we should change the default.

[OrenGitHub]

@NikolajBjorner thanks, most kinds of queries we generate have similar running times for z3 and z3str3. The above example is strictly in favor of z3str3, and #1678 is clearly in favor of z3 (unless it's a bug?). It looks like the example below (from #1516) in which z3str3 is 1000x faster than z3 is caused too by negated contains constraints (originating from the indexof original constraint) right?

(declare-const dst    String)
(declare-const src    String)

(assert (= (str.len dst) 1025))
(assert (= (str.len src) 1050))

(assert (< (str.len dst) (str.indexof src "\x00" 0)))

(check-sat)
(get-value (dst src))

[NikolajBjorner]

BTW, z3str3 now diverges or takes a long time on this one.