diff options
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/Makefile.am | 1 | ||||
| -rw-r--r-- | src/proof/options | 11 | ||||
| -rw-r--r-- | src/proof/proof.h | 8 |
3 files changed, 16 insertions, 4 deletions
diff --git a/src/proof/Makefile.am b/src/proof/Makefile.am index d657dfa80..7588f0dc3 100644 --- a/src/proof/Makefile.am +++ b/src/proof/Makefile.am @@ -16,3 +16,4 @@ libproof_la_SOURCES = \ proof_manager.h \ proof_manager.cpp +EXTRA_DIST = diff --git a/src/proof/options b/src/proof/options new file mode 100644 index 000000000..f00c8fc75 --- /dev/null +++ b/src/proof/options @@ -0,0 +1,11 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module PROOF "proof/options.h" Proof + +option proof produce-proofs --proof bool + turn on proof generation + +endmodule diff --git a/src/proof/proof.h b/src/proof/proof.h index a3270c4c0..39cf2b5bf 100644 --- a/src/proof/proof.h +++ b/src/proof/proof.h @@ -19,12 +19,12 @@ #ifndef __CVC4__PROOF__PROOF_H #define __CVC4__PROOF__PROOF_H -#include "util/options.h" +#include "options/options.h" #ifdef CVC4_PROOF -# define PROOF(x) if(Options::current()->proof) { x; } -# define NULLPROOF(x) (Options::current()->proof)? x : NULL -# define PROOF_ON() Options::current()->proof +# define PROOF(x) if(options::proof()) { x; } +# define NULLPROOF(x) (options::proof())? x : NULL +# define PROOF_ON() options::proof() #else /* CVC4_PROOF */ # define PROOF(x) # define NULLPROOF(x) NULL |