Should the prefix "Ref" of data sort be removed when translating from SL-COMP'18 to SL-COMP'14 syntax?

[ghost]

Hi,

I notice that the tool slcomp-parser in smtlib2Xparser-sl always adds a prefix Ref in front of each sort when translating test cases from SL-COMP'18 format to SL-COMP'14 format (illustrated by 2 examples at the end of this post).

Is it possible to remove this prefix?

The reason is that if a test case is repeatedly translated from SL-COM18 format to other prover format, via the intermediate syntax of SL-COMP'14, then the prefix Ref will be duplicated many times.

For example, given a test case A in the SL-COMP'18 format, the problem arises by the following steps:

1. Translate A to a file B in SLEEK format (the data sort will be prefixed by Ref, because of the tool slcomp-parser).
2. Translate B to a file C in SL-COMP'18 format (the prefix Ref is unchanged)
3. Translate C to a file D in SLEEK format (now new the prefix of data sort will be RefRef, because of the tool slcomp-parser)

====================

Test case: 01.tst.smt2.sl14, generated by the tool slcomp-parser agains the file 01.tst.smt2 in the benchmarks of SL-COMP'18:

(set-logic QF_S)
(set-info :source |
  James Brotherston, Nikos Gorogiannis, and Rasmus Petersen
  A Generic Cyclic Theorem Prover. APLAS, 2012.
  https://github.com/ngorogiannis/cyclist
n|)

(set-info :smt-lib-version 2)
(set-info :category "crafted")
(set-info :status unsat)
(set-info :version "2014-05-31")

(declare-sort RefGTyp 0)

;; Declare cell type GTyp
(declare-fun f0 () (Field RefGTyp RefGTyp))

;; IGNORE declare-heap
(define-fun RList ((?x RefGTyp) (?y RefGTyp)) Space
  (tospace (or
            (and
             (distinct nil  ?x)
             (tobool (pto ?x (ref f0 ?y))))
            (exists ((?xp RefGTyp))
                    (and
                     (distinct nil  ?xp)
                     (tobool (ssep
                              (pto ?xp (ref f0 ?y))
                              (RList ?x ?xp))))))))

(check-sat)
(declare-fun x () RefGTyp)
(declare-fun y () RefGTyp)
(declare-fun z () RefGTyp)

(assert (tobool (ssep
                 (pto x (ref f0 y))
                 (RList y z))))

(assert (not (tobool (RList x z))))

(check-sat)

Test case: 01.tst.smt2 in the original benchmark SL-COMP'14

(set-logic QF_S)
(set-info :source |
  James Brotherston, Nikos Gorogiannis, and Rasmus Petersen
  A Generic Cyclic Theorem Prover. APLAS, 2012.
  https://github.com/ngorogiannis/cyclist
|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(set-info :version 2014-05-31)

;generic sort
(declare-sort GTyp 0)

;generic fields
(declare-fun f0 () (Field GTyp GTyp))
(declare-fun f1 () (Field GTyp GTyp))

(define-fun RList ((?x GTyp) (?y GTyp)) Space
  (tospace (or
            (and (distinct nil ?x)
                 (tobool (pto ?x  (ref f0 ?y))))
            (exists ((?xp GTyp))
                    (and (distinct ?xp nil)
                         (tobool
                          (ssep (pto ?xp  (ref f0 ?y))
                                (RList ?x ?xp))))))))

;;;x->y * RList(y,z) |- RList(x,z)

(declare-fun x () GTyp)
(declare-fun y () GTyp)
(declare-fun z () GTyp)

(assert (tobool (ssep
                   (pto x (ref f0 y))
                   (RList y z))))

(assert (not (tobool
                (RList x z))))

(check-sat)

[slcomp]

The problem comes from the fact that in SL-COMP'14 format, the declared-sort is interpreted as a reference to a cell and not as the type of the cell. The SL-COMP'18 format interprets declare-sort as a reference declaration and declare-datatype as a cell type declaration (not a reference). Therefore, the translation from '18 fields (constructor's argument names) to '14 fields has to add a 'Ref' prefix to the argument of the source sort. This can be changed in the translation from '18 to '14, but you shall be aware about this change of semantics.

[ghost]

Thank you for the clarification. Should it be considered as a bug of the SL-COMP'14 format? If it is the case, then will a direct translation from SL-COMP'18 format to each prover fix the problem?

[slcomp]

I plan indeed to include latter this week a direct translation from SL-COMP'18 format to each input format required by the participants. Of course, this is done only if the solver has not yet this translator.