Head

GCC Code Coverage Report

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