Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/decision_options.cpp	Lines:	10	125	8.0 %
Date:	2021-08-06	Branches:	9	119	7.6 %


/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * Option template for option modules.
 *
 * For each <module>_options.toml configuration file, mkoptions.py
 * expands this template and generates a <module>_options.cpp file.
 */
#include "options/decision_options.h"

#include <iostream>

#include "base/check.h"
#include "options/option_exception.h"

// clang-format off
namespace cvc5 {



namespace options {

thread_local struct decisionRandomWeight__option_t decisionRandomWeight;
thread_local struct decisionThreshold__option_t decisionThreshold;
thread_local struct decisionUseWeight__option_t decisionUseWeight;
thread_local struct decisionWeightInternal__option_t decisionWeightInternal;
thread_local struct decisionMode__option_t decisionMode;
thread_local struct jhRlvOrder__option_t jhRlvOrder;
thread_local struct jhSkolemRlvMode__option_t jhSkolemRlvMode;
thread_local struct jhSkolemMode__option_t jhSkolemMode;


std::ostream& operator<<(std::ostream& os, DecisionWeightInternal mode)
{
  switch(mode) {
    case DecisionWeightInternal::USR1:
      return os << "DecisionWeightInternal::USR1";
    case DecisionWeightInternal::MAX:
      return os << "DecisionWeightInternal::MAX";
    case DecisionWeightInternal::SUM:
      return os << "DecisionWeightInternal::SUM";
    case DecisionWeightInternal::OFF:
      return os << "DecisionWeightInternal::OFF";
    default:
      Unreachable();
  }
  return os;
}

DecisionWeightInternal stringToDecisionWeightInternal(const std::string& optarg)
{
  if (optarg == "usr1")
  {
    return DecisionWeightInternal::USR1;
  }
  else if (optarg == "max")
  {
    return DecisionWeightInternal::MAX;
  }
  else if (optarg == "sum")
  {
    return DecisionWeightInternal::SUM;
  }
  else if (optarg == "off")
  {
    return DecisionWeightInternal::OFF;
  }
  else if (optarg == "help")
  {
    std::cerr << "Decision weight internal mode.\n"
         "Available hows for --decision-weight-internal are:\n"
         "+ usr1\n"
         "+ max\n"
         "+ sum\n"
         "+ off (default)\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --decision-weight-internal: `") +
                        optarg + "'.  Try --decision-weight-internal=help.");
}

std::ostream& operator<<(std::ostream& os, DecisionMode mode)
{
  switch(mode) {
    case DecisionMode::INTERNAL:
      return os << "DecisionMode::INTERNAL";
    case DecisionMode::STOPONLY:
      return os << "DecisionMode::STOPONLY";
    case DecisionMode::STOPONLY_OLD:
      return os << "DecisionMode::STOPONLY_OLD";
    case DecisionMode::JUSTIFICATION_OLD:
      return os << "DecisionMode::JUSTIFICATION_OLD";
    case DecisionMode::JUSTIFICATION:
      return os << "DecisionMode::JUSTIFICATION";
    default:
      Unreachable();
  }
  return os;
}

DecisionMode stringToDecisionMode(const std::string& optarg)
{
  if (optarg == "internal")
  {
    return DecisionMode::INTERNAL;
  }
  else if (optarg == "stoponly")
  {
    return DecisionMode::STOPONLY;
  }
  else if (optarg == "stoponly-old")
  {
    return DecisionMode::STOPONLY_OLD;
  }
  else if (optarg == "justification-old")
  {
    return DecisionMode::JUSTIFICATION_OLD;
  }
  else if (optarg == "justification")
  {
    return DecisionMode::JUSTIFICATION;
  }
  else if (optarg == "help")
  {
    std::cerr << "Decision modes.\n"
         "Available modes for --decision are:\n"
         "+ internal (default)\n"
         "  Use the internal decision heuristics of the SAT solver.\n"
         "+ stoponly\n"
         "  Use the justification heuristic only to stop early, not for decisions.\n"
         "+ stoponly-old\n"
         "  Use the old implementation of justification heuristic only to stop early, not\n"
         "  for decisions.\n"
         "+ justification-old\n"
         "  Older implementation of an ATGP-inspired justification heuristic.\n"
         "+ justification\n"
         "  An ATGP-inspired justification heuristic.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --decision: `") +
                        optarg + "'.  Try --decision=help.");
}

