diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-12-16 17:04:31 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-16 20:04:31 +0000 |
| commit | b8a5b453e3a4f6d2ae15ac727358540b191c186e (patch) | |
| tree | 476dbae24aebd3df630b8bea63000e26e4401d07 /src/prop/sat_proof_manager.h | |
| parent | 94c5c54989a7ddbff74c7d7e497e4725c2b36fa7 (diff) | |
[proofs] Simplifying and adding new utils to SAT proof manager and Proof Cnf Stream (#7826)
These will be necessary for upcoming changes to the SAT proof manager and Proof Cnf Stream to handle incremental proofs when optimizing the level of SAT clauses.
Diffstat (limited to 'src/prop/sat_proof_manager.h')
| -rw-r--r-- | src/prop/sat_proof_manager.h | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index a224f3a28..98d125591 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -568,14 +568,11 @@ class SatProofManager /** All clauses added to the SAT solver, kept in a context-dependent manner. */ context::CDHashSet<Node> d_assumptions; - /** * A placeholder that may be used to store the literal with the final * conflict. */ SatLiteral d_conflictLit; - /** Gets node equivalent to literal */ - Node getClauseNode(SatLiteral satLit); /** Gets node equivalent to clause. * * To avoid generating different nodes for the same clause, modulo ordering, |