src/proof/proof_checker.cpp

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