Merge remote-tracking branch 'fork/loopProcessOpts' into cav2019strings

1 files changed, 13 insertions, 0 deletions

diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 32833d9a1..78ddeebd0 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -78,6 +78,11 @@ protected:
 
   ClauseIdSet d_explanations;
 
+  // The clause ID of the unit clause defining the true SAT literal.
+  ClauseId d_trueUnitClause;
+  // The clause ID of the unit clause defining the false SAT literal.
+  ClauseId d_falseUnitClause;
+
   bool isDefinition(Node node);
 
   Node getDefinitionForClause(ClauseId clause);
@@ -110,6 +115,14 @@ public:
   // already in CNF
   void registerConvertedClause(ClauseId clause, bool explanation=false);
 
+  // The CNF proof has a special relationship to true and false.
+  // In particular, it need to know the identity of clauses defining
+  // canonical true and false literals in the underlying SAT solver.
+  void registerTrueUnitClause(ClauseId clauseId);
+  void registerFalseUnitClause(ClauseId clauseId);
+  inline ClauseId getTrueUnitClause() { return d_trueUnitClause; };
+  inline ClauseId getFalseUnitClause() { return d_falseUnitClause; };
+
   /** Clause is one of the clauses defining the node expression*/
   void setClauseDefinition(ClauseId clause, Node node);