diff options
Diffstat (limited to 'src/proof/clause_id.h')
| -rw-r--r-- | src/proof/clause_id.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/proof/clause_id.h b/src/proof/clause_id.h index b2d36c9cb..5d7ec94f6 100644 --- a/src/proof/clause_id.h +++ b/src/proof/clause_id.h @@ -28,6 +28,13 @@ namespace CVC4 { */ typedef unsigned ClauseId; +/** Reserved clauseId values used in the resolution proof. The represent, + * respectively, the empty clause, that adding the clause to the SAT solver was + * a no-op, and that an error occurred when trying to add. */ +const ClauseId ClauseIdEmpty(-1); +const ClauseId ClauseIdUndef(-2); +const ClauseId ClauseIdError(-3); + }/* CVC4 namespace */ #endif /* CVC4__PROOF__CLAUSE_ID_H */ |