diff options
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! |