src/expr/proof.cpp

   1 /*********************                                                        */
   2 /*! \file proof.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 proof
  13  **/
  14
  15 #include "expr/proof.h"
  16
  17 using namespace CVC4::kind;
  18
  19 namespace CVC4 {
  20
  21 std::ostream& operator<<(std::ostream& out, CDPOverwrite opol)
  22 {
  23   switch (opol)
  24   {
  25     case CDPOverwrite::ALWAYS: out << "ALWAYS"; break;
  26     case CDPOverwrite::ASSUME_ONLY: out << "ASSUME_ONLY"; break;
  27     case CDPOverwrite::NEVER: out << "NEVER"; break;
  28     default: out << "CDPOverwrite:unknown"; break;
  29   }
  30   return out;
  31 }
  32
  33 CDProof::CDProof(ProofNodeManager* pnm, context::Context* c)
  34     : d_manager(pnm), d_context(), d_nodes(c ? c : &d_context)
  35 {
  36 }
  37
  38 CDProof::~CDProof() {}
  39
  40 std::shared_ptr<ProofNode> CDProof::mkProof(Node fact)
  41 {
  42   std::shared_ptr<ProofNode> pf = getProofSymm(fact);
  43   if (pf != nullptr)
  44   {
  45     return pf;
  46   }
  47   // add as assumption
  48   std::vector<Node> pargs = {fact};
  49   std::vector<std::shared_ptr<ProofNode>> passume;
  50   std::shared_ptr<ProofNode> pfa =
  51       d_manager->mkNode(PfRule::ASSUME, passume, pargs, fact);
  52   d_nodes.insert(fact, pfa);
  53   return pfa;
  54 }
  55
  56 std::shared_ptr<ProofNode> CDProof::getProof(Node fact) const
  57 {
  58   NodeProofNodeMap::iterator it = d_nodes.find(fact);
  59   if (it != d_nodes.end())
  60   {
  61     return (*it).second;
  62   }
  63   return nullptr;
  64 }
  65
  66 std::shared_ptr<ProofNode> CDProof::getProofSymm(Node fact)
  67 {
  68   Trace("cdproof") << "CDProof::getProofSymm: " << fact << std::endl;
  69   std::shared_ptr<ProofNode> pf = getProof(fact);
  70   if (pf != nullptr && !isAssumption(pf.get()))
  71   {
  72     Trace("cdproof") << "...existing non-assume " << pf->getRule() << std::endl;
  73     return pf;
  74   }
  75   Node symFact = getSymmFact(fact);
  76   if (symFact.isNull())
  77   {
  78     Trace("cdproof") << "...no possible symm" << std::endl;
  79     // no symmetry possible, return original proof (possibly assumption)
  80     return pf;
  81   }
  82   // See if a proof exists for the opposite direction, if so, add the step.
  83   // Notice that SYMM is also disallowed.
  84   std::shared_ptr<ProofNode> pfs = getProof(symFact);
  85   if (pfs != nullptr)
  86   {
  87     // The symmetric fact exists, and the current one either does not, or is
  88     // an assumption. We make a new proof that applies SYMM to pfs.
  89     std::vector<std::shared_ptr<ProofNode>> pschild;
  90     pschild.push_back(pfs);
  91     std::vector<Node> args;
  92     if (pf == nullptr)
  93     {
  94       Trace("cdproof") << "...fresh make symm" << std::endl;
  95       std::shared_ptr<ProofNode> psym =
  96           d_manager->mkNode(PfRule::SYMM, pschild, args, fact);
  97       Assert(psym != nullptr);
  98       d_nodes.insert(fact, psym);
  99       return psym;
 100     }
 101     else if (!isAssumption(pfs.get()))
 102     {
 103       // if its not an assumption, make the connection
 104       Trace("cdproof") << "...update symm" << std::endl;
 105       // update pf
 106       bool sret = d_manager->updateNode(pf.get(), PfRule::SYMM, pschild, args);
 107       AlwaysAssert(sret);
 108     }
 109   }
 110   else
 111   {
 112     Trace("cdproof") << "...no symm, return "
 113                      << (pf == nullptr ? "null" : "non-null") << std::endl;
 114   }
 115   // return original proof (possibly assumption)
 116   return pf;
 117 }
 118
 119 bool CDProof::addStep(Node expected,
 120                       PfRule id,
 121                       const std::vector<Node>& children,
 122                       const std::vector<Node>& args,
 123                       bool ensureChildren,
 124                       CDPOverwrite opolicy)
 125 {
 126   Trace("cdproof") << "CDProof::addStep: " << id << " " << expected
 127                    << ", ensureChildren = " << ensureChildren
 128                    << ", overwrite policy = " << opolicy << std::endl;
 129   // We must always provide expected to this method
 130   Assert(!expected.isNull());
 131
 132   std::shared_ptr<ProofNode> pprev = getProofSymm(expected);
 133   if (pprev != nullptr)
 134   {
 135     if (!shouldOverwrite(pprev.get(), id, opolicy))
 136     {
 137       // we should not overwrite the current step
 138       Trace("cdproof") << "...success, no overwrite" << std::endl;
 139       return true;
 140     }
 141     Trace("cdproof") << "existing proof " << pprev->getRule()
 142                      << ", overwrite..." << std::endl;
 143     // we will overwrite the existing proof node by updating its contents below
 144   }
 145   // collect the child proofs, for each premise
 146   std::vector<std::shared_ptr<ProofNode>> pchildren;
 147   for (const Node& c : children)
 148   {
 149     Trace("cdproof") << "- get child " << c << std::endl;
 150     std::shared_ptr<ProofNode> pc = getProofSymm(c);
 151     if (pc == nullptr)
 152     {
 153       if (ensureChildren)
 154       {
 155         // failed to get a proof for a child, fail
 156         Trace("cdproof") << "...fail, no child" << std::endl;
 157         return false;
 158       }
 159       Trace("cdproof") << "--- add assume" << std::endl;
 160       // otherwise, we initialize it as an assumption
 161       std::vector<Node> pcargs = {c};
 162       std::vector<std::shared_ptr<ProofNode>> pcassume;
 163       pc = d_manager->mkNode(PfRule::ASSUME, pcassume, pcargs, c);
 164       // assumptions never fail to check
 165       Assert(pc != nullptr);
 166       d_nodes.insert(c, pc);
 167     }
 168     pchildren.push_back(pc);
 169   }
 170
 171   // the user may have provided SYMM of an assumption
 172   if (id == PfRule::SYMM)
 173   {
 174     Assert(pchildren.size() == 1);
 175     if (isAssumption(pchildren[0].get()))
 176     {
 177       // the step we are constructing is a (symmetric fact of an) assumption, so
 178       // there is no use adding it to the proof.
 179       return true;
 180     }
 181   }
 182
 183   bool ret = true;
 184   // create or update it
 185   std::shared_ptr<ProofNode> pthis;
 186   if (pprev == nullptr)
 187   {
 188     Trace("cdproof") << "  new node " << expected << "..." << std::endl;
 189     pthis = d_manager->mkNode(id, pchildren, args, expected);
 190     if (pthis == nullptr)
 191     {
 192       // failed to construct the node, perhaps due to a proof checking failure
 193       Trace("cdproof") << "...fail, proof checking" << std::endl;
 194       return false;
 195     }
 196     d_nodes.insert(expected, pthis);
 197   }
 198   else
 199   {
 200     Trace("cdproof") << "  update node " << expected << "..." << std::endl;
 201     // update its value
 202     pthis = pprev;
 203     // We return the value of updateNode here. This means this method may return
 204     // false if this call failed, regardless of whether we already have a proof
 205     // step for expected.
 206     ret = d_manager->updateNode(pthis.get(), id, pchildren, args);
 207   }
 208   if (ret)
 209   {
 210     // the result of the proof node should be expected
 211     Assert(pthis->getResult() == expected);
 212
 213     // notify new proof
 214     notifyNewProof(expected);
 215   }
 216
 217   Trace("cdproof") << "...return " << ret << std::endl;
 218   return ret;
 219 }
 220
 221 void CDProof::notifyNewProof(Node expected)
 222 {
 223   // ensure SYMM proof is also linked to an existing proof, if it is an
 224   // assumption.
 225   Node symExpected = getSymmFact(expected);
 226   if (!symExpected.isNull())
 227   {
 228     Trace("cdproof") << "  check connect symmetry " << symExpected << std::endl;
 229     // if it exists, we may need to update it
 230     std::shared_ptr<ProofNode> pfs = getProof(symExpected);
 231     if (pfs != nullptr)
 232     {
 233       Trace("cdproof") << "  connect via getProofSymm method..." << std::endl;
 234       // call the get function with symmetry, which will do the update
 235       std::shared_ptr<ProofNode> pfss = getProofSymm(symExpected);
 236     }
 237     else
 238     {
 239       Trace("cdproof") << "  no connect" << std::endl;
 240     }
 241   }
 242 }
 243
 244 bool CDProof::addStep(Node expected,
 245                       const ProofStep& step,
 246                       bool ensureChildren,
 247                       CDPOverwrite opolicy)
 248 {
 249   return addStep(expected,
 250                  step.d_rule,
 251                  step.d_children,
 252                  step.d_args,
 253                  ensureChildren,
 254                  opolicy);
 255 }
 256
 257 bool CDProof::addSteps(const ProofStepBuffer& psb,
 258                        bool ensureChildren,
 259                        CDPOverwrite opolicy)
 260 {
 261   const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
 262   for (const std::pair<Node, ProofStep>& ps : steps)
 263   {
 264     if (!addStep(ps.first, ps.second, ensureChildren, opolicy))
 265     {
 266       return false;
 267     }
 268   }
 269   return true;
 270 }
 271
 272 bool CDProof::addProof(std::shared_ptr<ProofNode> pn,
 273                        CDPOverwrite opolicy,
 274                        bool doCopy)
 275 {
 276   if (!doCopy)
 277   {
 278     // If we aren't doing a deep copy, we either store pn or link its top
 279     // node into the existing pointer
 280     Node curFact = pn->getResult();
 281     std::shared_ptr<ProofNode> cur = getProofSymm(curFact);
 282     if (cur == nullptr)
 283     {
 284       // Assert that the checker of this class agrees with (the externally
 285       // provided) pn. This ensures that if pn was checked by a different
 286       // checker than the one of the manager in this class, then it is double
 287       // checked here, so that this class maintains the invariant that all of
 288       // its nodes in d_nodes have been checked by the underlying checker.
 289       Assert(d_manager->getChecker() == nullptr
 290              || d_manager->getChecker()->check(pn.get(), curFact) == curFact);
 291       // just store the proof for fact
 292       d_nodes.insert(curFact, pn);
 293     }
 294     else if (shouldOverwrite(cur.get(), pn->getRule(), opolicy))
 295     {
 296       // We update cur to have the structure of the top node of pn. Notice that
 297       // the interface to update this node will ensure that the proof apf is a
 298       // proof of the assumption. If it does not, then pn was wrong.
 299       if (!d_manager->updateNode(
 300               cur.get(), pn->getRule(), pn->getChildren(), pn->getArguments()))
 301       {
 302         return false;
 303       }
 304     }
 305     // also need to connect via SYMM if necessary
 306     notifyNewProof(curFact);
 307     return true;
 308   }
 309   std::unordered_map<ProofNode*, bool> visited;
 310   std::unordered_map<ProofNode*, bool>::iterator it;
 311   std::vector<ProofNode*> visit;
 312   ProofNode* cur;
 313   Node curFact;
 314   visit.push_back(pn.get());
 315   bool retValue = true;
 316   do
 317   {
 318     cur = visit.back();
 319     curFact = cur->getResult();
 320     visit.pop_back();
 321     it = visited.find(cur);
 322     if (it == visited.end())
 323     {
 324       // visit the children
 325       visited[cur] = false;
 326       visit.push_back(cur);
 327       const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
 328       for (const std::shared_ptr<ProofNode>& c : cs)
 329       {
 330         visit.push_back(c.get());
 331       }
 332     }
 333     else if (!it->second)
 334     {
 335       // we always call addStep, which may or may not overwrite the
 336       // current step
 337       std::vector<Node> pexp;
 338       const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
 339       for (const std::shared_ptr<ProofNode>& c : cs)
 340       {
 341         Assert(!c->getResult().isNull());
 342         pexp.push_back(c->getResult());
 343       }
 344       // can ensure children at this point
 345       bool res = addStep(
 346           curFact, cur->getRule(), pexp, cur->getArguments(), true, opolicy);
 347       // should always succeed
 348       Assert(res);
 349       retValue = retValue && res;
 350       visited[cur] = true;
 351     }
 352   } while (!visit.empty());
 353
 354   return retValue;
 355 }
 356
 357 bool CDProof::hasStep(Node fact)
 358 {
 359   std::shared_ptr<ProofNode> pf = getProof(fact);
 360   if (pf != nullptr && !isAssumption(pf.get()))
 361   {
 362     return true;
 363   }
 364   Node symFact = getSymmFact(fact);
 365   if (symFact.isNull())
 366   {
 367     return false;
 368   }
 369   pf = getProof(symFact);
 370   if (pf != nullptr && !isAssumption(pf.get()))
 371   {
 372     return true;
 373   }
 374   return false;
 375 }
 376
 377 ProofNodeManager* CDProof::getManager() const { return d_manager; }
 378
 379 bool CDProof::shouldOverwrite(ProofNode* pn, PfRule newId, CDPOverwrite opol)
 380 {
 381   Assert(pn != nullptr);
 382   // we overwrite only if opol is CDPOverwrite::ALWAYS, or if
 383   // opol is CDPOverwrite::ASSUME_ONLY and the previously
 384   // provided proof pn was an assumption and the currently provided step is not
 385   return opol == CDPOverwrite::ALWAYS
 386          || (opol == CDPOverwrite::ASSUME_ONLY && isAssumption(pn)
 387              && newId != PfRule::ASSUME);
 388 }
 389
 390 bool CDProof::isAssumption(ProofNode* pn)
 391 {
 392   PfRule rule = pn->getRule();
 393   if (rule == PfRule::ASSUME)
 394   {
 395     return true;
 396   }
 397   else if (rule == PfRule::SYMM)
 398   {
 399     const std::vector<std::shared_ptr<ProofNode>>& pc = pn->getChildren();
 400     Assert(pc.size() == 1);
 401     return pc[0]->getRule() == PfRule::ASSUME;
 402   }
 403   return false;
 404 }
 405
 406 bool CDProof::isSame(TNode f, TNode g)
 407 {
 408   if (f == g)
 409   {
 410     return true;
 411   }
 412   Kind fk = f.getKind();
 413   Kind gk = g.getKind();
 414   if (fk == EQUAL && gk == EQUAL && f[0] == g[1] && f[1] == g[0])
 415   {
 416     // symmetric equality
 417     return true;
 418   }
 419   if (fk == NOT && gk == NOT && f[0][0] == g[0][1] && f[0][1] == g[0][0])
 420   {
 421     // symmetric disequality
 422     return true;
 423   }
 424   return false;
 425 }
 426
 427 Node CDProof::getSymmFact(TNode f)
 428 {
 429   bool polarity = f.getKind() != NOT;
 430   TNode fatom = polarity ? f : f[0];
 431   if (fatom.getKind() != EQUAL || fatom[0] == fatom[1])
 432   {
 433     return Node::null();
 434   }
 435   Node symFact = fatom[1].eqNode(fatom[0]);
 436   return polarity ? symFact : symFact.notNode();
 437 }
 438
 439 }  // namespace CVC4