chipmunk-project/chipmunk

Adding counterexample input values vs adding negation of hole value assignments

Closed this issue · 1 comments

Both of them would let us avoid the failed hole value assignments, but I wonder whether the latter really helps us. After #139 it will only provide additional constraints, and adding counterexamples theoretically let us avoid the same hole value assignments. I don't think --hole-elimination flag helps us.

I agree. @XiangyuG's preliminary experiments showed that cex generation was much more effective than hole elimination. But let's keep both around for benchmarking so that we can actually run an experiment comparing the two.