diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-03-15 20:32:13 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-03-15 20:32:13 +0000 |
| commit | 8fb7c711588cb070c1e4a1d076b47f9277bfc3fe (patch) | |
| tree | cedd18e59b24d8b6adf79bb6581b66b1af23d17a /src/util/configuration_private.h | |
| parent | 1bdb81e52c7865f89663f97f6bc1244f3e4f6b12 (diff) | |
Merge from cudd branch. This mostly just adds support for linking
against cudd libraries, the propositional_query class (in util/),
which uses cudd if it's available (and otherwise answers UNKNOWN for
all queries), and the arith theory support for it (currently disabled
per Tim's request, so he can clean it up).
Other changes include:
* contrib/debug-keys - script to print all used keys under Debug(), Trace()
* test/regress/run_regression - minor fix (don't export a variable)
* configure.ac - replace a comment removed by dejan's google perf commit
* some minor copyright/documentation updates, and minor changes to source
text to make 'clang --analyze' happy.
Diffstat (limited to 'src/util/configuration_private.h')
| -rw-r--r-- | src/util/configuration_private.h | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index 56423e7d5..c0ce86c97 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -70,6 +70,12 @@ namespace CVC4 { # define IS_COMPETITION_BUILD false #endif /* CVC4_COMPETITION_MODE */ +#ifdef CVC4_CUDD +# define IS_CUDD_BUILD true +#else /* CVC4_CUDD */ +# define IS_CUDD_BUILD false +#endif /* CVC4_CUDD */ + #ifdef CVC4_GMP_IMP # define IS_GMP_BUILD true #else /* CVC4_GMP_IMP */ @@ -90,7 +96,7 @@ namespace CVC4 { #define CVC4_ABOUT_STRING string("\ This is CVC4 version " CVC4_RELEASE_STRING "\n\n\ -Copyright (C) 2009, 2010\n\ +Copyright (C) 2009, 2010, 2011\n\ The ACSys Group\n\ Courant Institute of Mathematical Sciences\n\ New York University\n\ |