Modify the SMT-LIB printer to declare arrays in a deterministic (alphabetical) order.

[pcc]

I also reformatted the SMT-LIB printer with clang-format for consistency with the rest of KLEE.

[delcypher]

Thanks peter. I had been meaning to reformat that code for a while.

The code looks fine at a glance. I'm curious though, what is the motivation for wanting arrays declared in a deterministic order?

[MartinNowack]

Hi @ppc, @delcypher,

I'm not a big fan of re-format-only patches (beside the header is now broken, have a look at http://llvm.org/docs/CodingStandards.html#commenting; comments are broken; ...).
Let's change format as we go.

But thanks for the other patch - looks good to me as well.

[pcc]

@delcypher At least two that I can think of: one is that it makes testing the SMT-LIB printer easier (as you can rely on the arrays being declared in a consistent order), the other is that it allows for (potentially expensive) queries to be automatically deduplicated based on the text of the query.

@MartinNowack Sorry, but I really don't like the existing formatting. I have more changes to the SMT-LIB printer in the pipeline that will probably end up moving code around and I'd rather take care of all the reformatting in one go at the start. I can probably go back and clean up some of the comments that clang-format misformatted.

[ccadar]

Thanks for the patch, @pcc, I agree it's a useful change. Regarding the formatting, as you know, the basic rule is, citing LLVM standards, that "If you are extending, enhancing, or bug fixing already implemented code, use the style that is already being used so that the source is uniform and easy to follow." Otherwise, if everyone reformatted each file in which they send a patch, things would become quite messy. This being said, if the original author of that file, @delcypher in this case, agrees with the reformatting, I am happy to change it too (and in general, I think we all agree that we should start formatting new code using the LLVM style, and clang-format looks like a useful tool).

[delcypher]

@pcc Sorry for taking a while at looking at this. I was going to merge but I noticed this has broken the Expr/print-smt.pc test. Can you please fix the test? We've switched to using lit now so hopefully you'll find running tests in KLEE much easier than it used to be :)

Once you've done this I'll merge.

[pcc]

Done.

[delcypher]

Thanks.