search

sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.
Apache License 2.0
186 stars 46 forks source link

Entry point for Logging*Environment #17

Closed cheshire closed 8 years ago

cheshire commented 8 years ago

Currently it's just orphaned, as the wrapping was done by the Solver class in CPAchecker.

One solution would be to migrate (some part of) the Solver class to JavaSMT.

cheshire commented 8 years ago

Or we can just move it to FormulaManager. However logging is exposed using an @Option, which can't be attached to interfaces. @PhilippWendler would you hate changing FormulaManager to abstract class? Any other solutions?

cheshire commented 8 years ago

Oh wait there is AbstractFormulaManager already, somehow missed that.

cheshire commented 8 years ago

Can anyone shed any light on on-demand wrapping with InterpolatingProverWithAssumptionsWrapper? Shouldn't it be in JavaSMT as well?

PhilippWendler commented 8 years ago

What do you want to know about InterpolatingProverWithAssumptionsWrapper? How is this related to Logging*Environment?

cheshire commented 8 years ago

Funny enough it is.

Look at the code in Solver for creating the InterpolatingEnvironmentWithLogging: it checks whether the returned environment has assumptions first, and if it doesn't, wraps it with InterpolatingProverWithAssumptionsWrapper.

I assume it is because the LoggingWrapper implements *WithAssumptions interface, in order to avoid having to have two logging wrappers.

This leads to some funny logic, where the environment gets wrapped only if logging is on.

On Thu, Jan 7, 2016 at 6:35 AM, Philipp Wendler notifications@github.com wrote:

What do you want to know about InterpolatingProverWithAssumptionsWrapper? How is this related to Logging*Environment?

— Reply to this email directly or view it on GitHub https://github.com/sosy-lab/java-smt/issues/17#issuecomment-169558762.

PhilippWendler commented 8 years ago

The code in Solver is not like this because of logging. We want to have support for InterpolatingProverEnvironmentWithAssumptions no matter which solver is used, but some solvers do not support it, so in that case we use our own implementation. The logging is completely orthogonal to that.

Of course InterpolatingProverWithAssumptionsWrapper can be moved to JavaSMT.

cheshire commented 8 years ago

Fixed by 6bbe7c6856ff8bb06c1538582f12d2b664e39c1f