PPTransSMT: incorrect translation for B definitions

[VTrelat]

Mostly to @DavidDeharbe: See file ppTrans.cpp function ppTrans_mem: https://github.com/CLEARSY/pptranssmt/blob/09b5a4bcebce292b25c7dfb5cf6e7ce42812fc05/PPTRANSSMT/ppTrans.cpp#L1877-L1922

• Issue: Axioms (defined as constants) defining B constants like NAT, INT, etc are added as follows (e.g. for NAT):

  (define-fun ... () Bool (forall ( (x Int) ) (= (and (<= 0 x) (<= x MaxInt)) (and (>= x 0) (<= x MaxInt)))))

  namely $\forall x: \texttt{Int}.\ (0 \leq x \land x \leq \texttt{MaxInt}) \iff (x \geq 0 \land x \leq \texttt{MaxInt})$

  The theory solver probably trivially reduces this assertion to $\forall x. \top$ using reflexivity of $\leq$ and together with the SAT solver this constant is probably simply reduced to True. I think this is not what we want. Fortunately, this does not corrupt the proof since any proof obligation of the form x : NAT is translated to and (<= 0 x) (<= x MaxInt). This is useless though.

• Fun fact Translating NAT = {nn | nn : NAT} leads to an assertion identical to the aforesaid constant

• Possible fix: I think the correct definition should be similar to (e.g. for NAT) either an axiom (conjunctly added when needed):

  (define-fun |def_B definitions_0| () Bool (forall ((x Int)) (and (<= 0 x) (<= x MaxInt))))

  or directly as a set (through a define-fun or an assert statement):

  (define-fun |def_B definitions_0| () Bool (forall ( (x Int) ) (= (mem0 x NAT) (and (>= x 0) (<= x MaxInt)))))

[dde-cls]

(define-fun |def_B definitions_0| () Bool (forall ((x Int)) (and (<= 0 x) (<= x MaxInt))))

SMT-Lib's Int is the set of all numerals, so the above constant is false since (+ 1 Maxint) is an Int. This is not what we want.

(define-fun |def_B definitions_0| () Bool (forall ( (x Int) ) (= (mem0 x NAT) (and (>= x 0) (<= x MaxInt)))))

That would be ok, and we could then suppress rewriting of NAT in the encoder.

My thoughts:

• The current situation results in inserting axioms that are useless. This is not a threat to validity, and does not seem to pose performance problems either.

• Adding an explict axiomatization as you suggested puts the burden on the solver to be aware of what NAT is and to reason about it. This is not a threat to validity and would probably not have a meaningful impact on performance.

• Another solution would be to stop writing the useless axioms (useless because all instances of NAT and INT are rewritten).

One unwritten requirement of ppTransXXX is that it should be possible to obtain a meaningful unsat core from the produced output. Assume a goal is proved because of an assertion using NAT, say the goal is 0 : NAT. The encoded goal would then be roughly (and (<= 0 0) (<= 0 <MAXINT>)) and a minimal unsat core would be (goal). This is satisfying as long as we assume that any prover would be able to prove a POG file with the single goal 0: NAT, which would be the case if we assume that the B definitions is always present in such POG file.

Remark If an encoder choses to expand the definitions of the sets NAT and INT, then

1. It shall not output axioms corresponding to the Define name="B definitions" element.
2. The contents of that element should be added to the unsat core produced by any proof stemming from the resulting encoding.

Conclusion For PPTransTPTP and PPTRANSSMT, we should chose one of

1. Keep rewriting NAT and INT and stop producing output for the Define name="B definitions" element. Any unsat core obtained with this approach should be extended with the definitions of NAT and INT.
2. Stop rewriting NAT and INT and keep producing an output for Define name="B definitions" (which should then be meaningful as the rewrite inside it would not occur).

P.S. Check what happens with NAT, NAT1, NATURAL, NATURAL1.

[dde-cls]

PPTrans* no longer process hypotheses in "B definitions".