How to define a transducer for convolution/interleaving projection?

[hongjianjiang]

Hi,

I would like to ask how to define a transducer for a convolution/interleaving encoding in Z3-Noodler.

Background

In my setting, I have two strings x and y, and I encode them using a padded convolution encoding.

Intuitively, the convolution stores the two strings symbol by symbol. For example, without padding:

x = abc
y = 123
conv(x, y) = a1b2c3

Here, the odd positions of the encoded string correspond to symbols from x, and the even positions correspond to symbols from y.

I would like to define transducers or projection relations such that, given the encoded string,

str = a1b2c3

Z3-Noodler can recover or check:

x = abc
y = 123

More generally, I want to support padded convolution. If one component is shorter, a padding symbol is used. For example, using _ as the padding symbol:

x = ab
y = 123
conv(x, y) = a1b2_3

The projection should ignore the padding symbol, so the result should be:

x = ab
y = 123

Desired Relation

Ideally, I would like to express a ternary relation such as:

Conv(str, x, y)

where str is the convolution encoding of x and y.

Equivalently, it would also be fine to define two projection relations:

Proj1(str, x)
Proj2(str, y)

where:

• Proj1(str, x) extracts the symbols belonging to the first component and ignores padding.
• Proj2(str, y) extracts the symbols belonging to the second component and ignores padding.

Question

How should this convolution/interleaving projection be written using Z3-Noodler's SMT-LIB transducer syntax?

For example, is the intended approach to define two recursive transducers that scan the encoded string and alternate between the first and second component?

Conceptually, I want something like:

(set-logic QF_S)
(set-option :parse-transducers true)

; Proj1(encoded, x): extract symbols in odd positions, ignoring padding
; Proj2(encoded, y): extract symbols in even positions, ignoring padding

Or is there a better way to define the ternary convolution relation directly as:

Conv(str, x, y)

Example 1: Non-padded Case

I would like to check satisfiability of a formula like:

(assert (Conv "a1b2c3" x y))
(assert (= x "abc"))
(assert (= y "123"))
(check-sat)

or, using projections:

(assert (Proj1 "a1b2c3" x))
(assert (Proj2 "a1b2c3" y))
(assert (= x "abc"))
(assert (= y "123"))
(check-sat)

The expected result should be:

sat

Example 2: Padded Case

I would also like to support padding. For example, using _ as the padding symbol:

(assert (Conv "a1b2_3" x y))
(assert (= x "ab"))
(assert (= y "123"))
(check-sat)

or equivalently:

(assert (Proj1 "a1b2_3" x))
(assert (Proj2 "a1b2_3" y))
(assert (= x "ab"))
(assert (= y "123"))
(check-sat)

The expected result should also be:

sat

What I Am Unsure About

I am not sure how to express this correctly in Z3-Noodler's transducer syntax.

In particular:

1. Should I define two separate binary transducers Proj1 and Proj2?
2. Is it possible or recommended to define the ternary relation Conv(str, x, y) directly?
3. How should padding symbols be handled inside the transducer?
4. Could you provide a small complete SMT-LIB example for this kind of convolution/projection encoding?

Thank you very much!

[jurajsic]

Hi, currently, Z3-Noodler does not support parsing arbitrary transducers. The only way a transducer can be defined is trough replace_all operations.

However, we are planning to add the option to parse arbitrary transducers, probably trough the mata format. Then it would be possible to define transducers Proj1 and Proj2 from which you could define Conv.

Do you have an example of a formula showing how you would use Conv? Would you need it to be functional for the whole unicode/ascii or just for some limited alphabet?

[hongjianjiang]

Hi, thanks for the reply. My use case is to recover $n$ string variables from a given convolution-encoded string. More precisely, I would like to express a relation $Conv(w,x_1,\ldots,x_n)$,

where $w$ is the padded convolution encoding of the $n$ strings $x_1,\ldots,x_n$.

The variables may be symbolic, while $w$ may additionally be constrained by a regular language. I need the relation to be functional from $w$ to the tuple $(x_1,\ldots,x_n)$: for every well-formed encoded string $w$, the projected component strings should be uniquely determined.

It is sufficient for this to work over a fixed, limited alphabet; support for the full ASCII or Unicode alphabet is not required.

[jurajsic]

I added a support for reasoning about rational relations with some basic operations in https://github.com/VeriFIT/z3-noodler/tree/rational_relations.
Can you try playing with it if it works for you?
You can find the explanations for the operations. For your use case, you can define the projection operations (for n=2) for example as

(define-fun proj1 () RatRel
   (rat.++
      (rat.* (rat.++ (rat.identity (re.diff re.allchar (str.to_re "_"))) (rat.left re.allchar)))
      (rat.* (rat.++ (rat.left (str.to_re "_")) (rat.left re.allchar)))
   )
)
(define-fun proj2 () RatRel
   (rat.++
      (rat.* (rat.++ (rat.left re.allchar) (rat.identity (re.diff re.allchar (str.to_re "_")))))
      (rat.* (rat.++ (rat.left re.allchar) (rat.left (str.to_re "_"))))
   )
)

To check if Conv(str, x, y)holds, you can then write

