| Class | Description | 
|---|---|
| SMTFile | |
| SMTFunction | |
| SMTFunctionDef | |
| SMTSort | |
| SMTTerm | |
| SMTTerm.False | |
| SMTTerm.True | |
| SMTTermBinOp | |
| SMTTermCall | 
 SMTLib supports functions as well as predicates. 
 | 
| SMTTermITE | |
| SMTTermMultOp | |
| SMTTermNumber | |
| SMTTermQuant | |
| SMTTerms | |
| SMTTermUnaryOp | |
| SMTTermVariable | |
| Util | 
| Enum | Description | 
|---|---|
| SMTTermBinOp.Op | |
| SMTTermBinOp.OpProperty | |
| SMTTermMultOp.Op | |
| SMTTermMultOp.OpProperty | |
| SMTTermQuant.Quant | |
| SMTTermUnaryOp.Op |