src/theory/builtin/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-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 equality proof checker
  13  **/
  14
  15 #include "theory/builtin/proof_checker.h"
  16
  17 #include "expr/proof_skolem_cache.h"
  18 #include "theory/rewriter.h"
  19 #include "theory/theory.h"
  20
  21 using namespace CVC4::kind;
  22
  23 namespace CVC4 {
  24 namespace theory {
  25
  26 const char* toString(MethodId id)
  27 {
  28   switch (id)
  29   {
  30     case MethodId::RW_REWRITE: return "RW_REWRITE";
  31     case MethodId::RW_IDENTITY: return "RW_IDENTITY";
  32     case MethodId::SB_DEFAULT: return "SB_DEFAULT";
  33     case MethodId::SB_LITERAL: return "SB_LITERAL";
  34     case MethodId::SB_FORMULA: return "SB_FORMULA";
  35     default: return "MethodId::Unknown";
  36   };
  37 }
  38
  39 std::ostream& operator<<(std::ostream& out, MethodId id)
  40 {
  41   out << toString(id);
  42   return out;
  43 }
  44
  45 Node mkMethodId(MethodId id)
  46 {
  47   return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id)));
  48 }
  49
  50 namespace builtin {
  51
  52 void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
  53 {
  54   pc->registerChecker(PfRule::ASSUME, this);
  55   pc->registerChecker(PfRule::SCOPE, this);
  56   pc->registerChecker(PfRule::SUBS, this);
  57   pc->registerChecker(PfRule::REWRITE, this);
  58   pc->registerChecker(PfRule::MACRO_SR_EQ_INTRO, this);
  59   pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this);
  60   pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this);
  61   pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this);
  62 }
  63
  64 Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr)
  65 {
  66   Node nk = ProofSkolemCache::getSkolemForm(n);
  67   Node nkr = applyRewriteExternal(nk, idr);
  68   return ProofSkolemCache::getWitnessForm(nkr);
  69 }
  70
  71 Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids)
  72 {
  73   if (exp.isNull() || exp.getKind() != EQUAL)
  74   {
  75     return Node::null();
  76   }
  77   Node nk = ProofSkolemCache::getSkolemForm(n);
  78   Node nks = applySubstitutionExternal(nk, exp, ids);
  79   return ProofSkolemCache::getWitnessForm(nks);
  80 }
  81
  82 Node BuiltinProofRuleChecker::applySubstitution(Node n,
  83                                                 const std::vector<Node>& exp,
  84                                                 MethodId ids)
  85 {
  86   Node nk = ProofSkolemCache::getSkolemForm(n);
  87   Node nks = applySubstitutionExternal(nk, exp, ids);
  88   return ProofSkolemCache::getWitnessForm(nks);
  89 }
  90
  91 Node BuiltinProofRuleChecker::applySubstitutionRewrite(
  92     Node n, const std::vector<Node>& exp, MethodId ids, MethodId idr)
  93 {
  94   Node nk = ProofSkolemCache::getSkolemForm(n);
  95   Node nks = applySubstitutionExternal(nk, exp, ids);
  96   Node nksr = applyRewriteExternal(nks, idr);
  97   return ProofSkolemCache::getWitnessForm(nksr);
  98 }
  99
 100 Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, MethodId idr)
 101 {
 102   Trace("builtin-pfcheck-debug")
 103       << "applyRewriteExternal (" << idr << "): " << n << std::endl;
 104   if (idr == MethodId::RW_REWRITE)
 105   {
 106     return Rewriter::rewrite(n);
 107   }
 108   else if (idr == MethodId::RW_IDENTITY)
 109   {
 110     // does nothing
 111     return n;
 112   }
 113   // unknown rewriter
 114   Assert(false)
 115       << "BuiltinProofRuleChecker::applyRewriteExternal: no rewriter for "
 116       << idr << std::endl;
 117   return n;
 118 }
 119
 120 Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n,
 121                                                         Node exp,
 122                                                         MethodId ids)
 123 {
 124   Assert(!exp.isNull());
 125   Node expk = ProofSkolemCache::getSkolemForm(exp);
 126   TNode var, subs;
 127   if (ids == MethodId::SB_DEFAULT)
 128   {
 129     if (expk.getKind() != EQUAL)
 130     {
 131       return Node::null();
 132     }
 133     var = expk[0];
 134     subs = expk[1];
 135   }
 136   else if (ids == MethodId::SB_LITERAL)
 137   {
 138     bool polarity = expk.getKind() != NOT;
 139     var = polarity ? expk : expk[0];
 140     subs = NodeManager::currentNM()->mkConst(polarity);
 141   }
 142   else if (ids == MethodId::SB_FORMULA)
 143   {
 144     var = expk;
 145     subs = NodeManager::currentNM()->mkConst(true);
 146   }
 147   else
 148   {
 149     Assert(false) << "BuiltinProofRuleChecker::applySubstitutionExternal: no "
 150                      "substitution for "
 151                   << ids << std::endl;
 152   }
 153   return n.substitute(var, subs);
 154 }
 155
 156 Node BuiltinProofRuleChecker::applySubstitutionExternal(
 157     Node n, const std::vector<Node>& exp, MethodId ids)
 158 {
 159   Node curr = n;
 160   // apply substitution one at a time, in reverse order
 161   for (size_t i = 0, nexp = exp.size(); i < nexp; i++)
 162   {
 163     if (exp[nexp - 1 - i].isNull())
 164     {
 165       return Node::null();
 166     }
 167     curr = applySubstitutionExternal(curr, exp[nexp - 1 - i], ids);
 168     if (curr.isNull())
 169     {
 170       break;
 171     }
 172   }
 173   return curr;
 174 }
 175
 176 bool BuiltinProofRuleChecker::getMethodId(TNode n, MethodId& i)
 177 {
 178   uint32_t index;
 179   if (!getUInt32(n, index))
 180   {
 181     return false;
 182   }
 183   i = static_cast<MethodId>(index);
 184   return true;
 185 }
 186
 187 Node BuiltinProofRuleChecker::checkInternal(PfRule id,
 188                                             const std::vector<Node>& children,
 189                                             const std::vector<Node>& args)
 190 {
 191   // compute what was proven
 192   if (id == PfRule::ASSUME)
 193   {
 194     Assert(children.empty());
 195     Assert(args.size() == 1);
 196     Assert(args[0].getType().isBoolean());
 197     return args[0];
 198   }
 199   else if (id == PfRule::SCOPE)
 200   {
 201     Assert(children.size() == 1);
 202     if (args.empty())
 203     {
 204       // no antecedant
 205       return children[0];
 206     }
 207     Node ant = mkAnd(args);
 208     // if the conclusion is false, its the negated antencedant only
 209     if (children[0].isConst() && !children[0].getConst<bool>())
 210     {
 211       return ant.notNode();
 212     }
 213     return NodeManager::currentNM()->mkNode(IMPLIES, ant, children[0]);
 214   }
 215   else if (id == PfRule::SUBS)
 216   {
 217     Assert(children.size() > 0);
 218     Assert(1 <= args.size() && args.size() <= 2);
 219     MethodId ids = MethodId::SB_DEFAULT;
 220     if (args.size() == 2 && !getMethodId(args[1], ids))
 221     {
 222       return Node::null();
 223     }
 224     std::vector<Node> exp;
 225     for (size_t i = 0, nchild = children.size(); i < nchild; i++)
 226     {
 227       exp.push_back(children[i]);
 228     }
 229     Node res = applySubstitution(args[0], exp);
 230     return args[0].eqNode(res);
 231   }
 232   else if (id == PfRule::REWRITE)
 233   {
 234     Assert(children.empty());
 235     Assert(1 <= args.size() && args.size() <= 2);
 236     MethodId ids = MethodId::RW_REWRITE;
 237     if (args.size() == 2 && !getMethodId(args[1], ids))
 238     {
 239       return Node::null();
 240     }
 241     Node res = applyRewrite(args[0]);
 242     return args[0].eqNode(res);
 243   }
 244   else if (id == PfRule::MACRO_SR_EQ_INTRO)
 245   {
 246     Assert(1 <= args.size() && args.size() <= 3);
 247     MethodId ids, idr;
 248     if (!getMethodIds(args, ids, idr, 1))
 249     {
 250       return Node::null();
 251     }
 252     Node res = applySubstitutionRewrite(args[0], children, idr);
 253     return args[0].eqNode(res);
 254   }
 255   else if (id == PfRule::MACRO_SR_PRED_INTRO)
 256   {
 257     Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
 258                              << args.size() << std::endl;
 259     Assert(1 <= args.size() && args.size() <= 3);
 260     MethodId ids, idr;
 261     if (!getMethodIds(args, ids, idr, 1))
 262     {
 263       return Node::null();
 264     }
 265     Node res = applySubstitutionRewrite(args[0], children, ids, idr);
 266     if (res.isNull())
 267     {
 268       return Node::null();
 269     }
 270     // **** NOTE: can rewrite the witness form here. This enables certain lemmas
 271     // to be provable, e.g. (= k t) where k is a purification Skolem for t.
 272     res = Rewriter::rewrite(res);
 273     if (!res.isConst() || !res.getConst<bool>())
 274     {
 275       Trace("builtin-pfcheck")
 276           << "Failed to rewrite to true, res=" << res << std::endl;
 277       return Node::null();
 278     }
 279     return args[0];
 280   }
 281   else if (id == PfRule::MACRO_SR_PRED_ELIM)
 282   {
 283     Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
 284                              << args.size() << std::endl;
 285     Assert(children.size() >= 1);
 286     Assert(args.size() <= 2);
 287     std::vector<Node> exp;
 288     exp.insert(exp.end(), children.begin() + 1, children.end());
 289     MethodId ids, idr;
 290     if (!getMethodIds(args, ids, idr, 0))
 291     {
 292       return Node::null();
 293     }
 294     Node res1 = applySubstitutionRewrite(children[0], exp, ids, idr);
 295     Trace("builtin-pfcheck") << "Returned " << res1 << std::endl;
 296     return res1;
 297   }
 298   else if (id == PfRule::MACRO_SR_PRED_TRANSFORM)
 299   {
 300     Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " "
 301                              << args.size() << std::endl;
 302     Assert(children.size() >= 1);
 303     Assert(1 <= args.size() && args.size() <= 3);
 304     Assert(args[0].getType().isBoolean());
 305     MethodId ids, idr;
 306     if (!getMethodIds(args, ids, idr, 1))
 307     {
 308       return Node::null();
 309     }
 310     std::vector<Node> exp;
 311     exp.insert(exp.end(), children.begin() + 1, children.end());
 312     Node res1 = applySubstitutionRewrite(children[0], exp, ids, idr);
 313     Node res2 = applySubstitutionRewrite(args[0], exp, ids, idr);
 314     // can rewrite the witness forms
 315     res1 = Rewriter::rewrite(res1);
 316     res2 = Rewriter::rewrite(res2);
 317     if (res1.isNull() || res1 != res2)
 318     {
 319       Trace("builtin-pfcheck") << "Failed to match results" << std::endl;
 320       Trace("builtin-pfcheck-debug") << res1 << " vs " << res2 << std::endl;
 321       return Node::null();
 322     }
 323     return args[0];
 324   }
 325   // no rule
 326   return Node::null();
 327 }
 328
 329 bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args,
 330                                            MethodId& ids,
 331                                            MethodId& idr,
 332                                            size_t index)
 333 {
 334   ids = MethodId::SB_DEFAULT;
 335   idr = MethodId::RW_REWRITE;
 336   if (args.size() > index)
 337   {
 338     if (!getMethodId(args[index], ids))
 339     {
 340       Trace("builtin-pfcheck")
 341           << "Failed to get id from " << args[index] << std::endl;
 342       return false;
 343     }
 344   }
 345   if (args.size() > index + 1)
 346   {
 347     if (!getMethodId(args[index + 1], idr))
 348     {
 349       Trace("builtin-pfcheck")
 350           << "Failed to get id from " << args[index + 1] << std::endl;
 351       return false;
 352     }
 353   }
 354   return true;
 355 }
 356
 357 }  // namespace builtin
 358 }  // namespace theory
 359 }  // namespace CVC4