Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/decision_options.h	Lines:	5	9	55.6 %
Date:	2021-08-17	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 DecisionWeightInternal
{
  SUM,
  MAX,
  USR1,
  OFF
};

static constexpr size_t DecisionWeightInternal__numValues = 4;

std::ostream& operator<<(std::ostream& os, DecisionWeightInternal mode);
DecisionWeightInternal stringToDecisionWeightInternal(const std::string& optarg);

enum class DecisionMode
{
  INTERNAL,
  STOPONLY,
  JUSTIFICATION_OLD,
  JUSTIFICATION,
  STOPONLY_OLD
};

static constexpr size_t DecisionMode__numValues = 5;

std::ostream& operator<<(std::ostream& os, DecisionMode mode);
DecisionMode stringToDecisionMode(const std::string& optarg);

enum class JutificationSkolemRlvMode
{
  ALWAYS,
  ASSERT
};

static constexpr size_t JutificationSkolemRlvMode__numValues = 2;

std::ostream& operator<<(std::ostream& os, JutificationSkolemRlvMode mode);
JutificationSkolemRlvMode stringToJutificationSkolemRlvMode(const std::string& optarg);

enum class JutificationSkolemMode
{
  FIRST,
  LAST
};

static constexpr size_t JutificationSkolemMode__numValues = 2;

std::ostream& operator<<(std::ostream& os, JutificationSkolemMode mode);
JutificationSkolemMode stringToJutificationSkolemMode(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
  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;
  DecisionMode decisionMode = DecisionMode::INTERNAL;
  bool decisionModeWasSetByUser = false;
  bool jhRlvOrder = false;
  bool jhRlvOrderWasSetByUser = false;
  JutificationSkolemRlvMode jhSkolemRlvMode = JutificationSkolemRlvMode::ASSERT;
  bool jhSkolemRlvModeWasSetByUser = false;
  JutificationSkolemMode jhSkolemMode = JutificationSkolemMode::FIRST;
  bool jhSkolemModeWasSetByUser = false;
// clang-format on
};

#undef DO_SEMANTIC_CHECKS_BY_DEFAULT

// clang-format off
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 DecisionMode decisionMode() { return Options::current().decision.decisionMode; }
inline bool jhRlvOrder() { return Options::current().decision.jhRlvOrder; }
inline JutificationSkolemRlvMode jhSkolemRlvMode() { return Options::current().decision.jhSkolemRlvMode; }
inline JutificationSkolemMode jhSkolemMode() { return Options::current().decision.jhSkolemMode; }
// clang-format on

namespace decision
{
// clang-format off
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* decisionMode__name = "decision";
static constexpr const char* jhRlvOrder__name = "jh-rlv-order";
static constexpr const char* jhSkolemRlvMode__name = "jh-skolem-rlv";
static constexpr const char* jhSkolemMode__name = "jh-skolem";

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