projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5f714e7) | patch
[proof-new] Proof utilities for normalizing clauses at the Node level (#5089)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Fri, 18 Sep 2020 16:32:47 +0000 (13:32 -0300)
committerGitHub <noreply@github.com>
Fri, 18 Sep 2020 16:32:47 +0000 (11:32 -0500)
commite040d5e9e9d8c01138b4b961a1118b7342735d87
treebfaa28d1433e4699fb8112385361727a9be61fcatree
parent5f714e763e57a8e7fc32c6bd0fbab279eac2f993commit | diff
[proof-new] Proof utilities for normalizing clauses at the Node level (#5089)

Extends Theory Proof Step Buffer. These utilities are used so that we can account for the fact that Minisat silenly does these transformations on added clauses.
src/theory/theory_proof_step_buffer.cpp diff | blob | history
src/theory/theory_proof_step_buffer.h diff | blob | history