diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2018-12-17 15:01:23 -0800 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-12-17 15:01:23 -0800 |
| commit | 6660ab05c399d309208251263faeff3be2964f7b (patch) | |
| tree | ec7ba5d8c9d1ff90611bfce726acb3044be39d6d /src/base | |
| parent | 332357104e9ab1937049f0ea8e53042d8534f966 (diff) | |
Configured for linking against drat2er (#2754)
drat2er is a C/C++ project which includes support for
* Checking DRAT proofs
* Converting DRAT proofs to LRAT proofs
* Converting DRAT proofs to ER proofs
It does the first 2 by using drat-trim under the hood.
I've modified our CMake configuration to allow drat2er to be linked into
CVC4, and I added a contrib script.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/configuration_private.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 5164d46bc..77f3f5e77 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -126,6 +126,12 @@ namespace CVC4 { # define IS_CRYPTOMINISAT_BUILD false #endif /* CVC4_USE_CRYPTOMINISAT */ +#if CVC4_USE_DRAT2ER +# define IS_DRAT2ER_BUILD true +#else /* CVC4_USE_DRAT2ER */ +# define IS_DRAT2ER_BUILD false +#endif /* CVC4_USE_DRAT2ER */ + #if CVC4_USE_LFSC #define IS_LFSC_BUILD true #else /* CVC4_USE_LFSC */ |