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-2021 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/proof_node.h"
  18 #include "expr/skolem_manager.h"
  19 #include "options/proof_options.h"
  20 #include "smt/smt_statistics_registry.h"
  21
  22 using namespace CVC4::kind;
  23
  24 namespace CVC4 {
  25
  26 Node ProofRuleChecker::check(PfRule id,
  27                              const std::vector<Node>& children,
  28                              const std::vector<Node>& args)
  29 {
  30   // call instance-specific checkInternal method
  31   return checkInternal(id, children, args);
  32 }
  33
  34 bool ProofRuleChecker::getUInt32(TNode n, uint32_t& i)
  35 {
  36   // must be a non-negative integer constant that fits an unsigned int
  37   if (n.isConst() && n.getType().isInteger()
  38       && n.getConst<Rational>().sgn() >= 0
  39       && n.getConst<Rational>().getNumerator().fitsUnsignedInt())
  40   {
  41     i = n.getConst<Rational>().getNumerator().toUnsignedInt();
  42     return true;
  43   }
  44   return false;
  45 }
  46
  47 bool ProofRuleChecker::getBool(TNode n, bool& b)
  48 {
  49   if (n.isConst() && n.getType().isBoolean())
  50   {
  51     b = n.getConst<bool>();
  52     return true;
  53   }
  54   return false;
  55 }
  56
  57 bool ProofRuleChecker::getKind(TNode n, Kind& k)
  58 {
  59   uint32_t i;
  60   if (!getUInt32(n, i))
  61   {
  62     return false;
  63   }
  64   k = static_cast<Kind>(i);
  65   return true;
  66 }
  67
  68 Node ProofRuleChecker::mkKindNode(Kind k)
  69 {
  70   if (k == UNDEFINED_KIND)
  71   {
  72     // UNDEFINED_KIND is negative, hence return null to avoid cast
  73     return Node::null();
  74   }
  75   return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(k)));
  76 }
  77
  78 ProofCheckerStatistics::ProofCheckerStatistics()
  79     : d_ruleChecks("ProofCheckerStatistics::ruleChecks"),
  80     d_totalRuleChecks("ProofCheckerStatistics::totalRuleChecks", 0)
  81 {
  82   smtStatisticsRegistry()->registerStat(&d_ruleChecks);
  83   smtStatisticsRegistry()->registerStat(&d_totalRuleChecks);
  84 }
  85
  86 ProofCheckerStatistics::~ProofCheckerStatistics()
  87 {
  88   smtStatisticsRegistry()->unregisterStat(&d_ruleChecks);
  89   smtStatisticsRegistry()->unregisterStat(&d_totalRuleChecks);
  90 }
  91
  92 Node ProofChecker::check(ProofNode* pn, Node expected)
  93 {
  94   return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected);
  95 }
  96
  97 Node ProofChecker::check(
  98     PfRule id,
  99     const std::vector<std::shared_ptr<ProofNode>>& children,
 100     const std::vector<Node>& args,
 101     Node expected)
 102 {
 103   // optimization: immediately return for ASSUME
 104   if (id == PfRule::ASSUME)
 105   {
 106     Assert(children.empty());
 107     Assert(args.size() == 1 && args[0].getType().isBoolean());
 108     Assert(expected.isNull() || expected == args[0]);
 109     return expected;
 110   }
 111   // record stat
 112   d_stats.d_ruleChecks << id;
 113   ++d_stats.d_totalRuleChecks;
 114   Trace("pfcheck") << "ProofChecker::check: " << id << std::endl;
 115   std::vector<Node> cchildren;
 116   for (const std::shared_ptr<ProofNode>& pc : children)
 117   {
 118     Assert(pc != nullptr);
 119     Node cres = pc->getResult();
 120     if (cres.isNull())
 121     {
 122       Trace("pfcheck") << "ProofChecker::check: failed child" << std::endl;
 123       Unreachable()
 124           << "ProofChecker::check: child proof was invalid (null conclusion)"
 125           << std::endl;
 126       // should not have been able to create such a proof node
 127       return Node::null();
 128     }
 129     cchildren.push_back(cres);
 130     if (Trace.isOn("pfcheck"))
 131     {
 132       std::stringstream ssc;
 133       pc->printDebug(ssc);
 134       Trace("pfcheck") << "     child: " << ssc.str() << " : " << cres
 135                        << std::endl;
 136     }
 137   }
 138   Trace("pfcheck") << "      args: " << args << std::endl;
 139   Trace("pfcheck") << "  expected: " << expected << std::endl;
 140   std::stringstream out;
 141   // we use trusted (null) checkers here, since we want the proof generation to
 142   // proceed without failing here. We always enable output since a failure
 143   // implies that we will exit with the error message below.
 144   Node res = checkInternal(id, cchildren, args, expected, out, true, true);
 145   if (res.isNull())
 146   {
 147     Trace("pfcheck") << "ProofChecker::check: failed" << std::endl;
 148     Unreachable() << "ProofChecker::check: failed, " << out.str() << std::endl;
 149     // it did not match the given expectation, fail
 150     return Node::null();
 151   }
 152   Trace("pfcheck") << "ProofChecker::check: success!" << std::endl;
 153   return res;
 154 }
 155
 156 Node ProofChecker::checkDebug(PfRule id,
 157                               const std::vector<Node>& cchildren,
 158                               const std::vector<Node>& args,
 159                               Node expected,
 160                               const char* traceTag)
 161 {
 162   std::stringstream out;
 163   bool traceEnabled = Trace.isOn(traceTag);
 164   // Since we are debugging, we want to treat trusted (null) checkers as
 165   // a failure. We only enable output if the trace is enabled for efficiency.
 166   Node res =
 167       checkInternal(id, cchildren, args, expected, out, false, traceEnabled);
 168   if (traceEnabled)
 169   {
 170     Trace(traceTag) << "ProofChecker::checkDebug: " << id;
 171     if (res.isNull())
 172     {
 173       Trace(traceTag) << " failed, " << out.str() << std::endl;
 174     }
 175     else
 176     {
 177       Trace(traceTag) << " success" << std::endl;
 178     }
 179     Trace(traceTag) << "cchildren: " << cchildren << std::endl;
 180     Trace(traceTag) << "     args: " << args << std::endl;
 181   }
 182   return res;
 183 }
 184
 185 Node ProofChecker::checkInternal(PfRule id,
 186                                  const std::vector<Node>& cchildren,
 187                                  const std::vector<Node>& args,
 188                                  Node expected,
 189                                  std::stringstream& out,
 190                                  bool useTrustedChecker,
 191                                  bool enableOutput)
 192 {
 193   std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
 194   if (it == d_checker.end())
 195   {
 196     // no checker for the rule
 197     if (enableOutput)
 198     {
 199       out << "no checker for rule " << id << std::endl;
 200     }
 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       if (enableOutput)
 214       {
 215         out << "trusted checker for rule " << id << std::endl;
 216       }
 217       return Node::null();
 218     }
 219   }
 220   // check it with the corresponding checker
 221   Node res = it->second->check(id, cchildren, args);
 222   if (!expected.isNull())
 223   {
 224     Node expectedw = expected;
 225     if (res != expectedw)
 226     {
 227       if (enableOutput)
 228       {
 229         out << "result does not match expected value." << std::endl
 230             << "    PfRule: " << id << std::endl;
 231         for (const Node& c : cchildren)
 232         {
 233           out << "     child: " << c << std::endl;
 234         }
 235         for (const Node& a : args)
 236         {
 237           out << "       arg: " << a << std::endl;
 238         }
 239         out << "    result: " << res << std::endl
 240             << "  expected: " << expected << std::endl;
 241       }
 242       // it did not match the given expectation, fail
 243       return Node::null();
 244     }
 245   }
 246   // fails if pedantic level is not met
 247   if (options::proofEagerChecking())
 248   {
 249     std::stringstream serr;
 250     if (isPedanticFailure(id, serr, enableOutput))
 251     {
 252       if (enableOutput)
 253       {
 254         out << serr.str() << std::endl;
 255         if (Trace.isOn("proof-pedantic"))
 256         {
 257           Trace("proof-pedantic")
 258               << "Failed pedantic check for " << id << std::endl;
 259           Trace("proof-pedantic") << "Expected: " << expected << std::endl;
 260           out << "Expected: " << expected << std::endl;
 261         }
 262       }
 263       return Node::null();
 264     }
 265   }
 266   return res;
 267 }
 268
 269 void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc)
 270 {
 271   std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id);
 272   if (it != d_checker.end())
 273   {
 274     // checker is already provided
 275     Notice() << "ProofChecker::registerChecker: checker already exists for "
 276              << id << std::endl;
 277     return;
 278   }
 279   d_checker[id] = psc;
 280 }
 281
 282 void ProofChecker::registerTrustedChecker(PfRule id,
 283                                           ProofRuleChecker* psc,
 284                                           uint32_t plevel)
 285 {
 286   AlwaysAssert(plevel <= 10) << "ProofChecker::registerTrustedChecker: "
 287                                 "pedantic level must be 0-10, got "
 288                              << plevel << " for " << id;
 289   registerChecker(id, psc);
 290   // overwrites if already there
 291   if (d_plevel.find(id) != d_plevel.end())
 292   {
 293     Notice() << "ProofChecker::registerTrustedRule: already provided pedantic "
 294                 "level for "
 295              << id << std::endl;
 296   }
 297   d_plevel[id] = plevel;
 298 }
 299
 300 ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id)
 301 {
 302   std::map<PfRule, ProofRuleChecker*>::const_iterator it = d_checker.find(id);
 303   if (it == d_checker.end())
 304   {
 305     return nullptr;
 306   }
 307   return it->second;
 308 }
 309
 310 uint32_t ProofChecker::getPedanticLevel(PfRule id) const
 311 {
 312   std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id);
 313   if (itp != d_plevel.end())
 314   {
 315     return itp->second;
 316   }
 317   return 0;
 318 }
 319
 320 bool ProofChecker::isPedanticFailure(PfRule id,
 321                                      std::ostream& out,
 322                                      bool enableOutput) const
 323 {
 324   if (d_pclevel == 0)
 325   {
 326     return false;
 327   }
 328   std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id);
 329   if (itp != d_plevel.end())
 330   {
 331     if (itp->second <= d_pclevel)
 332     {
 333       if (enableOutput)
 334       {
 335         out << "pedantic level for " << id << " not met (rule level is "
 336             << itp->second << " which is at or below the pedantic level "
 337             << d_pclevel << ")";
 338         bool pedanticTraceEnabled = Trace.isOn("proof-pedantic");
 339         if (!pedanticTraceEnabled)
 340         {
 341           out << ", use -t proof-pedantic for details";
 342         }
 343       }
 344       return true;
 345     }
 346   }
 347   return false;
 348 }
 349
 350 }  // namespace CVC4