(assert (str.in_rat str x proj1))
(assert (str.in_rat str y proj2))

[jurajsic]

If you have any questions how to use the operations, please ask.

[jurajsic]

Just for completion, for this formula:

(set-option :produce-models true)
(define-fun proj1 () RatRel
   (rat.++
      (rat.* (rat.++ (rat.identity (re.diff re.allchar (str.to_re "_"))) (rat.left re.allchar)))
      (rat.* (rat.++ (rat.left (str.to_re "_")) (rat.left re.allchar)))
   )
)
(define-fun proj2 () RatRel
   (rat.++
      (rat.* (rat.++ (rat.left re.allchar) (rat.identity (re.diff re.allchar (str.to_re "_")))))
      (rat.* (rat.++ (rat.left re.allchar) (rat.left (str.to_re "_"))))
   )
)

(declare-const str String)
(declare-const x String)
(declare-const y String)

(assert (str.in_rat str x proj1))
(assert (str.in_rat str y proj2))

(assert (= str "a1b2c3"))

(check-sat)
(get-model)

Z3-Noodler built in that branch returns:

sat
(
  (define-fun y () String
    "123")
  (define-fun x () String
    "abc")
  (define-fun proj1 () RatRel
    (let ((a!1 (rat.++ (rat.identity (re.diff re.allchar (str.to_re "_")))
                   (rat.left re.allchar)))
      (a!2 (rat.* (rat.++ (rat.left (str.to_re "_")) (rat.left re.allchar)))))
  (rat.++ (rat.* a!1) a!2)))
  (define-fun proj2 () RatRel
    (let ((a!1 (rat.++ (rat.left re.allchar)
                   (rat.identity (re.diff re.allchar (str.to_re "_")))))
      (a!2 (rat.* (rat.++ (rat.left re.allchar) (rat.left (str.to_re "_"))))))
  (rat.++ (rat.* a!1) a!2)))
  (define-fun str () String
    "a1b2c3")
)

[hongjianjiang]

Hi, thanks for this update. It solves my problem partially. While running my program, it returns unknown for the below fomula:

 (set-option :produce-models true)
(define-fun proj1 () RatRel
  (rat.++
    (rat.* (rat.++ (rat.identity (re.diff re.allchar (str.to_re "p"))) (rat.++ (rat.left re.allchar) (rat.left re.allchar))))
    (rat.* (rat.++ (rat.left (str.to_re "p")) (rat.++ (rat.left re.allchar) (rat.left re.allchar))))))
(define-fun proj2 () RatRel
  (rat.++
    (rat.* (rat.++ (rat.left re.allchar) (rat.++ (rat.identity (re.diff re.allchar (str.to_re "p"))) (rat.left re.allchar))))
    (rat.* (rat.++ (rat.left re.allchar) (rat.++ (rat.left (str.to_re "p")) (rat.left re.allchar))))))
(define-fun proj3 () RatRel
  (rat.++
    (rat.* (rat.++ (rat.left re.allchar) (rat.++ (rat.left re.allchar) (rat.identity (re.diff re.allchar (str.to_re "p"))))))
    (rat.* (rat.++ (rat.left re.allchar) (rat.++ (rat.left re.allchar) (rat.left (str.to_re "p")))))))
(declare-fun varout () String)
(assert (let ((a!1 (re.* (re.union (re.union (str.to_re "b") (str.to_re "a"))
                           (str.to_re "p")))))
  (str.in_re varout a!1)))
(declare-fun varin () String)
(assert (let ((a!1 (re.* (re.union (re.union (str.to_re "b") (str.to_re "a"))
                           (str.to_re "p")))))
  (str.in_re varin a!1)))
(declare-fun rem () String)
(declare-fun out1 () String)
(declare-fun out2 () String)
(declare-fun isin () Bool)
(declare-fun isout () Bool)
(assert (let ((a!1 (str.in_re out1 (re.* (re.union (str.to_re "a") (str.to_re "b")))))
      (a!2 (str.in_re out2 (re.* (re.union (str.to_re "a") (str.to_re "b")))))
      (a!3 (re.* (re.union (re.union (str.to_re "b") (str.to_re "a"))
                           (str.to_re "p")))))
  (or (and true
           a!1
           a!2
           (str.in_re rem a!3)
           (str.in_re out1 a!3)
           (str.in_re out2 a!3)
           (str.in_rat varin (str.++ "a" rem) proj1)
           (str.in_rat varin (str.++ out1 "b") proj2)
           (str.in_rat varin (str.++ out2 "b") proj3)
           isin
           (str.in_rat varout rem proj1)
           (str.in_rat varout out1 proj2)
           (str.in_rat varout out2 proj3)
           isout))))
