diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/arith/kinds | 2 | ||||
| -rw-r--r-- | src/theory/theoryof_table_epilogue.h | 3 | ||||
| -rw-r--r-- | src/theory/theoryof_table_middle.h | 3 | ||||
| -rw-r--r-- | src/theory/theoryof_table_prologue.h | 3 |
4 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 994416838..fd784ccce 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -1 +1,3 @@ PLUS +MULT +UMINUS diff --git a/src/theory/theoryof_table_epilogue.h b/src/theory/theoryof_table_epilogue.h index 7483248ec..11f75183a 100644 --- a/src/theory/theoryof_table_epilogue.h +++ b/src/theory/theoryof_table_epilogue.h @@ -10,7 +10,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** The theoryOf table. + ** The epilogue section for the automatically-generated theoryOf table. + ** See the mktheoryof script. **/ };/* class TheoryOfTable */ diff --git a/src/theory/theoryof_table_middle.h b/src/theory/theoryof_table_middle.h index 17a945d01..f3ad433a3 100644 --- a/src/theory/theoryof_table_middle.h +++ b/src/theory/theoryof_table_middle.h @@ -10,7 +10,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** The theoryOf table. + ** The middle section for the automatically-generated theoryOf table. + ** See the mktheoryof script. **/ namespace CVC4 { diff --git a/src/theory/theoryof_table_prologue.h b/src/theory/theoryof_table_prologue.h index 47fd2d9b2..6e83d6d2c 100644 --- a/src/theory/theoryof_table_prologue.h +++ b/src/theory/theoryof_table_prologue.h @@ -10,7 +10,8 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** The theoryOf table. + ** The prologue section for the automatically-generated theoryOf table. + ** See the mktheoryof script. **/ #include "cvc4_private.h" |