diff options
| author | François Bobot <francois@bobot.eu> | 2012-02-13 23:12:15 +0000 |
|---|---|---|
| committer | François Bobot <francois@bobot.eu> | 2012-02-13 23:12:15 +0000 |
| commit | 093fa1757392e7bfc18493f2daa87ff540aeea86 (patch) | |
| tree | d44573a73e8918b7c7d885b258938668c1ae28bf /contrib/theoryskel | |
| parent | c691f9118e104129bf894b568542c7509e9747a0 (diff) | |
precision in theoryskel
Diffstat (limited to 'contrib/theoryskel')
| -rw-r--r-- | contrib/theoryskel/README.WHATS-NEXT | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/contrib/theoryskel/README.WHATS-NEXT b/contrib/theoryskel/README.WHATS-NEXT index ce07eafb9..e860c5373 100644 --- a/contrib/theoryskel/README.WHATS-NEXT +++ b/contrib/theoryskel/README.WHATS-NEXT @@ -16,7 +16,14 @@ Your next steps will likely be: and finally: * to implement a decision procedure for your theory by implementing - Theory$camel::check() in theory_$dir.cpp + Theory$camel::check() in theory_$dir.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! |