Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/options.h	Lines:	13	13	100.0 %
Date:	2021-08-01	Branches:	0	2	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 "base/listener.h"
#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(OptionsListener* ol = nullptr);
  ~Options();

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

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

  /** Set the generic listener associated with this class to ol */
  void setListener(OptionsListener* ol);

  void notifyListener(const std::string& key);

 private:
  /** Pointer to the options listener, if one exists */
  OptionsListener* d_olisten = nullptr;

// 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 "base/listener.h"
27		#include "cvc5_export.h"
28
29		namespace cvc5 {
30		namespace options {
31		class OptionsHandler;
32		// clang-format off
33		struct HolderARITH;
34		struct HolderARRAYS;
35		struct HolderBASE;
36		struct HolderBOOLEANS;
37		struct HolderBUILTIN;
38		struct HolderBV;
39		struct HolderDATATYPES;
40		struct HolderDECISION;
41		struct HolderEXPR;
42		struct HolderFP;
43		struct HolderDRIVER;
44		struct HolderPARSER;
45		struct HolderPRINTER;
46		struct HolderPROOF;
47		struct HolderPROP;
48		struct HolderQUANTIFIERS;
49		struct HolderSEP;
50		struct HolderSETS;
51		struct HolderSMT;
52		struct HolderSTRINGS;
53		struct HolderTHEORY;
54		struct HolderUF;
55		// clang-format on
56		} // namespace options
57
58		class OptionsListener;
59
60		class CVC5_EXPORT Options
61		{
62		public:
63		/**
64		* Options cannot be copied as they are given an explicit list of
65		* Listeners to respond to.
66		*/
67		Options(const Options& options) = delete;
68
69		/**
70		* Options cannot be assigned as they are given an explicit list of
71		* Listeners to respond to.
72		*/
73		Options& operator=(const Options& options) = delete;
74
75		class OptionsScope
76		{
77		private:
78		Options* d_oldOptions;
79		public:
80	159579	OptionsScope(Options* newOptions) :
81	342730598	d_oldOptions(Options::s_current)
82		{
83	159579	Options::s_current = newOptions;
84	159579	}
85	319158	~OptionsScope(){
86	159579	Options::s_current = d_oldOptions;
87	159579	}
88		};
89		friend class OptionsScope;
90
91		/** Return true if current Options are null */
92	100032	static inline bool isCurrentNull() {
93	100032	return s_current == nullptr;
94		}
95
96		/** Get the current Options in effect */
97	341992250	static inline Options& current() {
98	341992250	return *s_current;
99		}
100
101		Options(OptionsListener* ol = nullptr);
102		~Options();
103
104	3456	options::OptionsHandler& handler() const {
105	3456	return *d_handler;
106		}
107
108		/**
109		* Copies the value of the options stored in OptionsHolder into the current
110		* Options object.
111		* This does not copy the listeners in the Options object.
112		*/
113		void copyValues(const Options& options);
114
115		/** Set the generic listener associated with this class to ol */
116		void setListener(OptionsListener* ol);
117
118		void notifyListener(const std::string& key);
119
120		private:
121		/** Pointer to the options listener, if one exists */
122		OptionsListener* d_olisten = nullptr;
123
124		// clang-format off
125		std::unique_ptr<options::HolderARITH> d_arith;
126		std::unique_ptr<options::HolderARRAYS> d_arrays;
127		std::unique_ptr<options::HolderBASE> d_base;
128		std::unique_ptr<options::HolderBOOLEANS> d_booleans;
129		std::unique_ptr<options::HolderBUILTIN> d_builtin;
130		std::unique_ptr<options::HolderBV> d_bv;
131		std::unique_ptr<options::HolderDATATYPES> d_datatypes;
132		std::unique_ptr<options::HolderDECISION> d_decision;
133		std::unique_ptr<options::HolderEXPR> d_expr;
134		std::unique_ptr<options::HolderFP> d_fp;
135		std::unique_ptr<options::HolderDRIVER> d_driver;
136		std::unique_ptr<options::HolderPARSER> d_parser;
137		std::unique_ptr<options::HolderPRINTER> d_printer;
138		std::unique_ptr<options::HolderPROOF> d_proof;
139		std::unique_ptr<options::HolderPROP> d_prop;
140		std::unique_ptr<options::HolderQUANTIFIERS> d_quantifiers;
141		std::unique_ptr<options::HolderSEP> d_sep;
142		std::unique_ptr<options::HolderSETS> d_sets;
143		std::unique_ptr<options::HolderSMT> d_smt;
144		std::unique_ptr<options::HolderSTRINGS> d_strings;
145		std::unique_ptr<options::HolderTHEORY> d_theory;
146		std::unique_ptr<options::HolderUF> d_uf;
147		// clang-format on
148		public:
149		// clang-format off
150		options::HolderARITH& arith;
151		options::HolderARRAYS& arrays;
152		options::HolderBASE& base;
153		options::HolderBOOLEANS& booleans;
154		options::HolderBUILTIN& builtin;
155		options::HolderBV& bv;
156		options::HolderDATATYPES& datatypes;
157		options::HolderDECISION& decision;
158		options::HolderEXPR& expr;
159		options::HolderFP& fp;
160		options::HolderDRIVER& driver;
161		options::HolderPARSER& parser;
162		options::HolderPRINTER& printer;
163		options::HolderPROOF& proof;
164		options::HolderPROP& prop;
165		options::HolderQUANTIFIERS& quantifiers;
166		options::HolderSEP& sep;
167		options::HolderSETS& sets;
168		options::HolderSMT& smt;
169		options::HolderSTRINGS& strings;
170		options::HolderTHEORY& theory;
171		options::HolderUF& uf;
172		// clang-format on
173
174		private:
175		/** The handler for the options of the theory. */
176		std::unique_ptr<options::OptionsHandler> d_handler;
177
178		/** The current Options in effect */
179		static thread_local Options* s_current;
180
181
182		}; /* class Options */
183
184		} // namespace cvc5
185
186		#endif /* CVC5__OPTIONS__OPTIONS_H */