std::ostream& operator<<(std::ostream& os, JutificationSkolemRlvMode mode)
{
  switch(mode) {
    case JutificationSkolemRlvMode::ALWAYS:
      return os << "JutificationSkolemRlvMode::ALWAYS";
    case JutificationSkolemRlvMode::ASSERT:
      return os << "JutificationSkolemRlvMode::ASSERT";
    default:
      Unreachable();
  }
  return os;
}

JutificationSkolemRlvMode stringToJutificationSkolemRlvMode(const std::string& optarg)
{
  if (optarg == "always")
  {
    return JutificationSkolemRlvMode::ALWAYS;
  }
  else if (optarg == "assert")
  {
    return JutificationSkolemRlvMode::ASSERT;
  }
  else if (optarg == "help")
  {
    std::cerr << "Policy for when to consider skolem definitions relevant in justification\n"
         "heuristic\n"
         "Available modes for --jh-skolem-rlv are:\n"
         "+ always\n"
         "  skolems are always relevant\n"
         "+ assert (default)\n"
         "  skolems are relevant when they occur in an asserted literal\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --jh-skolem-rlv: `") +
                        optarg + "'.  Try --jh-skolem-rlv=help.");
}

std::ostream& operator<<(std::ostream& os, JutificationSkolemMode mode)
{
  switch(mode) {
    case JutificationSkolemMode::LAST:
      return os << "JutificationSkolemMode::LAST";
    case JutificationSkolemMode::FIRST:
      return os << "JutificationSkolemMode::FIRST";
    default:
      Unreachable();
  }
  return os;
}

JutificationSkolemMode stringToJutificationSkolemMode(const std::string& optarg)
{
  if (optarg == "last")
  {
    return JutificationSkolemMode::LAST;
  }
  else if (optarg == "first")
  {
    return JutificationSkolemMode::FIRST;
  }
  else if (optarg == "help")
  {
    std::cerr << "Policy for when to satisfy skolem definitions in justification heuristic\n"
         "Available modes for --jh-skolem are:\n"
         "+ last\n"
         "  satisfy pending relevant skolem definitions after input assertions\n"
         "+ first (default)\n"
         "  satisfy pending relevant skolem definitions before input assertions\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --jh-skolem: `") +
                        optarg + "'.  Try --jh-skolem=help.");
}



