1 /******************************************************************************
2 * Top contributors (to current version):
5 * This file is part of the cvc5 project.
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 * ****************************************************************************
13 * Method identifier enumeration
16 #include "cvc5_private.h"
18 #ifndef CVC5__PROOF__METHOD_ID_H
19 #define CVC5__PROOF__METHOD_ID_H
21 #include "expr/node.h"
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.
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.
35 * A substitution is a method for turning a formula into a substitution.
37 enum class MethodId
: uint32_t
39 //---------------------------- Rewriters
40 // Rewriter::rewrite(n)
42 // d_ext_rew.extendedRewrite(n);
44 // Rewriter::rewriteExtEquality(n)
46 // Evaluator::evaluate(n)
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
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
60 // P, (not P) are interpreted as P -> true, P -> false using Node::substitute
62 // P is interpreted as P -> true using Node::substitute
64 //---------------------------- Substitution applications
65 // multiple substitutions are applied sequentially
67 // multiple substitutions are applied simultaneously
69 // multiple substitutions are applied to fix point
71 // For example, for x -> u, y -> f(z), z -> g(x), applying this substituion to
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
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
);
87 /** get a method identifier from a node, return false if we fail */
88 bool getMethodId(TNode n
, MethodId
& i
);
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.
94 bool getMethodIds(const std::vector
<Node
>& args
,
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.
103 void addMethodIds(std::vector
<Node
>& args
,
110 #endif /* CVC5__PROOF__METHOD_ID_H */