src/expr/proof_checker.cpp

   1 /*********************                                                        */
   2 /*! \file proof_checker.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-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 proof checker
  13  **/
  14
  15 #include "expr/proof_checker.h"
  16
  17 #include "expr/skolem_manager.h"
  18 #include "smt/smt_statistics_registry.h"
  19
  20 using namespace CVC4::kind;
  21
  22 namespace CVC4 {
  23
  24 Node ProofRuleChecker::check(PfRule id,
  25                              const std::vector<Node>& children,
  26                              const std::vector<Node>& args)
  27 {
  28   // call instance-specific checkInternal method
  29   return checkInternal(id, children, args);
  30 }
  31
  32 Node ProofRuleChecker::checkChildrenArg(PfRule id,
  33                                         const std::vector<Node>& children,
  34                                         Node arg)
  35 {
  36   return check(id, children, {arg});
  37 }
  38 Node ProofRuleChecker::checkChildren(PfRule id,
  39                                      const std::vector<Node>& children)
  40 {
  41   return check(id, children, {});
  42 }
  43 Node ProofRuleChecker::checkChild(PfRule id, Node child)
  44 {
  45   return check(id, {child}, {});
  46 }
  47 Node ProofRuleChecker::checkArg(PfRule id, Node arg)
  48 {
  49   return check(id, {}, {arg});
  50 }
  51
  52 Node ProofRuleChecker::mkAnd(const std::vector<Node>& a)
  53 {
  54   if (a.empty())
  55   {
  56     return NodeManager::currentNM()->mkConst(true);
  57   }
  58   else if (a.size() == 1)
  59   {
  60     return a[0];
  61   }
  62   return NodeManager::currentNM()->mkNode(AND, a);
  63 }
  64
  65 bool ProofRuleChecker::getUInt32(TNode n, uint32_t& i)
  66 {
  67   // must be a non-negative integer constant that fits an unsigned int
  68   if (n.isConst() && n.getType().isInteger()
  69       && n.getConst<Rational>().sgn() >= 0
  70       && n.getConst<Rational>().getNumerator().fitsUnsignedInt())
  71   {
  72     i = n.getConst<Rational>().getNumerator().toUnsignedInt();
  73     return true;
  74   }
  75   return false;
  76 }
  77
  78 bool ProofRuleChecker::getBool(TNode n, bool& b)
  79 {
  80   if (n.isConst() && n.getType().isBoolean())
  81   {
  82     b = n.getConst<bool>();
  83     return true;
  84   }
  85   return false;
  86 }
  87
  88 ProofCheckerStatistics::ProofCheckerStatistics()
  89     : d_ruleChecks("ProofCheckerStatistics::ruleChecks"),
  90     d_totalRuleChecks("ProofCheckerStatistics::totalRuleChecks", 0)
  91 {
  92   smtStatisticsRegistry()->registerStat(&d_ruleChecks);
  93   smtStatisticsRegistry()->registerStat(&d_totalRuleChecks);
  94 }
  95
  96 ProofCheckerStatistics::~ProofCheckerStatistics()
  97 {
  98   smtStatisticsRegistry()->unregisterStat(&d_ruleChecks);
  99   smtStatisticsRegistry()->unregisterStat(&d_totalRuleChecks);
 100 }
 101
 102 Node ProofChecker::check(ProofNode* pn, Node expected)
 103 {
 104   return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected);
 105 }
 106
 107 Node ProofChecker::check(
 108     PfRule id,
 109     const std::vector<std::shared_ptr<ProofNode>>& children,
 110     const std::vector<Node>& args,
 111     Node expected)
 112 {
 113   // optimization: immediately return for ASSUME
 114   if (id == PfRule::ASSUME)
 115   {
 116     Assert(children.empty());
 117     Assert(args.size() == 1 && args[0].getType().isBoolean());
 118     Assert(expected.isNull() || expected == args[0]);
 119     return expected;
 120   }
 121   // record stat
 122   d_stats.d_ruleChecks << id;
 123   ++d_stats.d_totalRuleChecks;
 124   Trace("pfcheck") << "ProofChecker::check: " << id << std::endl;
 125   std::vector<Node> cchildren;
 126   for (const std::shared_ptr<ProofNode>& pc : children)
 127   {
 128     Assert(pc != nullptr);
 129     Node cres = pc->getResult();
 130     if (cres.isNull())
 131     {
 132       Trace("pfcheck") << "ProofChecker::check: failed child" << std::endl;
 133       Unreachable()
 134           << "ProofChecker::check: child proof was invalid (null conclusion)"
 135           << std::endl;
 136       // should not have been able to create such a proof node
 137       return Node::null();
 138     }
 139     cchildren.push_back(cres);
 140     if (Trace.isOn("pfcheck"))
 141     {
 142       std::stringstream ssc;
 143       pc->printDebug(ssc);
 144       Trace("pfcheck") << "     child: " << ssc.str() << " : " << cres
 145                        << std::endl;
 146     }
 147   }
 148   Trace("pfcheck") << "      args: " << args << std::endl;
 149   Trace("pfcheck") << "  expected: " << expected << std::endl;
 150   std::stringstream out;
 151   // we use trusted (null) checkers here, since we want the proof generation to
 152   // proceed without failing here.
 153   Node res = checkInternal(id, cchildren, args, expected, out, true);
 154   if (res.isNull())
 155   {
 156     Trace("pfcheck") << "ProofChecker::check: failed" << std::endl;
 157     Unreachable() << "ProofChecker::check: failed, " << out.str() << std::endl;
 158     // it did not match the given expectation, fail
 159     return Node::null();
 160   }
 161   Trace("pfcheck") << "ProofChecker::check: success!" << std::endl;
 162   return res;
 163 }
 164
 165 Node ProofChecker::checkDebug(PfRule id,
 166                               const std::vector<Node>& cchildren,
 167                               const std::vector<Node>& args,
 168                               Node expected,
 169                               const char* traceTag)
 170 {
 171   std::stringstream out;
 172   // since we are debugging, we want to treat trusted (null) checkers as
 173   // a failure.
 174   Node res = checkInternal(id, cchildren, args, expected, out, false);
 175   Trace(traceTag) << "ProofChecker::checkDebug: " << id;
 176   if (res.isNull())
 177   {
 178     Trace(traceTag) << " failed, " << out.str() << std::endl;
 179   }
 180   else
 181   {
 182     Trace(traceTag) << " success" << std::endl;
 183   }
 184   Trace(traceTag) << "cchildren: " << cchildren << std::endl;
 185   Trace(traceTag) << "     args: " << args << std::endl;
 186   return res;
 187 }
 188
 189 Node ProofChecker::checkInternal(PfRule id,
 190                                  const std::vector<Node>& cchildren,
 191                                  const std::vector<Node>& args,
 192                                  Node expected,
 193                                  std::stringstream& out,
 194                                  bool useTrustedChecker)
 195 {
 196   std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
 197   if (it == d_checker.end())
 198   {
 199     // no checker for the rule
 200     out << "no checker for rule " << id << std::endl;
 201     return Node::null();
 202   }
 203   else if (it->second == nullptr)
 204   {
 205     if (useTrustedChecker)
 206     {
 207       Notice() << "ProofChecker::check: trusting PfRule " << id << std::endl;
 208       // trusted checker
 209       return expected;
 210     }
 211     else
 212     {
 213       out << "trusted checker for rule " << id << std::endl;
 214       return Node::null();
 215     }
 216   }
 217   // check it with the corresponding checker
 218   Node res = it->second->check(id, cchildren, args);
 219   if (!expected.isNull())
 220   {
 221     Node expectedw = expected;
 222     if (res != expectedw)
 223     {
 224       out << "result does not match expected value." << std::endl
 225           << "    PfRule: " << id << std::endl;
 226       for (const Node& c : cchildren)
 227       {
 228         out << "     child: " << c << std::endl;
 229       }
 230       for (const Node& a : args)
 231       {
 232         out << "       arg: " << a << std::endl;
 233       }
 234       out << "    result: " << res << std::endl
 235           << "  expected: " << expected << std::endl;
 236       // it did not match the given expectation, fail
 237       return Node::null();
 238     }
 239   }
 240   return res;
 241 }
 242
 243 void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc)
 244 {
 245   std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
 246   if (it != d_checker.end())
 247   {
 248     // checker is already provided
 249     Notice() << "ProofChecker::registerChecker: checker already exists for "
 250              << id << std::endl;
 251     return;
 252   }
 253   d_checker[id] = psc;
 254 }
 255
 256 ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id)
 257 {
 258   std::map<PfRule, ProofRuleChecker*>::const_iterator it = d_checker.find(id);
 259   if (it == d_checker.end())
 260   {
 261     return nullptr;
 262   }
 263   return it->second;
 264 }
 265
 266 }  // namespace CVC4