namespace decision
{
// clang-format off
void setDefaultDecisionRandomWeight(Options& opts, int64_t value)
{
    if (!opts.decision.decisionRandomWeightWasSetByUser) {
        opts.decision.decisionRandomWeight = value;
    }
}
void setDefaultDecisionThreshold(Options& opts, cvc5::decision::DecisionWeight value)
{
    if (!opts.decision.decisionThresholdWasSetByUser) {
        opts.decision.decisionThreshold = value;
    }
}
void setDefaultDecisionUseWeight(Options& opts, bool value)
{
    if (!opts.decision.decisionUseWeightWasSetByUser) {
        opts.decision.decisionUseWeight = value;
    }
}
void setDefaultDecisionWeightInternal(Options& opts, DecisionWeightInternal value)
{
    if (!opts.decision.decisionWeightInternalWasSetByUser) {
        opts.decision.decisionWeightInternal = value;
    }
}
void setDefaultDecisionMode(Options& opts, DecisionMode value)
{
    if (!opts.decision.decisionModeWasSetByUser) {
        opts.decision.decisionMode = value;
    }
}
void setDefaultJhRlvOrder(Options& opts, bool value)
{
    if (!opts.decision.jhRlvOrderWasSetByUser) {
        opts.decision.jhRlvOrder = value;
    }
}
void setDefaultJhSkolemRlvMode(Options& opts, JutificationSkolemRlvMode value)
{
    if (!opts.decision.jhSkolemRlvModeWasSetByUser) {
        opts.decision.jhSkolemRlvMode = value;
    }
}
void setDefaultJhSkolemMode(Options& opts, JutificationSkolemMode value)
{
    if (!opts.decision.jhSkolemModeWasSetByUser) {
        opts.decision.jhSkolemMode = value;
    }
}
// clang-format on
}

}  // namespace options
}  // namespace cvc5
// clang-format on


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		* Option template for option modules.
14		*
15		* For each <module>_options.toml configuration file, mkoptions.py
16		* expands this template and generates a <module>_options.cpp file.
17		*/
18		#include "options/decision_options.h"
19
20		#include <iostream>
21
22		#include "base/check.h"
23		#include "options/option_exception.h"
24
25		// clang-format off
26		namespace cvc5 {
27
28
29
30		namespace options {
31
32		thread_local struct decisionRandomWeight__option_t decisionRandomWeight;
33		thread_local struct decisionThreshold__option_t decisionThreshold;
34		thread_local struct decisionUseWeight__option_t decisionUseWeight;
35		thread_local struct decisionWeightInternal__option_t decisionWeightInternal;
36		thread_local struct decisionMode__option_t decisionMode;
37		thread_local struct jhRlvOrder__option_t jhRlvOrder;
38		thread_local struct jhSkolemRlvMode__option_t jhSkolemRlvMode;
39		thread_local struct jhSkolemMode__option_t jhSkolemMode;
40
41
42		std::ostream& operator<<(std::ostream& os, DecisionWeightInternal mode)
43		{
44		switch(mode) {
45		case DecisionWeightInternal::USR1:
46		return os << "DecisionWeightInternal::USR1";
47		case DecisionWeightInternal::MAX:
48		return os << "DecisionWeightInternal::MAX";
49		case DecisionWeightInternal::SUM:
50		return os << "DecisionWeightInternal::SUM";
51		case DecisionWeightInternal::OFF:
52		return os << "DecisionWeightInternal::OFF";
53		default:
54		Unreachable();
55		}
56		return os;
57		}
58
59		DecisionWeightInternal stringToDecisionWeightInternal(const std::string& optarg)
60		{
61		if (optarg == "usr1")
62		{
63		return DecisionWeightInternal::USR1;
64		}
65		else if (optarg == "max")
66		{
67		return DecisionWeightInternal::MAX;
68		}
69		else if (optarg == "sum")
70		{
71		return DecisionWeightInternal::SUM;
72		}
73		else if (optarg == "off")
74		{
75		return DecisionWeightInternal::OFF;
76		}
77		else if (optarg == "help")
78		{
79		std::cerr << "Decision weight internal mode.\n"
80		"Available hows for --decision-weight-internal are:\n"
81		"+ usr1\n"
82		"+ max\n"
83		"+ sum\n"
84		"+ off (default)\n";
85		std::exit(1);
86		}
87		throw OptionException(std::string("unknown option for --decision-weight-internal: `") +
88		optarg + "'. Try --decision-weight-internal=help.");
89		}
90
91		std::ostream& operator<<(std::ostream& os, DecisionMode mode)
92		{
93		switch(mode) {
94		case DecisionMode::INTERNAL:
95		return os << "DecisionMode::INTERNAL";
96		case DecisionMode::STOPONLY:
97		return os << "DecisionMode::STOPONLY";
98		case DecisionMode::STOPONLY_OLD:
99		return os << "DecisionMode::STOPONLY_OLD";
100		case DecisionMode::JUSTIFICATION_OLD:
101		return os << "DecisionMode::JUSTIFICATION_OLD";
102		case DecisionMode::JUSTIFICATION:
103		return os << "DecisionMode::JUSTIFICATION";
104		default:
105		Unreachable();
106		}
107		return os;
108		}
109
110	94	DecisionMode stringToDecisionMode(const std::string& optarg)
111		{
112	94	if (optarg == "internal")
113		{
114	10	return DecisionMode::INTERNAL;
115		}
116	84	else if (optarg == "stoponly")
117		{
118		return DecisionMode::STOPONLY;
119		}
120	84	else if (optarg == "stoponly-old")
121		{
122		return DecisionMode::STOPONLY_OLD;
123		}
124	84	else if (optarg == "justification-old")
125		{
126	2	return DecisionMode::JUSTIFICATION_OLD;
127		}
128	82	else if (optarg == "justification")
129		{
130	82	return DecisionMode::JUSTIFICATION;
131		}
132		else if (optarg == "help")
133		{
134		std::cerr << "Decision modes.\n"
135		"Available modes for --decision are:\n"
136		"+ internal (default)\n"
137		" Use the internal decision heuristics of the SAT solver.\n"
138		"+ stoponly\n"
139		" Use the justification heuristic only to stop early, not for decisions.\n"
140		"+ stoponly-old\n"
141		" Use the old implementation of justification heuristic only to stop early, not\n"
142		" for decisions.\n"
143		"+ justification-old\n"
144		" Older implementation of an ATGP-inspired justification heuristic.\n"
145		"+ justification\n"
146		" An ATGP-inspired justification heuristic.\n";
147		std::exit(1);
148		}
149		throw OptionException(std::string("unknown option for --decision: `") +
150		optarg + "'. Try --decision=help.");
151		}
152
153		std::ostream& operator<<(std::ostream& os, JutificationSkolemRlvMode mode)
154		{
155		switch(mode) {
156		case JutificationSkolemRlvMode::ALWAYS:
157		return os << "JutificationSkolemRlvMode::ALWAYS";
158		case JutificationSkolemRlvMode::ASSERT:
159		return os << "JutificationSkolemRlvMode::ASSERT";
160		default:
161		Unreachable();
162		}
163		return os;
164		}
165
166		JutificationSkolemRlvMode stringToJutificationSkolemRlvMode(const std::string& optarg)
167		{
168		if (optarg == "always")
169		{
170		return JutificationSkolemRlvMode::ALWAYS;
171		}
172		else if (optarg == "assert")
173		{
174		return JutificationSkolemRlvMode::ASSERT;
175		}
176		else if (optarg == "help")
177		{
178		std::cerr << "Policy for when to consider skolem definitions relevant in justification\n"
179		"heuristic\n"
180		"Available modes for --jh-skolem-rlv are:\n"
181		"+ always\n"
182		" skolems are always relevant\n"
183		"+ assert (default)\n"
184		" skolems are relevant when they occur in an asserted literal\n";
185		std::exit(1);
186		}
187		throw OptionException(std::string("unknown option for --jh-skolem-rlv: `") +
188		optarg + "'. Try --jh-skolem-rlv=help.");
189		}
190
191		std::ostream& operator<<(std::ostream& os, JutificationSkolemMode mode)
192		{
193		switch(mode) {
194		case JutificationSkolemMode::LAST:
195		return os << "JutificationSkolemMode::LAST";
196		case JutificationSkolemMode::FIRST:
197		return os << "JutificationSkolemMode::FIRST";
198		default:
199		Unreachable();
200		}
201		return os;
202		}
203
204		JutificationSkolemMode stringToJutificationSkolemMode(const std::string& optarg)
205		{
206		if (optarg == "last")
207		{
208		return JutificationSkolemMode::LAST;
209		}
210		else if (optarg == "first")
211		{
212		return JutificationSkolemMode::FIRST;
213		}
214		else if (optarg == "help")
215		{
216		std::cerr << "Policy for when to satisfy skolem definitions in justification heuristic\n"
217		"Available modes for --jh-skolem are:\n"
218		"+ last\n"
219		" satisfy pending relevant skolem definitions after input assertions\n"
220		"+ first (default)\n"
221		" satisfy pending relevant skolem definitions before input assertions\n";
222		std::exit(1);
223		}
224		throw OptionException(std::string("unknown option for --jh-skolem: `") +
225		optarg + "'. Try --jh-skolem=help.");
226		}
227
228
229
230		namespace decision
231		{
232		// clang-format off
233		void setDefaultDecisionRandomWeight(Options& opts, int64_t value)
234		{
235		if (!opts.decision.decisionRandomWeightWasSetByUser) {
236		opts.decision.decisionRandomWeight = value;
237		}
238		}
239		void setDefaultDecisionThreshold(Options& opts, cvc5::decision::DecisionWeight value)
240		{
241		if (!opts.decision.decisionThresholdWasSetByUser) {
242		opts.decision.decisionThreshold = value;
243		}
244		}
245		void setDefaultDecisionUseWeight(Options& opts, bool value)
246		{
247		if (!opts.decision.decisionUseWeightWasSetByUser) {
248		opts.decision.decisionUseWeight = value;
249		}
250		}
251		void setDefaultDecisionWeightInternal(Options& opts, DecisionWeightInternal value)
252		{
253		if (!opts.decision.decisionWeightInternalWasSetByUser) {
254		opts.decision.decisionWeightInternal = value;
255		}
256		}
257		void setDefaultDecisionMode(Options& opts, DecisionMode value)
258		{
259		if (!opts.decision.decisionModeWasSetByUser) {
260		opts.decision.decisionMode = value;
261		}
262		}
263		void setDefaultJhRlvOrder(Options& opts, bool value)
264		{
265		if (!opts.decision.jhRlvOrderWasSetByUser) {
266		opts.decision.jhRlvOrder = value;
267		}
268		}
269		void setDefaultJhSkolemRlvMode(Options& opts, JutificationSkolemRlvMode value)
270		{
271		if (!opts.decision.jhSkolemRlvModeWasSetByUser) {
272		opts.decision.jhSkolemRlvMode = value;
273		}
274		}
275		void setDefaultJhSkolemMode(Options& opts, JutificationSkolemMode value)
276		{
277		if (!opts.decision.jhSkolemModeWasSetByUser) {
278		opts.decision.jhSkolemMode = value;
279		}
280		}
281		// clang-format on
282		}
283
284		} // namespace options
285	29322	} // namespace cvc5
286		// clang-format on