diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/rewriterules/README.WHATS-NEXT | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
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! |