Head

GCC Code Coverage Report

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


/******************************************************************************
 * Top contributors (to current version):
 *   Mathias Preiner, Aina Niemetz
 *
 * 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.
 * ****************************************************************************
 *
 * Contains code for handling command-line options.
 *
 * For each <module>_options.toml configuration file, mkoptions.py
 * expands this template and generates a <module>_options.h file.
 */

#include "cvc5_private.h"

#ifndef CVC5__OPTIONS__THEORY_H
#define CVC5__OPTIONS__THEORY_H

#include "options/options.h"

// clang-format off

// clang-format on

namespace cvc5 {
namespace options {

// clang-format off

enum class EqEngineMode
{
  CENTRAL,
  DISTRIBUTED
};

static constexpr size_t EqEngineMode__numValues = 2;

std::ostream& operator<<(std::ostream& os, EqEngineMode mode);
EqEngineMode stringToEqEngineMode(const std::string& optarg);
enum class TcMode
{
  CARE_GRAPH
};

static constexpr size_t TcMode__numValues = 1;

std::ostream& operator<<(std::ostream& os, TcMode mode);
TcMode stringToTcMode(const std::string& optarg);
enum class TheoryOfMode
{
  THEORY_OF_TERM_BASED,
  THEORY_OF_TYPE_BASED
};

static constexpr size_t TheoryOfMode__numValues = 2;

std::ostream& operator<<(std::ostream& os, TheoryOfMode mode);
TheoryOfMode stringToTheoryOfMode(const std::string& optarg);
// clang-format on

#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)
#  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
#  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */

struct HolderTHEORY
{
// clang-format off
  bool assignFunctionValues = true;
  bool assignFunctionValuesWasSetByUser = false;
  bool condenseFunctionValues = true;
  bool condenseFunctionValuesWasSetByUser = false;
  EqEngineMode eeMode = EqEngineMode::DISTRIBUTED;
  bool eeModeWasSetByUser = false;
  bool relevanceFilter = false;
  bool relevanceFilterWasSetByUser = false;
  TcMode tcMode = TcMode::CARE_GRAPH;
  bool tcModeWasSetByUser = false;
  TheoryOfMode theoryOfMode = TheoryOfMode::THEORY_OF_TYPE_BASED;
  bool theoryOfModeWasSetByUser = false;
// clang-format on
};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off
extern struct assignFunctionValues__option_t
{
  typedef bool type;
  type operator()() const;
} thread_local assignFunctionValues;
extern struct condenseFunctionValues__option_t
{
  typedef bool type;
  type operator()() const;
} thread_local condenseFunctionValues;
extern struct eeMode__option_t
{
  typedef EqEngineMode type;
  type operator()() const;
} thread_local eeMode;
extern struct relevanceFilter__option_t
{
  typedef bool type;
  type operator()() const;
} thread_local relevanceFilter;
extern struct tcMode__option_t
{
  typedef TcMode type;
  type operator()() const;
} thread_local tcMode;
extern struct theoryOfMode__option_t
{
  typedef TheoryOfMode type;
  type operator()() const;
} thread_local theoryOfMode;
// clang-format on

namespace theory
{
// clang-format off
static constexpr const char* assignFunctionValues__name = "assign-function-values";
static constexpr const char* condenseFunctionValues__name = "condense-function-values";
static constexpr const char* eeMode__name = "ee-mode";
static constexpr const char* relevanceFilter__name = "relevance-filter";
static constexpr const char* tcMode__name = "tc-mode";
static constexpr const char* theoryOfMode__name = "theoryof-mode";
// clang-format on
}

}  // namespace options

// clang-format off

// clang-format on

namespace options {
// clang-format off
inline bool assignFunctionValues__option_t::operator()() const
{ return Options::current().theory.assignFunctionValues; }
inline bool condenseFunctionValues__option_t::operator()() const
{ return Options::current().theory.condenseFunctionValues; }
inline EqEngineMode eeMode__option_t::operator()() const
{ return Options::current().theory.eeMode; }
inline bool relevanceFilter__option_t::operator()() const
{ return Options::current().theory.relevanceFilter; }
inline TcMode tcMode__option_t::operator()() const
{ return Options::current().theory.tcMode; }
inline TheoryOfMode theoryOfMode__option_t::operator()() const
{ return Options::current().theory.theoryOfMode; }
// clang-format on

namespace theory
{
// clang-format off
void setDefaultAssignFunctionValues(Options& opts, bool value);
void setDefaultCondenseFunctionValues(Options& opts, bool value);
void setDefaultEeMode(Options& opts, EqEngineMode value);
void setDefaultRelevanceFilter(Options& opts, bool value);
void setDefaultTcMode(Options& opts, TcMode value);
void setDefaultTheoryOfMode(Options& opts, TheoryOfMode value);
// clang-format on
}

}  // namespace options
}  // namespace cvc5

