diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-14 17:09:59 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-14 17:09:59 -0600 |
| commit | 528e801343c692b0ce8123f8754e069e6523f5dc (patch) | |
| tree | 517c86381e7a0535c376d244c830365d04e3aa62 /src/api/cvc4cppkind.h | |
| parent | 08289dd911aff28110baf0fd815fd912f8b76fd3 (diff) | |
Remove quantifiers rewrite rules infrastructure (#3754)
Diffstat (limited to 'src/api/cvc4cppkind.h')
| -rw-r--r-- | src/api/cvc4cppkind.h | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index bb2700706..2242c8e00 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -2181,14 +2181,6 @@ enum CVC4_PUBLIC Kind : int32_t INST_PATTERN_LIST, /* predicate for specifying term in instantiation closure. */ INST_CLOSURE, - /* general rewrite rule (for rewrite-rules theory) */ - REWRITE_RULE, - /* actual rewrite rule (for rewrite-rules theory) */ - RR_REWRITE, - /* actual reduction rule (for rewrite-rules theory) */ - RR_REDUCTION, - /* actual deduction rule (for rewrite-rules theory) */ - RR_DEDUCTION, /* Sort Kinds ------------------------------------------------------------ */ |