src/proof/arith_proof.cpp

   1 /*********************                                                        */
   2 /*! \file arith_proof.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Guy Katz, Tim King, Andrew Reynolds
   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/arith_proof.h"
  18
  19 #include <memory>
  20 #include <stack>
  21
  22 #include "proof/proof_manager.h"
  23 #include "proof/theory_proof.h"
  24 #include "theory/arith/theory_arith.h"
  25
  26 namespace CVC4 {
  27
  28 inline static Node eqNode(TNode n1, TNode n2) {
  29   return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2);
  30 }
  31
  32 // congrence matching term helper
  33 inline static bool match(TNode n1, TNode n2) {
  34   Debug("pf::arith") << "match " << n1 << " " << n2 << std::endl;
  35   if(ProofManager::currentPM()->hasOp(n1)) {
  36     n1 = ProofManager::currentPM()->lookupOp(n1);
  37   }
  38   if(ProofManager::currentPM()->hasOp(n2)) {
  39     n2 = ProofManager::currentPM()->lookupOp(n2);
  40   }
  41   Debug("pf::arith") << "+ match " << n1 << " " << n2 << std::endl;
  42   if(n1 == n2) {
  43     return true;
  44   }
  45   if(n1.getType().isFunction() && n2.hasOperator()) {
  46     if(ProofManager::currentPM()->hasOp(n2.getOperator())) {
  47       return n1 == ProofManager::currentPM()->lookupOp(n2.getOperator());
  48     } else {
  49       return n1 == n2.getOperator();
  50     }
  51   }
  52   if(n2.getType().isFunction() && n1.hasOperator()) {
  53     if(ProofManager::currentPM()->hasOp(n1.getOperator())) {
  54       return n2 == ProofManager::currentPM()->lookupOp(n1.getOperator());
  55     } else {
  56       return n2 == n1.getOperator();
  57     }
  58   }
  59   if(n1.hasOperator() && n2.hasOperator() && n1.getOperator() != n2.getOperator()) {
  60     return false;
  61   }
  62   for(size_t i = 0; i < n1.getNumChildren() && i < n2.getNumChildren(); ++i) {
  63     if(n1[i] != n2[i]) {
  64       return false;
  65     }
  66   }
  67   return true;
  68 }
  69
  70 void ProofArith::toStream(std::ostream& out) const
  71 {
  72   Trace("theory-proof-debug") << "; Print Arith proof..." << std::endl;
  73   //AJR : carry this further?
  74   ProofLetMap map;
  75   toStreamLFSC(out, ProofManager::getArithProof(), *d_proof, map);
  76 }
  77
  78 void ProofArith::toStreamLFSC(std::ostream& out,
  79                               TheoryProof* tp,
  80                               const theory::eq::EqProof& pf,
  81                               const ProofLetMap& map)
  82 {
  83   Debug("lfsc-arith") << "Printing arith proof in LFSC : " << std::endl;
  84   pf.debug_print("lfsc-arith");
  85   Debug("lfsc-arith") << std::endl;
  86   toStreamRecLFSC(out, tp, pf, 0, map);
  87 }
  88
  89 Node ProofArith::toStreamRecLFSC(std::ostream& out,
  90                                  TheoryProof* tp,
  91                                  const theory::eq::EqProof& pf,
  92                                  unsigned tb,
  93                                  const ProofLetMap& map)
  94 {
  95   Debug("pf::arith") << std::endl
  96                      << std::endl
  97                      << "toStreamRecLFSC called. tb = " << tb
  98                      << " . proof:" << std::endl;
  99   pf.debug_print("pf::arith");
 100   Debug("pf::arith") << std::endl;
 101
 102   if(tb == 0) {
 103     Assert(pf.d_id == theory::eq::MERGED_THROUGH_TRANS);
 104     Assert(!pf.d_node.isNull());
 105     Assert(pf.d_children.size() >= 2);
 106
 107     int neg = -1;
 108     std::shared_ptr<theory::eq::EqProof> subTrans =
 109         std::make_shared<theory::eq::EqProof>();
 110     subTrans->d_id = theory::eq::MERGED_THROUGH_TRANS;
 111     subTrans->d_node = pf.d_node;
 112
 113     size_t i = 0;
 114     while (i < pf.d_children.size()) {
 115       // Look for the negative clause, with which we will form a contradiction.
 116       if(!pf.d_children[i]->d_node.isNull() && pf.d_children[i]->d_node.getKind() == kind::NOT) {
 117         Assert(neg < 0);
 118         neg = i;
 119         ++i;
 120       }
 121
 122       // Handle congruence closures over equalities.
 123       else if (pf.d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf.d_children[i]->d_node.isNull()) {
 124         Debug("pf::arith") << "Handling congruence over equalities" << std::endl;
 125
 126         // Gather the sequence of consecutive congruence closures.
 127         std::vector<std::shared_ptr<const theory::eq::EqProof>> congruenceClosures;
 128         unsigned count;
 129         Debug("pf::arith") << "Collecting congruence sequence" << std::endl;
 130         for (count = 0;
 131              i + count < pf.d_children.size() &&
 132              pf.d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
 133              pf.d_children[i + count]->d_node.isNull();
 134              ++count) {
 135           Debug("pf::arith") << "Found a congruence: " << std::endl;
 136           pf.d_children[i+count]->debug_print("pf::arith");
 137           congruenceClosures.push_back(pf.d_children[i+count]);
 138         }
 139
 140         Debug("pf::arith") << "Total number of congruences found: " << congruenceClosures.size() << std::endl;
 141
 142         // Determine if the "target" of the congruence sequence appears right before or right after the sequence.
 143         bool targetAppearsBefore = true;
 144         bool targetAppearsAfter = true;
 145
 146         if ((i == 0) || (i == 1 && neg == 0)) {
 147           Debug("pf::arith") << "Target does not appear before" << std::endl;
 148           targetAppearsBefore = false;
 149         }
 150
 151         if ((i + count >= pf.d_children.size()) ||
 152             (!pf.d_children[i + count]->d_node.isNull() &&
 153              pf.d_children[i + count]->d_node.getKind() == kind::NOT)) {
 154           Debug("pf::arith") << "Target does not appear after" << std::endl;
 155           targetAppearsAfter = false;
 156         }
 157
 158         // Assert that we have precisely one target clause.
 159         Assert(targetAppearsBefore != targetAppearsAfter);
 160
 161         // Begin breaking up the congruences and ordering the equalities correctly.
 162         std::vector<std::shared_ptr<theory::eq::EqProof>> orderedEqualities;
 163
 164
 165         // Insert target clause first.
 166         if (targetAppearsBefore) {
 167           orderedEqualities.push_back(pf.d_children[i - 1]);
 168           // The target has already been added to subTrans; remove it.
 169           subTrans->d_children.pop_back();
 170         } else {
 171           orderedEqualities.push_back(pf.d_children[i + count]);
 172         }
 173
 174         // Start with the congruence closure closest to the target clause, and work our way back/forward.
 175         if (targetAppearsBefore) {
 176           for (unsigned j = 0; j < count; ++j) {
 177             if (pf.d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
 178               orderedEqualities.insert(orderedEqualities.begin(), pf.d_children[i + j]->d_children[0]);
 179             if (pf.d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
 180             orderedEqualities.insert(orderedEqualities.end(), pf.d_children[i + j]->d_children[1]);
 181           }
 182         } else {
 183           for (unsigned j = 0; j < count; ++j) {
 184             if (pf.d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
 185               orderedEqualities.insert(orderedEqualities.begin(), pf.d_children[i + count - 1 - j]->d_children[0]);
 186             if (pf.d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
 187               orderedEqualities.insert(orderedEqualities.end(), pf.d_children[i + count - 1 - j]->d_children[1]);
 188           }
 189         }
 190
 191         // Copy the result into the main transitivity proof.
 192         subTrans->d_children.insert(subTrans->d_children.end(), orderedEqualities.begin(), orderedEqualities.end());
 193
 194         // Increase i to skip over the children that have been processed.
 195         i += count;
 196         if (targetAppearsAfter) {
 197           ++i;
 198         }
 199       }
 200
 201       // Else, just copy the child proof as is
 202       else {
 203         subTrans->d_children.push_back(pf.d_children[i]);
 204         ++i;
 205       }
 206     }
 207     Assert(neg >= 0);
 208
 209     Node n1;
 210     std::stringstream ss;
 211     //Assert(subTrans->d_children.size() == pf.d_children.size() - 1);
 212     Debug("pf::arith") << "\nsubtrans has " << subTrans->d_children.size() << " children\n";
 213     if(pf.d_children.size() > 2) {
 214       n1 = toStreamRecLFSC(ss, tp, *subTrans, 1, map);
 215     } else {
 216       n1 = toStreamRecLFSC(ss, tp, *(subTrans->d_children[0]), 1, map);
 217       Debug("pf::arith") << "\nsubTrans unique child " << subTrans->d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
 218     }
 219
 220     Node n2 = pf.d_children[neg]->d_node;
 221     Assert(n2.getKind() == kind::NOT);
 222     out << "(clausify_false (contra _ ";
 223     Debug("pf::arith") << "\nhave proven: " << n1 << std::endl;
 224     Debug("pf::arith") << "n2 is " << n2[0] << std::endl;
 225
 226     if (n2[0].getNumChildren() > 0) { Debug("pf::arith") << "\nn2[0]: " << n2[0][0] << std::endl; }
 227     if (n1.getNumChildren() > 1) { Debug("pf::arith") << "n1[1]: " << n1[1] << std::endl; }
 228
 229     if(n2[0].getKind() == kind::APPLY_UF) {
 230       out << "(trans _ _ _ _ ";
 231       out << "(symm _ _ _ ";
 232       out << ss.str();
 233       out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl;
 234     } else {
 235       Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
 236       if(n1[1] == n2[0][0]) {
 237         out << "(symm _ _ _ " << ss.str() << ")";
 238       } else {
 239         out << ss.str();
 240       }
 241       out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
 242     }
 243     return Node();
 244   }
 245
 246   switch(pf.d_id) {
 247   case theory::eq::MERGED_THROUGH_CONGRUENCE: {
 248     Debug("pf::arith") << "\nok, looking at congruence:\n";
 249     pf.debug_print("pf::arith");
 250     std::stack<const theory::eq::EqProof*> stk;
 251     for (const theory::eq::EqProof* pf2 = &pf;
 252          pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE;
 253          pf2 = pf2->d_children[0].get()) {
 254       Assert(!pf2->d_node.isNull());
 255       Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || pf2->d_node.getKind() == kind::BUILTIN || pf2->d_node.getKind() == kind::APPLY_UF || pf2->d_node.getKind() == kind::SELECT || pf2->d_node.getKind() == kind::STORE);
 256       Assert(pf2->d_children.size() == 2);
 257       out << "(cong _ _ _ _ _ _ ";
 258       stk.push(pf2);
 259     }
 260     Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE);
 261     NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF);
 262     const theory::eq::EqProof* pf2 = stk.top();
 263     stk.pop();
 264     Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
 265     Node n1 = toStreamRecLFSC(out, tp, *(pf2->d_children[0]), tb + 1, map);
 266     out << " ";
 267     std::stringstream ss;
 268     Node n2 = toStreamRecLFSC(ss, tp, *(pf2->d_children[1]), tb + 1, map);
 269     Debug("pf::arith") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
 270     pf2->debug_print("pf::arith");
 271     Debug("pf::arith") << "looking at " << pf2->d_node << "\n";
 272     Debug("pf::arith") << "           " << n1 << "\n";
 273     Debug("pf::arith") << "           " << n2 << "\n";
 274     int side = 0;
 275     if(match(pf2->d_node, n1[0])) {
 276       //if(tb == 1) {
 277       Debug("pf::arith") << "SIDE IS 0\n";
 278       //}
 279       side = 0;
 280     } else {
 281       //if(tb == 1) {
 282       Debug("pf::arith") << "SIDE IS 1\n";
 283       //}
 284       if(!match(pf2->d_node, n1[1])) {
 285       Debug("pf::arith") << "IN BAD CASE, our first subproof is\n";
 286       pf2->d_children[0]->debug_print("pf::arith");
 287       }
 288       Assert(match(pf2->d_node, n1[1]));
 289       side = 1;
 290     }
 291     if(n1[side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::PARTIAL_APPLY_UF || n1[side].getKind() == kind::SELECT || n1[side].getKind() == kind::STORE) {
 292       if(n1[side].getKind() == kind::APPLY_UF || n1[side].getKind() == kind::PARTIAL_APPLY_UF) {
 293         b1 << n1[side].getOperator();
 294       } else {
 295         b1 << ProofManager::currentPM()->mkOp(n1[side].getOperator());
 296       }
 297       b1.append(n1[side].begin(), n1[side].end());
 298     } else {
 299       b1 << n1[side];
 300     }
 301     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) {
 302       if(n1[1-side].getKind() == kind::PARTIAL_APPLY_UF || n1[1-side].getKind() == kind::APPLY_UF) {
 303         b2 << n1[1-side].getOperator();
 304       } else {
 305         b2 << ProofManager::currentPM()->mkOp(n1[1-side].getOperator());
 306       }
 307       b2.append(n1[1-side].begin(), n1[1-side].end());
 308     } else {
 309       b2 << n1[1-side];
 310     }
 311     Debug("pf::arith") << "pf2->d_node " << pf2->d_node << std::endl;
 312     Debug("pf::arith") << "b1.getNumChildren() " << b1.getNumChildren() << std::endl;
 313     Debug("pf::arith") << "n1 " << n1 << std::endl;
 314     Debug("pf::arith") << "n2 " << n2 << std::endl;
 315     Debug("pf::arith") << "side " << side << std::endl;
 316     if(pf2->d_node[b1.getNumChildren() - (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[side]) {
 317       b1 << n2[side];
 318       b2 << n2[1-side];
 319       out << ss.str();
 320     } else {
 321       Assert(pf2->d_node[b1.getNumChildren() - (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[1-side]);
 322       b1 << n2[1-side];
 323       b2 << n2[side];
 324       out << "(symm _ _ _ " << ss.str() << ")";
 325     }
 326     out << ")";
 327     while(!stk.empty()) {
 328       if(tb == 1) {
 329       Debug("pf::arith") << "\nMORE TO DO\n";
 330       }
 331       pf2 = stk.top();
 332       stk.pop();
 333       Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
 334       out << " ";
 335       ss.str("");
 336       n2 = toStreamRecLFSC(ss, tp, *(pf2->d_children[1]), tb + 1, map);
 337       Debug("pf::arith") << "\nok, in cong[" << stk.size() << "]" << "\n";
 338       Debug("pf::arith") << "looking at " << pf2->d_node << "\n";
 339       Debug("pf::arith") << "           " << n1 << "\n";
 340       Debug("pf::arith") << "           " << n2 << "\n";
 341       Debug("pf::arith") << "           " << b1 << "\n";
 342       Debug("pf::arith") << "           " << b2 << "\n";
 343       if(pf2->d_node[b1.getNumChildren()] == n2[side]) {
 344         b1 << n2[side];
 345         b2 << n2[1-side];
 346         out << ss.str();
 347       } else {
 348         Assert(pf2->d_node[b1.getNumChildren()] == n2[1-side]);
 349         b1 << n2[1-side];
 350         b2 << n2[side];
 351         out << "(symm _ _ _ " << ss.str() << ")";
 352       }
 353       out << ")";
 354     }
 355     n1 = b1;
 356     n2 = b2;
 357     Debug("pf::arith") << "at end assert, got " << pf2->d_node << "  and  " << n1 << std::endl;
 358     if(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF) {
 359       Assert(n1 == pf2->d_node);
 360     }
 361     if(n1.getOperator().getType().getNumChildren() == n1.getNumChildren() + 1) {
 362       if(ProofManager::currentPM()->hasOp(n1.getOperator())) {
 363         b1.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>());
 364       } else {
 365         b1.clear(kind::APPLY_UF);
 366         b1 << n1.getOperator();
 367       }
 368       b1.append(n1.begin(), n1.end());
 369       n1 = b1;
 370       Debug("pf::arith") << "at[2] end assert, got " << pf2->d_node << "  and  " << n1 << std::endl;
 371       if(pf2->d_node.getKind() == kind::APPLY_UF) {
 372         Assert(n1 == pf2->d_node);
 373       }
 374     }
 375     if(n2.getOperator().getType().getNumChildren() == n2.getNumChildren() + 1) {
 376       if(ProofManager::currentPM()->hasOp(n2.getOperator())) {
 377         b2.clear(ProofManager::currentPM()->lookupOp(n2.getOperator()).getConst<Kind>());
 378       } else {
 379         b2.clear(kind::APPLY_UF);
 380         b2 << n2.getOperator();
 381       }
 382       b2.append(n2.begin(), n2.end());
 383       n2 = b2;
 384     }
 385     Node n = (side == 0 ? eqNode(n1, n2) : eqNode(n2, n1));
 386     if(tb == 1) {
 387     Debug("pf::arith") << "\ncong proved: " << n << "\n";
 388     }
 389     return n;
 390   }
 391
 392   case theory::eq::MERGED_THROUGH_REFLEXIVITY:
 393     Assert(!pf.d_node.isNull());
 394     Assert(pf.d_children.empty());
 395     out << "(refl _ ";
 396     tp->printTerm(NodeManager::currentNM()->toExpr(pf.d_node), out, map);
 397     out << ")";
 398     return eqNode(pf.d_node, pf.d_node);
 399
 400   case theory::eq::MERGED_THROUGH_EQUALITY:
 401     Assert(!pf.d_node.isNull());
 402     Assert(pf.d_children.empty());
 403     out << ProofManager::getLitName(pf.d_node.negate());
 404     return pf.d_node;
 405
 406   case theory::eq::MERGED_THROUGH_TRANS: {
 407     Assert(!pf.d_node.isNull());
 408     Assert(pf.d_children.size() >= 2);
 409     std::stringstream ss;
 410     Debug("pf::arith") << "\ndoing trans proof[[\n";
 411     pf.debug_print("pf::arith");
 412     Debug("pf::arith") << "\n";
 413     Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map);
 414     Debug("pf::arith") << "\ndoing trans proof, got n1 " << n1 << "\n";
 415     if(tb == 1) {
 416       Debug("pf::arith") << "\ntrans proof[0], got n1 " << n1 << "\n";
 417     }
 418
 419     bool identicalEqualities = false;
 420     bool evenLengthSequence;
 421     Node nodeAfterEqualitySequence;
 422
 423     std::map<size_t, Node> childToStream;
 424
 425     for(size_t i = 1; i < pf.d_children.size(); ++i) {
 426       std::stringstream ss1(ss.str()), ss2;
 427       ss.str("");
 428
 429       // It is possible that we've already converted the i'th child to stream. If so,
 430       // use previously stored result. Otherwise, convert and store.
 431       Node n2;
 432       if (childToStream.find(i) != childToStream.end())
 433         n2 = childToStream[i];
 434       else {
 435         n2 = toStreamRecLFSC(ss2, tp, *(pf.d_children[i]), tb + 1, map);
 436         childToStream[i] = n2;
 437       }
 438
 439       // The following branch is dedicated to handling sequences of identical equalities,
 440       // i.e. trans[ a=b, a=b, a=b ].
 441       //
 442       // There are two cases:
 443       //    1. The number of equalities is odd. Then, the sequence can be collapsed to just one equality,
 444       //       i.e. a=b.
 445       //    2. The number of equalities is even. Now, we have two options: a=a or b=b. To determine this,
 446       //       we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs
 447       //       b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof,
 448       //       and use it to determine which option we need.
 449       if(n2.getKind() == kind::EQUAL) {
 450         if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) {
 451           // We are in a sequence of identical equalities
 452
 453           Debug("pf::arith") << "Detected identical equalities: " << std::endl << "\t" << n1 << std::endl;
 454
 455           if (!identicalEqualities) {
 456             // The sequence of identical equalities has started just now
 457             identicalEqualities = true;
 458
 459             Debug("pf::arith") << "The sequence is just beginning. Determining length..." << std::endl;
 460
 461             // Determine whether the length of this sequence is odd or even.
 462             evenLengthSequence = true;
 463             bool sequenceOver = false;
 464             size_t j = i + 1;
 465
 466             while (j < pf.d_children.size() && !sequenceOver) {
 467               std::stringstream dontCare;
 468               nodeAfterEqualitySequence = toStreamRecLFSC(
 469                   dontCare, tp, *(pf.d_children[j]), tb + 1, map);
 470
 471               if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) ||
 472                   ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) {
 473                 evenLengthSequence = !evenLengthSequence;
 474               } else {
 475                 sequenceOver = true;
 476               }
 477
 478               ++j;
 479             }
 480
 481             if (evenLengthSequence) {
 482               // If the length is even, we need to apply transitivity for the "correct" hand of the equality.
 483
 484               Debug("pf::arith") << "Equality sequence of even length" << std::endl;
 485               Debug("pf::arith") << "n1 is: " << n1 << std::endl;
 486               Debug("pf::arith") << "n2 is: " << n2 << std::endl;
 487               Debug("pf::arith") << "pf-d_node is: " << pf.d_node << std::endl;
 488               Debug("pf::arith") << "Next node is: " << nodeAfterEqualitySequence << std::endl;
 489
 490               ss << "(trans _ _ _ _ ";
 491
 492               // If the sequence is at the very end of the transitivity proof, use pf.d_node to guide us.
 493               if (!sequenceOver) {
 494                 if (match(n1[0], pf.d_node[0])) {
 495                   n1 = eqNode(n1[0], n1[0]);
 496                   ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")";
 497                 } else if (match(n1[1], pf.d_node[1])) {
 498                   n1 = eqNode(n1[1], n1[1]);
 499                   ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str();
 500                 } else {
 501                   Debug("pf::arith") << "Error: identical equalities over, but hands don't match what we're proving."
 502                                      << std::endl;
 503                   Assert(false);
 504                 }
 505               } else {
 506                 // We have a "next node". Use it to guide us.
 507
 508                 Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL);
 509
 510                 if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) {
 511
 512                   // Eliminate n1[1]
 513                   ss << ss1.str() << " (symm _ _ _ " << ss1.str() << ")";
 514                   n1 = eqNode(n1[0], n1[0]);
 515
 516                 } else if ((n1[1] == nodeAfterEqualitySequence[0]) || (n1[1] == nodeAfterEqualitySequence[1])) {
 517
 518                   // Eliminate n1[0]
 519                   ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str();
 520                   n1 = eqNode(n1[1], n1[1]);
 521
 522                 } else {
 523                   Debug("pf::arith") << "Error: even length sequence, but I don't know which hand to keep!" << std::endl;
 524                   Assert(false);
 525                 }
 526               }
 527
 528               ss << ")";
 529
 530             } else {
 531               Debug("pf::arith") << "Equality sequence length is odd!" << std::endl;
 532               ss.str(ss1.str());
 533             }
 534
 535             Debug("pf::arith") << "Have proven: " << n1 << std::endl;
 536           } else {
 537             ss.str(ss1.str());
 538           }
 539
 540           // Ignore the redundancy.
 541           continue;
 542         }
 543       }
 544
 545       if (identicalEqualities) {
 546         // We were in a sequence of identical equalities, but it has now ended. Resume normal operation.
 547         identicalEqualities = false;
 548       }
 549
 550       Debug("pf::arith") << "\ndoing trans proof, got n2 " << n2 << "\n";
 551       if(tb == 1) {
 552         Debug("pf::arith") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n";
 553         Debug("pf::arith") << (n2.getKind() == kind::EQUAL) << "\n";
 554
 555         if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) {
 556           Debug("pf::arith") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n";
 557           Debug("pf::arith") << n1[0].getId() << " " << n1[0] << "\n";
 558           Debug("pf::arith") << n1[1].getId() << " " << n1[1] << "\n";
 559           Debug("pf::arith") << n2[0].getId() << " " << n2[0] << "\n";
 560           Debug("pf::arith") << n2[1].getId() << " " << n2[1] << "\n";
 561           Debug("pf::arith") << (n1[0] == n2[0]) << "\n";
 562           Debug("pf::arith") << (n1[1] == n2[1]) << "\n";
 563           Debug("pf::arith") << (n1[0] == n2[1]) << "\n";
 564           Debug("pf::arith") << (n1[1] == n2[0]) << "\n";
 565         }
 566       }
 567       ss << "(trans _ _ _ _ ";
 568
 569       if((n2.getKind() == kind::EQUAL) && (n1.getKind() == kind::EQUAL))
 570         // Both elements of the transitivity rule are equalities/iffs
 571       {
 572         if(n1[0] == n2[0]) {
 573             if(tb == 1) { Debug("pf::arith") << "case 1\n"; }
 574             n1 = eqNode(n1[1], n2[1]);
 575             ss << "(symm _ _ _ " << ss1.str() << ") " << ss2.str();
 576         } else if(n1[1] == n2[1]) {
 577           if(tb == 1) { Debug("pf::arith") << "case 2\n"; }
 578           n1 = eqNode(n1[0], n2[0]);
 579           ss << ss1.str() << " (symm _ _ _ " << ss2.str() << ")";
 580         } else if(n1[0] == n2[1]) {
 581             if(tb == 1) { Debug("pf::arith") << "case 3\n"; }
 582             n1 = eqNode(n2[0], n1[1]);
 583             ss << ss2.str() << " " << ss1.str();
 584             if(tb == 1) { Debug("pf::arith") << "++ proved " << n1 << "\n"; }
 585         } else if(n1[1] == n2[0]) {
 586           if(tb == 1) { Debug("pf::arith") << "case 4\n"; }
 587           n1 = eqNode(n1[0], n2[1]);
 588           ss << ss1.str() << " " << ss2.str();
 589         } else {
 590           Warning() << "\n\ntrans proof failure at step " << i << "\n\n";
 591           Warning() << "0 proves " << n1 << "\n";
 592           Warning() << "1 proves " << n2 << "\n\n";
 593           pf.debug_print("pf::arith",0);
 594           //toStreamRec(Warning.getStream(), pf, 0);
 595           Warning() << "\n\n";
 596           Unreachable();
 597         }
 598         Debug("pf::arith") << "++ trans proof[" << i << "], now have " << n1 << std::endl;
 599       } else if(n1.getKind() == kind::EQUAL) {
 600         // n1 is an equality/iff, but n2 is a predicate
 601         if(n1[0] == n2) {
 602           n1 = n1[1];
 603           ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")";
 604         } else if(n1[1] == n2) {
 605           n1 = n1[0];
 606           ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")";
 607         } else {
 608           Unreachable();
 609         }
 610       } else if(n2.getKind() == kind::EQUAL) {
 611         // n2 is an equality/iff, but n1 is a predicate
 612         if(n2[0] == n1) {
 613           n1 = n2[1];
 614           ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")";
 615         } else if(n2[1] == n1) {
 616           n1 = n2[0];
 617           ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")";
 618         } else {
 619           Unreachable();
 620         }
 621       } else {
 622         // Both n1 and n2 are prediacates. Don't know what to do...
 623         Unreachable();
 624       }
 625
 626       ss << ")";
 627     }
 628     out << ss.str();
 629     Debug("pf::arith") << "\n++ trans proof done, have proven " << n1 << std::endl;
 630     return n1;
 631   }
 632
 633   default:
 634     Assert(!pf.d_node.isNull());
 635     Assert(pf.d_children.empty());
 636     Debug("pf::arith") << "theory proof: " << pf.d_node << " by rule " << int(pf.d_id) << std::endl;
 637     AlwaysAssert(false);
 638     return pf.d_node;
 639   }
 640 }
 641
 642 ArithProof::ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* pe)
 643   : TheoryProof(arith, pe), d_realMode(false)
 644 {}
 645
 646 theory::TheoryId ArithProof::getTheoryId() { return theory::THEORY_ARITH; }
 647 void ArithProof::registerTerm(Expr term) {
 648   Debug("pf::arith") << "Arith register term: " << term << ". Kind: " << term.getKind()
 649                             << ". Type: " << term.getType() << std::endl;
 650
 651   if (term.getType().isReal() && !term.getType().isInteger()) {
 652     Debug("pf::arith") << "Entering real mode" << std::endl;
 653     d_realMode = true;
 654   }
 655
 656   if (term.isVariable() && !ProofManager::getSkolemizationManager()->isSkolem(term)) {
 657     d_declarations.insert(term);
 658   }
 659
 660   // recursively declare all other terms
 661   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
 662     // could belong to other theories
 663     d_proofEngine->registerTerm(term[i]);
 664   }
 665 }
 666
 667 void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
 668   Debug("pf::arith") << "Arith print term: " << term << ". Kind: " << term.getKind()
 669                      << ". Type: " << term.getType()
 670                      << ". Number of children: " << term.getNumChildren() << std::endl;
 671
 672   // !d_realMode <--> term.getType().isInteger()
 673
 674   Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARITH);
 675   switch (term.getKind()) {
 676
 677   case kind::CONST_RATIONAL: {
 678     Assert (term.getNumChildren() == 0);
 679     Assert (term.getType().isInteger() || term.getType().isReal());
 680
 681     const Rational& r = term.getConst<Rational>();
 682     bool neg = (r < 0);
 683
 684     os << (!d_realMode ? "(a_int " : "(a_real ");
 685
 686     if (neg) {
 687       os << "(~ ";
 688     }
 689
 690     if (!d_realMode) {
 691       os << r.abs();
 692     } else {
 693       os << r.abs().getNumerator();
 694       os << "/";
 695       os << r.getDenominator();
 696     }
 697
 698     if (neg) {
 699       os << ") ";
 700     }
 701
 702     os << ") ";
 703     return;
 704   }
 705
 706   case kind::UMINUS: {
 707     Assert (term.getNumChildren() == 1);
 708     Assert (term.getType().isInteger() || term.getType().isReal());
 709     os << (!d_realMode ? "(u-_Int " : "(u-_Real ");
 710     d_proofEngine->printBoundTerm(term[0], os, map);
 711     os << ") ";
 712     return;
 713   }
 714
 715   case kind::PLUS: {
 716     Assert (term.getNumChildren() >= 2);
 717
 718     std::stringstream paren;
 719     for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
 720       os << (!d_realMode ? "(+_Int " : "(+_Real ");
 721       d_proofEngine->printBoundTerm(term[i], os, map);
 722       os << " ";
 723       paren << ") ";
 724     }
 725
 726     d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
 727     os << paren.str();
 728     return;
 729   }
 730
 731   case kind::MINUS: {
 732     Assert (term.getNumChildren() >= 2);
 733
 734     std::stringstream paren;
 735     for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
 736       os << (!d_realMode ? "(-_Int " : "(-_Real ");
 737       d_proofEngine->printBoundTerm(term[i], os, map);
 738       os << " ";
 739       paren << ") ";
 740     }
 741
 742     d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
 743     os << paren.str();
 744     return;
 745   }
 746
 747   case kind::MULT: {
 748     Assert (term.getNumChildren() >= 2);
 749
 750     std::stringstream paren;
 751     for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
 752       os << (!d_realMode ? "(*_Int " : "(*_Real ");
 753       d_proofEngine->printBoundTerm(term[i], os, map);
 754       os << " ";
 755       paren << ") ";
 756     }
 757
 758     d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
 759     os << paren.str();
 760     return;
 761   }
 762
 763   case kind::DIVISION:
 764   case kind::DIVISION_TOTAL: {
 765     Assert (term.getNumChildren() >= 2);
 766
 767     std::stringstream paren;
 768     for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) {
 769       os << (!d_realMode ? "(/_Int " : "(/_Real ");
 770       d_proofEngine->printBoundTerm(term[i], os, map);
 771       os << " ";
 772       paren << ") ";
 773     }
 774
 775     d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map);
 776     os << paren.str();
 777     return;
 778   }
 779
 780   case kind::GT:
 781     Assert (term.getNumChildren() == 2);
 782     os << (!d_realMode ? "(>_Int " : "(>_Real ");
 783     d_proofEngine->printBoundTerm(term[0], os, map);
 784     os << " ";
 785     d_proofEngine->printBoundTerm(term[1], os, map);
 786     os << ") ";
 787     return;
 788
 789   case kind::GEQ:
 790     Assert (term.getNumChildren() == 2);
 791     os << (!d_realMode ? "(>=_Int " : "(>=_Real ");
 792     d_proofEngine->printBoundTerm(term[0], os, map);
 793     os << " ";
 794     d_proofEngine->printBoundTerm(term[1], os, map);
 795     os << ") ";
 796     return;
 797
 798   case kind::LT:
 799     Assert (term.getNumChildren() == 2);
 800     os << (!d_realMode ? "(<_Int " : "(<_Real ");
 801     d_proofEngine->printBoundTerm(term[0], os, map);
 802     os << " ";
 803     d_proofEngine->printBoundTerm(term[1], os, map);
 804     os << ") ";
 805     return;
 806
 807   case kind::LEQ:
 808     Assert (term.getNumChildren() == 2);
 809     os << (!d_realMode ? "(<=_Int " : "(<=_Real ");
 810     d_proofEngine->printBoundTerm(term[0], os, map);
 811     os << " ";
 812     d_proofEngine->printBoundTerm(term[1], os, map);
 813     os << ") ";
 814     return;
 815
 816   default:
 817     Debug("pf::arith") << "Default printing of term: " << term << std::endl;
 818     os << term;
 819     return;
 820   }
 821 }
 822
 823 void LFSCArithProof::printOwnedSort(Type type, std::ostream& os) {
 824   Debug("pf::arith") << "Arith print sort: " << type << std::endl;
 825
 826   if (type.isInteger() && d_realMode) {
 827     // If in "real mode", don't use type Int for, e.g., equality.
 828     os << "Real";
 829   } else {
 830     os << type;
 831   }
 832 }
 833
 834 void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
 835   os << " ;; Arith Theory Lemma \n;;";
 836   for (unsigned i = 0; i < lemma.size(); ++i) {
 837     os << lemma[i] <<" ";
 838   }
 839   os <<"\n";
 840   //os << " (clausify_false trust)";
 841   ArithProof::printTheoryLemmaProof(lemma, os, paren, map);
 842 }
 843
 844 void LFSCArithProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
 845 }
 846
 847 void LFSCArithProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
 848   for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) {
 849     Expr term = *it;
 850     Assert(term.isVariable());
 851     os << "(% " << ProofManager::sanitize(term) << " ";
 852     os << "(term ";
 853     os << term.getType() << ")\n";
 854     paren << ")";
 855   }
 856 }
 857
 858 void LFSCArithProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) {
 859   // Nothing to do here at this point.
 860 }
 861
 862 void LFSCArithProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
 863   // Nothing to do here at this point.
 864 }
 865
 866 } /* CVC4  namespace */