src/theory/datatypes/infer_proof_cons.cpp

   1 /*********************                                                        */
   2 /*! \file infer_proof_cons.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 inference to proof conversion  for datatypes
  13  **/
  14
  15 #include "theory/datatypes/infer_proof_cons.h"
  16
  17 #include "theory/datatypes/theory_datatypes_utils.h"
  18 #include "theory/rewriter.h"
  19
  20 using namespace CVC4::kind;
  21
  22 namespace CVC4 {
  23 namespace theory {
  24 namespace datatypes {
  25
  26 InferProofCons::InferProofCons(context::Context* c, ProofNodeManager* pnm)
  27     : d_pnm(pnm), d_lazyFactMap(c == nullptr ? &d_context : c)
  28 {
  29   Assert(d_pnm != nullptr);
  30 }
  31
  32 void InferProofCons::notifyFact(const std::shared_ptr<DatatypesInference>& di)
  33 {
  34   TNode fact = di->d_conc;
  35   if (d_lazyFactMap.find(fact) != d_lazyFactMap.end())
  36   {
  37     return;
  38   }
  39   Node symFact = CDProof::getSymmFact(fact);
  40   if (!symFact.isNull() && d_lazyFactMap.find(symFact) != d_lazyFactMap.end())
  41   {
  42     return;
  43   }
  44   d_lazyFactMap.insert(fact, di);
  45 }
  46
  47 void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof* cdp)
  48 {
  49   Trace("dt-ipc") << "convert: " << infer << ": " << conc << " by " << exp
  50                   << std::endl;
  51   // split into vector
  52   std::vector<Node> expv;
  53   if (!exp.isNull() && !exp.isConst())
  54   {
  55     if (exp.getKind() == AND)
  56     {
  57       for (const Node& ec : exp)
  58       {
  59         expv.push_back(ec);
  60       }
  61     }
  62     else
  63     {
  64       expv.push_back(exp);
  65     }
  66   }
  67   NodeManager* nm = NodeManager::currentNM();
  68   bool success = false;
  69   switch (infer)
  70   {
  71     case InferenceId::DATATYPES_UNIF:
  72     {
  73       Assert(expv.size() == 1);
  74       Assert(exp.getKind() == EQUAL && exp[0].getKind() == APPLY_CONSTRUCTOR
  75              && exp[1].getKind() == APPLY_CONSTRUCTOR
  76              && exp[0].getOperator() == exp[1].getOperator());
  77       Node narg;
  78       // we may be asked for a proof of (not P) coming from (= P false) or
  79       // (= false P), or similarly P from (= P true) or (= true P).
  80       bool concPol = conc.getKind() != NOT;
  81       Node concAtom = concPol ? conc : conc[0];
  82       Node unifConc = conc;
  83       for (size_t i = 0, nchild = exp[0].getNumChildren(); i < nchild; i++)
  84       {
  85         bool argSuccess = false;
  86         if (conc.getKind() == EQUAL)
  87         {
  88           argSuccess = (exp[0][i] == conc[0] && exp[1][i] == conc[1]);
  89         }
  90         else
  91         {
  92           for (size_t j = 0; j < 2; j++)
  93           {
  94             if (exp[j][i] == concAtom && exp[1 - j][i].isConst()
  95                 && exp[1 - j][i].getConst<bool>() == concPol)
  96             {
  97               argSuccess = true;
  98               unifConc = exp[0][i].eqNode(exp[1][i]);
  99               break;
 100             }
 101           }
 102         }
 103         if (argSuccess)
 104         {
 105           narg = nm->mkConst(Rational(i));
 106           break;
 107         }
 108       }
 109       if (!narg.isNull())
 110       {
 111         if (conc.getKind() == EQUAL)
 112         {
 113           // normal case where we conclude an equality
 114           cdp->addStep(conc, PfRule::DT_UNIF, {exp}, {narg});
 115         }
 116         else
 117         {
 118           // must use true or false elim to prove the final
 119           cdp->addStep(unifConc, PfRule::DT_UNIF, {exp}, {narg});
 120           // may use symmetry
 121           Node eq = concAtom.eqNode(nm->mkConst(concPol));
 122           cdp->addStep(
 123               conc, concPol ? PfRule::TRUE_ELIM : PfRule::FALSE_ELIM, {eq}, {});
 124         }
 125         success = true;
 126       }
 127     }
 128     break;
 129     case InferenceId::DATATYPES_INST:
 130     {
 131       if (expv.size() == 1)
 132       {
 133         Assert(conc.getKind() == EQUAL);
 134         int n = utils::isTester(exp);
 135         if (n >= 0)
 136         {
 137           Node t = exp[0];
 138           Node nn = nm->mkConst(Rational(n));
 139           Node eq = exp.eqNode(conc);
 140           cdp->addStep(eq, PfRule::DT_INST, {}, {t, nn});
 141           cdp->addStep(conc, PfRule::EQ_RESOLVE, {exp, eq}, {});
 142           success = true;
 143         }
 144       }
 145     }
 146     break;
 147     case InferenceId::DATATYPES_SPLIT:
 148     {
 149       Assert(expv.empty());
 150       Node t = conc.getKind() == OR ? conc[0][0] : conc[0];
 151       cdp->addStep(conc, PfRule::DT_SPLIT, {}, {t});
 152       success = true;
 153     }
 154     break;
 155     case InferenceId::DATATYPES_COLLAPSE_SEL:
 156     {
 157       Assert(exp.getKind() == EQUAL);
 158       Node concEq = conc;
 159       // might be a Boolean conclusion
 160       if (conc.getKind() != EQUAL)
 161       {
 162         bool concPol = conc.getKind() != NOT;
 163         Node concAtom = concPol ? conc : conc[0];
 164         concEq = concAtom.eqNode(nm->mkConst(concPol));
 165       }
 166       Assert(concEq.getKind() == EQUAL
 167              && concEq[0].getKind() == APPLY_SELECTOR_TOTAL);
 168       Assert(exp[0].getType().isDatatype());
 169       Node sop = concEq[0].getOperator();
 170       Node sl = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[0]);
 171       Node sr = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[1]);
 172       // exp[0] = exp[1]
 173       // --------------------- CONG        ----------------- DT_COLLAPSE
 174       // s(exp[0]) = s(exp[1])             s(exp[1]) = r
 175       // --------------------------------------------------- TRANS
 176       // s(exp[0]) = r
 177       Node asn = ProofRuleChecker::mkKindNode(APPLY_SELECTOR_TOTAL);
 178       Node seq = sl.eqNode(sr);
 179       cdp->addStep(seq, PfRule::CONG, {exp}, {asn, sop});
 180       Node sceq = sr.eqNode(concEq[1]);
 181       cdp->addStep(sceq, PfRule::DT_COLLAPSE, {}, {sr});
 182       cdp->addStep(sl.eqNode(concEq[1]), PfRule::TRANS, {seq, sceq}, {});
 183       if (conc.getKind() != EQUAL)
 184       {
 185         PfRule eid =
 186             conc.getKind() == NOT ? PfRule::FALSE_ELIM : PfRule::TRUE_ELIM;
 187         cdp->addStep(conc, eid, {concEq}, {});
 188       }
 189       success = true;
 190     }
 191     break;
 192     case InferenceId::DATATYPES_CLASH_CONFLICT:
 193     {
 194       cdp->addStep(conc, PfRule::MACRO_SR_PRED_ELIM, {exp}, {});
 195       success = true;
 196     }
 197     break;
 198     case InferenceId::DATATYPES_TESTER_CONFLICT:
 199     {
 200       // rewrites to false under substitution
 201       Node fn = nm->mkConst(false);
 202       cdp->addStep(fn, PfRule::MACRO_SR_PRED_ELIM, expv, {});
 203       success = true;
 204     }
 205     break;
 206     case InferenceId::DATATYPES_TESTER_MERGE_CONFLICT:
 207     {
 208       Assert(expv.size() == 3);
 209       Node tester1 = expv[0];
 210       Node tester1c =
 211           nm->mkNode(APPLY_TESTER, expv[1].getOperator(), expv[0][0]);
 212       cdp->addStep(tester1c,
 213                    PfRule::MACRO_SR_PRED_TRANSFORM,
 214                    {expv[1], expv[2]},
 215                    {tester1c});
 216       Node fn = nm->mkConst(false);
 217       cdp->addStep(fn, PfRule::DT_CLASH, {tester1, tester1c}, {});
 218       success = true;
 219     }
 220     break;
 221     // inferences currently not supported
 222     case InferenceId::DATATYPES_LABEL_EXH:
 223     case InferenceId::DATATYPES_BISIMILAR:
 224     case InferenceId::DATATYPES_CYCLE:
 225     default:
 226       Trace("dt-ipc") << "...no conversion for inference " << infer
 227                       << std::endl;
 228       break;
 229   }
 230
 231   if (!success)
 232   {
 233     // failed to reconstruct, add trust
 234     Trace("dt-ipc") << "...failed " << infer << std::endl;
 235     cdp->addStep(conc, PfRule::DT_TRUST, expv, {conc});
 236   }
 237   else
 238   {
 239     Trace("dt-ipc") << "...success" << std::endl;
 240   }
 241 }
 242
 243 std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
 244 {
 245   Trace("dt-ipc") << "dt-ipc: Ask proof for " << fact << std::endl;
 246   // temporary proof
 247   CDProof pf(d_pnm);
 248   // get the inference
 249   NodeDatatypesInferenceMap::iterator it = d_lazyFactMap.find(fact);
 250   if (it == d_lazyFactMap.end())
 251   {
 252     Node factSym = CDProof::getSymmFact(fact);
 253     if (!factSym.isNull())
 254     {
 255       // Use the symmetric fact. There is no need to explictly make a
 256       // SYMM proof, as this is handled by CDProof::getProofFor below.
 257       it = d_lazyFactMap.find(factSym);
 258     }
 259   }
 260   AlwaysAssert(it != d_lazyFactMap.end());
 261   // now go back and convert it to proof steps and add to proof
 262   std::shared_ptr<DatatypesInference> di = (*it).second;
 263   // run the conversion
 264   convert(di->getId(), di->d_conc, di->d_exp, &pf);
 265   return pf.getProofFor(fact);
 266 }
 267
 268 std::string InferProofCons::identify() const
 269 {
 270   return "datatypes::InferProofCons";
 271 }
 272
 273 }  // namespace datatypes
 274 }  // namespace theory
 275 }  // namespace CVC4