Constructing smtlib set_info

[anmaped]

There is a make function for Terms but it is not available in the signature. I think it should be mk instead.

I leave where an example

Dolmen.Statement.set_info ( Dolmen.Term.mk ( Dolmen.Term.Colon (
	    		Dolmen.Term.mk (Dolmen.Term.Symbol (Dolmen.Id.mk Dolmen.Id.Attr ":smt-lib-version") ),
	    		Dolmen.Term.mk (Dolmen.Term.Symbol (Dolmen.Id.mk Dolmen.Id.Term "2.5"))
	    	)
	))

We could also add mk_symbol, mk_colon etc. as shorthands.

Do you have pretty printers for smtlib? I'm interested in that.

[Gbury]

Not exporting make (or mk) was a conscious design choice. Instead, users should be encouraged to use the dedicate term building functions (e.g. Term.colon and Term.const in your example).

Admittedly, the documentation generated by ocamldoc doesn't really help in finding these functions in the Term module: they are part of the Term_intf.Logic signature included in the Term module, so ocamldoc only prints a single line stating the signature inclusion here:
http://gbury.github.io/dolmen/dev/Term.html#2_Implementedinterfaces
And thus almost all functions for building terms are documented here:
http://gbury.github.io/dolmen/dev/Term_intf.Logic.html

About printer for smtlib, I haven't implemented them yet. The most tricky part of printing terms in smtlib syntax is when the term printed comes from another language, for instance tptp: in that case, tptp constants (such as $i, $o, ...) should be translated into the corresponding term builtins in order to be printed correctly in smtlib... So basically, I need to implement a term normalizer together with the printing functions, ^^

[anmaped]

@Gbury Thanks for your support. Yes, I see the point.

Can we do the normalizer and the printing functions quickly? I can help you if you want.

[Gbury]

I'm currently finishing the writing of my thesis, so it's not really the best moment for me right now... How soon would you need the normalizer and printer ? I should have some time to work on that next week.

[Gbury]

Closing this issue in favour of #7 and #8 (the original problem is solved if I'm not mistaken).

[anmaped]

Yes. In this example, It should be

Statement.set_info ( Term.colon 
	    		(Term.const (Id.mk Id.Attr ":smt-lib-version"))
	    		(Term.const (Id.mk Id.Term "2.5"))
	    	)