Move assertion out of loop for better performance
authorAndres Noetzli <noetzli@stanford.edu>
Fri, 21 Apr 2017 21:39:56 +0000 (14:39 -0700)
committerAndres Noetzli <noetzli@stanford.edu>
Fri, 21 Apr 2017 21:39:56 +0000 (14:39 -0700)
commitfdd9d43ba0102f4d77f1a8a2cf826091731e1983
tree32ca6764d7125a9d789705f4a6c5a6409af439fa
parent23e5362ba8d356b72ba8b488278327cf43c59f66
Move assertion out of loop for better performance

This is related to bug 508. The debug build was taking much longer than the
production build to compute the result. The issue was an assertion in a loop in
nonClausalSimplify(). By moving the assertion outside of the loop, the debug
build is now roughly an order of magnitude slower than the production build
(instead of two orders of magnitude), which seems to be roughly in line with
the difference for other benchmarks:

Debug version before change:
- Bug (minified version): 1065.6s
- regress3/friedman_n6_i4.smt: 6.9s
- regress2/uflia-error0.smt2: 6.3s
- regress2/fuzz_2.smt: 2.3s

Debug version after change:
- Bug (minified version): 131.4s
- regress3/friedman_n6_i4.smt: 6.7s
- regress2/uflia-error0.smt2: 6.2s
- regress2/fuzz_2.smt: 1.9s

Production version:
- Bug (minified version): 18.8s
- regress3/friedman_n6_i4.smt: 0.8s
- regress2/uflia-error0.smt2: 0.8s
- regress2/fuzz_2.smt: 0.2s
src/smt/smt_engine.cpp