Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/decision_options.cpp	Lines:	8	125	6.4 %
Date:	2021-08-15	Branches:	7	119	5.9 %


/******************************************************************************
 * 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::options {

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