Add Tactics for Formula Rewriting

[PhilippWendler]

Z3 supports several tactics for rewriting formulas. We should implement the most useful ones for the other solvers (in the basicimpl package such that they can be reused) and expose them.

[PhilippWendler]

There should also be tests for these tactics, both for our default implementations (to ensure they are correct) as well as for the solver's implementations (to ensure they match our expectations).

[cheshire]

Thomas did an excellent job of writing tests. @stieglma I think this one can be closed?

[stieglma]

Currently only the default tactics are tested, but it should be easy to expand these tests to also test the native implementation if there is one available

[cheshire]

I don't think it's our job to test native implementations though?..

On Fri, Dec 18, 2015 at 1:44 PM, Thomas Stieglmaier <
notifications@github.com> wrote:

Currently only the default tactics are tested, but it should be easy to
expand these tests to also test the native implementation if there is one
available

—
Reply to this email directly or view it on GitHub
#3 (comment).

[PhilippWendler]

I don't think it's our job to test native implementations though?..

As I said, it would be good to have tests that ensure that the solver's implementation matches what we expect from it.

For example, does every solver rewrite non-boolean ITEs for NNF tactic?

[cheshire]

Point taken, I'll expand those.

[cheshire]

I would prefer to remove the method Tactic#applyDefault altogether, the point is that we should get consistently correct results across all solvers, what is the point of explicitly requesting default implementation?

[PhilippWendler]

Exactly, that's why the method is discouraged and why it is called applyDefault instead of apply. However, there needs to be some public entry point to the tactics implementation because they are called from a different package.

[cheshire]

Well there is a public entry point (NNFVisitor), the question is whether it is worth it to make an explicit connection between the value in the enum and the implementation.

[PhilippWendler]

I would suggest to rename applyTactic to applyFormulaRewriting or similar, this is more descriptive and can also be understood by people that are not familiar with Z3.

[cheshire]

Hm tactic is standard for automatic theorem provers.
I'm going to close this as tactics are implemented, re-open for more specific issues.