From 58f059a967ccb968f127b2d56f69c20700a943fb Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Tue, 1 Sep 2020 10:57:51 -0700 Subject: [PATCH] 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). --- src/theory/arith/proof_macros.h | 34 +++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 src/theory/arith/proof_macros.h 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 -- 2.30.2