diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-02-11 13:13:18 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-11 13:13:18 -0300 |
| commit | 8fcb59d072b09bfaf8f56334182d425274842461 (patch) | |
| tree | 9e546589f4832d20ee58b1799e2ee80bfd392265 /src/theory/strings/infer_info.h | |
| parent | 1d0492104a200f6fa5cc7a1cee539436ee26ea99 (diff) | |
[proof-new] Adding a proof-producing ensure literal method (#5889)
The ensureLiteral method in CnfStream may apply CNF conversion to the given literal (for example if it's an IFF), which needs to be recorded in the proof. This commit adds a proof-producing ensureLiteral to ProofCnfStream, which is called by the prop engine if proofs are enabled.
This commit also simplifies the interfaces on ensureLit and convertAtom by removing the preRegistration flag, which was never used.
Diffstat (limited to 'src/theory/strings/infer_info.h')
0 files changed, 0 insertions, 0 deletions