src/theory/builtin/proof_checker.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   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  * Builtin proof checker utility.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY__BUILTIN__PROOF_CHECKER_H
  19 #define CVC5__THEORY__BUILTIN__PROOF_CHECKER_H
  20
  21 #include "expr/node.h"
  22 #include "proof/method_id.h"
  23 #include "proof/proof_checker.h"
  24 #include "proof/proof_node.h"
  25 #include "theory/quantifiers/extended_rewrite.h"
  26
  27 namespace cvc5 {
  28
  29 class Env;
  30
  31 namespace theory {
  32 namespace builtin {
  33
  34 /** A checker for builtin proofs */
  35 class BuiltinProofRuleChecker : public ProofRuleChecker
  36 {
  37  public:
  38   /** Constructor. */
  39   BuiltinProofRuleChecker(Env& env);
  40   /** Destructor. */
  41   ~BuiltinProofRuleChecker() {}
  42   /**
  43    * Apply rewrite on n (in skolem form). This encapsulates the exact behavior
  44    * of a REWRITE step in a proof.
  45    *
  46    * @param n The node to rewrite,
  47    * @param idr The method identifier of the rewriter, by default RW_REWRITE
  48    * specifying a call to Rewriter::rewrite.
  49    * @return The rewritten form of n.
  50    */
  51   Node applyRewrite(TNode n, MethodId idr = MethodId::RW_REWRITE);
  52   /**
  53    * Get substitution for literal exp. Updates vars/subs to the substitution
  54    * specified by exp for the substitution method ids.
  55    */
  56   static bool getSubstitutionForLit(Node exp,
  57                                     TNode& var,
  58                                     TNode& subs,
  59                                     MethodId ids = MethodId::SB_DEFAULT);
  60   /**
  61    * Get substitution for formula exp. Adds to vars/subs to the substitution
  62    * specified by exp for the substitution method ids, which may be multiple
  63    * substitutions if exp is of kind AND and ids is SB_DEFAULT (note the other
  64    * substitution types always interpret applications of AND as a formula).
  65    * The vector "from" are the literals from exp that each substitution in
  66    * vars/subs are based on. For example, if exp is (and (= x t) (= y s)), then
  67    * vars = { x, y }, subs = { t, s }, from = { (= x y), (= y s) }.
  68    */
  69   static bool getSubstitutionFor(Node exp,
  70                                  std::vector<TNode>& vars,
  71                                  std::vector<TNode>& subs,
  72                                  std::vector<TNode>& from,
  73                                  MethodId ids = MethodId::SB_DEFAULT);
  74
  75   /**
  76    * Apply substitution on n in skolem form. This encapsulates the exact
  77    * behavior of a SUBS step in a proof.
  78    *
  79    * @param n The node to substitute,
  80    * @param exp The (set of) equalities/literals/formulas that the substitution
  81    * is derived from
  82    * @param ids The method identifier of the substitution, by default SB_DEFAULT
  83    * specifying that lhs/rhs of equalities are interpreted as a substitution.
  84    * @param ida The method identifier of the substitution application, by
  85    * default SB_SEQUENTIAL specifying that substitutions are to be applied
  86    * sequentially
  87    * @return The substituted form of n.
  88    */
  89   static Node applySubstitution(Node n,
  90                                 Node exp,
  91                                 MethodId ids = MethodId::SB_DEFAULT,
  92                                 MethodId ida = MethodId::SBA_SEQUENTIAL);
  93   static Node applySubstitution(Node n,
  94                                 const std::vector<Node>& exp,
  95                                 MethodId ids = MethodId::SB_DEFAULT,
  96                                 MethodId ida = MethodId::SBA_SEQUENTIAL);
  97   /** Apply substitution + rewriting
  98    *
  99    * Combines the above two steps.
 100    *
 101    * @param n The node to substitute and rewrite,
 102    * @param exp The (set of) equalities corresponding to the substitution
 103    * @param ids The method identifier of the substitution.
 104    * @param ida The method identifier of the substitution application.
 105    * @param idr The method identifier of the rewriter.
 106    * @return The substituted, rewritten form of n.
 107    */
 108   Node applySubstitutionRewrite(Node n,
 109                                 const std::vector<Node>& exp,
 110                                 MethodId ids = MethodId::SB_DEFAULT,
 111                                 MethodId ida = MethodId::SBA_SEQUENTIAL,
 112                                 MethodId idr = MethodId::RW_REWRITE);
 113
 114   /** get a TheoryId from a node, return false if we fail */
 115   static bool getTheoryId(TNode n, TheoryId& tid);
 116   /** Make a TheoryId into a node */
 117   static Node mkTheoryIdNode(TheoryId tid);
 118
 119   /** Register all rules owned by this rule checker into pc. */
 120   void registerTo(ProofChecker* pc) override;
 121  protected:
 122   /** Return the conclusion of the given proof step, or null if it is invalid */
 123   Node checkInternal(PfRule id,
 124                      const std::vector<Node>& children,
 125                      const std::vector<Node>& args) override;
 126
 127   /** extended rewriter object */
 128   quantifiers::ExtendedRewriter d_ext_rewriter;
 129
 130  private:
 131   /** Reference to the environment. */
 132   Env& d_env;
 133 };
 134
 135 }  // namespace builtin
 136 }  // namespace theory
 137 }  // namespace cvc5
 138
 139 #endif /* CVC5__THEORY__BUILTIN__PROOF_CHECKER_H */