Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/options.h	Lines:	13	13	100.0 %
Date:	2021-08-14	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Morgan Deters, Paul Meng
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * Global (command-line, set-option, ...) parameters for SMT.
 */

#include "cvc5_public.h"

#ifndef CVC5__OPTIONS__OPTIONS_H
#define CVC5__OPTIONS__OPTIONS_H

#include <iosfwd>
#include <memory>
#include <string>
#include <vector>

#include "cvc5_export.h"

namespace cvc5 {
namespace options {
  class OptionsHandler;
// clang-format off
  struct HolderARITH;
  struct HolderARRAYS;
  struct HolderBASE;
  struct HolderBOOLEANS;
  struct HolderBUILTIN;
  struct HolderBV;
  struct HolderDATATYPES;
  struct HolderDECISION;
  struct HolderEXPR;
  struct HolderFP;
  struct HolderDRIVER;
  struct HolderPARSER;
  struct HolderPRINTER;
  struct HolderPROOF;
  struct HolderPROP;
  struct HolderQUANTIFIERS;
  struct HolderSEP;
  struct HolderSETS;
  struct HolderSMT;
  struct HolderSTRINGS;
  struct HolderTHEORY;
  struct HolderUF;
// clang-format on
}  // namespace options

class OptionsListener;

class CVC5_EXPORT Options
{
  public:
  /**
   * Options cannot be copied as they are given an explicit list of
   * Listeners to respond to.
   */
  Options(const Options& options) = delete;

  /**
   * Options cannot be assigned as they are given an explicit list of
   * Listeners to respond to.
   */
  Options& operator=(const Options& options) = delete;

  class OptionsScope
  {
   private:
     Options* d_oldOptions;
   public:
     OptionsScope(Options* newOptions) :
         d_oldOptions(Options::s_current)
     {
       Options::s_current = newOptions;
     }
     ~OptionsScope(){
       Options::s_current = d_oldOptions;
     }
  };
  friend class OptionsScope;

  /** Return true if current Options are null */
  static inline bool isCurrentNull() {
    return s_current == nullptr;
  }

  /** Get the current Options in effect */
  static inline Options& current() {
    return *s_current;
  }

  Options();
  ~Options();

  options::OptionsHandler& handler() const {
    return *d_handler;
  }

  /**
   * Copies the value of the options stored in OptionsHolder into the current
   * Options object.
   */
  void copyValues(const Options& options);

 private:

// clang-format off
    std::unique_ptr<options::HolderARITH> d_arith;
    std::unique_ptr<options::HolderARRAYS> d_arrays;
    std::unique_ptr<options::HolderBASE> d_base;
    std::unique_ptr<options::HolderBOOLEANS> d_booleans;
    std::unique_ptr<options::HolderBUILTIN> d_builtin;
    std::unique_ptr<options::HolderBV> d_bv;
    std::unique_ptr<options::HolderDATATYPES> d_datatypes;
    std::unique_ptr<options::HolderDECISION> d_decision;
    std::unique_ptr<options::HolderEXPR> d_expr;
    std::unique_ptr<options::HolderFP> d_fp;
    std::unique_ptr<options::HolderDRIVER> d_driver;
    std::unique_ptr<options::HolderPARSER> d_parser;
    std::unique_ptr<options::HolderPRINTER> d_printer;
    std::unique_ptr<options::HolderPROOF> d_proof;
    std::unique_ptr<options::HolderPROP> d_prop;
    std::unique_ptr<options::HolderQUANTIFIERS> d_quantifiers;
    std::unique_ptr<options::HolderSEP> d_sep;
    std::unique_ptr<options::HolderSETS> d_sets;
    std::unique_ptr<options::HolderSMT> d_smt;
    std::unique_ptr<options::HolderSTRINGS> d_strings;
    std::unique_ptr<options::HolderTHEORY> d_theory;
    std::unique_ptr<options::HolderUF> d_uf;
// clang-format on
 public:
// clang-format off
  options::HolderARITH& arith;
  options::HolderARRAYS& arrays;
  options::HolderBASE& base;
  options::HolderBOOLEANS& booleans;
  options::HolderBUILTIN& builtin;
  options::HolderBV& bv;
  options::HolderDATATYPES& datatypes;
  options::HolderDECISION& decision;
  options::HolderEXPR& expr;
  options::HolderFP& fp;
  options::HolderDRIVER& driver;
  options::HolderPARSER& parser;
  options::HolderPRINTER& printer;
  options::HolderPROOF& proof;
  options::HolderPROP& prop;
  options::HolderQUANTIFIERS& quantifiers;
  options::HolderSEP& sep;
  options::HolderSETS& sets;
  options::HolderSMT& smt;
  options::HolderSTRINGS& strings;
  options::HolderTHEORY& theory;
  options::HolderUF& uf;
// clang-format on

 private:
  /** The handler for the options of the theory. */
  std::unique_ptr<options::OptionsHandler> d_handler;

  /** The current Options in effect */
  static thread_local Options* s_current;


}; /* class Options */

}  // namespace cvc5

