diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-21 15:48:39 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-21 15:48:39 -0500 |
| commit | d99cc0f25aad013886a9648c93423c64fab9bdd4 (patch) | |
| tree | adb26c02ec799882324df32997c520ceb3384be7 | |
| parent | d7f3cf539939c717692d1309bda742801817ad64 (diff) | |
Minor simplification to boolean proof checker (#6590)
| -rw-r--r-- | src/theory/booleans/proof_checker.cpp | 10 |
1 files 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<bool>(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) { |