summaryrefslogtreecommitdiff
path: root/src/theory/theory_state.cpp
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/theory/theory_state.cpp
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/theory/theory_state.cpp')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback