Typo in smtlib grammar

[anmaped]

function_def:
  | s=SYMBOL OPEN args=sorted_var* CLOSE ret=sort body=term CLOSE
{ I.(mk term s), args, ret, body }

The last CLOSE is a typo. It should be removed.

[Gbury]

You're right, I'll fix that. By the way, would you have some files on which dolmen fails currently because of this typo ? I could add them to the testsuite ( https://github.com/Gbury/dolmen/tree/master/tests/smtlib ).

[anmaped]

Yes. You could use one of these examples:

(declare-datatypes () ((Threevalue (TVTRUE) (TVFALSE) (TVUNKNOWN) )))
(define-fun tvnot ((phi Threevalue)) Threevalue
	(ite (= phi TVTRUE) TVFALSE (ite (= phi TVFALSE) TVTRUE TVUNKNOWN) )
)

(declare-datatypes () ((Threevalue (TVTRUE) (TVFALSE) (TVUNKNOWN) )))
(define-fun tvor ((phi1 Threevalue) (phi2 Threevalue)) Threevalue
	(ite (or (= phi1 TVTRUE) (= phi2 TVTRUE) ) TVTRUE (ite (and (= phi1 TVFALSE) (= phi2 TVFALSE)) TVFALSE TVUNKNOWN ) )
)

If you want some use case tests for the smtlib pretty printer, I can provide some ocaml code as well.

By the way, I also noted that comments in smtlib are not allowed by the parser.

[Gbury]

Closed with the last commits. Note that the files in your last comment are not valid in smtlib v2.6 because of the datatype declaration (see https://github.com/Gbury/dolmen/blob/master/tests/smtlib/test-fun_def_1.smt2 for instance).

[anmaped]

Yes. It's right. I just copy paste the data type to the example to be self-contained. Thanks.