Print definition axioms for functions and constants.

[zafer-esen]

When a function / constant has a definition axiom, in generated Boogie files, these axioms were not printed inside uses clauses of that function / constant. They were instead printed as top level declarations. This caused issues when using that printed file with the "/prune" option since some of these axioms could now be pruned.

This PR attempts to fix this issue such that axioms that define a constant / function are now (only) printed inside uses clauses of the function / constant they are defining.

[zafer-esen]

Would it be possible for @keyboardDrummer and @shazqadeer to review this small PR?

Background
Dafny uses \prune by default. In the presence of definition axioms, verification results were inconsistent between:

• verifying a program directly from Dafny,
• printing Boogie files, then verifying those using Boogie.

@atomb pointed out that definition axioms were not printed inside uses clauses when printing Boogie files - which resulted in some axioms to be incorrectly pruned away.

[shazqadeer]

Could you move

if (this.DefinitionAxioms.Any())
      {
        stream.WriteLine();
        stream.WriteLine("uses {");
        this.DefinitionAxioms.ForEach(axiom => axiom.Emit(stream, level));
        stream.WriteLine("}");
      }

as part of the chained if-then-else construction above? Then you won't need the change on line 2180.

[zafer-esen]

Would that work when a function has both a body and definition axioms? I think with the :inline attribute this becomes possible.

Example:

function {:inline} foo(x: int): bool {
    // some body
} uses {
    // some axioms
}

[shazqadeer]

ok

[shazqadeer]

ok

[shazqadeer]

@zafer-esen : Thanks for this PR. If you are ready to land, leave a note here. Also, I am curious what you are using Boogie for.

[zafer-esen]

@shazqadeer, thank you for the review! From my side the PR is ready to be merged.

I am currently working on Dafny with @atomb and mainly experimenting with the monomorphic encoding; however, pruning seems to introduce incompleteness and in some cases errors (related: #560 and Dafny #3217), which seems to be less of an issue in other type encodings.

I came across the bug from this PR while experimenting as I was printing Boogie files from Dafny.