Bv synonyms

[typerSniper]

feat: /useBvSynonyms flag to use bv synonyms. Instead of defining bit vector operations directly as Z3 builtins, I add a dafny level function with an axiom saying that it is equal to the builtin. Just like multiplication.

I've also inserted split_here assertions to make one of the tests go through faster.

Future Work: Allow synonyms and builtins to be used at a finer granularity, i.e., let the programmer control for each method/function, whether or not the synonyms are used.

[typerSniper]

@RustanLeino, I couldn't figure out some of the code formatting errors. It looks like a recent change?

[keyboardDrummer]

@RustanLeino, I couldn't figure out some of the code formatting errors. It looks like a recent change?

You can run dotnet-format -w Source/Dafny.sln to resolve them, although if you're editing with Rider/Visual Studio I wouldn't expect them to occur. You can also use pre-commit to run the dotnet-format command on your commits.

[typerSniper]

That works! Thanks

[typerSniper]

@RustanLeino, can you take a look and merge ;p

[RustanLeino]

Looks good, and I have but one comment: Please make the flag /useBvSynonyms take an argument (like 0 or 1). This will make it easier for us to change the default of this option in the future, without breaking anyone using the switch already.

[typerSniper]

I updated the flag to take a 0/1 argument.

@RustanLeino, @keyboardDrummer, the failing case is a SegFault during build. Can you take a look?

[keyboardDrummer]

@RustanLeino, @keyboardDrummer, the failing case is a SegFault during build. Can you take a look?

Not sure what causes those. Restarted the build.