add owi replay

[zapashcanon]

No description provided.

[zapashcanon]

@filipeom, so I got the main mechanism working. Before completing this, I think it would be great if we could discuss the format used for representing model. I have a few questions:

• I'll have to parse models in Owi, but the printing is done in Smt.ml, should we implement the parsing in Smt.ml or Owi? Having both in Smt.ml will make it easier to detect new incompatibilities but I'm not sure it's usefull for Smt.ml to parse them.
• Is there a model format coming from the smtlib already?
• Would you be OK in using another format than S-expressions ? I'm thinking about scfg which would work quite well IMO while allowing to display more complex structures in the future while maintaining good readability (I find S-expressions less readable than scfg). Also, I'm the author of the OCaml implementaiton of scfg. :-)

I'm also wondering if I should keep this as an owi replay command or simply add a --replay-file argument to owi sym (or owi run ?) and even maybe owi c etc.

[filipeom]

I'll have to parse models in Owi, but the printing is done in Smt.ml, should we implement the parsing in Smt.ml or Owi? Having both in Smt.ml will make it easier to detect new incompatibilities but I'm not sure it's usefull for Smt.ml to parse them.

I think it makes sense to also have it in smtml, even if we just implement it in Owi. I'd like to be able to do to_string to print a model and of_string to parse it.

Is there a model format coming from the smtlib already?

The current format is not smtlib compliant, I'd have to go over the spec again to fix the model printing. But I can do this pretty quickly, and provide a of_string function as well if you would like

Would you be OK in using another format than S-expressions ? I'm thinking about scfg which would work quite well IMO while allowing to display more complex structures in the future while maintaining good readability (I find S-expressions less readable than scfg). Also, I'm the author of the OCaml implementaiton of scfg. :-)

Yes this is fine with me. If this is to be done in smtml, ideally we would support the three formats (smtlib, json, and scfg)

[filipeom]

I'm also wondering if I should keep this as an owi replay command or simply add a --replay-file argument to owi sym (or owi run ?) and even maybe owi c etc.

Regarding this, I like the --replay-file option in owi run. Although, it might make more sense to have it in owi sym so that it is easy to use with owi c. But I don't dislike having the owi replay command, so to me you can leave it as is.

[zapashcanon]

I made a draft PR in smtml for model parsing.

It makes sense in owi run but in owi sym unfortunately most options are incompatible with --replay-file. I think I'm going to leave it this way and think more about it.

I'll wait for the smtml model parsing to be done and then we should be good to go with this one ! :)

[filipeom]

smtml.0.4.0 already supports scfg model parsing. Do you want me to finish this PR?

From what I can tell this still needs:

• Output models in scfg in owi sym
• Floats (symbol_f32 and symbol_f64) and implement stubs for the remaining external functions
• Maybe one test

[zapashcanon]

Oh great! I did not see the release. I'll update the PR today, thanks! :)

[zapashcanon]

@filipeom, actually we'll probably have to change the API in smt.ml :/

The various to_scfg to_scfg_string should have a ~no_value parameter otherwise it's too cumbersome to use in Owi (we would need to traverse the model again to remove them and rebuild a new one, whereas in can be done more easily when building directly the correct model in scfg).

[filipeom]

The various to_scfg to_scfg_string should have a ~no_value parameter otherwise it's too cumbersome to use in Owi (we would need to traverse the model again to remove them and rebuild a new one, whereas in can be done more easily when building directly the correct model in scfg).

I completely forgot about this. I'll make a patch asap

[zapashcanon]

I made a PR in formalsec/smtml#256 ; everything is OK with it. We'll have to wait for it to be published in opam before merging. This leave me some time to write more tests. :-)

[zapashcanon]

@filipeom, there was a bug in the parsing of models. I made a PR in smtml formalsec/smtml#258 ; you can see the diff in the last commit where this patch is applied.

[filipeom]

Version 0.4.1 of smtml is live. I re-ran the CI but it fails because Cmd_replay.run's arguments are not named

[zapashcanon]

Great, thanks! IIRC the parsing fix is not in smtml.0.4.1, is it? If not, we'll have to wait for the next release before merging, otherwise the tests won't pass.

[zapashcanon]

It seems to be working, I'm a little bit surprised but let's merge... :)

[filipeom]

It seems to be working, I'm a little bit surprised but let's merge... :)

It should be working, version 0.4.1 includes formalsec/smtml#258