#endif /* CVC5__OPTIONS__OPTIONS_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Morgan Deters, Paul Meng
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Global (command-line, set-option, ...) parameters for SMT.
14		*/
15
16		#include "cvc5_public.h"
17
18		#ifndef CVC5__OPTIONS__OPTIONS_H
19		#define CVC5__OPTIONS__OPTIONS_H
20
21		#include <iosfwd>
22		#include <memory>
23		#include <string>
24		#include <vector>
25
26		#include "cvc5_export.h"
27
28		namespace cvc5 {
29		namespace options {
30		class OptionsHandler;
31		// clang-format off
32		struct HolderARITH;
33		struct HolderARRAYS;
34		struct HolderBASE;
35		struct HolderBOOLEANS;
36		struct HolderBUILTIN;
37		struct HolderBV;
38		struct HolderDATATYPES;
39		struct HolderDECISION;
40		struct HolderEXPR;
41		struct HolderFP;
42		struct HolderDRIVER;
43		struct HolderPARSER;
44		struct HolderPRINTER;
45		struct HolderPROOF;
46		struct HolderPROP;
47		struct HolderQUANTIFIERS;
48		struct HolderSEP;
49		struct HolderSETS;
50		struct HolderSMT;
51		struct HolderSTRINGS;
52		struct HolderTHEORY;
53		struct HolderUF;
54		// clang-format on
55		} // namespace options
56
57		class OptionsListener;
58
59		class CVC5_EXPORT Options
60		{
61		public:
62		/**
63		* Options cannot be copied as they are given an explicit list of
64		* Listeners to respond to.
65		*/
66		Options(const Options& options) = delete;
67
68		/**
69		* Options cannot be assigned as they are given an explicit list of
70		* Listeners to respond to.
71		*/
72		Options& operator=(const Options& options) = delete;
73
74		class OptionsScope
75		{
76		private:
77		Options* d_oldOptions;
78		public:
79	159103	OptionsScope(Options* newOptions) :
80	349124075	d_oldOptions(Options::s_current)
81		{
82	159103	Options::s_current = newOptions;
83	159103	}
84	318206	~OptionsScope(){
85	159103	Options::s_current = d_oldOptions;
86	159103	}
87		};
88		friend class OptionsScope;
89
90		/** Return true if current Options are null */
91	100325	static inline bool isCurrentNull() {
92	100325	return s_current == nullptr;
93		}
94
95		/** Get the current Options in effect */
96	348387338	static inline Options& current() {
97	348387338	return *s_current;
98		}
99
100		Options();
101		~Options();
102
103	3517	options::OptionsHandler& handler() const {
104	3517	return *d_handler;
105		}
106
107		/**
108		* Copies the value of the options stored in OptionsHolder into the current
109		* Options object.
110		*/
111		void copyValues(const Options& options);
112
113		private:
114
115		// clang-format off
116		std::unique_ptr<options::HolderARITH> d_arith;
117		std::unique_ptr<options::HolderARRAYS> d_arrays;
118		std::unique_ptr<options::HolderBASE> d_base;
119		std::unique_ptr<options::HolderBOOLEANS> d_booleans;
120		std::unique_ptr<options::HolderBUILTIN> d_builtin;
121		std::unique_ptr<options::HolderBV> d_bv;
122		std::unique_ptr<options::HolderDATATYPES> d_datatypes;
123		std::unique_ptr<options::HolderDECISION> d_decision;
124		std::unique_ptr<options::HolderEXPR> d_expr;
125		std::unique_ptr<options::HolderFP> d_fp;
126		std::unique_ptr<options::HolderDRIVER> d_driver;
127		std::unique_ptr<options::HolderPARSER> d_parser;
128		std::unique_ptr<options::HolderPRINTER> d_printer;
129		std::unique_ptr<options::HolderPROOF> d_proof;
130		std::unique_ptr<options::HolderPROP> d_prop;
131		std::unique_ptr<options::HolderQUANTIFIERS> d_quantifiers;
132		std::unique_ptr<options::HolderSEP> d_sep;
133		std::unique_ptr<options::HolderSETS> d_sets;
134		std::unique_ptr<options::HolderSMT> d_smt;
135		std::unique_ptr<options::HolderSTRINGS> d_strings;
136		std::unique_ptr<options::HolderTHEORY> d_theory;
137		std::unique_ptr<options::HolderUF> d_uf;
138		// clang-format on
139		public:
140		// clang-format off
141		options::HolderARITH& arith;
142		options::HolderARRAYS& arrays;
143		options::HolderBASE& base;
144		options::HolderBOOLEANS& booleans;
145		options::HolderBUILTIN& builtin;
146		options::HolderBV& bv;
147		options::HolderDATATYPES& datatypes;
148		options::HolderDECISION& decision;
149		options::HolderEXPR& expr;
150		options::HolderFP& fp;
151		options::HolderDRIVER& driver;
152		options::HolderPARSER& parser;
153		options::HolderPRINTER& printer;
154		options::HolderPROOF& proof;
155		options::HolderPROP& prop;
156		options::HolderQUANTIFIERS& quantifiers;
157		options::HolderSEP& sep;
158		options::HolderSETS& sets;
159		options::HolderSMT& smt;
160		options::HolderSTRINGS& strings;
161		options::HolderTHEORY& theory;
162		options::HolderUF& uf;
163		// clang-format on
164
165		private:
166		/** The handler for the options of the theory. */
167		std::unique_ptr<options::OptionsHandler> d_handler;
168
169		/** The current Options in effect */
170		static thread_local Options* s_current;
171
172
173		}; /* class Options */
174
175		} // namespace cvc5
176
177		#endif /* CVC5__OPTIONS__OPTIONS_H */