From d99cc0f25aad013886a9648c93423c64fab9bdd4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 21 May 2021 15:48:39 -0500 Subject: Minor simplification to boolean proof checker (#6590) --- src/theory/booleans/proof_checker.cpp | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 2d2155f44..d0461248c 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -157,10 +157,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, return Node::null(); } NodeManager* nm = NodeManager::currentNM(); - return disjuncts.empty() - ? nm->mkConst(false) - : disjuncts.size() == 1 ? disjuncts[0] - : nm->mkNode(kind::OR, disjuncts); + return nm->mkOr(disjuncts); } if (id == PfRule::REORDERING) { @@ -297,10 +294,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n"; } Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n" << pop; - return clauseNodes.empty() - ? nm->mkConst(false) - : clauseNodes.size() == 1 ? clauseNodes[0] - : nm->mkNode(kind::OR, clauseNodes); + return nm->mkOr(clauseNodes); } if (id == PfRule::MACRO_RESOLUTION_TRUST) { -- cgit v1.2.3