diff options
Diffstat (limited to 'src/proof/proof.h')
| -rw-r--r-- | src/proof/proof.h | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/src/proof/proof.h b/src/proof/proof.h index ae4c940a0..d69cd6198 100644 --- a/src/proof/proof.h +++ b/src/proof/proof.h @@ -9,9 +9,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Proof manager + ** \brief Proof macros ** - ** Proof manager + ** Proof macros **/ #include "cvc4_private.h" @@ -46,14 +46,25 @@ */ #ifdef CVC4_PROOF -# define PROOF(x) if(options::proof() || options::unsatCores()) { x; } -# define NULLPROOF(x) (options::proof() || options::unsatCores()) ? x : NULL -# define PROOF_ON() (options::proof() || options::unsatCores()) +# define PROOF(x) if(CVC4::options::proof() || CVC4::options::unsatCores()) { x; } +# define NULLPROOF(x) (CVC4::options::proof() || CVC4::options::unsatCores()) ? x : NULL +# define PROOF_ON() (CVC4::options::proof() || CVC4::options::unsatCores()) +# define THEORY_PROOF(x) if(CVC4::options::proof()) { x; } +# define THEORY_NULLPROOF(x) CVC4::options::proof() ? x : NULL +# define THEORY_PROOF_ON() CVC4::options::proof() #else /* CVC4_PROOF */ # define PROOF(x) # define NULLPROOF(x) NULL # define PROOF_ON() false +# define THEORY_PROOF(x) +# define THEORY_NULLPROOF(x) NULL +# define THEORY_PROOF_ON() false #endif /* CVC4_PROOF */ +#ifdef CVC4_PROOF_STATS /* CVC4_PROOF_STATS */ +# define PSTATS(x) { x; } +#else +# define PSTATS(x) +#endif /* CVC4_PROOF_STATS */ #endif /* __CVC4__PROOF__PROOF_H */ |