(rework of #1112)
review by @gkossakowski (/cc @paulp)
don't crash on unsupported pattern -- diagnose
Apart from cleaning up things LGTM.
I think 256 recursion depth should be more than enough. I'd be very worried if we have formulas with more than 256 levels of nesting.
damn, forgot to push -f -- I already had a version without AnalysisBudget.stackOverflow
don't catch StackOverFlowError: kills performance
instead, use a recursion counter in negationNormalForm as in conjunctiveNormalForm
(except we only limit recursion depth, not formula-size
reuse the same config variable in hopes it'll do for both)
PLS REBUILD ALL
I'd say the formulae can get pretty big without cause for concern -- I have a prototype version that uses Sat4J for solving, where 10K formulae is routine. The main cost is my naive NNF/CNF transform. Should use a more efficient approach, but that requires more substantial rewrites to how the formulae are constructed during the analyses. Will work on this for 2.10.1.
I know it can get big in length but I'd be surprised if it gets very deeply nested. Or does it?
alternatives tend to blow up -- so does the encoding of the subtyping relation into binary proposition logic, especially when sealed classes are involved
Started jenkins job pr-rangepos at https://scala-webapps.epfl.ch/jenkins/job/pr-rangepos/203/
Started jenkins job pr-scala-testsuite-linux-opt at https://scala-webapps.epfl.ch/jenkins/job/pr-scala-testsuite-linux-opt/909/
I see. Since you can customize this with an option then I think we are fine with default nesting limit.
I see you pushed cleaned up commit. LGTM.
jenkins job pr-rangepos: Success - https://scala-webapps.epfl.ch/jenkins/job/pr-rangepos/203/
jenkins job pr-scala-testsuite-linux-opt: Success - https://scala-webapps.epfl.ch/jenkins/job/pr-scala-testsuite-linux-opt/909/