Typo in smtlib grammar about dolmen HOT 4 CLOSED

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 ).

from dolmen.

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.

from dolmen.

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).

from dolmen.

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

from dolmen.