search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.42k stars 1.47k forks source link

Slow simple regular expression #1121

Closed facferreira closed 4 years ago

facferreira commented 7 years ago

Hi, I have a more or less complex example that has several expressions, but noticed that one expression involving regular expressions is slowing extremely, making Z3 timeout (given an timeout of 10s).

(declare-datatypes () ((General (G_Boolean (of_G_Boolean Bool)) (G_Integer (of_G_Integer Int)) (G_String (of_G_String String)) (G_Null))))
(declare-sort SVMap)
(declare-sort IVMap)
(declare-datatypes () ((Value (G (out_G General)) (E (out_E SVMap)) (C (out_C IVMap)) (R (type String) (id Int)))))
(declare-datatypes () ((General (G_Boolean (of_G_Boolean Bool)) (G_Integer (of_G_Integer Int)) (G_String (of_G_String String)) (G_Null))))
(declare-datatypes () ((General (G_Boolean (of_G_Boolean Bool)) (G_Integer (of_G_Integer Int)) (G_String (of_G_String String)) (G_Null))))
(declare-sort SVMap)
(declare-sort IVMap)
(declare-datatypes () ((Value (G (out_G General)) (E (out_E SVMap)) (C (out_C IVMap)) (R (type String) (id Int)))))
(declare-datatypes () ((ValueOption (NoValue) (SomeValue (of_SomeValue Value)))))
(declare-sort IVMap)
(declare-sort SVMap)
(declare-fun r_resourceidof (Value Value) Value)
(declare-fun v_ff () Value)
(declare-fun In_String (Value) Bool)
(declare-fun r_representationof (Value Value) Value)
(declare-fun v_contains (Value Value) Value)
(declare-fun v_tt () Value)
(declare-fun v_nth (Value Value) Value)
(declare-fun v_integer (Int) Value)
(declare-fun v_length (Value) Value)
(declare-fun Good_C (Value) Bool)
(declare-fun alphai (IVMap) (Array Int ValueOption))
(declare-fun FiniteC ((Array Int ValueOption)) Bool)
(declare-fun betai ((Array Int ValueOption)) IVMap)
(declare-fun v_dot (String Value) Value)
(declare-fun Good_E (Value) Bool)
(declare-fun alphas (SVMap) (Array String ValueOption))
(declare-fun v_has_field (String Value) Bool)
(declare-fun FiniteE ((Array String ValueOption)) Bool)
(declare-fun betas ((Array String ValueOption)) SVMap)
(declare-fun v_string (String) Value)
(declare-fun O_LE (Value Value) Value)
(declare-fun O_LT (Value Value) Value)
(declare-fun O_GT (Value Value) Value)
(declare-fun O_GE (Value Value) Value)
(declare-fun O_Or (Value Value) Value)
(declare-fun O_And (Value Value) Value)
(declare-fun O_Minus (Value) Value)
(declare-fun O_Not (Value) Value)
(declare-fun O_NE (Value Value) Value)
(declare-fun O_EQ (Value Value) Value)
(declare-fun O_Mult (Value Value) Value)
(declare-fun O_Sub (Value Value) Value)
(declare-fun O_Sum (Value Value) Value)
(declare-fun In_Integer (Value) Bool)
(declare-fun In_Boolean (Value) Bool)
(declare-fun v_boolean (Bool) Value)
(declare-fun v_null () Value)
(declare-fun Good_R (Value) Bool)
(declare-fun maze () Value)
(declare-fun request () Value)
(declare-fun root () Value)
(assert (let ((a!1 (forall ((b Bool))
             (! (= (v_boolean b) (G (G_Boolean b))) :pattern ((v_boolean b)))))
      (a!2 (forall ((i Int))
             (! (= (v_integer i) (G (G_Integer i))) :pattern ((v_integer i)))))
      (a!3 (forall ((s String))
             (! (= (v_string s) (G (G_String s))) :pattern ((v_string s)))))
      (a!4 (forall ((v Value))
             (! (= (In_Boolean v) (and (is-G v) (is-G_Boolean (out_G v))))
                :pattern ((In_Boolean v)))))
      (a!5 (forall ((v Value))
             (! (= (In_Integer v) (and (is-G v) (is-G_Integer (out_G v))))
                :pattern ((In_Integer v)))))
      (a!6 (forall ((v Value))
             (! (= (In_String v) (and (is-G v) (is-G_String (out_G v))))
                :pattern ((In_String v)))))
      (a!7 (forall ((v1 Value) (v2 Value))
             (! (= (O_EQ v1 v2) (ite (= v1 v2) v_tt v_ff))
                :pattern ((O_EQ v1 v2)))))
      (a!8 (forall ((v1 Value) (v2 Value))
             (! (= (O_NE v1 v2) (ite (= v1 v2) v_ff v_tt))
                :pattern ((O_NE v1 v2)))))
      (a!9 (forall ((v Value))
             (! (= (O_Not v) (ite (not (= v v_tt)) v_tt v_ff))
                :pattern ((O_Not v)))))
      (a!10 (forall ((v1 Value) (v2 Value))
              (! (= (O_And v1 v2) (ite (and (= v1 v_tt) (= v2 v_tt)) v_tt v_ff))
                 :pattern ((O_And v1 v2)))))
      (a!11 (forall ((v1 Value) (v2 Value))
              (! (= (O_Or v1 v2) (ite (or (= v1 v_tt) (= v2 v_tt)) v_tt v_ff))
                 :pattern ((O_Or v1 v2)))))
      (a!12 (forall ((v Value))
              (! (let ((a!1 (= (str.len (of_G_String (out_G v)))
                               (of_G_Integer (out_G (v_length v))))))
                   (=> (and (is-G v) (is-G_String (out_G v))) a!1))
                 :pattern ((v_length v)))))
      (a!13 (forall ((v1 Value) (v2 Value))
              (! (let ((a!1 (ite (str.contains (of_G_String (out_G v1))
                                               (of_G_String (out_G v2)))
                                 v_tt
                                 v_ff)))
                   (=> (and (is-G v1)
                            (is-G_String (out_G v1))
                            (is-G v2)
                            (is-G_String (out_G v2)))
                       (= (v_contains v1 v2) a!1)))
                 :pattern ((v_contains v1 v2)))))
      (a!14 (forall ((v Value) (i Int))
              (! (let ((a!1 (v_string (str.at (of_G_String (out_G v)) i))))
                   (=> (and (is-G v) (is-G_String (out_G v)))
                       (= (v_nth v (v_integer i)) a!1)))
                 :pattern ((v_nth v (v_integer i))))))
      (a!15 (forall ((am (Array String ValueOption)))
              (=> (FiniteE am) (= (alphas (betas am)) am))))
      (a!16 (forall ((svm SVMap))
              (and (FiniteE (alphas svm)) (= (betas (alphas svm)) svm))))
      (a!17 (forall ((svm (Array String ValueOption)))
              (! (= (FiniteE svm) (= (default svm) NoValue))
                 :pattern ((FiniteE svm)))))
      (a!18 (forall ((l String) (svm SVMap))
              (! (let ((a!1 (not (= (select (alphas svm) l) NoValue))))
                   (= (v_has_field l (E svm)) a!1))
                 :pattern ((v_has_field l (E svm))))))
      (a!19 (forall ((l String) (svm SVMap))
              (! (= (v_dot l (E svm)) (of_SomeValue (select (alphas svm) l)))
                 :pattern ((Good_E (E svm)) (v_dot l (E svm))))))
      (a!20 (forall ((am (Array Int ValueOption)))
              (=> (FiniteC am) (= (alphai (betai am)) am))))
      (a!21 (forall ((ivm IVMap))
              (and (FiniteC (alphai ivm)) (= (betai (alphai ivm)) ivm))))
      (a!22 (forall ((ivm (Array Int ValueOption)))
              (! (= (FiniteC ivm) (= (default ivm) NoValue))
                 :pattern ((FiniteC ivm)))))
      (a!23 (forall ((v Value) (i Int))
              (! (let ((a!1 (of_SomeValue (select (alphai (out_C v)) i))))
                   (=> (Good_C v) (= (v_nth v (v_integer i)) a!1)))
                 :pattern ((Good_C v) (v_nth v (v_integer i))))))
      (a!24 (forall ((v1 Value) (v2 Value))
              (! (let ((a!1 (exists ((i Int))
                              (let ((a!1 (< i
                                            (of_G_Integer (out_G (v_length v1))))))
                                (and (<= 0 i)
                                     a!1
                                     (= (v_nth v1 (v_integer i)) v2))))))
                   (=> (and (is-C v1))
                       (= (v_contains v1 v2) (ite a!1 v_tt v_ff))))
                 :pattern ((v_contains v1 v2)))))
      (a!25 (forall ((v Value) (r Value))
              (! (=> (is-R r) (=> (is-R v) (= (r_representationof v r) v_ff)))
                 :pattern ((is-R r) (r_representationof v r)))))
      (a!26 (forall ((v Value) (r Value))
              (! (=> (is-R r)
                     (=> (not (In_String v)) (= (r_resourceidof v r) v_ff)))
                 :pattern ((is-R r) (r_resourceidof v r)))))
      (a!27 (v_boolean (and (Good_E (v_dot "template" request)))))
      (a!28 (forall ((|\|\\\\\\\|#3\\\\\\\|\|| Int))
              (let ((a!1 (= (type (v_nth maze
                                         (v_integer |\|\\\\\\\|#3\\\\\\\|\||)))
                            "Maze")))
                (and (Good_R (v_nth maze (v_integer |\|\\\\\\\|#3\\\\\\\|\||)))
                     a!1))))
      (a!29 (of_G_String (out_G (v_dot "name" (v_dot "body" request)))))
      (a!30 (re.union (re.union (re.union (re.range "a" "z") (re.range "A" "Z"))
                                (re.range "0" "9"))
                      (re.union (re.range " " " ")
                                (re.union (re.range "\x09" "\x09")
                                          (re.range "\n" "\n"))))))
(let ((a!31 (and (In_String (v_dot "name" (v_dot "body" request)))
                 (str.in.re a!29 ((_ re.loop 3 50) a!30)))))
(let ((a!32 (and (Good_E (v_dot "body" request))
                 (v_has_field "name" (v_dot "body" request))
                 (In_String (v_dot "name" (v_dot "body" request)))
                 (= (ite a!31 v_tt v_ff) v_tt))))
(let ((a!33 (O_And (ite (= v_tt (v_boolean a!32))
                        (v_boolean true)
                        (v_boolean false))
                   (O_EQ (v_nth maze (v_integer 1)) (v_nth maze (v_integer 2))))))
  (and (forall ((v Value)) (! (= (Good_C v) (is-C v)) :pattern ((Good_C v))))
       (forall ((v Value)) (! (= (Good_E v) (is-E v)) :pattern ((Good_E v))))
       (forall ((v Value)) (! (= (Good_R v) (is-R v)) :pattern ((Good_R v))))
       (= v_tt (G (G_Boolean true)))
       (= v_ff (G (G_Boolean false)))
       (= v_null (G G_Null))
       a!1
       a!2
       a!3
       a!4
       a!5
       a!6
       (forall ((v1 Value) (v2 Value))
         (! (let ((a!1 (v_integer (+ (of_G_Integer (out_G v1))
                                     (of_G_Integer (out_G v2))))))
              (= (O_Sum v1 v2) a!1))
            :pattern ((O_Sum v1 v2))))
       (forall ((v1 Value) (v2 Value))
         (! (let ((a!1 (v_integer (- (of_G_Integer (out_G v1))
                                     (of_G_Integer (out_G v2))))))
              (= (O_Sub v1 v2) a!1))
            :pattern ((O_Sub v1 v2))))
       (forall ((v1 Value) (v2 Value))
         (! (let ((a!1 (v_integer (* (of_G_Integer (out_G v1))
                                     (of_G_Integer (out_G v2))))))
              (= (O_Mult v1 v2) a!1))
            :pattern ((O_Mult v1 v2))))
       a!7
       a!8
       a!9
       (forall ((v Value))
         (! (let ((a!1 (v_integer (- (of_G_Integer (out_G v))))))
              (= (O_Minus v) a!1))
            :pattern ((O_Minus v))))
       a!10
       a!11
       (forall ((v1 Value) (v2 Value))
         (! (let ((a!1 (ite (>= (of_G_Integer (out_G v1))
                                (of_G_Integer (out_G v2)))
                            v_tt
                            v_ff)))
              (= (O_GE v1 v2) a!1))
            :pattern ((O_GE v1 v2))))
       (forall ((v1 Value) (v2 Value))
         (! (let ((a!1 (ite (> (of_G_Integer (out_G v1))
                               (of_G_Integer (out_G v2)))
                            v_tt
                            v_ff)))
              (= (O_GT v1 v2) a!1))
            :pattern ((O_GT v1 v2))))
       (forall ((v1 Value) (v2 Value))
         (! (let ((a!1 (ite (< (of_G_Integer (out_G v1))
                               (of_G_Integer (out_G v2)))
                            v_tt
                            v_ff)))
              (= (O_LT v1 v2) a!1))
            :pattern ((O_LT v1 v2))))
       (forall ((v1 Value) (v2 Value))
         (! (let ((a!1 (ite (<= (of_G_Integer (out_G v1))
                                (of_G_Integer (out_G v2)))
                            v_tt
                            v_ff)))
              (= (O_LE v1 v2) a!1))
            :pattern ((O_LE v1 v2))))
       a!12
       a!13
       a!14
       a!15
       a!16
       a!17
       (forall ((v Value))
         (! (let ((a!1 (and (is-E v) (FiniteE (alphas (out_E v))))))
              (= (Good_E v) a!1))
            :pattern ((Good_E v))))
       a!18
       a!19
       a!20
       a!21
       a!22
       (forall ((v Value))
         (! (let ((a!1 (and (is-C v) (FiniteC (alphai (out_C v))))))
              (= (Good_C v) a!1))
            :pattern ((Good_C v))))
       (forall ((v Value))
         (! (let ((a!1 (>= (of_G_Integer (out_G (v_length v))) 0)))
              (=> (Good_C v) a!1))
            :pattern ((Good_C v))))
       (forall ((v Value))
         (! (let ((a!1 (forall ((i Int))
                         (let ((a!1 (< i (of_G_Integer (out_G (v_length v)))))
                               (a!2 (is-SomeValue (select (alphai (out_C v)) i))))
                           (=> (and (<= 0 i) a!1) a!2)))))
              (= (Good_C v) a!1))
            :pattern ((Good_C v))))
       a!23
       a!24
       a!25
       a!26
       (In_String root)
       (Good_E request)
       (v_has_field "template" request)
       true
       (= a!27 v_tt)
       (v_has_field "header" request)
       (Good_E (v_dot "header" request))
       (v_has_field "location" request)
       (In_String (v_dot "location" request))
       (v_has_field "body" request)
       true
       (Good_C maze)
       a!28
       (= (O_EQ (v_length maze) (v_integer 3)) v_tt)
       (= a!33 v_tt)))))))

In the middle of the example, there is one expression

(str.in.re a!29 ((_ re.loop 3 50) a!30))

For easy reference,

(a!29 (of_G_String (out_G (v_dot "name" (v_dot "body" request)))))
(a!30 (re.union (re.union (re.union (re.range "a" "z") (re.range "A" "Z"))
                                (re.range "0" "9"))
                      (re.union (re.range " " " ")
                                (re.union (re.range "\x09" "\x09")
                                          (re.range "\n" "\n")))))

If this expression is present, Z3 timeouts after 10s. However, removing that same expression makes Z3 return "unknown" with a candidate model after just 0.08s.

Also, I tried to change the 3 of re.loop to 1 and it produced a result in less than 1s. Increasing that to 2 leads to timeout. One other attempt I did, was change a!30 to (re.range "a" "z"), which Z3 returned a result in less than 1s.

So, is it normal that a relatively simple regular expression leads to timeout?

Thanks.

NikolajBjorner commented 7 years ago

Thanks for the scenario.

@mtrberzi: it crashes with z3 smt.string_solver=z3str3

mtrberzi commented 7 years ago

@NikolajBjorner thanks, I'll look into this one (it may be due to having no implementation of re.loop but I'll double-check)

NikolajBjorner commented 5 years ago

is there an update on the z3str3 side?

mtrberzi commented 4 years ago

The example given is actually incomplete (no check-sat) and produces several parser errors referring to multiple declarations of several functions and sorts