Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/decision_options.h	Lines:	7	9	77.8 %
Date:	2021-09-16	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__DECISION_H
#define CVC5__OPTIONS__DECISION_H

#include "options/options.h"

// clang-format off
#include "options/decision_weight.h"
// clang-format on

namespace cvc5::options {

// clang-format off
enum class DecisionMode
{
  JUSTIFICATION, STOPONLY_OLD, JUSTIFICATION_OLD, STOPONLY, INTERNAL
};
static constexpr size_t DecisionMode__numValues = 5;
std::ostream& operator<<(std::ostream& os, DecisionMode mode);
DecisionMode stringToDecisionMode(const std::string& optarg);

enum class DecisionWeightInternal
{
  OFF, USR1, SUM, MAX
};
static constexpr size_t DecisionWeightInternal__numValues = 4;
std::ostream& operator<<(std::ostream& os, DecisionWeightInternal mode);
DecisionWeightInternal stringToDecisionWeightInternal(const std::string& optarg);

enum class JutificationSkolemMode
{
  LAST, FIRST
};
static constexpr size_t JutificationSkolemMode__numValues = 2;
std::ostream& operator<<(std::ostream& os, JutificationSkolemMode mode);
JutificationSkolemMode stringToJutificationSkolemMode(const std::string& optarg);

enum class JutificationSkolemRlvMode
{
  ASSERT, ALWAYS
};
static constexpr size_t JutificationSkolemRlvMode__numValues = 2;
std::ostream& operator<<(std::ostream& os, JutificationSkolemRlvMode mode);
JutificationSkolemRlvMode stringToJutificationSkolemRlvMode(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 HolderDECISION
{
// clang-format off
DecisionMode decisionMode = DecisionMode::INTERNAL;
  bool decisionModeWasSetByUser = false;
  int64_t decisionRandomWeight = 0;
  bool decisionRandomWeightWasSetByUser = false;
  cvc5::decision::DecisionWeight decisionThreshold = 0;
  bool decisionThresholdWasSetByUser = false;
  bool decisionUseWeight = false;
  bool decisionUseWeightWasSetByUser = false;
  DecisionWeightInternal decisionWeightInternal = DecisionWeightInternal::OFF;
  bool decisionWeightInternalWasSetByUser = false;
  bool jhRlvOrder = false;
  bool jhRlvOrderWasSetByUser = false;
  JutificationSkolemMode jhSkolemMode = JutificationSkolemMode::FIRST;
  bool jhSkolemModeWasSetByUser = false;
  JutificationSkolemRlvMode jhSkolemRlvMode = JutificationSkolemRlvMode::ASSERT;
  bool jhSkolemRlvModeWasSetByUser = false;
// clang-format on
};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off
inline DecisionMode decisionMode() { return Options::current().decision.decisionMode; }
inline int64_t decisionRandomWeight() { return Options::current().decision.decisionRandomWeight; }
inline cvc5::decision::DecisionWeight decisionThreshold() { return Options::current().decision.decisionThreshold; }
inline bool decisionUseWeight() { return Options::current().decision.decisionUseWeight; }
inline DecisionWeightInternal decisionWeightInternal() { return Options::current().decision.decisionWeightInternal; }
inline bool jhRlvOrder() { return Options::current().decision.jhRlvOrder; }
inline JutificationSkolemMode jhSkolemMode() { return Options::current().decision.jhSkolemMode; }
inline JutificationSkolemRlvMode jhSkolemRlvMode() { return Options::current().decision.jhSkolemRlvMode; }
// clang-format on

namespace decision
{
// clang-format off
static constexpr const char* decisionMode__name = "decision";
static constexpr const char* decisionRandomWeight__name = "decision-random-weight";
static constexpr const char* decisionThreshold__name = "decision-threshold";
static constexpr const char* decisionUseWeight__name = "decision-use-weight";
static constexpr const char* decisionWeightInternal__name = "decision-weight-internal";
static constexpr const char* jhRlvOrder__name = "jh-rlv-order";
static constexpr const char* jhSkolemMode__name = "jh-skolem";
static constexpr const char* jhSkolemRlvMode__name = "jh-skolem-rlv";

void setDefaultDecisionMode(Options& opts, DecisionMode value);
void setDefaultDecisionRandomWeight(Options& opts, int64_t value);
void setDefaultDecisionThreshold(Options& opts, cvc5::decision::DecisionWeight value);
void setDefaultDecisionUseWeight(Options& opts, bool value);
void setDefaultDecisionWeightInternal(Options& opts, DecisionWeightInternal value);
void setDefaultJhRlvOrder(Options& opts, bool value);
void setDefaultJhSkolemMode(Options& opts, JutificationSkolemMode value);
void setDefaultJhSkolemRlvMode(Options& opts, JutificationSkolemRlvMode value);
// clang-format on
}

}  // namespace cvc5::options

#endif /* CVC5__OPTIONS__DECISION_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__DECISION_H
22		#define CVC5__OPTIONS__DECISION_H
23
24		#include "options/options.h"
25
26		// clang-format off
27		#include "options/decision_weight.h"
28		// clang-format on
29
30		namespace cvc5::options {
31
32		// clang-format off
33		enum class DecisionMode
34		{
35		JUSTIFICATION, STOPONLY_OLD, JUSTIFICATION_OLD, STOPONLY, INTERNAL
36		};
37		static constexpr size_t DecisionMode__numValues = 5;
38		std::ostream& operator<<(std::ostream& os, DecisionMode mode);
39		DecisionMode stringToDecisionMode(const std::string& optarg);
40
41		enum class DecisionWeightInternal
42		{
43		OFF, USR1, SUM, MAX
44		};
45		static constexpr size_t DecisionWeightInternal__numValues = 4;
46		std::ostream& operator<<(std::ostream& os, DecisionWeightInternal mode);
47		DecisionWeightInternal stringToDecisionWeightInternal(const std::string& optarg);
48
49		enum class JutificationSkolemMode
50		{
51		LAST, FIRST
52		};
53		static constexpr size_t JutificationSkolemMode__numValues = 2;
54		std::ostream& operator<<(std::ostream& os, JutificationSkolemMode mode);
55		JutificationSkolemMode stringToJutificationSkolemMode(const std::string& optarg);
56
57		enum class JutificationSkolemRlvMode
58		{
59		ASSERT, ALWAYS
60		};
61		static constexpr size_t JutificationSkolemRlvMode__numValues = 2;
62		std::ostream& operator<<(std::ostream& os, JutificationSkolemRlvMode mode);
63		JutificationSkolemRlvMode stringToJutificationSkolemRlvMode(const std::string& optarg);
64
65		// clang-format on
66
67		#if defined(CVC5_MUZZLED) \|\| defined(CVC5_COMPETITION_MODE)
68		# define DO_SEMANTIC_CHECKS_BY_DEFAULT false
69		#else /* CVC5_MUZZLED \|\| CVC5_COMPETITION_MODE */
70		# define DO_SEMANTIC_CHECKS_BY_DEFAULT true
71		#endif /* CVC5_MUZZLED \|\| CVC5_COMPETITION_MODE */
72
73	24139	struct HolderDECISION
74		{
75		// clang-format off
76		DecisionMode decisionMode = DecisionMode::INTERNAL;
77		bool decisionModeWasSetByUser = false;
78		int64_t decisionRandomWeight = 0;
79		bool decisionRandomWeightWasSetByUser = false;
80		cvc5::decision::DecisionWeight decisionThreshold = 0;
81		bool decisionThresholdWasSetByUser = false;
82		bool decisionUseWeight = false;
83		bool decisionUseWeightWasSetByUser = false;
84		DecisionWeightInternal decisionWeightInternal = DecisionWeightInternal::OFF;
85		bool decisionWeightInternalWasSetByUser = false;
86		bool jhRlvOrder = false;
87		bool jhRlvOrderWasSetByUser = false;
88		JutificationSkolemMode jhSkolemMode = JutificationSkolemMode::FIRST;
89		bool jhSkolemModeWasSetByUser = false;
90		JutificationSkolemRlvMode jhSkolemRlvMode = JutificationSkolemRlvMode::ASSERT;
91		bool jhSkolemRlvModeWasSetByUser = false;
92		// clang-format on
93		};
94
95		#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
96
97		// clang-format off
98	35510	inline DecisionMode decisionMode() { return Options::current().decision.decisionMode; }
99		inline int64_t decisionRandomWeight() { return Options::current().decision.decisionRandomWeight; }
100	10	inline cvc5::decision::DecisionWeight decisionThreshold() { return Options::current().decision.decisionThreshold; }
101	10	inline bool decisionUseWeight() { return Options::current().decision.decisionUseWeight; }
102		inline DecisionWeightInternal decisionWeightInternal() { return Options::current().decision.decisionWeightInternal; }
103	15506	inline bool jhRlvOrder() { return Options::current().decision.jhRlvOrder; }
104	7753	inline JutificationSkolemMode jhSkolemMode() { return Options::current().decision.jhSkolemMode; }
105	7753	inline JutificationSkolemRlvMode jhSkolemRlvMode() { return Options::current().decision.jhSkolemRlvMode; }
106		// clang-format on
107
108		namespace decision
109		{
110		// clang-format off
111		static constexpr const char* decisionMode__name = "decision";
112		static constexpr const char* decisionRandomWeight__name = "decision-random-weight";
113		static constexpr const char* decisionThreshold__name = "decision-threshold";
114		static constexpr const char* decisionUseWeight__name = "decision-use-weight";
115		static constexpr const char* decisionWeightInternal__name = "decision-weight-internal";
116		static constexpr const char* jhRlvOrder__name = "jh-rlv-order";
117		static constexpr const char* jhSkolemMode__name = "jh-skolem";
118		static constexpr const char* jhSkolemRlvMode__name = "jh-skolem-rlv";
119
120		void setDefaultDecisionMode(Options& opts, DecisionMode value);
121		void setDefaultDecisionRandomWeight(Options& opts, int64_t value);
122		void setDefaultDecisionThreshold(Options& opts, cvc5::decision::DecisionWeight value);
123		void setDefaultDecisionUseWeight(Options& opts, bool value);
124		void setDefaultDecisionWeightInternal(Options& opts, DecisionWeightInternal value);
125		void setDefaultJhRlvOrder(Options& opts, bool value);
126		void setDefaultJhSkolemMode(Options& opts, JutificationSkolemMode value);
127		void setDefaultJhSkolemRlvMode(Options& opts, JutificationSkolemRlvMode value);
128		// clang-format on
129		}
130
131		} // namespace cvc5::options
132
133		#endif /* CVC5__OPTIONS__DECISION_H */