From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Tue, 1 Sep 2020 17:57:51 +0000 (-0700)
Subject: Add arithmetic-specific, runtime, proof-macros. (#4992)
X-Git-Tag: cvc5-1.0.0~2928
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=58f059a967ccb968f127b2d56f69c20700a943fb;p=cvc5.git

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).
---

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