projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7635ca0) | patch
LratInstruction inheritance (#2784)
authorAlex Ozdemir <aozdemir@hmc.edu>
Sat, 12 Jan 2019 00:04:56 +0000 (16:04 -0800)
committerGitHub <noreply@github.com>
Sat, 12 Jan 2019 00:04:56 +0000 (16:04 -0800)
commitc652449ac9f4a54fc8f37796f0bff3960434cf40
treeb024ed3f108225e966b3e94893e5d1ed8b0c0e69tree
parent7635ca090c5866b0cc4eeb5beb279032f93bd654commit | diff
LratInstruction inheritance (#2784)

While implementing and testing LRAT proof output as LFSC, I discovered
that my implementation of LratInstruction as a tagged union was subtly
broken for reasons related to move/copy assignment/constructors.

While I could have figured out how to fix it, I decided to stop fighting
the system and use inheritance.

This PR will be followed by one using the inheritance-based
LratInstruction to implement output to LFSC.
src/proof/lrat/lrat_proof.cpp diff | blob | history
src/proof/lrat/lrat_proof.h diff | blob | history