projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4d7417b) | patch
[proofs] [sat] Add manager for optimized clauses and their proofs (#7824)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Tue, 4 Jan 2022 16:16:39 +0000 (13:16 -0300)
committerGitHub <noreply@github.com>
Tue, 4 Jan 2022 16:16:39 +0000 (16:16 +0000)
commitb22a7df42d9591625e9f43ea737c9fbc1658cb2a
treefbc3594d60e535b6a83e21c8101198b716836456tree
parent4d7417bbc2ea2b166e17afe201e7770a8aff3d36commit | diff
[proofs] [sat] Add manager for optimized clauses and their proofs (#7824)

This utility is going to be used by both the proof cnf stream and the sat proof manager to re-add to their respective internal proofs the proof nodes that were stored for clauses saved within the SAT solver at an assertion level below the current user level.

The utility is a context notify object, which means that it can be called when the tracked context pops.
src/CMakeLists.txt diff | blob | history
src/prop/opt_clauses_manager.cpp [new file with mode: 0644] blob
src/prop/opt_clauses_manager.h [new file with mode: 0644] blob