#endif /* CVC5__OPTIONS__THEORY_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Mathias Preiner, Aina Niemetz
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		* Contains code for handling command-line options.
14		*
15		* For each <module>_options.toml configuration file, mkoptions.py
16		* expands this template and generates a <module>_options.h file.
17		*/
18
19		#include "cvc5_private.h"
20
21		#ifndef CVC5__OPTIONS__THEORY_H
22		#define CVC5__OPTIONS__THEORY_H
23
24		#include "options/options.h"
25
26		// clang-format off
27
28		// clang-format on
29
30		namespace cvc5 {
31		namespace options {
32
33		// clang-format off
34
35		enum class EqEngineMode
36		{
37		CENTRAL,
38		DISTRIBUTED
39		};
40
41		static constexpr size_t EqEngineMode__numValues = 2;
42
43		std::ostream& operator<<(std::ostream& os, EqEngineMode mode);
44		EqEngineMode stringToEqEngineMode(const std::string& optarg);
45		enum class TcMode
46		{
47		CARE_GRAPH
48		};
49
50		static constexpr size_t TcMode__numValues = 1;
51
52		std::ostream& operator<<(std::ostream& os, TcMode mode);
53		TcMode stringToTcMode(const std::string& optarg);
54		enum class TheoryOfMode
55		{
56		THEORY_OF_TERM_BASED,
57		THEORY_OF_TYPE_BASED
58		};
59
60		static constexpr size_t TheoryOfMode__numValues = 2;
61
62		std::ostream& operator<<(std::ostream& os, TheoryOfMode mode);
63		TheoryOfMode stringToTheoryOfMode(const std::string& optarg);
64		// clang-format on
65
66		#if defined(CVC5_MUZZLED) \|\| defined(CVC5_COMPETITION_MODE)
67		# define DO_SEMANTIC_CHECKS_BY_DEFAULT false
68		#else /* CVC5_MUZZLED \|\| CVC5_COMPETITION_MODE */
69		# define DO_SEMANTIC_CHECKS_BY_DEFAULT true
70		#endif /* CVC5_MUZZLED \|\| CVC5_COMPETITION_MODE */
71
72	27397	struct HolderTHEORY
73		{
74		// clang-format off
75		bool assignFunctionValues = true;
76		bool assignFunctionValuesWasSetByUser = false;
77		bool condenseFunctionValues = true;
78		bool condenseFunctionValuesWasSetByUser = false;
79		EqEngineMode eeMode = EqEngineMode::DISTRIBUTED;
80		bool eeModeWasSetByUser = false;
81		bool relevanceFilter = false;
82		bool relevanceFilterWasSetByUser = false;
83		TcMode tcMode = TcMode::CARE_GRAPH;
84		bool tcModeWasSetByUser = false;
85		TheoryOfMode theoryOfMode = TheoryOfMode::THEORY_OF_TYPE_BASED;
86		bool theoryOfModeWasSetByUser = false;
87		// clang-format on
88		};
89
90		#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
91
92		// clang-format off
93		extern struct assignFunctionValues__option_t
94		{
95		typedef bool type;
96		type operator()() const;
97		} thread_local assignFunctionValues;
98		extern struct condenseFunctionValues__option_t
99		{
100		typedef bool type;
101		type operator()() const;
102		} thread_local condenseFunctionValues;
103		extern struct eeMode__option_t
104		{
105		typedef EqEngineMode type;
106		type operator()() const;
107		} thread_local eeMode;
108		extern struct relevanceFilter__option_t
109		{
110		typedef bool type;
111		type operator()() const;
112		} thread_local relevanceFilter;
113		extern struct tcMode__option_t
114		{
115		typedef TcMode type;
116		type operator()() const;
117		} thread_local tcMode;
118		extern struct theoryOfMode__option_t
119		{
120		typedef TheoryOfMode type;
121		type operator()() const;
122		} thread_local theoryOfMode;
123		// clang-format on
124
125		namespace theory
126		{
127		// clang-format off
128		static constexpr const char* assignFunctionValues__name = "assign-function-values";
129		static constexpr const char* condenseFunctionValues__name = "condense-function-values";
130		static constexpr const char* eeMode__name = "ee-mode";
131		static constexpr const char* relevanceFilter__name = "relevance-filter";
132		static constexpr const char* tcMode__name = "tc-mode";
133		static constexpr const char* theoryOfMode__name = "theoryof-mode";
134		// clang-format on
135		}
136
137		} // namespace options
138
139		// clang-format off
140
141		// clang-format on
142
143		namespace options {
144		// clang-format off
145	26543	inline bool assignFunctionValues__option_t::operator()() const
146	26543	{ return Options::current().theory.assignFunctionValues; }
147	4666	inline bool condenseFunctionValues__option_t::operator()() const
148	4666	{ return Options::current().theory.condenseFunctionValues; }
149	15838395	inline EqEngineMode eeMode__option_t::operator()() const
150	15838395	{ return Options::current().theory.eeMode; }
151	9866	inline bool relevanceFilter__option_t::operator()() const
152	9866	{ return Options::current().theory.relevanceFilter; }
153	9841	inline TcMode tcMode__option_t::operator()() const
154	9841	{ return Options::current().theory.tcMode; }
155	174419695	inline TheoryOfMode theoryOfMode__option_t::operator()() const
156	174419695	{ return Options::current().theory.theoryOfMode; }
157		// clang-format on
158
159		namespace theory
160		{
161		// clang-format off
162		void setDefaultAssignFunctionValues(Options& opts, bool value);
163		void setDefaultCondenseFunctionValues(Options& opts, bool value);
164		void setDefaultEeMode(Options& opts, EqEngineMode value);
165		void setDefaultRelevanceFilter(Options& opts, bool value);
166		void setDefaultTcMode(Options& opts, TcMode value);
167		void setDefaultTheoryOfMode(Options& opts, TheoryOfMode value);
168		// clang-format on
169		}
170
171		} // namespace options
172		} // namespace cvc5
173
174		#endif /* CVC5__OPTIONS__THEORY_H */