diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-09-01 10:57:51 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-01 14:57:51 -0300 |
| commit | 58f059a967ccb968f127b2d56f69c20700a943fb (patch) | |
| tree | 86dc604488e7faa371020b59283339ee8bce3714 | |
| parent | a276c5259782f867584bdd5e6e5cd50adc3c5dae (diff) | |
Add arithmetic-specific, runtime, proof-macros. (#4992)
We'll use this to gate farkas-coefficient machinery after we remove the
old proof-macros.
I've changed the macros slightly from the proof-new branch: I removed the dependence on options::proof() (no longer wanted) and options::unsatCores() (I had copied this from the original proof macros, but it's not needed either, since we're in a theory).
| -rw-r--r-- | src/theory/arith/proof_macros.h | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/src/theory/arith/proof_macros.h b/src/theory/arith/proof_macros.h new file mode 100644 index 000000000..6cc1b3b15 --- /dev/null +++ b/src/theory/arith/proof_macros.h @@ -0,0 +1,34 @@ +/********************* */ +/*! \file proof_macros.h + ** \verbatim + ** Top contributors (to current version): + ** Alex Ozdemir + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Macros which run code when the old or new proof system is enabled, + ** or unsat cores are enabled. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__ARITH__PROOF_MACROS_H +#define CVC4__THEORY__ARITH__PROOF_MACROS_H + +#include "options/smt_options.h" + +#define ARITH_PROOF(x) \ + if (CVC4::options::proofNew()) \ + { \ + x; \ + } +#define ARITH_NULLPROOF(x) \ + (CVC4::options::proofNew()) \ + ? x \ + : NULL +#define ARITH_PROOF_ON() CVC4::options::proofNew() + +#endif // CVC4__THEORY__ARITH__PROOF_MACROS_H |