Tseitin Transformation with Z3 and final output Variable

[Flessent]

Hey,
I'm actually working with Z3-Solver. I constructed a Z3 formula based on my CNF in Dimacs format and applied Tseitin Transformation on my Z3 formula.
I construted the Z3 formula on CNF like following. Assuming that we have this CNF in Dimacs format :
p cnf 3 3
1 -2 0
3 2 -1 0
-3 0
The Z3 Formula is : And( Or (x_1 , Not(x_2) , Or(x_3, x_2 ,Not(x_1) ) , Or(Not(x_3) ) )
Let us call this fomula the_formula
Then applied Tseitin using tactic :
g = Goal()
g.add(the_formula)
t = Tactic('tseitin-cnf')
print(t(g))
It prints exactly the Z3 formula unchanged.
What I know about Tseitin Transformation is the basic principle of Bi-Implication rule (o<-> input)and the final output variable of the whole formula at the end since Tseitin introduces new auxiliary or intermediate variables for building each sub-fomula and its outputs. My qeuestion are why I can't see new introduced variables with Tactic ? and how can I get the final output variable of my Tseitin transformation ?

Thanks

[ThomasHaas]

Isn't the purpose of Tseitin to convert non-CNF formulas into CNF? If you start with a CNF, I would expect nothing to happen.

[ThomasHaas]

It is unlikely that Z3 applies the transformation blindly like this because it would result in more complex formulas, i.e., it would be a counter-productive transformation.
If you want to force Tseitin transformation on a CNF F, you can probably construct the non-CNF formula F' = A /\ F (A is some new atom) forcing F to be a proper subexpression.

[Flessent]

If I should define a certain F' als F'= A ^F , how should A be declared or defined ? Since my purpose is to obtain a variable at the end as output of a whole formula. That is why I firstly think of Tseitin transformation. Or otherweise is there a possibility for Tactic to return an output variable of the whole formula ?

[ThomasHaas]

Oh, I meant to say F' = A \/ F (the other formula would be in CNF again).
I'm not sure what your goal is, but you could also start from y <=> Fand then apply Tseitin. The fresh variable y will be equivalent to your formula (by definition) and you won't need to care about the intermediary variables at all (those are only to achieve CNF).

[Flessent]

Yesssss that is the point. y <-> F.

Thanks ThomasHaas