diff options
Diffstat (limited to 'contrib/theoryskel/README.WHATS-NEXT')
| -rw-r--r-- | contrib/theoryskel/README.WHATS-NEXT | 46 |
1 files changed, 0 insertions, 46 deletions
diff --git a/contrib/theoryskel/README.WHATS-NEXT b/contrib/theoryskel/README.WHATS-NEXT deleted file mode 100644 index 213004d5b..000000000 --- a/contrib/theoryskel/README.WHATS-NEXT +++ /dev/null @@ -1,46 +0,0 @@ -Congratulations, you now have a new theory of $dir ! - -Your next steps will likely be: - -* to specify theory constants, types, and operators in your \`kinds' file -* 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; 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 - in src/expr/type_node.h and a corresponding Type derived class in - src/expr/type.h. -* to write parser rules in src/parser/cvc/Cvc.g to support the CVC input - language, src/parser/smt/Smt.g to support the (deprecated) SMT-LIBv1 - language, and src/parser/smt2/Smt2.g to support SMT-LIBv2 -* to write printer code in -src/printer/*/*_printer* to support printing - your theory terms and types in various output languages - -and finally: - -* to implement a decision procedure for your theory by implementing - Theory$camel::check() in theory_$dir.cpp. Before writing the actual - code, you will need : - - * to determine which data structures are context dependent and use for - them context-dependent data structures (context/cd*.h) - * to choose which work will be done at QUICK_CHECK, STANDARD or at - FULL_EFFORT. - -You'll probably find the Developer's wiki useful: - - http://cvc4.cs.stanford.edu/wiki/ - -...and the Developer's Guide: - - https://github.com/CVC4/CVC4/wiki/Developer-Guide - -which contains coding guidelines for the CVC4 project. - -Good luck, and please contact cvc4-devel@cs.stanford.edu for assistance -should you need it! |