search

ckaestne / TypeChef

Type checking ifdef variability
https://ckaestne.github.io/TypeChef/
Other
76 stars 36 forks source link

Caching for BDDs Enabled Although Documented as Erroneous #45

Open pmbittner opened 3 years ago

pmbittner commented 3 years ago

Hi @ckaestne and TypeChef devs,

on the master branch, in the SATBDDSolver the CACHING is activated although there is a comment indicating that this may yield incorrect results:

https://github.com/ckaestne/TypeChef/blob/fb4d7add1e54ba31d3dd41900b09c34ed6f528de/FeatureExprLib/src/main/scala/de/fosd/typechef/featureexpr/bdd/SatBDDSolver.scala#L78-L83

So I wonder if caching shouldn't be deactivated here as stated by the comment? Could I obtain wrong results when running TypeChef and having CACHING set to true here?

Thanks for any help!

ckaestne commented 3 years ago

Sorry, this has been too long. I vaguely remember that there were some issues, but I suspect that it has been fixed and the comment is outdated. I think this was a weird nondeterministic problem but unloading clauses from the solver in early attempts to use it.

pmbittner commented 3 years ago

Ok, thank you very much for the fast reply! I will leave this set to true then.

Interestingly, the CACHING is deactivated for the SatSolver (for propositional formulas instead of BDDs) with the very same comment:

https://github.com/ckaestne/TypeChef/blob/fb4d7add1e54ba31d3dd41900b09c34ed6f528de/FeatureExprLib/src/main/scala/de/fosd/typechef/featureexpr/sat/SatSolver.scala#L18-L23

So maybe this should be activated then, too.

ckaestne commented 3 years ago

So this is way too long ago to trust anything that I say (and I don't even remember how much of it I wrote myself), but:

The implementation of how constraints are removed differ slightly:

https://github.com/ckaestne/TypeChef/blob/fb4d7add1e54ba31d3dd41900b09c34ed6f528de/FeatureExprLib/src/main/scala/de/fosd/typechef/featureexpr/bdd/SatBDDSolver.scala#L221-L230

vs

https://github.com/ckaestne/TypeChef/blob/fb4d7add1e54ba31d3dd41900b09c34ed6f528de/FeatureExprLib/src/main/scala/de/fosd/typechef/featureexpr/sat/SatSolver.scala#L203-L204

which may very well be responsible for this differences. It could be that one is fixed for an issue in the other.

The key idea of caching is to add all clauses from the feature model only once and then add and remove the clauses from the individual expressions on every satisfiability check. At some point there were issues that removing clauses didn't work as intended. I don't remember whether and how it got fixed, but I assume it works as in the repo. It may work with caching in the Sat implementation or not or only after adding and removing clauses the same way.

Sorry to not be of more help and good luck!

pmbittner commented 3 years ago

Interesting and sounds reasonable. This is already a big help, thank you! We will leave things as is then for now.