src/proof/method_id.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  * Method identifier enumeration
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__PROOF__METHOD_ID_H
  19 #define CVC5__PROOF__METHOD_ID_H
  20
  21 #include "expr/node.h"
  22
  23 namespace cvc5 {
  24
  25 /**
  26  * Identifiers for rewriters and substitutions, which we abstractly
  27  * classify as "methods".  Methods have a unique identifier in the internal
  28  * proof calculus implemented by the checker below.
  29  *
  30  * A "rewriter" is abstractly a method from Node to Node, where the output
  31  * is semantically equivalent to the input. The identifiers below list
  32  * various methods that have this contract. This identifier is used
  33  * in a number of the builtin rules.
  34  *
  35  * A substitution is a method for turning a formula into a substitution.
  36  */
  37 enum class MethodId : uint32_t
  38 {
  39   //---------------------------- Rewriters
  40   // Rewriter::rewrite(n)
  41   RW_REWRITE,
  42   // d_ext_rew.extendedRewrite(n);
  43   RW_EXT_REWRITE,
  44   // Rewriter::rewriteExtEquality(n)
  45   RW_REWRITE_EQ_EXT,
  46   // Evaluator::evaluate(n)
  47   RW_EVALUATE,
  48   // identity
  49   RW_IDENTITY,
  50   // theory preRewrite, note this is only intended to be used as an argument
  51   // to THEORY_REWRITE in the final proof. It is not implemented in
  52   // Rewriter::rewriteViaMethod, see documentation in proof_rule.h for
  53   // THEORY_REWRITE.
  54   RW_REWRITE_THEORY_PRE,
  55   // same as above, for theory postRewrite
  56   RW_REWRITE_THEORY_POST,
  57   //---------------------------- Substitutions
  58   // (= x y) is interpreted as x -> y, using Node::substitute
  59   SB_DEFAULT,
  60   // P, (not P) are interpreted as P -> true, P -> false using Node::substitute
  61   SB_LITERAL,
  62   // P is interpreted as P -> true using Node::substitute
  63   SB_FORMULA,
  64   //---------------------------- Substitution applications
  65   // multiple substitutions are applied sequentially
  66   SBA_SEQUENTIAL,
  67   // multiple substitutions are applied simultaneously
  68   SBA_SIMUL,
  69   // multiple substitutions are applied to fix point
  70   SBA_FIXPOINT
  71   // For example, for x -> u, y -> f(z), z -> g(x), applying this substituion to
  72   // y gives:
  73   // - f(g(x)) for SBA_SEQUENTIAL
  74   // - f(z) for SBA_SIMUL
  75   // - f(g(u)) for SBA_FIXPOINT
  76   // Notice that SBA_FIXPOINT should provide a terminating rewrite system
  77   // as a substitution, or else non-termination will occur during proof
  78   // checking.
  79 };
  80 /** Converts a rewriter id to a string. */
  81 const char* toString(MethodId id);
  82 /** Write a rewriter id to out */
  83 std::ostream& operator<<(std::ostream& out, MethodId id);
  84 /** Make a method id node */
  85 Node mkMethodId(MethodId id);
  86
  87 /** get a method identifier from a node, return false if we fail */
  88 bool getMethodId(TNode n, MethodId& i);
  89 /**
  90  * Get method identifiers from args starting at the given index. Store their
  91  * values into ids, ida, and idr. This method returns false if args does not
  92  * contain valid method identifiers at position index in args.
  93  */
  94 bool getMethodIds(const std::vector<Node>& args,
  95                   MethodId& ids,
  96                   MethodId& ida,
  97                   MethodId& idr,
  98                   size_t index);
  99 /**
 100  * Add method identifiers ids, ida and idr as nodes to args. This does not add
 101  * ids, ida or idr if their values are the default ones.
 102  */
 103 void addMethodIds(std::vector<Node>& args,
 104                   MethodId ids,
 105                   MethodId ida,
 106                   MethodId idr);
 107
 108 }  // namespace cvc5
 109
 110 #endif /* CVC5__PROOF__METHOD_ID_H */