summaryrefslogtreecommitdiff
path: root/src/util/floatingpoint_size.h
diff options
context:
space:
mode:
authorHaniel Barbosa <hanielbbarbosa@gmail.com>2021-04-09 17:30:44 -0300
committerGitHub <noreply@github.com>2021-04-09 15:30:44 -0500
commit62f5fb8db269e12f13ce5c4e1c3f975776737836 (patch)
treebdf16437b8c0c5ead202ac7fb08f6483aa3a9c19 /src/util/floatingpoint_size.h
parent6923f0cb9930332a61e187d3b4d1a7ec7e65b15c (diff)
[proof-new] Optimizing sat proof (#6324)
For some benchmarks, checking MACRO_RESOLUTION can be up to 80% (!!!) of the running time. This commit introduces a new rule that does not perform checking. The old rule and checker are kept for ground truth. Some miscellaneous minor changes are also made in the PR.
Diffstat (limited to 'src/util/floatingpoint_size.h')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback