src/theory/booleans/proof_checker.cpp

   1 /*********************                                                        */
   2 /*! \file proof_checker.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Haniel Barbosa, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of equality proof checker
  13  **/
  14
  15 #include "theory/booleans/proof_checker.h"
  16 #include "expr/skolem_manager.h"
  17 #include "theory/rewriter.h"
  18
  19 namespace CVC4 {
  20 namespace theory {
  21 namespace booleans {
  22
  23 void BoolProofRuleChecker::registerTo(ProofChecker* pc)
  24 {
  25   pc->registerChecker(PfRule::SPLIT, this);
  26   pc->registerChecker(PfRule::RESOLUTION, this);
  27   pc->registerChecker(PfRule::CHAIN_RESOLUTION, this);
  28   pc->registerChecker(PfRule::FACTORING, this);
  29   pc->registerChecker(PfRule::REORDERING, this);
  30   pc->registerChecker(PfRule::EQ_RESOLVE, this);
  31   pc->registerChecker(PfRule::MODUS_PONENS, this);
  32   pc->registerChecker(PfRule::NOT_NOT_ELIM, this);
  33   pc->registerChecker(PfRule::CONTRA, this);
  34   pc->registerChecker(PfRule::AND_ELIM, this);
  35   pc->registerChecker(PfRule::AND_INTRO, this);
  36   pc->registerChecker(PfRule::NOT_OR_ELIM, this);
  37   pc->registerChecker(PfRule::IMPLIES_ELIM, this);
  38   pc->registerChecker(PfRule::NOT_IMPLIES_ELIM1, this);
  39   pc->registerChecker(PfRule::NOT_IMPLIES_ELIM2, this);
  40   pc->registerChecker(PfRule::EQUIV_ELIM1, this);
  41   pc->registerChecker(PfRule::EQUIV_ELIM2, this);
  42   pc->registerChecker(PfRule::NOT_EQUIV_ELIM1, this);
  43   pc->registerChecker(PfRule::NOT_EQUIV_ELIM2, this);
  44   pc->registerChecker(PfRule::XOR_ELIM1, this);
  45   pc->registerChecker(PfRule::XOR_ELIM2, this);
  46   pc->registerChecker(PfRule::NOT_XOR_ELIM1, this);
  47   pc->registerChecker(PfRule::NOT_XOR_ELIM2, this);
  48   pc->registerChecker(PfRule::ITE_ELIM1, this);
  49   pc->registerChecker(PfRule::ITE_ELIM2, this);
  50   pc->registerChecker(PfRule::NOT_ITE_ELIM1, this);
  51   pc->registerChecker(PfRule::NOT_ITE_ELIM2, this);
  52   pc->registerChecker(PfRule::NOT_AND, this);
  53   pc->registerChecker(PfRule::CNF_AND_POS, this);
  54   pc->registerChecker(PfRule::CNF_AND_NEG, this);
  55   pc->registerChecker(PfRule::CNF_OR_POS, this);
  56   pc->registerChecker(PfRule::CNF_OR_NEG, this);
  57   pc->registerChecker(PfRule::CNF_IMPLIES_POS, this);
  58   pc->registerChecker(PfRule::CNF_IMPLIES_NEG1, this);
  59   pc->registerChecker(PfRule::CNF_IMPLIES_NEG2, this);
  60   pc->registerChecker(PfRule::CNF_EQUIV_POS1, this);
  61   pc->registerChecker(PfRule::CNF_EQUIV_POS2, this);
  62   pc->registerChecker(PfRule::CNF_EQUIV_NEG1, this);
  63   pc->registerChecker(PfRule::CNF_EQUIV_NEG2, this);
  64   pc->registerChecker(PfRule::CNF_XOR_POS1, this);
  65   pc->registerChecker(PfRule::CNF_XOR_POS2, this);
  66   pc->registerChecker(PfRule::CNF_XOR_NEG1, this);
  67   pc->registerChecker(PfRule::CNF_XOR_NEG2, this);
  68   pc->registerChecker(PfRule::CNF_ITE_POS1, this);
  69   pc->registerChecker(PfRule::CNF_ITE_POS2, this);
  70   pc->registerChecker(PfRule::CNF_ITE_POS3, this);
  71   pc->registerChecker(PfRule::CNF_ITE_NEG1, this);
  72   pc->registerChecker(PfRule::CNF_ITE_NEG2, this);
  73   pc->registerChecker(PfRule::CNF_ITE_NEG3, this);
  74 }
  75
  76 Node BoolProofRuleChecker::checkInternal(PfRule id,
  77                                          const std::vector<Node>& children,
  78                                          const std::vector<Node>& args)
  79 {
  80   if (id == PfRule::RESOLUTION)
  81   {
  82     Assert(children.size() == 2);
  83     Assert(args.size() == 1);
  84     std::vector<Node> disjuncts;
  85     for (unsigned i = 0; i < 2; ++i)
  86     {
  87       // if first clause, eliminate pivot, otherwise its negation
  88       Node elim = i == 0 ? args[0] : args[0].notNode();
  89       for (unsigned j = 0, size = children[i].getNumChildren(); j < size; ++j)
  90       {
  91         if (elim != children[i][j])
  92         {
  93           disjuncts.push_back(children[i][j]);
  94         }
  95       }
  96     }
  97     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
  98   }
  99   if (id == PfRule::FACTORING)
 100   {
 101     Assert(children.size() == 1);
 102     Assert(args.empty());
 103     if (children[0].getKind() != kind::OR)
 104     {
 105       return Node::null();
 106     }
 107     // remove duplicates while keeping the order of children
 108     std::unordered_set<TNode, TNodeHashFunction> clauseSet;
 109     std::vector<Node> disjuncts;
 110     unsigned size = children[0].getNumChildren();
 111     for (unsigned i = 0; i < size; ++i)
 112     {
 113       if (clauseSet.count(children[0][i]))
 114       {
 115         continue;
 116       }
 117       disjuncts.push_back(children[0][i]);
 118       clauseSet.insert(children[0][i]);
 119     }
 120     if (disjuncts.size() == size)
 121     {
 122       return Node::null();
 123     }
 124     NodeManager* nm = NodeManager::currentNM();
 125     return disjuncts.empty()
 126                ? nm->mkConst<bool>(false)
 127                : disjuncts.size() == 1 ? disjuncts[0]
 128                                        : nm->mkNode(kind::OR, disjuncts);
 129   }
 130   if (id == PfRule::REORDERING)
 131   {
 132     Assert(children.size() == 1);
 133     Assert(args.size() == 1);
 134     std::unordered_set<Node, NodeHashFunction> clauseSet1, clauseSet2;
 135     if (children[0].getKind() == kind::OR)
 136     {
 137       clauseSet1.insert(children[0].begin(), children[0].end());
 138     }
 139     else
 140     {
 141       clauseSet1.insert(children[0]);
 142     }
 143     if (args[0].getKind() == kind::OR)
 144     {
 145       clauseSet2.insert(args[0].begin(), args[0].end());
 146     }
 147     else
 148     {
 149       clauseSet2.insert(args[0]);
 150     }
 151     if (clauseSet1 != clauseSet2)
 152     {
 153       Trace("bool-pfcheck") << id << ": clause set1: " << clauseSet1 << "\n"
 154                             << id << ": clause set2: " << clauseSet2 << "\n";
 155       return Node::null();
 156     }
 157     return args[0];
 158   }
 159   if (id == PfRule::CHAIN_RESOLUTION)
 160   {
 161     Assert(children.size() > 1);
 162     Assert(args.size() == children.size() - 1);
 163     Trace("bool-pfcheck") << "chain_res:\n" << push;
 164     std::vector<Node> clauseNodes;
 165     for (unsigned i = 0, childrenSize = children.size(); i < childrenSize; ++i)
 166     {
 167       std::unordered_set<Node, NodeHashFunction> elim;
 168       // literals to be removed from "first" clause
 169       if (i < childrenSize - 1)
 170       {
 171         elim.insert(args.begin() + i, args.end());
 172       }
 173       // literal to be removed from "second" clause. They will be negated
 174       if (i > 0)
 175       {
 176         elim.insert(args[i - 1].negate());
 177       }
 178       Trace("bool-pfcheck") << i << ": elimination set: " << elim << "\n";
 179       // only add to conclusion nodes that are not in elimination set. First get
 180       // the nodes.
 181       //
 182       // Since unit clauses can also be OR nodes, we rely on the invariant that
 183       // non-unit clauses will not occur themselves in their elimination sets.
 184       // If they do then they must be unit.
 185       std::vector<Node> lits;
 186       if (children[i].getKind() == kind::OR && elim.count(children[i]) == 0)
 187       {
 188         lits.insert(lits.end(), children[i].begin(), children[i].end());
 189       }
 190       else
 191       {
 192         lits.push_back(children[i]);
 193       }
 194       Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n";
 195       std::vector<Node> added;
 196       for (unsigned j = 0, size = lits.size(); j < size; ++j)
 197       {
 198         if (elim.count(lits[j]) == 0)
 199         {
 200           clauseNodes.push_back(lits[j]);
 201           added.push_back(lits[j]);
 202         }
 203       }
 204       Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n";
 205     }
 206     Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n" << pop;
 207     NodeManager* nm = NodeManager::currentNM();
 208     return clauseNodes.empty()
 209                ? nm->mkConst<bool>(false)
 210                : clauseNodes.size() == 1 ? clauseNodes[0]
 211                                          : nm->mkNode(kind::OR, clauseNodes);
 212   }
 213   if (id == PfRule::SPLIT)
 214   {
 215     Assert(children.empty());
 216     Assert(args.size() == 1);
 217     return NodeManager::currentNM()->mkNode(
 218         kind::OR, args[0], args[0].notNode());
 219   }
 220   if (id == PfRule::CONTRA)
 221   {
 222     Assert(children.size() == 2);
 223     if (children[1].getKind() == Kind::NOT && children[0] == children[1][0])
 224     {
 225       return NodeManager::currentNM()->mkConst(false);
 226     }
 227     return Node::null();
 228   }
 229   if (id == PfRule::EQ_RESOLVE)
 230   {
 231     Assert(children.size() == 2);
 232     Assert(args.empty());
 233     if (children[1].getKind() != kind::EQUAL || children[0] != children[1][0])
 234     {
 235       return Node::null();
 236     }
 237     return children[1][1];
 238   }
 239   if (id == PfRule::MODUS_PONENS)
 240   {
 241     Assert(children.size() == 2);
 242     Assert(args.empty());
 243     if (children[1].getKind() != kind::IMPLIES || children[0] != children[1][0])
 244     {
 245       return Node::null();
 246     }
 247     return children[1][1];
 248   }
 249   if (id == PfRule::NOT_NOT_ELIM)
 250   {
 251     Assert(children.size() == 1);
 252     Assert(args.empty());
 253     if (children[0].getKind() != kind::NOT || children[0][0].getKind() != kind::NOT)
 254     {
 255       return Node::null();
 256     }
 257     return children[0][0][0];
 258   }
 259   // natural deduction rules
 260   if (id == PfRule::AND_ELIM)
 261   {
 262     Assert(children.size() == 1);
 263     Assert(args.size() == 1);
 264     uint32_t i;
 265     if (children[0].getKind() != kind::AND || !getUInt32(args[0], i))
 266     {
 267       return Node::null();
 268     }
 269     if (i >= children[0].getNumChildren())
 270     {
 271       return Node::null();
 272     }
 273     return children[0][i];
 274   }
 275   if (id == PfRule::AND_INTRO)
 276   {
 277     Assert(children.size() >= 1);
 278     return children.size() == 1
 279                ? children[0]
 280                : NodeManager::currentNM()->mkNode(kind::AND, children);
 281   }
 282   if (id == PfRule::NOT_OR_ELIM)
 283   {
 284     Assert(children.size() == 1);
 285     Assert(args.size() == 1);
 286     uint32_t i;
 287     if (children[0].getKind() != kind::NOT
 288         || children[0][0].getKind() != kind::OR || !getUInt32(args[0], i))
 289     {
 290       return Node::null();
 291     }
 292     if (i >= children[0][0].getNumChildren())
 293     {
 294       return Node::null();
 295     }
 296     return children[0][0][i].notNode();
 297   }
 298   if (id == PfRule::IMPLIES_ELIM)
 299   {
 300     Assert(children.size() == 1);
 301     Assert(args.empty());
 302     if (children[0].getKind() != kind::IMPLIES)
 303     {
 304       return Node::null();
 305     }
 306     return NodeManager::currentNM()->mkNode(
 307         kind::OR, children[0][0].notNode(), children[0][1]);
 308   }
 309   if (id == PfRule::NOT_IMPLIES_ELIM1)
 310   {
 311     Assert(children.size() == 1);
 312     Assert(args.empty());
 313     if (children[0].getKind() != kind::NOT
 314         || children[0][0].getKind() != kind::IMPLIES)
 315     {
 316       return Node::null();
 317     }
 318     return children[0][0][0];
 319   }
 320   if (id == PfRule::NOT_IMPLIES_ELIM2)
 321   {
 322     Assert(children.size() == 1);
 323     Assert(args.empty());
 324     if (children[0].getKind() != kind::NOT
 325         || children[0][0].getKind() != kind::IMPLIES)
 326     {
 327       return Node::null();
 328     }
 329     return children[0][0][1].notNode();
 330   }
 331   if (id == PfRule::EQUIV_ELIM1)
 332   {
 333     Assert(children.size() == 1);
 334     Assert(args.empty());
 335     if (children[0].getKind() != kind::EQUAL)
 336     {
 337       return Node::null();
 338     }
 339     return NodeManager::currentNM()->mkNode(
 340         kind::OR, children[0][0].notNode(), children[0][1]);
 341   }
 342   if (id == PfRule::EQUIV_ELIM2)
 343   {
 344     Assert(children.size() == 1);
 345     Assert(args.empty());
 346     if (children[0].getKind() != kind::EQUAL)
 347     {
 348       return Node::null();
 349     }
 350     return NodeManager::currentNM()->mkNode(
 351         kind::OR, children[0][0], children[0][1].notNode());
 352   }
 353   if (id == PfRule::NOT_EQUIV_ELIM1)
 354   {
 355     Assert(children.size() == 1);
 356     Assert(args.empty());
 357     if (children[0].getKind() != kind::NOT
 358         || children[0][0].getKind() != kind::EQUAL)
 359     {
 360       return Node::null();
 361     }
 362     return NodeManager::currentNM()->mkNode(
 363         kind::OR, children[0][0][0], children[0][0][1]);
 364   }
 365   if (id == PfRule::NOT_EQUIV_ELIM2)
 366   {
 367     Assert(children.size() == 1);
 368     Assert(args.empty());
 369     if (children[0].getKind() != kind::NOT
 370         || children[0][0].getKind() != kind::EQUAL)
 371     {
 372       return Node::null();
 373     }
 374     return NodeManager::currentNM()->mkNode(
 375         kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode());
 376   }
 377   if (id == PfRule::XOR_ELIM1)
 378   {
 379     Assert(children.size() == 1);
 380     Assert(args.empty());
 381     if (children[0].getKind() != kind::XOR)
 382     {
 383       return Node::null();
 384     }
 385     return NodeManager::currentNM()->mkNode(
 386         kind::OR, children[0][0], children[0][1]);
 387   }
 388   if (id == PfRule::XOR_ELIM2)
 389   {
 390     Assert(children.size() == 1);
 391     Assert(args.empty());
 392     if (children[0].getKind() != kind::XOR)
 393     {
 394       return Node::null();
 395     }
 396     return NodeManager::currentNM()->mkNode(
 397         kind::OR, children[0][0].notNode(), children[0][1].notNode());
 398   }
 399   if (id == PfRule::NOT_XOR_ELIM1)
 400   {
 401     Assert(children.size() == 1);
 402     Assert(args.empty());
 403     if (children[0].getKind() != kind::NOT
 404         || children[0][0].getKind() != kind::XOR)
 405     {
 406       return Node::null();
 407     }
 408     return NodeManager::currentNM()->mkNode(
 409         kind::OR, children[0][0][0], children[0][0][1].notNode());
 410   }
 411   if (id == PfRule::NOT_XOR_ELIM2)
 412   {
 413     Assert(children.size() == 1);
 414     Assert(args.empty());
 415     if (children[0].getKind() != kind::NOT
 416         || children[0][0].getKind() != kind::XOR)
 417     {
 418       return Node::null();
 419     }
 420     return NodeManager::currentNM()->mkNode(
 421         kind::OR, children[0][0][0].notNode(), children[0][0][1]);
 422   }
 423   if (id == PfRule::ITE_ELIM1)
 424   {
 425     Assert(children.size() == 1);
 426     Assert(args.empty());
 427     if (children[0].getKind() != kind::ITE)
 428     {
 429       return Node::null();
 430     }
 431     return NodeManager::currentNM()->mkNode(
 432         kind::OR, children[0][0].notNode(), children[0][1]);
 433   }
 434   if (id == PfRule::ITE_ELIM2)
 435   {
 436     Assert(children.size() == 1);
 437     Assert(args.empty());
 438     if (children[0].getKind() != kind::ITE)
 439     {
 440       return Node::null();
 441     }
 442     return NodeManager::currentNM()->mkNode(
 443         kind::OR, children[0][0], children[0][2]);
 444   }
 445   if (id == PfRule::NOT_ITE_ELIM1)
 446   {
 447     Assert(children.size() == 1);
 448     Assert(args.empty());
 449     if (children[0].getKind() != kind::NOT
 450         || children[0][0].getKind() != kind::ITE)
 451     {
 452       return Node::null();
 453     }
 454     return NodeManager::currentNM()->mkNode(
 455         kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode());
 456   }
 457   if (id == PfRule::NOT_ITE_ELIM2)
 458   {
 459     Assert(children.size() == 1);
 460     Assert(args.empty());
 461     if (children[0].getKind() != kind::NOT
 462         || children[0][0].getKind() != kind::ITE)
 463     {
 464       return Node::null();
 465     }
 466     return NodeManager::currentNM()->mkNode(
 467         kind::OR, children[0][0][0], children[0][0][2].notNode());
 468   }
 469   // De Morgan
 470   if (id == PfRule::NOT_AND)
 471   {
 472     Assert(children.size() == 1);
 473     Assert(args.empty());
 474     if (children[0].getKind() != kind::NOT
 475         || children[0][0].getKind() != kind::AND)
 476     {
 477       return Node::null();
 478     }
 479     std::vector<Node> disjuncts;
 480     for (unsigned i = 0, size = children[0][0].getNumChildren(); i < size; ++i)
 481     {
 482       disjuncts.push_back(children[0][0][i].notNode());
 483     }
 484     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 485   }
 486   // valid clauses rules for Tseitin CNF transformation
 487   if (id == PfRule::CNF_AND_POS)
 488   {
 489     Assert(children.empty());
 490     Assert(args.size() == 2);
 491     uint32_t i;
 492     if (args[0].getKind() != kind::AND || !getUInt32(args[1], i))
 493     {
 494       return Node::null();
 495     }
 496     if (i >= args[0].getNumChildren())
 497     {
 498       return Node::null();
 499     }
 500     return NodeManager::currentNM()->mkNode(
 501         kind::OR, args[0].notNode(), args[0][i]);
 502   }
 503   if (id == PfRule::CNF_AND_NEG)
 504   {
 505     Assert(children.empty());
 506     Assert(args.size() == 1);
 507     if (args[0].getKind() != kind::AND)
 508     {
 509       return Node::null();
 510     }
 511     std::vector<Node> disjuncts{args[0]};
 512     for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i)
 513     {
 514       disjuncts.push_back(args[0][i].notNode());
 515     }
 516     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 517   }
 518   if (id == PfRule::CNF_OR_POS)
 519   {
 520     Assert(children.empty());
 521     Assert(args.size() == 1);
 522     if (args[0].getKind() != kind::OR)
 523     {
 524       return Node::null();
 525     }
 526     std::vector<Node> disjuncts{args[0].notNode()};
 527     for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i)
 528     {
 529       disjuncts.push_back(args[0][i]);
 530     }
 531     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 532   }
 533   if (id == PfRule::CNF_OR_NEG)
 534   {
 535     Assert(children.empty());
 536     Assert(args.size() == 2);
 537     uint32_t i;
 538     if (args[0].getKind() != kind::OR || !getUInt32(args[1], i))
 539     {
 540       return Node::null();
 541     }
 542     if (i >= args[0].getNumChildren())
 543     {
 544       return Node::null();
 545     }
 546     return NodeManager::currentNM()->mkNode(
 547         kind::OR, args[0], args[0][i].notNode());
 548   }
 549   if (id == PfRule::CNF_IMPLIES_POS)
 550   {
 551     Assert(children.empty());
 552     Assert(args.size() == 1);
 553     if (args[0].getKind() != kind::IMPLIES)
 554     {
 555       return Node::null();
 556     }
 557     std::vector<Node> disjuncts{
 558         args[0].notNode(), args[0][0].notNode(), args[0][1]};
 559     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 560   }
 561   if (id == PfRule::CNF_IMPLIES_NEG1)
 562   {
 563     Assert(children.empty());
 564     Assert(args.size() == 1);
 565     if (args[0].getKind() != kind::IMPLIES)
 566     {
 567       return Node::null();
 568     }
 569     std::vector<Node> disjuncts{args[0], args[0][0]};
 570     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 571   }
 572   if (id == PfRule::CNF_IMPLIES_NEG2)
 573   {
 574     Assert(children.empty());
 575     Assert(args.size() == 1);
 576     if (args[0].getKind() != kind::IMPLIES)
 577     {
 578       return Node::null();
 579     }
 580     std::vector<Node> disjuncts{args[0], args[0][1].notNode()};
 581     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 582   }
 583   if (id == PfRule::CNF_EQUIV_POS1)
 584   {
 585     Assert(children.empty());
 586     Assert(args.size() == 1);
 587     if (args[0].getKind() != kind::EQUAL)
 588     {
 589       return Node::null();
 590     }
 591     std::vector<Node> disjuncts{
 592         args[0].notNode(), args[0][0].notNode(), args[0][1]};
 593     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 594   }
 595   if (id == PfRule::CNF_EQUIV_POS2)
 596   {
 597     Assert(children.empty());
 598     Assert(args.size() == 1);
 599     if (args[0].getKind() != kind::EQUAL)
 600     {
 601       return Node::null();
 602     }
 603     std::vector<Node> disjuncts{
 604         args[0].notNode(), args[0][0], args[0][1].notNode()};
 605     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 606   }
 607   if (id == PfRule::CNF_EQUIV_NEG1)
 608   {
 609     Assert(children.empty());
 610     Assert(args.size() == 1);
 611     if (args[0].getKind() != kind::EQUAL)
 612     {
 613       return Node::null();
 614     }
 615     std::vector<Node> disjuncts{args[0], args[0][0], args[0][1]};
 616     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 617   }
 618   if (id == PfRule::CNF_EQUIV_NEG2)
 619   {
 620     Assert(children.empty());
 621     Assert(args.size() == 1);
 622     if (args[0].getKind() != kind::EQUAL)
 623     {
 624       return Node::null();
 625     }
 626     std::vector<Node> disjuncts{
 627         args[0], args[0][0].notNode(), args[0][1].notNode()};
 628     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 629   }
 630   if (id == PfRule::CNF_XOR_POS1)
 631   {
 632     Assert(children.empty());
 633     Assert(args.size() == 1);
 634     if (args[0].getKind() != kind::XOR)
 635     {
 636       return Node::null();
 637     }
 638     std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][1]};
 639     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 640   }
 641   if (id == PfRule::CNF_XOR_POS2)
 642   {
 643     Assert(children.empty());
 644     Assert(args.size() == 1);
 645     if (args[0].getKind() != kind::XOR)
 646     {
 647       return Node::null();
 648     }
 649     std::vector<Node> disjuncts{
 650         args[0].notNode(), args[0][0].notNode(), args[0][1].notNode()};
 651     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 652   }
 653   if (id == PfRule::CNF_XOR_NEG1)
 654   {
 655     Assert(children.empty());
 656     Assert(args.size() == 1);
 657     if (args[0].getKind() != kind::XOR)
 658     {
 659       return Node::null();
 660     }
 661     std::vector<Node> disjuncts{args[0], args[0][0].notNode(), args[0][1]};
 662     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 663   }
 664   if (id == PfRule::CNF_XOR_NEG2)
 665   {
 666     Assert(children.empty());
 667     Assert(args.size() == 1);
 668     if (args[0].getKind() != kind::XOR)
 669     {
 670       return Node::null();
 671     }
 672     std::vector<Node> disjuncts{args[0], args[0][0], args[0][1].notNode()};
 673     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 674   }
 675   if (id == PfRule::CNF_ITE_POS1)
 676   {
 677     Assert(children.empty());
 678     Assert(args.size() == 1);
 679     if (args[0].getKind() != kind::ITE)
 680     {
 681       return Node::null();
 682     }
 683     std::vector<Node> disjuncts{
 684         args[0].notNode(), args[0][0].notNode(), args[0][1]};
 685     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 686   }
 687   if (id == PfRule::CNF_ITE_POS2)
 688   {
 689     Assert(children.empty());
 690     Assert(args.size() == 1);
 691     if (args[0].getKind() != kind::ITE)
 692     {
 693       return Node::null();
 694     }
 695     std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][2]};
 696     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 697   }
 698   if (id == PfRule::CNF_ITE_POS3)
 699   {
 700     Assert(children.empty());
 701     Assert(args.size() == 1);
 702     if (args[0].getKind() != kind::ITE)
 703     {
 704       return Node::null();
 705     }
 706     std::vector<Node> disjuncts{args[0].notNode(), args[0][1], args[0][2]};
 707     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 708   }
 709   if (id == PfRule::CNF_ITE_NEG1)
 710   {
 711     Assert(children.empty());
 712     Assert(args.size() == 1);
 713     if (args[0].getKind() != kind::ITE)
 714     {
 715       return Node::null();
 716     }
 717     std::vector<Node> disjuncts{
 718         args[0], args[0][0].notNode(), args[0][1].notNode()};
 719     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 720   }
 721   if (id == PfRule::CNF_ITE_NEG2)
 722   {
 723     Assert(children.empty());
 724     Assert(args.size() == 1);
 725     if (args[0].getKind() != kind::ITE)
 726     {
 727       return Node::null();
 728     }
 729     std::vector<Node> disjuncts{args[0], args[0][0], args[0][2].notNode()};
 730     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 731   }
 732   if (id == PfRule::CNF_ITE_NEG3)
 733   {
 734     Assert(children.empty());
 735     Assert(args.size() == 1);
 736     if (args[0].getKind() != kind::ITE)
 737     {
 738       return Node::null();
 739     }
 740     std::vector<Node> disjuncts{
 741         args[0], args[0][1].notNode(), args[0][2].notNode()};
 742     return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
 743   }
 744   // no rule
 745   return Node::null();
 746 }
 747
 748 }  // namespace booleans
 749 }  // namespace theory
 750 }  // namespace CVC4