Fix proofs for ppAssert for theory Bool (#8708)

Fixes #8705.

This also impacts unsat cores when proofs are enabled.

diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 9857636728e1081db6300c2c138c09908d2cff69..f491e40033643364598e3d8eaf72e53d32f7d4ca 100644 (file)
--- 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 a6e16e855fb62a580f1772d4983122d7267ce4ff..46f09cc9d19d1bda2337fc099145aee8197e3940 100644 (file)
--- 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 7c8f0451e4b1c65dbbb7272d4a0c102dd7d016a5..55a15e2abd9bc1e86fadc8523bc339040cceaf14 100644 (file)
--- 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 15977b980c65b9e19984fdd637000c15f6e3fb47..4a9489cf6854cb05da89988c5a0831a30923fdcd 100644 (file)
--- 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 (file)
index 0000000..70593a8
--- /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)