src/proof/uf_proof.cpp

   1 /*********************                                                        */
   2 /*! \file uf_proof.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Guy Katz, Yoni Zohar
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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  ** [[ Add lengthier description here ]]
  13
  14  ** \todo document this file
  15
  16 **/
  17 #include "proof/uf_proof.h"
  18
  19 #include <stack>
  20
  21 #include "proof/proof_manager.h"
  22 #include "proof/simplify_boolean_node.h"
  23 #include "theory/uf/theory_uf.h"
  24
  25 namespace CVC4 {
  26
  27 void ProofUF::toStream(std::ostream& out) const
  28 {
  29   ProofLetMap map;
  30   toStream(out, map);
  31 }
  32
  33 void ProofUF::toStream(std::ostream& out, const ProofLetMap& map) const
  34 {
  35   Trace("theory-proof-debug") << "; Print UF proof..." << std::endl;
  36   //AJR : carry this further?
  37   toStreamLFSC(out, ProofManager::getUfProof(), *d_proof, map);
  38 }
  39
  40 void ProofUF::toStreamLFSC(std::ostream& out,
  41                            TheoryProof* tp,
  42                            const theory::eq::EqProof& pf,
  43                            const ProofLetMap& map)
  44 {
  45   Debug("pf::uf") << "ProofUF::toStreamLFSC starting" << std::endl;
  46   Debug("lfsc-uf") << "Printing uf proof in LFSC : " << std::endl;
  47   pf.debug_print("lfsc-uf");
  48   Debug("lfsc-uf") << std::endl;
  49   toStreamRecLFSC( out, tp, pf, 0, map );
  50 }
  51
  52 Node ProofUF::toStreamRecLFSC(std::ostream& out,
  53                               TheoryProof* tp,
  54                               const theory::eq::EqProof& pf,
  55                               unsigned tb,
  56                               const ProofLetMap& map)
  57 {
  58   Debug("pf::uf") << std::endl
  59                   << std::endl
  60                   << "toStreamRecLFSC called. tb = " << tb
  61                   << " . proof:" << std::endl;
  62   if (tb == 0)
  63   {
  64     // Special case: false was an input, so the proof is just "false".
  65     if (pf.d_id == theory::eq::MERGED_THROUGH_EQUALITY &&
  66         pf.d_node == NodeManager::currentNM()->mkConst(false)) {
  67       out << "(clausify_false ";
  68       out << ProofManager::getLitName(NodeManager::currentNM()->mkConst(false).notNode());
  69       out << ")" << std::endl;
  70       return Node();
  71     }
  72
  73     std::shared_ptr<theory::eq::EqProof> subTrans =
  74         std::make_shared<theory::eq::EqProof>();
  75
  76     int neg = tp->assertAndPrint(pf, map, subTrans);
  77
  78     Node n1;
  79     std::stringstream ss, ss2;
  80     Debug("pf::uf") << "\nsubtrans has " << subTrans->d_children.size() << " children\n";
  81     bool disequalityFound = (neg >= 0);
  82
  83     if(!disequalityFound || subTrans->d_children.size() >= 2) {
  84       n1 = toStreamRecLFSC(ss, tp, *subTrans, 1, map);
  85     } else {
  86       n1 = toStreamRecLFSC(ss, tp, *(subTrans->d_children[0]), 1, map);
  87       Debug("pf::uf") << "\nsubTrans unique child "
  88                       << subTrans->d_children[0]->d_id
  89                       << " was proven\ngot: " << n1 << std::endl;
  90     }
  91
  92     Debug("pf::uf") << "\nhave proven: " << n1 << std::endl;
  93
  94     out << "(clausify_false (contra _ ";
  95     if (disequalityFound) {
  96       Node n2 = pf.d_children[neg]->d_node;
  97       Assert(n2.getKind() == kind::NOT);
  98
  99       Debug("pf::uf") << "n2 is " << n2[0] << std::endl;
 100
 101       if (n2[0].getNumChildren() > 0)
 102       {
 103         Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl;
 104       }
 105       if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; }
 106
 107       if(n2[0].getKind() == kind::APPLY_UF) {
 108         out << "(trans _ _ _ _ ";
 109
 110         if (n1[0] == n2[0]) {
 111           out << "(symm _ _ _ ";
 112           out << ss.str();
 113           out << ") ";
 114         } else {
 115           Assert(n1[1] == n2[0]);
 116           out << ss.str();
 117         }
 118         out << "(pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl;
 119       } else if (n2[0].getKind() == kind::BOOLEAN_TERM_VARIABLE) {
 120         out << ss.str() << " " << ProofManager::getLitName(n2[0]) << "))";
 121       } else {
 122         Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
 123         if(n1[1] == n2[0][0]) {
 124           out << "(symm _ _ _ " << ss.str() << ")";
 125         } else {
 126           out << ss.str();
 127         }
 128         out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
 129       }
 130     } else {
 131       Node n2 = pf.d_node;
 132       Assert(n2.getKind() == kind::EQUAL);
 133       Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1]));
 134
 135       out << ss.str();
 136       out << " ";
 137       ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(
 138           out, n1[0].toExpr(), n1[1].toExpr(), map);
 139       out << "))" << std::endl;
 140     }
 141
 142     return Node();
 143   }
 144
 145   switch(pf.d_id) {
 146   case theory::eq::MERGED_THROUGH_CONGRUENCE: {
 147     Debug("pf::uf") << "\nok, looking at congruence:\n";
 148     pf.debug_print("pf::uf");
 149     std::stack<const theory::eq::EqProof*> stk;
 150     for (const theory::eq::EqProof* pf2 = &pf;
 151          pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE;
 152          pf2 = pf2->d_children[0].get()) {
 153       Assert(!pf2->d_node.isNull());
 154       Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF
 155              || pf2->d_node.getKind() == kind::BUILTIN
 156              || pf2->d_node.getKind() == kind::APPLY_UF
 157              || pf2->d_node.getKind() == kind::SELECT
 158              || pf2->d_node.getKind() == kind::STORE);
 159       Assert(pf2->d_children.size() == 2);
 160       out << "(cong _ _ _ _ _ _ ";
 161       stk.push(pf2);
 162     }
 163     Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE);
 164     NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF);
 165     const theory::eq::EqProof* pf2 = stk.top();
 166     stk.pop();
 167     Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
 168     Node n1 = toStreamRecLFSC(out, tp, *(pf2->d_children[0]), tb + 1, map);
 169     out << " ";
 170     std::stringstream ss;
 171     Node n2 = toStreamRecLFSC(ss, tp, *(pf2->d_children[1]), tb + 1, map);
 172     Debug("pf::uf") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
 173     pf2->debug_print("pf::uf");
 174     Debug("pf::uf") << "looking at " << pf2->d_node << "\n";
 175     Debug("pf::uf") << "           " << n1 << "\n";
 176     Debug("pf::uf") << "           " << n2 << "\n";
 177     int side = 0;
 178     if (tp->match(pf2->d_node, n1[0]))
 179     {
 180       //if(tb == 1) {
 181       Debug("pf::uf") << "SIDE IS 0\n";
 182       //}
 183       side = 0;
 184     } else {
 185       //if(tb == 1) {
 186       Debug("pf::uf") << "SIDE IS 1\n";
 187       //}
 188       if (!tp->match(pf2->d_node, n1[1]))
 189       {
 190         Debug("pf::uf") << "IN BAD CASE, our first subproof is\n";
 191         pf2->d_children[0]->debug_print("pf::uf");
 192       }
 193       Assert(tp->match(pf2->d_node, n1[1]));
 194       side = 1;
 195     }
 196     if (n1[side].getKind() == kind::APPLY_UF
 197         || n1[side].getKind() == kind::PARTIAL_APPLY_UF
 198         || n1[side].getKind() == kind::SELECT
 199         || n1[side].getKind() == kind::STORE)
 200     {
 201       if (n1[side].getKind() == kind::APPLY_UF
 202           || n1[side].getKind() == kind::PARTIAL_APPLY_UF)
 203       {
 204         b1 << n1[side].getOperator();
 205       } else {
 206         b1 << ProofManager::currentPM()->mkOp(n1[side].getOperator());
 207       }
 208       b1.append(n1[side].begin(), n1[side].end());
 209     } else {
 210       b1 << n1[side];
 211     }
 212     if(n1[1-side].getKind() == kind::PARTIAL_APPLY_UF || n1[1-side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::SELECT || n1[side].getKind() == kind::STORE) {
 213       if (n1[1 - side].getKind() == kind::PARTIAL_APPLY_UF
 214           || n1[1 - side].getKind() == kind::APPLY_UF)
 215       {
 216         b2 << n1[1-side].getOperator();
 217       } else {
 218         b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator());
 219       }
 220       b2.append(n1[1-side].begin(), n1[1-side].end());
 221     } else {
 222       b2 << n1[1-side];
 223     }
 224     Debug("pf::uf") << "pf2->d_node " << pf2->d_node << std::endl;
 225     Debug("pf::uf") << "b1.getNumChildren() " << b1.getNumChildren() << std::endl;
 226     Debug("pf::uf") << "n1 " << n1 << std::endl;
 227     Debug("pf::uf") << "n2 " << n2 << std::endl;
 228     Debug("pf::uf") << "side " << side << std::endl;
 229     if(pf2->d_node[b1.getNumChildren() - (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[side]) {
 230       b1 << n2[side];
 231       b2 << n2[1-side];
 232       out << ss.str();
 233     } else {
 234       Assert(pf2->d_node[b1.getNumChildren() - (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[1-side]);
 235       b1 << n2[1-side];
 236       b2 << n2[side];
 237       out << "(symm _ _ _ " << ss.str() << ")";
 238     }
 239     out << ")";
 240     while(!stk.empty()) {
 241       if(tb == 1) {
 242         Debug("pf::uf") << "\nMORE TO DO\n";
 243       }
 244       pf2 = stk.top();
 245       stk.pop();
 246       Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
 247       out << " ";
 248       ss.str("");
 249       n2 = toStreamRecLFSC(ss, tp, *(pf2->d_children[1]), tb + 1, map);
 250       Debug("pf::uf") << "\nok, in cong[" << stk.size() << "]" << "\n";
 251       Debug("pf::uf") << "looking at " << pf2->d_node << "\n";
 252       Debug("pf::uf") << "           " << n1 << "\n";
 253       Debug("pf::uf") << "           " << n2 << "\n";
 254       Debug("pf::uf") << "           " << b1 << "\n";
 255       Debug("pf::uf") << "           " << b2 << "\n";
 256       if(pf2->d_node[b1.getNumChildren()] == n2[side]) {
 257         b1 << n2[side];
 258         b2 << n2[1-side];
 259         out << ss.str();
 260       } else {
 261         Assert(pf2->d_node[b1.getNumChildren()] == n2[1-side]);
 262         b1 << n2[1-side];
 263         b2 << n2[side];
 264         out << "(symm _ _ _ " << ss.str() << ")";
 265       }
 266       out << ")";
 267     }
 268     n1 = b1;
 269     n2 = b2;
 270     Debug("pf::uf") << "at end assert, got " << pf2->d_node << "  and  " << n1 << std::endl;
 271     if(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF) {
 272       Assert(n1 == pf2->d_node);
 273     }
 274     if(n1.getOperator().getType().getNumChildren() == n1.getNumChildren() + 1) {
 275       if(ProofManager::currentPM()->hasOp(n1.getOperator())) {
 276         b1.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>());
 277       } else {
 278         b1.clear(kind::APPLY_UF);
 279         b1 << n1.getOperator();
 280       }
 281       b1.append(n1.begin(), n1.end());
 282       n1 = b1;
 283       Debug("pf::uf") << "at[2] end assert, got " << pf2->d_node << "  and  " << n1 << std::endl;
 284       if(pf2->d_node.getKind() == kind::APPLY_UF) {
 285         Assert(n1 == pf2->d_node);
 286       }
 287     }
 288     if(n2.getOperator().getType().getNumChildren() == n2.getNumChildren() + 1) {
 289       if(ProofManager::currentPM()->hasOp(n2.getOperator())) {
 290         b2.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>());
 291       } else {
 292         b2.clear(kind::APPLY_UF);
 293         b2 << n2.getOperator();
 294       }
 295       b2.append(n2.begin(), n2.end());
 296       n2 = b2;
 297     }
 298     Node n = (side == 0 ? n1.eqNode(n2) : n2.eqNode(n1));
 299     if(tb == 1) {
 300       Debug("pf::uf") << "\ncong proved: " << n << "\n";
 301     }
 302     return n;
 303   }
 304
 305   case theory::eq::MERGED_THROUGH_REFLEXIVITY:
 306   {
 307     Assert(!pf.d_node.isNull());
 308     Assert(pf.d_children.empty());
 309     out << "(refl _ ";
 310     tp->printTerm(NodeManager::currentNM()->toExpr(pf.d_node), out, map);
 311     out << ")";
 312     return pf.d_node.eqNode(pf.d_node);
 313   }
 314   case theory::eq::MERGED_THROUGH_EQUALITY:
 315     Assert(!pf.d_node.isNull());
 316     Assert(pf.d_children.empty());
 317     out << ProofManager::getLitName(pf.d_node.negate());
 318     return pf.d_node;
 319
 320   case theory::eq::MERGED_THROUGH_TRANS: {
 321     Assert(!pf.d_node.isNull());
 322     Assert(pf.d_children.size() >= 2);
 323     std::stringstream ss;
 324     Debug("pf::uf") << "\ndoing trans proof[[\n";
 325     pf.debug_print("pf::uf");
 326     Debug("pf::uf") << "\n";
 327
 328     pf.d_children[0]->d_node = simplifyBooleanNode(pf.d_children[0]->d_node);
 329
 330     Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map);
 331     Debug("pf::uf") << "\ndoing trans proof, got n1 " << n1 << "\n";
 332     Node n2;
 333     if(tb == 1) {
 334       Debug("pf::uf") << "\ntrans proof[0], got n1 " << n1 << "\n";
 335     }
 336
 337     bool identicalEqualities = false;
 338     bool evenLengthSequence;
 339     std::stringstream dontCare;
 340     Node nodeAfterEqualitySequence =
 341         toStreamRecLFSC(dontCare, tp, *(pf.d_children[0]), tb + 1, map);
 342
 343     std::map<size_t, Node> childToStream;
 344     std::stringstream ss1(ss.str()), ss2;
 345     std::pair<Node, Node> nodePair;
 346     for(size_t i = 1; i < pf.d_children.size(); ++i) {
 347       std::stringstream ss1(ss.str()), ss2;
 348       ss.str("");
 349
 350       pf.d_children[i]->d_node = simplifyBooleanNode(pf.d_children[i]->d_node);
 351
 352       // It is possible that we've already converted the i'th child to stream.
 353       // If so,
 354       // use previously stored result. Otherwise, convert and store.
 355       Node n2;
 356       if (childToStream.find(i) != childToStream.end())
 357         n2 = childToStream[i];
 358       else
 359       {
 360         n2 = toStreamRecLFSC(ss2, tp, *(pf.d_children[i]), tb + 1, map);
 361         childToStream[i] = n2;
 362       }
 363
 364       // The following branch is dedicated to handling sequences of identical
 365       // equalities,
 366       // i.e. trans[ a=b, a=b, a=b ].
 367       //
 368       // There are two cases:
 369       //    1. The number of equalities is odd. Then, the sequence can be
 370       //    collapsed to just one equality,
 371       //       i.e. a=b.
 372       //    2. The number of equalities is even. Now, we have two options: a=a
 373       //    or b=b. To determine this,
 374       //       we look at the node after the equality sequence. If it needs a,
 375       //       we go for a=a; and if it needs
 376       //       b, we go for b=b. If there is no following node, we look at the
 377       //       goal of the transitivity proof,
 378       //       and use it to determine which option we need.
 379       if (n2.getKind() == kind::EQUAL)
 380       {
 381         if (((n1[0] == n2[0]) && (n1[1] == n2[1]))
 382             || ((n1[0] == n2[1]) && (n1[1] == n2[0])))
 383         {
 384           // We are in a sequence of identical equalities
 385
 386           Debug("pf::uf") << "Detected identical equalities: " << std::endl
 387                           << "\t" << n1 << std::endl;
 388
 389           if (!identicalEqualities)
 390           {
 391             // The sequence of identical equalities has started just now
 392             identicalEqualities = true;
 393
 394             Debug("pf::uf")
 395                 << "The sequence is just beginning. Determining length..."
 396                 << std::endl;
 397
 398             // Determine whether the length of this sequence is odd or even.
 399             evenLengthSequence = true;
 400             bool sequenceOver = false;
 401             size_t j = i + 1;
 402
 403             while (j < pf.d_children.size() && !sequenceOver)
 404             {
 405               std::stringstream dontCare;
 406               nodeAfterEqualitySequence = toStreamRecLFSC(
 407                   dontCare, tp, *(pf.d_children[j]), tb + 1, map);
 408
 409               if (((nodeAfterEqualitySequence[0] == n1[0])
 410                    && (nodeAfterEqualitySequence[1] == n1[1]))
 411                   || ((nodeAfterEqualitySequence[0] == n1[1])
 412                       && (nodeAfterEqualitySequence[1] == n1[0])))
 413               {
 414                 evenLengthSequence = !evenLengthSequence;
 415               }
 416               else
 417               {
 418                 sequenceOver = true;
 419               }
 420
 421               ++j;
 422             }
 423
 424             nodePair =
 425                 tp->identicalEqualitiesPrinterHelper(evenLengthSequence,
 426                                                      sequenceOver,
 427                                                      pf,
 428                                                      map,
 429                                                      ss1.str(),
 430                                                      &ss,
 431                                                      n1,
 432                                                      nodeAfterEqualitySequence);
 433             n1 = nodePair.first;
 434             nodeAfterEqualitySequence = nodePair.second;
 435           } else {
 436             ss.str(ss1.str());
 437           }
 438
 439           // Ignore the redundancy.
 440           continue;
 441         }
 442       }
 443
 444       if (identicalEqualities) {
 445         // We were in a sequence of identical equalities, but it has now ended. Resume normal operation.
 446         identicalEqualities = false;
 447       }
 448
 449       Debug("pf::uf") << "\ndoing trans proof, got n2 " << n2 << "\n";
 450       if(tb == 1) {
 451         Debug("pf::uf") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n";
 452         Debug("pf::uf") << (n2.getKind() == kind::EQUAL) << "\n";
 453
 454         if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) {
 455           Debug("pf::uf") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n";
 456           Debug("pf::uf") << n1[0].getId() << " " << n1[0] << "\n";
 457           Debug("pf::uf") << n1[1].getId() << " " << n1[1] << "\n";
 458           Debug("pf::uf") << n2[0].getId() << " " << n2[0] << "\n";
 459           Debug("pf::uf") << n2[1].getId() << " " << n2[1] << "\n";
 460           Debug("pf::uf") << (n1[0] == n2[0]) << "\n";
 461           Debug("pf::uf") << (n1[1] == n2[1]) << "\n";
 462           Debug("pf::uf") << (n1[0] == n2[1]) << "\n";
 463           Debug("pf::uf") << (n1[1] == n2[0]) << "\n";
 464         }
 465       }
 466
 467       ss << "(trans _ _ _ _ ";
 468
 469       if(n2.getKind() == kind::EQUAL && n1.getKind() == kind::EQUAL)
 470         // Both elements of the transitivity rule are equalities/iffs
 471       {
 472         if(n1[0] == n2[0]) {
 473           if(tb == 1) { Debug("pf::uf") << "case 1\n"; }
 474           n1 = n1[1].eqNode(n2[1]);
 475           ss << "(symm _ _ _ " << ss1.str() << ") " << ss2.str();
 476         } else if(n1[1] == n2[1]) {
 477           if(tb == 1) { Debug("pf::uf") << "case 2\n"; }
 478           n1 = n1[0].eqNode(n2[0]);
 479           ss << ss1.str() << " (symm _ _ _ " << ss2.str() << ")";
 480         } else if(n1[0] == n2[1]) {
 481           if(tb == 1) { Debug("pf::uf") << "case 3\n"; }
 482           n1 = n2[0].eqNode(n1[1]);
 483           ss << ss2.str() << " " << ss1.str();
 484           if(tb == 1) { Debug("pf::uf") << "++ proved " << n1 << "\n"; }
 485         } else if(n1[1] == n2[0]) {
 486           if(tb == 1) { Debug("pf::uf") << "case 4\n"; }
 487           n1 = n1[0].eqNode(n2[1]);
 488           ss << ss1.str() << " " << ss2.str();
 489         } else {
 490           Warning() << "\n\ntrans proof failure at step " << i << "\n\n";
 491           Warning() << "0 proves " << n1 << "\n";
 492           Warning() << "1 proves " << n2 << "\n\n";
 493           pf.debug_print("pf::uf",0);
 494           //toStreamRec(Warning.getStream(), pf, 0);
 495           Warning() << "\n\n";
 496           Unreachable();
 497         }
 498         Debug("pf::uf") << "++ trans proof[" << i << "], now have " << n1 << std::endl;
 499       } else if(n1.getKind() == kind::EQUAL) {
 500         // n1 is an equality/iff, but n2 is a predicate
 501         if(n1[0] == n2) {
 502           n1 = n1[1].eqNode(NodeManager::currentNM()->mkConst(true));
 503           ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")";
 504         } else if(n1[1] == n2) {
 505           n1 = n1[0].eqNode(NodeManager::currentNM()->mkConst(true));
 506           ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")";
 507         } else {
 508           Unreachable();
 509         }
 510       } else if(n2.getKind() == kind::EQUAL) {
 511         // n2 is an equality/iff, but n1 is a predicate
 512         if(n2[0] == n1) {
 513           n1 = n2[1].eqNode(NodeManager::currentNM()->mkConst(true));
 514           ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")";
 515         } else if(n2[1] == n1) {
 516           n1 = n2[0].eqNode(NodeManager::currentNM()->mkConst(true));
 517           ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")";
 518         } else {
 519           Unreachable();
 520         }
 521       } else {
 522         // Both n1 and n2 are predicates.
 523         // We want to prove b1 = b2, and we know that ((b1), (b2)) or ((not b1), (not b2))
 524         if (n1.getKind() == kind::NOT) {
 525           Assert(n2.getKind() == kind::NOT);
 526           Assert(pf.d_node[0] == n1[0] || pf.d_node[0] == n2[0]);
 527           Assert(pf.d_node[1] == n1[0] || pf.d_node[1] == n2[0]);
 528           Assert(n1[0].getKind() == kind::BOOLEAN_TERM_VARIABLE);
 529           Assert(n2[0].getKind() == kind::BOOLEAN_TERM_VARIABLE);
 530
 531           if (pf.d_node[0] == n1[0]) {
 532             ss << "(false_preds_equal _ _ " << ss1.str() << " " << ss2.str() << ") ";
 533             ss << "(pred_refl_neg _ " << ss2.str() << ")";
 534           } else {
 535             ss << "(false_preds_equal _ _ " << ss2.str() << " " << ss1.str() << ") ";
 536             ss << "(pred_refl_neg _ " << ss1.str() << ")";
 537           }
 538           n1 = pf.d_node;
 539
 540         } else if (n1.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
 541           Assert(n2.getKind() == kind::BOOLEAN_TERM_VARIABLE);
 542           Assert(pf.d_node[0] == n1 || pf.d_node[0] == n2);
 543           Assert(pf.d_node[1] == n1 || pf.d_node[2] == n2);
 544
 545           if (pf.d_node[0] == n1) {
 546             ss << "(true_preds_equal _ _ " << ss1.str() << " " << ss2.str() << ") ";
 547             ss << "(pred_refl_pos _ " << ss2.str() << ")";
 548           } else {
 549             ss << "(true_preds_equal _ _ " << ss2.str() << " " << ss1.str() << ") ";
 550             ss << "(pred_refl_pos _ " << ss1.str() << ")";
 551           }
 552           n1 = pf.d_node;
 553
 554         } else {
 555
 556           Unreachable();
 557         }
 558       }
 559
 560       ss << ")";
 561     }
 562     out << ss.str();
 563     Debug("pf::uf") << "\n++ trans proof done, have proven " << n1 << std::endl;
 564     return n1;
 565   }
 566
 567   default:
 568     Assert(!pf.d_node.isNull());
 569     Assert(pf.d_children.empty());
 570     Debug("pf::uf") << "theory proof: " << pf.d_node << " by rule " << int(pf.d_id) << std::endl;
 571     AlwaysAssert(false);
 572     return pf.d_node;
 573   }
 574 }
 575
 576 UFProof::UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* pe)
 577   : TheoryProof(uf, pe)
 578 {}
 579
 580 theory::TheoryId UFProof::getTheoryId() { return theory::THEORY_UF; }
 581 void UFProof::registerTerm(Expr term) {
 582   // already registered
 583   if (d_declarations.find(term) != d_declarations.end())
 584     return;
 585
 586   Type type = term.getType();
 587   if (type.isSort()) {
 588     // declare uninterpreted sorts
 589     d_sorts.insert(type);
 590   }
 591
 592   if (term.getKind() == kind::APPLY_UF) {
 593     Expr function = term.getOperator();
 594     d_declarations.insert(function);
 595   }
 596
 597   if (term.isVariable()) {
 598     d_declarations.insert(term);
 599
 600
 601     if (term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
 602       // Ensure cnf literals
 603       Node asNode(term);
 604       ProofManager::currentPM()->ensureLiteral(
 605           asNode.eqNode(NodeManager::currentNM()->mkConst(true)));
 606       ProofManager::currentPM()->ensureLiteral(
 607           asNode.eqNode(NodeManager::currentNM()->mkConst(false)));
 608     }
 609   }
 610
 611   // recursively declare all other terms
 612   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
 613     // could belong to other theories
 614     d_proofEngine->registerTerm(term[i]);
 615   }
 616 }
 617
 618 void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
 619   Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term << std::endl;
 620
 621   Assert (theory::Theory::theoryOf(term) == theory::THEORY_UF);
 622
 623   if (term.getKind() == kind::VARIABLE ||
 624       term.getKind() == kind::SKOLEM ||
 625       term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
 626     os << term;
 627     return;
 628   }
 629
 630   Assert (term.getKind() == kind::APPLY_UF);
 631
 632   if(term.getType().isBoolean()) {
 633     os << "(p_app ";
 634   }
 635   Expr func = term.getOperator();
 636   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
 637     os << "(apply _ _ ";
 638   }
 639   os << func << " ";
 640   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
 641
 642     bool convertToBool = (term[i].getType().isBoolean() && !d_proofEngine->printsAsBool(term[i]));
 643     if (convertToBool) os << "(f_to_b ";
 644     d_proofEngine->printBoundTerm(term[i], os, map);
 645     if (convertToBool) os << ")";
 646     os << ")";
 647   }
 648   if(term.getType().isBoolean()) {
 649     os << ")";
 650   }
 651 }
 652
 653 void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) {
 654   Debug("pf::uf") << std::endl << "(pf::uf) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl;
 655
 656   Assert (type.isSort());
 657   os << type;
 658 }
 659
 660 void LFSCUFProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
 661   os << " ;; UF Theory Lemma \n;;";
 662   for (unsigned i = 0; i < lemma.size(); ++i) {
 663     os << lemma[i] <<" ";
 664   }
 665   os <<"\n";
 666   //os << " (clausify_false trust)";
 667   UFProof::printTheoryLemmaProof(lemma, os, paren, map);
 668 }
 669
 670 void LFSCUFProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
 671   for (TypeSet::const_iterator it = d_sorts.begin(); it != d_sorts.end(); ++it) {
 672     if (!ProofManager::currentPM()->wasPrinted(*it)) {
 673       os << "(% " << *it << " sort\n";
 674       paren << ")";
 675       ProofManager::currentPM()->markPrinted(*it);
 676     }
 677   }
 678 }
 679
 680 void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
 681   // declaring the terms
 682   Debug("pf::uf") << "LFSCUFProof::printTermDeclarations called" << std::endl;
 683
 684   for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) {
 685     Expr term = *it;
 686
 687     os << "(% " << ProofManager::sanitize(term) << " ";
 688     os << "(term ";
 689
 690     Type type = term.getType();
 691     if (type.isFunction()) {
 692       std::ostringstream fparen;
 693       FunctionType ftype = (FunctionType)type;
 694       std::vector<Type> args = ftype.getArgTypes();
 695       args.push_back(ftype.getRangeType());
 696       os << "(arrow";
 697       for (unsigned i = 0; i < args.size(); i++) {
 698         Type arg_type = args[i];
 699         os << " ";
 700         d_proofEngine->printSort(arg_type, os);
 701         if (i < args.size() - 2) {
 702           os << " (arrow";
 703           fparen << ")";
 704         }
 705       }
 706       os << fparen.str() << "))\n";
 707     } else {
 708       Assert (term.isVariable());
 709       os << type << ")\n";
 710     }
 711     paren << ")";
 712   }
 713
 714   Debug("pf::uf") << "LFSCUFProof::printTermDeclarations done" << std::endl;
 715 }
 716
 717 void LFSCUFProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) {
 718   // Nothing to do here at this point.
 719 }
 720
 721 void LFSCUFProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
 722   // Nothing to do here at this point.
 723 }
 724
 725 bool LFSCUFProof::printsAsBool(const Node &n) {
 726   if (n.getKind() == kind::BOOLEAN_TERM_VARIABLE)
 727     return true;
 728
 729   return false;
 730 }
 731
 732 void LFSCUFProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) {
 733   Node falseNode = NodeManager::currentNM()->mkConst(false);
 734   Node trueNode = NodeManager::currentNM()->mkConst(true);
 735
 736   Assert(c1 == falseNode.toExpr() || c1 == trueNode.toExpr());
 737   Assert(c2 == falseNode.toExpr() || c2 == trueNode.toExpr());
 738   Assert(c1 != c2);
 739
 740   if (c1 == trueNode.toExpr())
 741     os << "t_t_neq_f";
 742   else
 743     os << "(symm _ _ _ t_t_neq_f)";
 744 }
 745
 746 } /* namespace CVC4 */