From 4e44b19469f46def8b3b6db6f9bb8bcc2423c22f Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 6 May 2022 20:29:55 -0500
Subject: [PATCH] Fix proofs for ppAssert for theory Bool (#8708)

Fixes #8705.

This also impacts unsat cores when proofs are enabled.
---
 src/theory/booleans/theory_bool.cpp           | 25 +++++++++++++++----
 src/theory/theory.cpp                         | 18 +------------
 src/theory/theory_engine.cpp                  |  1 +
 test/regress/cli/CMakeLists.txt               |  1 +
 .../cores/issue8705-bool-ppassert.smt2        | 20 +++++++++++++++
 5 files changed, 43 insertions(+), 22 deletions(-)
 create mode 100644 test/regress/cli/regress0/cores/issue8705-bool-ppassert.smt2

diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 985763672..f491e4003 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -42,6 +42,7 @@ TheoryBool::TheoryBool(Env& env, OutputChannel& out, Valuation valuation)
 Theory::PPAssertStatus TheoryBool::ppAssert(
     TrustNode tin, TrustSubstitutionMap& outSubstitutions)
 {
+  Assert(tin.getKind() == TrustNodeKind::LEMMA);
   TNode in = tin.getNode();
   if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst<bool>()) {
     // If we get a false literal, we're in conflict
@@ -56,15 +57,29 @@ Theory::PPAssertStatus TheoryBool::ppAssert(
           in[0], NodeManager::currentNM()->mkConst<bool>(false), tin);
       return PP_ASSERT_STATUS_SOLVED;
     }
-  } else {
-    if (in.isVar())
+    else if (in[0].getKind() == kind::EQUAL && in[0][0].getType().isBoolean())
     {
-      outSubstitutions.addSubstitutionSolved(
-          in, NodeManager::currentNM()->mkConst<bool>(true), tin);
-      return PP_ASSERT_STATUS_SOLVED;
+      TNode eq = in[0];
+      if (eq[0].isVar() && isLegalElimination(eq[0], eq[1]))
+      {
+        outSubstitutions.addSubstitutionSolved(eq[0], eq[1].notNode(), tin);
+        return PP_ASSERT_STATUS_SOLVED;
+      }
+      else if (eq[1].isVar() && isLegalElimination(eq[1], eq[0]))
+      {
+        outSubstitutions.addSubstitutionSolved(eq[1], eq[0].notNode(), tin);
+        return PP_ASSERT_STATUS_SOLVED;
+      }
     }
   }
+  else if (in.isVar())
+  {
+    outSubstitutions.addSubstitutionSolved(
+        in, NodeManager::currentNM()->mkConst<bool>(true), tin);
+    return PP_ASSERT_STATUS_SOLVED;
+  }
 
+  // the positive Boolean equality case is handled in the default way
   return Theory::ppAssert(tin, outSubstitutions);
 }
 
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index a6e16e855..46f09cc9d 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -440,6 +440,7 @@ bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 Theory::PPAssertStatus Theory::ppAssert(TrustNode tin,
                                         TrustSubstitutionMap& outSubstitutions)
 {
+  Assert(tin.getKind() == TrustNodeKind::LEMMA);
   TNode in = tin.getNode();
   if (in.getKind() == kind::EQUAL)
   {
@@ -460,23 +461,6 @@ Theory::PPAssertStatus Theory::ppAssert(TrustNode tin,
       return PP_ASSERT_STATUS_SOLVED;
     }
   }
-  else if (in.getKind() == kind::NOT && in[0].getKind() == kind::EQUAL
-           && in[0][0].getType().isBoolean())
-  {
-    TNode eq = in[0];
-    if (eq[0].isVar())
-    {
-      Node res = eq[0].eqNode(eq[1].notNode());
-      TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr);
-      return ppAssert(tn, outSubstitutions);
-    }
-    else if (eq[1].isVar())
-    {
-      Node res = eq[1].eqNode(eq[0].notNode());
-      TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr);
-      return ppAssert(tn, outSubstitutions);
-    }
-  }
 
   return PP_ASSERT_STATUS_UNSOLVED;
 }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7c8f0451e..55a15e2ab 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -737,6 +737,7 @@ bool TheoryEngine::isRelevant(Node lit) const
 theory::Theory::PPAssertStatus TheoryEngine::solve(
     TrustNode tliteral, TrustSubstitutionMap& substitutionOut)
 {
+  Assert(tliteral.getKind() == TrustNodeKind::LEMMA);
   // Reset the interrupt flag
   d_interrupted = false;
 
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 15977b980..4a9489cf6 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -486,6 +486,7 @@ set(regress_0_tests
   regress0/cores/issue5238.smt2
   regress0/cores/issue5902.smt2
   regress0/cores/issue5908.smt2
+  regress0/cores/issue8705-bool-ppassert.smt2
   regress0/cvc-rerror-print.cvc.smt2
   regress0/cvc3-bug15.cvc.smt2
   regress0/cvc3.userdoc.01.cvc.smt2
diff --git a/test/regress/cli/regress0/cores/issue8705-bool-ppassert.smt2 b/test/regress/cli/regress0/cores/issue8705-bool-ppassert.smt2
new file mode 100644
index 000000000..70593a89e
--- /dev/null
+++ b/test/regress/cli/regress0/cores/issue8705-bool-ppassert.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --produce-proofs
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun a () String)  
+(declare-fun b () String) 
+(declare-fun c () Bool) 
+(declare-fun d () Bool) 
+(declare-fun g () Bool) 
+(declare-fun e () Bool) 
+(declare-fun f () String)       
+(assert (= b  f)) 
+(assert (= c (= "" b))) 
+(assert (= d (not c))) 
+(assert d)  
+(assert (= a f))   
+(assert (= g (not (= e (not (= "" a)))))) 
+(assert g)     
+(assert e) 
+(check-sat)  
-- 
2.30.2