Translation from Ivy to mypyvy

[dranov]

This PR adds a method to automatically translate Ivy specifications to mypyvy.

This works by retrofitting the SMT-LIB generated by Ivy into mypyvy syntax, so the resulting mypyvy specifications are quite a bit uglier than those a human would write.

You invoke the method by adding attribute method = convert_to_mypyvy in the isolate that needs to be translated (or at the top-level of the Ivy file), and then invoke ivy_check on the file. When invoked with the convert_to_mypyvy method, ivy_check takes two (optional, default to false) arguments:

• unfold_macros=true/false – determines whether macro definitions in the SMT-LIB generated by Ivy are unfolded (unfolding macros results in larger mypyvy transitions, but with fewer variables; these are more similar to what humans would write and might be easier for the SMT solver in certain cases)
• simplify=true/false – determines whether Z3's ctx-solver-simplify tactic is applied; this uses Z3 to remove redundant clauses in the SMT-LIB generated by Ivy, but this can take on the order of hours for larger Ivy specifications; when simplify=false, the much faster (but less effective) ctx-simplify tactic is used

The converted mypyvy specification is generated in the directory in which ivy_check is invoked and takes the name of the Ivy specification, e.g. tpc.ivy becomes tpc.pyv.

In terms of implementation:

• I have ported two files from mypyvy, syntax.py and utils.py so we generate mypyvy specifications directly in mypyvy's internal representation and use mypyvy's own pretty-printer. Both Ivy and mypyvy are MIT licensed. Would it be preferable to depend on mypyvy as package rather than copy the files?

• The only change I have made to Ivy proper is in ivy_solver.py, to disable some trivial optimizations of the generated SMT-LIB. As part of the translation (more specifically, the simplifications via Z3), I have added code to translate SMT-LIB generated by Ivy back into Ivy formulas and added a round-tripping test (Ivy -> SMT-LIB -> Ivy) to ensure my translation was faithful. I've disabled those simplifications in ivy_solver.py because they prevented my round-tripping tests from working.

Due to how it works (by leveraging Ivy's translation to SMT-LIB), the translation should support all Ivy features and it should require little to no maintenance if/when the language evolves. I have tested this only with Ivy specifications with #lang ivy1.7 and #lang ivy1.8.

To give you a sense of what the output looks like, this Ivy specification is translated into this .pyv file.

[dranov]

This doesn't yet handle native integers in the Ivy spec.