src/smt/witness_form.h

   1 /*********************                                                        */
   2 /*! \file witness_form.h
   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 "cvc4_private.h"
  16
  17 #ifndef CVC4__SMT__WITNESS_FORM_H
  18 #define CVC4__SMT__WITNESS_FORM_H
  19
  20 #include <unordered_set>
  21
  22 #include "expr/node_manager.h"
  23 #include "expr/proof.h"
  24 #include "expr/proof_generator.h"
  25 #include "expr/term_conversion_proof_generator.h"
  26
  27 namespace CVC4 {
  28 namespace smt {
  29
  30 /**
  31  * The witness form proof generator, which acts as a wrapper around a
  32  * TConvProofGenerator for adding rewrite steps for witness introduction.
  33  *
  34  * The proof steps managed by this class are stored in a context-independent
  35  * manager, which matches how witness forms are managed in SkolemManager.
  36  */
  37 class WitnessFormGenerator : public ProofGenerator
  38 {
  39  public:
  40   WitnessFormGenerator(ProofNodeManager* pnm);
  41   ~WitnessFormGenerator() {}
  42   /**
  43    * Get proof for, which expects an equality of the form t = toWitness(t).
  44    * This returns a proof based on the term conversion proof generator utility.
  45    * This proof may contain open assumptions of the form:
  46    *   k = toWitness(k)
  47    * Each of these assumptions are included in the set getWitnessFormEqs()
  48    * below after returning this call.
  49    */
  50   std::shared_ptr<ProofNode> getProofFor(Node eq) override;
  51   /** Identify */
  52   std::string identify() const override;
  53   /**
  54    * Does the rewrite require witness form conversion?
  55    * When calling this method, it should be the case that:
  56    *   Rewriter::rewrite(toWitness(t)) == Rewriter::rewrite(toWitness(s))
  57    * The rule MACRO_SR_PRED_TRANSFORM concludes t == s if the above holds.
  58    * This method returns false if:
  59    *   Rewriter::rewrite(t) == Rewriter::rewrite(s)
  60    * which means that the proof of the above fact does not need to do
  61    * witness form conversion to prove conclusions of MACRO_SR_PRED_TRANSFORM.
  62    */
  63   bool requiresWitnessFormTransform(Node t, Node s) const;
  64   /**
  65    * Same as above, with s = true. This is intended for use with
  66    * MACRO_SR_PRED_INTRO.
  67    */
  68   bool requiresWitnessFormIntro(Node t) const;
  69   /**
  70    * Get witness form equalities. This returns a set of equalities of the form:
  71    *   k = toWitness(k)
  72    * where k is a skolem, containing all rewrite steps used in calls to
  73    * getProofFor during the entire lifetime of this generator.
  74    */
  75   const std::unordered_set<Node, NodeHashFunction>& getWitnessFormEqs() const;
  76
  77  private:
  78   /**
  79    * Convert to witness form. This internally constructs rewrite steps that
  80    * suffice to show t = toWitness(t) using the term conversion proof generator
  81    * of this class (d_tcpg).
  82    */
  83   Node convertToWitnessForm(Node t);
  84   /**
  85    * Return a proof generator that can prove the given axiom exists.
  86    */
  87   ProofGenerator* convertExistsInternal(Node exists);
  88   /** The term conversion proof generator */
  89   TConvProofGenerator d_tcpg;
  90   /** The nodes we have already added rewrite steps for in d_tcpg */
  91   std::unordered_set<TNode, TNodeHashFunction> d_visited;
  92   /** The set of equalities added as proof steps */
  93   std::unordered_set<Node, NodeHashFunction> d_eqs;
  94   /** Lazy proof storing witness intro steps */
  95   LazyCDProof d_wintroPf;
  96   /** CDProof for justifying purification existentials */
  97   CDProof d_pskPf;
  98 };
  99
 100 }  // namespace smt
 101 }  // namespace CVC4
 102
 103 #endif