diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/theoryskel/README.WHATS-NEXT | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/contrib/theoryskel/README.WHATS-NEXT b/contrib/theoryskel/README.WHATS-NEXT index 31ff2d47a..17affade4 100644 --- a/contrib/theoryskel/README.WHATS-NEXT +++ b/contrib/theoryskel/README.WHATS-NEXT @@ -6,7 +6,9 @@ Your next steps will likely be: * to add typing rules to theory_$dir_type_rules.h for your operators and constants * to write code in theory_$dir_rewriter.h to implement a normal form - for your theory's terms + for your theory's terms; in particular, you should ensure that you + rewrite (= X X) to "true" for terms X of your theory's sorts, and + evaluate any constant terms * for any new types that you have introduced, add "mk*Type()" functions to the NodeManager and ExprManager in src/expr/node_manager.{h,cpp} and src/expr/expr_manager_template.{h,cpp}. You may also want "is*()" testers |