better support for proof production when encountering bool terms: handle the new proof constructs generated by the equality engine.

proof production for bool-array.smt2 passes

1 files changed, 14 insertions, 0 deletions

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index e245117fd..c684aa6bc 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -1092,6 +1092,20 @@ void BooleanProof::registerTerm(Expr term) {
   }
 }
 
+void LFSCBooleanProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) {
+  Node falseNode = NodeManager::currentNM()->mkConst(false);
+  Node trueNode = NodeManager::currentNM()->mkConst(true);
+
+  Assert(c1 == falseNode.toExpr() || c1 == trueNode.toExpr());
+  Assert(c2 == falseNode.toExpr() || c2 == trueNode.toExpr());
+  Assert(c1 != c2);
+
+  if (c1 == trueNode.toExpr())
+    os << "t_t_neq_f";
+  else
+    os << "(negsymm _ _ _ t_t_neq_f)";
+}
+
 void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
   Assert (term.getType().isBoolean());
   if (term.isVariable()) {