diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-09 16:14:21 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-09 23:14:21 +0000 |
commit | 550c49a7dd2b13ea29743458336f0c0a0fb6099a (patch) | |
tree | b06962055a5de77d39c95fc577e54c0d7d69dcfd /src/theory/builtin | |
parent | ca7e206c239d8de0f25fb23544e4923641b85d11 (diff) |
Rename CVC4__ header guards to CVC5__. (#6326)
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/proof_checker.h | 6 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin.h | 6 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.h | 6 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 6 | ||||
-rw-r--r-- | src/theory/builtin/type_enumerator.h | 6 |
5 files changed, 15 insertions, 15 deletions
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index f80434068..13d4dd552 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__BUILTIN__PROOF_CHECKER_H -#define CVC4__THEORY__BUILTIN__PROOF_CHECKER_H +#ifndef CVC5__THEORY__BUILTIN__PROOF_CHECKER_H +#define CVC5__THEORY__BUILTIN__PROOF_CHECKER_H #include "expr/node.h" #include "expr/proof_checker.h" @@ -181,4 +181,4 @@ class BuiltinProofRuleChecker : public ProofRuleChecker } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__BUILTIN__PROOF_CHECKER_H */ +#endif /* CVC5__THEORY__BUILTIN__PROOF_CHECKER_H */ diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index fca05d7ff..08f903527 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H -#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H +#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_H +#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_H #include "theory/builtin/proof_checker.h" #include "theory/builtin/theory_builtin_rewriter.h" @@ -58,4 +58,4 @@ class TheoryBuiltin : public Theory } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */ +#endif /* CVC5__THEORY__BUILTIN__THEORY_BUILTIN_H */ diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index 7625aa846..ef3835f58 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H -#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H +#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H +#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H #include "theory/theory_rewriter.h" @@ -121,4 +121,4 @@ class TheoryBuiltinRewriter : public TheoryRewriter } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */ +#endif /* CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */ diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 2c474aaee..f660a8477 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H -#define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H +#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H +#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H #include "expr/node.h" #include "expr/type_node.h" @@ -250,4 +250,4 @@ class FunctionProperties { } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */ +#endif /* CVC5__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */ diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index 7c14bb14c..0b51c3f51 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H -#define CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H +#ifndef CVC5__THEORY__BUILTIN__TYPE_ENUMERATOR_H +#define CVC5__THEORY__BUILTIN__TYPE_ENUMERATOR_H #include "expr/kind.h" #include "expr/type_node.h" @@ -108,4 +108,4 @@ class FunctionEnumerator : public TypeEnumeratorBase<FunctionEnumerator> } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__BUILTIN_TYPE_ENUMERATOR_H */ +#endif /* CVC5__THEORY__BUILTIN_TYPE_ENUMERATOR_H */ |