CODEWITHSUNDEEP
z3smt
0mer
0mer

Reputation: 45

Implement a formula that simulate the string Contains method

I'm trying to implement the String.Containts function. I have written some simple tests case, but the following one (which should return UNSAT) return SAT.

The test try to match the substring 'bd' in the string 'abcd' by comparig all possible substrings with the string wanted (text taken from the Z3 output):

{(exists ((i Int))
  (let ((a!1 (forall ((k Int))
               (and (>= k i)
                    (<= k (+ i 1))
                    (= (select stringToScan k) (select substring (- k i)))
                    (= (select stringToScan 0) #x0061)
                    (= (select stringToScan 1) #x0062)
                    (= (select stringToScan 2) #x0063)
                    (= (select stringToScan 3) #x0064)
                    (= (select stringToSearch 0) #x0062)
                    (= (select stringToSearch 1) #x0064)))))
    (and (>= i 0)
         (< i 2)
         a!1
         (= (select substring 0) (select stringToSearch 0))
         (= (select substring 1) (select stringToSearch 1)))))}

I have tried various implementation, but without any success.

Upvotes: 0

Views: 125

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 111

If you assert the formula, it returns UNSAT.

http://rise4fun.com/Z3/szN

The part:

(forall ((k Int))
           (and (>= k i)
                (<= k (+ i 1)) ...)))

is false becuase you can set k to i + 2 or i - 1. You probably mean to write an implication instead of a conjunction. Sometimes using arrays for strings is not the best way to perform the encoding. The automata toolkit (see: http://rise4fun.com/Rex ) uses sequences.

Upvotes: 1

Related Questions