fix (get-proof) command to respect option pp.simplify_implies

[someplaceguy]

This PR contains two parts:

1. Change to src/cmd_context/basic_cmds.cpp:

This change makes the pp.simplify_implies parameter work when using the (get-proof) command.

It is important that the pp.simplify_implies feature can be disabled by the user, because otherwise the pretty-printer will mangle the (asserted ...) proof rules in the proof output, which means that the terms in these rules will not match the actual terms that were asserted in the input file, therefore making reconstructing the Z3 proof significantly more difficult in some cases.

As a historical note, this issue has been breaking proof reconstruction in HOL4's HolSmt implementation (for some inputs) for at least 13 years, if not more.

2. Changes to src/ast/ast_smt_pp.cpp:

This fixes some bugs introduced around 6 years ago which are now preventing the simplify_implies parameter from being passed down from ast_smt_pp objects to smt_printer objects.

Specifically, commit b8e5fc9 removed the bool is_smt2 parameter from the constructor of the smt_printer class. Some places which constructed instances of this class were fixed to remove this parameter.

However, in other places, this parameter was not removed, thus all subsequent parameters were shifted one place to the right.

This means that in some places where ast_smt_pp objects were initializing the smt_printer class by passing the m_simplify_implies variable to the simplify_implies parameter, the variable was actually being passed to the indent parameter instead, while the simplify_implies parameter was always being initialized to true (which was meant to initialize the is_smt2 parameter that the commit removed).

[someplaceguy]

@microsoft-github-policy-service agree