| # Permission is hereby granted, free of charge, to any person obtaining a copy |
| # of this software and associated documentation files (the "Software"), to deal |
| # in the Software without restriction, including without limitation the rights |
| # to use, copy, modify, merge, publish, distribute, sublicense, and/or sell |
| # copies of the Software, and to permit persons to whom the Software is |
| # furnished to do so, subject to the following conditions: |
| # |
| # The above copyright notice and this permission notice shall be included in |
| # all copies or substantial portions of the Software. |
| # |
| # THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR |
| # IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, |
| # FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE |
| # AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER |
| # LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, |
| # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN |
| # THE SOFTWARE. |
| # |
| # |
| # name minkids maxkids category1 category2 |
| Categories: Term Form |
| |
| # Leaf nodes. |
| UNDEFINED 0 0 |
| SYMBOL 0 0 Term Form |
| |
| # These always produce terms |
| BVCONST 0 0 Term |
| BVNOT 1 1 Term |
| BVCONCAT 2 - Term |
| BVOR 1 - Term |
| BVAND 1 - Term |
| BVXOR 1 - Term |
| BVNAND 1 - Term |
| BVNOR 1 - Term |
| BVXNOR 1 - Term |
| BVEXTRACT 3 3 Term |
| BVLEFTSHIFT 3 3 Term |
| BVRIGHTSHIFT 3 3 Term |
| BVSRSHIFT 3 3 Term |
| BVPLUS 1 - Term |
| BVSUB 2 2 Term |
| BVUMINUS 1 1 Term |
| BVMULT 1 - Term |
| BVDIV 2 2 Term |
| BVMOD 2 2 Term |
| SBVDIV 2 2 Term |
| SBVREM 2 2 Term |
| SBVMOD 2 2 Term |
| BVSX 1 1 Term |
| BVZX 1 1 Term |
| #BOOLVEC 0 - Term |
| |
| # Formula OR term, depending on context |
| ITE 3 3 Term Form |
| |
| # These produce formulas. |
| BOOLEXTRACT 2 2 Form |
| BVLT 2 2 Form |
| BVLE 2 2 Form |
| BVGT 2 2 Form |
| BVGE 2 2 Form |
| BVSLT 2 2 Form |
| BVSLE 2 2 Form |
| BVSGT 2 2 Form |
| BVSGE 2 2 Form |
| EQ 2 2 Form |
| FALSE 0 0 Form |
| TRUE 0 0 Form |
| NOT 1 1 Form |
| AND 1 - Form |
| OR 1 - Form |
| NAND 1 - Form |
| NOR 1 - Form |
| XOR 1 - Form |
| IFF 1 - Form |
| IMPLIES 2 2 Form |
| PARAMBOOL 2 2 Form |
| |
| # array operations |
| READ 2 2 Term |
| WRITE 3 3 Term |
| |
| #Types: These kinds are used only in the API. Once processed inside |
| #the API, they are never used again in the system |
| ARRAY 0 0 |
| BITVECTOR 0 0 |
| BOOLEAN 0 0 |
| |