(assert (let ((a!1 (re.++ (re.union (str.to_re "b") (str.to_re "a"))
                  (re.* (re.union (str.to_re "b") (str.to_re "a")))))
      (a!3 (re.++ (re.* (re.union (str.to_re "b") (str.to_re "a")))
                  (str.to_re "p"))))
(let ((a!2 (re.++ (re.* (re.union (str.to_re "b") (str.to_re "a")))
                  (re.union (str.to_re "") a!1)))
      (a!4 (re.union (str.to_re "p")
                     (re.++ (re.union (str.to_re "b") (str.to_re "a")) a!3))))
(let ((a!5 (re.++ (re.* (re.union (str.to_re "b") (str.to_re "a"))) a!4)))
(let ((a!6 (re.* (re.union (str.to_re "b") (re.++ (str.to_re "a") a!5))))
      (a!11 (re.union (re.union (str.to_re "b") (str.to_re "a"))
                      (re.++ (str.to_re "p") a!5))))
(let ((a!7 (re.++ (re.union (str.to_re "b") (re.++ (str.to_re "a") a!5))
                  (re.++ a!6 (re.++ (str.to_re "a") a!2))))
      (a!9 (re.++ (re.union (str.to_re "b") (re.++ (str.to_re "a") a!5))
                  (re.++ a!6 (str.to_re "p")))))
(let ((a!8 (re.++ a!6 (re.union (re.++ (str.to_re "a") a!2) a!7)))
      (a!10 (re.++ a!5 (re.++ a!6 (re.union (str.to_re "p") a!9))))
      (a!12 (re.++ a!11 (re.++ a!6 (re.union (str.to_re "p") a!9)))))
(let ((a!13 (re.union (re.union (str.to_re "") (re.++ (str.to_re "p") a!2))
                      (re.++ a!11 a!8))))
(let ((a!14 (re.union a!13 (re.++ a!12 (re.++ (re.* a!12) a!13)))))
(let ((a!15 (re.union (re.union a!2 (re.++ a!5 a!8))
                      (re.++ a!10 (re.++ (re.* a!12) a!14)))))
  (str.in_re varin a!15)))))))))))
(assert (let ((a!1 (re.++ (re.* (re.union (str.to_re "b") (str.to_re "a")))
                  (str.to_re "p"))))
(let ((a!2 (re.union (str.to_re "p")
                     (re.++ (re.union (str.to_re "b") (str.to_re "a")) a!1))))
(let ((a!3 (re.++ (re.* (re.union (str.to_re "b") (str.to_re "a"))) a!2)))
(let ((a!4 (re.* (re.union (str.to_re "b") (re.++ (str.to_re "a") a!3))))
      (a!9 (re.union (re.union (str.to_re "b") (str.to_re "a"))
                     (re.++ (str.to_re "p") a!3))))
(let ((a!5 (re.++ (re.union (str.to_re "b") (re.++ (str.to_re "a") a!3)) a!4))
      (a!7 (re.++ (re.union (str.to_re "b") (re.++ (str.to_re "a") a!3))
                  (re.++ a!4 (str.to_re "p")))))
(let ((a!6 (re.++ a!3 (re.++ a!4 (re.union (str.to_re "") a!5))))
      (a!8 (re.++ a!3 (re.++ a!4 (re.union (str.to_re "p") a!7))))
      (a!10 (re.++ a!9 (re.++ a!4 (re.union (str.to_re "p") a!7))))
      (a!11 (re.++ a!9 (re.++ a!4 (re.union (str.to_re "") a!5)))))
(let ((a!12 (re.union a!11 (re.++ a!10 (re.++ (re.* a!10) a!11)))))
(let ((a!13 (re.union a!6 (re.++ a!8 (re.++ (re.* a!10) a!12)))))
  (str.in_re varout a!13))))))))))
(check-sat)

The large regular expression is basically a three-state automaton, I give the graphviz format:

digraph {
init_s0 [shape = point]; init_s0 -> s0;
s0 [shape=doublecircle];
s0 -> s2 [label="a"];
s0 -> s2 [label="b"];
s0 -> s1 [label="p"];
s2 -> s1 [label="a"];
s2 -> s0 [label="b"];
s2 -> s0 [label="p"];
s1 [shape=doublecircle];
s1 -> s2 [label="a"];
s1 -> s2 [label="b"];
s1 -> s2 [label="p"];
}

[jurajsic]

That is a limitation of our decision procedure in Z3-Noodler for transducers. More specifically, the problem is in:

           (str.in_rat varin (str.++ "a" rem) proj1)
           (str.in_rat varin (str.++ out1 "b") proj2)
           (str.in_rat varin (str.++ out2 "b") proj3)
           (str.in_rat varout rem proj1)
           (str.in_rat varout out1 proj2)
           (str.in_rat varout out2 proj3)

This constraint is not chain-free (see this paper for the definition, basically because both varin and varout are twice on one side with for example rem and out1 also twice, there is a cycle in the inclusion graph that goes into our decision procedure). Currently, we are not able to solve such constraints with transducers.

I will try to think if it is possible to add some simple preprocessing rule that could solve such constraints, because I feel this should be solvable. Just a question though, is the given formula an example of formulas that come from your problem, or is it just a part of some larger formula? If there is something more, then it could be harder.

[hongjianjiang]

I see! I am working on the synthesis of the invariant for constraint horn clauses over strings, where Z3-Noodler serves as the oracle. And the invariant is for an uninterpreted relation for now, that's why I want to use the transducer. This given formula is the last check that failed.