Z3 Proofs and Reverse Unit Propagation

[HarryBryant99]

Hi,

I am looking into Z3 with the new proof format and in particular the RUP proofs. I just want to check the notations please?

rup [Or(a, b)]

• A new clause "a or b" is derived with the RUP property.

rup [a, b]

• A new clause "a and b" is derived?
• I just want to check that this is indeed a conjunction? From what I have seen the clauses derived in Reverse Unit Propagation are disjunctions. This notation has come in proofs where the Tseitin rule has come previously in the proof. I just want to check my derivation processes for this case are correct.

Any clarification on this would be greatly appreciated

Many thanks
Harry

[NikolajBjorner]

Yes, the second argument in the callback is a clause. The meaning is that it is the disjunction of formulas in the list.
A formula may be a disjunction.
This is a unit clause [Or(a,b)]
This is a binary clause [a, b]
They are logically equivalent but have different representations.
When z3 processes formulas it applies a Tseitin transformation to create clauses.
For the formula Or(a,b) it creates the following clauses:
[Not(Or(a,b)), a, b]
[Not(a), Or(a,b)]
[Not(b), Or(a,b)]
The justification for these clauses is "Tseitin".

Suppose that it learns [Or(a,b)], then RUP on the first clause produces rup, [a,b]
On the other hand, if it learns [a], then RUP on the second clause produces rup, [Or(a,b)]

[HarryBryant99]

Thank you for explaining it. Much apprieciated.