diff options
Diffstat (limited to 'src/theory/rewriterules/README.WHATS-NEXT')
| -rw-r--r-- | src/theory/rewriterules/README.WHATS-NEXT | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/src/theory/rewriterules/README.WHATS-NEXT b/src/theory/rewriterules/README.WHATS-NEXT new file mode 100644 index 000000000..eda7dcbe6 --- /dev/null +++ b/src/theory/rewriterules/README.WHATS-NEXT @@ -0,0 +1,29 @@ +Congratulations, you now have a new theory of rewriterules ! + +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 +* 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 + TheoryRewriterules::check() in theory_rewriterules.cpp. Before writing the actual + code, you will need : + + * to determine which datastructures are context dependent and use for them + context dependent datastructures (context/cd*.h) + * to choose which work will be done at QUICK_CHECK, STANDARD or at + FULL_EFFORT. + + +Good luck, and please contact cvc4-devel@cs.nyu.edu for assistance +should you need it! |