diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-04-21 10:21:34 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-21 10:21:34 -0700 |
commit | ae5ee4b07dc3d3c792e7fe7f382ff490dd28aca4 (patch) | |
tree | a7c2ab8013f46dbea75fcd6e7da3fb83e2012b2f /contrib/theoryskel/README.WHATS-NEXT | |
parent | 86aa9bc35ba9dc9a57913a2ffc71619c7657cc35 (diff) |
Goodbye CVC4, hello cvc5! (#6371)
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
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! |