summaryrefslogtreecommitdiff
path: root/contrib/theoryskel/README.WHATS-NEXT
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2021-04-21 10:21:34 -0700
committerGitHub <noreply@github.com>2021-04-21 10:21:34 -0700
commitae5ee4b07dc3d3c792e7fe7f382ff490dd28aca4 (patch)
treea7c2ab8013f46dbea75fcd6e7da3fb83e2012b2f /contrib/theoryskel/README.WHATS-NEXT
parent86aa9bc35ba9dc9a57913a2ffc71619c7657cc35 (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-NEXT46
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!
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback