src/smt/witness_form.cpp

   1 /*********************                                                        */
   2 /*! \file witness_form.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 The module for managing witness form conversion in proofs
  13  **/
  14
  15 #include "smt/witness_form.h"
  16
  17 #include "expr/skolem_manager.h"
  18 #include "theory/rewriter.h"
  19
  20 namespace CVC4 {
  21 namespace smt {
  22
  23 WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm)
  24     : d_tcpg(pnm,
  25              nullptr,
  26              TConvPolicy::FIXPOINT,
  27              TConvCachePolicy::NEVER,
  28              "WfGenerator::TConvProofGenerator",
  29              nullptr,
  30              true),
  31       d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof"),
  32       d_pskPf(pnm, nullptr, "WfGenerator::PurifySkolemProof")
  33 {
  34 }
  35
  36 std::shared_ptr<ProofNode> WitnessFormGenerator::getProofFor(Node eq)
  37 {
  38   if (eq.getKind() != kind::EQUAL)
  39   {
  40     // expecting an equality
  41     return nullptr;
  42   }
  43   Node lhs = eq[0];
  44   Node rhs = convertToWitnessForm(eq[0]);
  45   if (rhs != eq[1])
  46   {
  47     // expecting witness form
  48     return nullptr;
  49   }
  50   std::shared_ptr<ProofNode> pn = d_tcpg.getProofFor(eq);
  51   Assert(pn != nullptr);
  52   return pn;
  53 }
  54
  55 std::string WitnessFormGenerator::identify() const
  56 {
  57   return "WitnessFormGenerator";
  58 }
  59
  60 Node WitnessFormGenerator::convertToWitnessForm(Node t)
  61 {
  62   NodeManager* nm = NodeManager::currentNM();
  63   SkolemManager* skm = nm->getSkolemManager();
  64   Node tw = SkolemManager::getWitnessForm(t);
  65   if (t == tw)
  66   {
  67     // trivial case
  68     return tw;
  69   }
  70   std::unordered_set<TNode, TNodeHashFunction>::iterator it;
  71   std::vector<TNode> visit;
  72   TNode cur;
  73   TNode curw;
  74   visit.push_back(t);
  75   do
  76   {
  77     cur = visit.back();
  78     visit.pop_back();
  79     it = d_visited.find(cur);
  80     if (it == d_visited.end())
  81     {
  82       d_visited.insert(cur);
  83       curw = SkolemManager::getWitnessForm(cur);
  84       // if its witness form is different
  85       if (cur != curw)
  86       {
  87         if (cur.isVar())
  88         {
  89           Node eq = cur.eqNode(curw);
  90           // equality between a variable and its witness form
  91           d_eqs.insert(eq);
  92           Assert(curw.getKind() == kind::WITNESS);
  93           Node skBody = SkolemManager::getSkolemForm(curw[1]);
  94           Node exists = nm->mkNode(kind::EXISTS, curw[0], skBody);
  95           ProofGenerator* pg = skm->getProofGenerator(exists);
  96           if (pg == nullptr)
  97           {
  98             // it may be a purification skolem
  99             pg = convertExistsInternal(exists);
 100             if (pg == nullptr)
 101             {
 102               // if no proof generator is provided, we justify the existential
 103               // using the WITNESS_AXIOM trusted rule by providing it to the
 104               // call to addLazyStep below.
 105               Trace("witness-form")
 106                   << "WitnessFormGenerator: No proof generator for " << exists
 107                   << std::endl;
 108             }
 109           }
 110           // --------------------------- from pg
 111           // (exists ((x T)) (P x))
 112           // --------------------------- WITNESS_INTRO
 113           // k = (witness ((x T)) (P x))
 114           d_wintroPf.addLazyStep(
 115               exists,
 116               pg,
 117               PfRule::WITNESS_AXIOM,
 118               true,
 119               "WitnessFormGenerator::convertToWitnessForm:witness_axiom");
 120           d_wintroPf.addStep(eq, PfRule::WITNESS_INTRO, {exists}, {});
 121           d_tcpg.addRewriteStep(cur, curw, &d_wintroPf, PfRule::ASSUME, true);
 122         }
 123         else
 124         {
 125           // A term whose witness form is different from itself, recurse.
 126           // It should be the case that cur has children, since the witness
 127           // form of constants are themselves.
 128           Assert(cur.getNumChildren() > 0);
 129           if (cur.hasOperator())
 130           {
 131             visit.push_back(cur.getOperator());
 132           }
 133           visit.insert(visit.end(), cur.begin(), cur.end());
 134         }
 135       }
 136     }
 137   } while (!visit.empty());
 138   return tw;
 139 }
 140
 141 bool WitnessFormGenerator::requiresWitnessFormTransform(Node t, Node s) const
 142 {
 143   return theory::Rewriter::rewrite(t) != theory::Rewriter::rewrite(s);
 144 }
 145
 146 bool WitnessFormGenerator::requiresWitnessFormIntro(Node t) const
 147 {
 148   Node tr = theory::Rewriter::rewrite(t);
 149   return !tr.isConst() || !tr.getConst<bool>();
 150 }
 151
 152 const std::unordered_set<Node, NodeHashFunction>&
 153 WitnessFormGenerator::getWitnessFormEqs() const
 154 {
 155   return d_eqs;
 156 }
 157
 158 ProofGenerator* WitnessFormGenerator::convertExistsInternal(Node exists)
 159 {
 160   Assert(exists.getKind() == kind::EXISTS);
 161   if (exists[0].getNumChildren() == 1 && exists[1].getKind() == kind::EQUAL
 162       && exists[1][0] == exists[0][0])
 163   {
 164     Node tpurified = exists[1][1];
 165     Trace("witness-form") << "convertExistsInternal: infer purification "
 166                           << exists << " for " << tpurified << std::endl;
 167     // ------ REFL
 168     // t = t
 169     // ---------------- EXISTS_INTRO
 170     // exists x. x = t
 171     // The concluded existential is then used to construct the witness term
 172     // via witness intro.
 173     Node teq = tpurified.eqNode(tpurified);
 174     d_pskPf.addStep(teq, PfRule::REFL, {}, {tpurified});
 175     d_pskPf.addStep(exists, PfRule::EXISTS_INTRO, {teq}, {exists});
 176     return &d_pskPf;
 177   }
 178   return nullptr;
 179 }
 180
 181 }  // namespace smt
 182 }  // namespace CVC4