diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-23 23:03:37 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-23 23:16:58 -0400 |
| commit | b25991f4c2779c34b51cd51b943290a4a3d2a9fd (patch) | |
| tree | aaec41cf29cc3574288c6110ba246f361d84ec3a /contrib/alttheoryskel/README.WHATS-NEXT | |
| parent | a006e7b92327668b76a1ab993007f42fe91052c3 (diff) | |
Theory "alternates" support
* This is a feature that Dejan and I want for the upcoming tutorial.
It allows rapid prototyping of new decision procedure implementations
(which we may choose to demonstrate), and a new --use-theory command-line
option to select from different available implementations. It has no
affect on the current set of theories, as no "alternates" are defined.
* Also update the new-theory script, which was broken and incomplete.
Diffstat (limited to 'contrib/alttheoryskel/README.WHATS-NEXT')
| -rw-r--r-- | contrib/alttheoryskel/README.WHATS-NEXT | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/contrib/alttheoryskel/README.WHATS-NEXT b/contrib/alttheoryskel/README.WHATS-NEXT new file mode 100644 index 000000000..c6ad91c3f --- /dev/null +++ b/contrib/alttheoryskel/README.WHATS-NEXT @@ -0,0 +1,25 @@ +Congratulations, you now have a new theory of $dir ! + +Your next steps will likely be: + +* 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.nyu.edu/wiki/ + +...and in particular the Developer's Guide: + + http://cvc4.cs.nyu.edu/wiki/Developer%27s_Guide + +which contains coding guidelines for the CVC4 project. + +Good luck, and please contact cvc4-devel@cs.nyu.edu for assistance +should you need it! |