Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/theory_options.cpp	Lines:	28	83	33.7 %
Date:	2021-05-22	Branches:	5	61	8.2 %


/******************************************************************************
 * 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/theory_options.h"

#include <iostream>

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

// clang-format off
namespace cvc5 {

template <> options::assignFunctionValues__option_t::type& Options::ref(
    options::assignFunctionValues__option_t)
{
    return theory().assignFunctionValues;
}
template <> const options::assignFunctionValues__option_t::type& Options::operator[](
    options::assignFunctionValues__option_t) const
{
  return theory().assignFunctionValues;
}
template <> bool Options::wasSetByUser(options::assignFunctionValues__option_t) const
{
  return theory().assignFunctionValues__setByUser__;
}
template <> options::condenseFunctionValues__option_t::type& Options::ref(
    options::condenseFunctionValues__option_t)
{
    return theory().condenseFunctionValues;
}
template <> const options::condenseFunctionValues__option_t::type& Options::operator[](
    options::condenseFunctionValues__option_t) const
{
  return theory().condenseFunctionValues;
}
template <> bool Options::wasSetByUser(options::condenseFunctionValues__option_t) const
{
  return theory().condenseFunctionValues__setByUser__;
}
template <> options::eeMode__option_t::type& Options::ref(
    options::eeMode__option_t)
{
    return theory().eeMode;
}
template <> const options::eeMode__option_t::type& Options::operator[](
    options::eeMode__option_t) const
{
  return theory().eeMode;
}
template <> bool Options::wasSetByUser(options::eeMode__option_t) const
{
  return theory().eeMode__setByUser__;
}
template <> options::relevanceFilter__option_t::type& Options::ref(
    options::relevanceFilter__option_t)
{
    return theory().relevanceFilter;
}
template <> const options::relevanceFilter__option_t::type& Options::operator[](
    options::relevanceFilter__option_t) const
{
  return theory().relevanceFilter;
}
template <> bool Options::wasSetByUser(options::relevanceFilter__option_t) const
{
  return theory().relevanceFilter__setByUser__;
}
template <> options::tcMode__option_t::type& Options::ref(
    options::tcMode__option_t)
{
    return theory().tcMode;
}
template <> const options::tcMode__option_t::type& Options::operator[](
    options::tcMode__option_t) const
{
  return theory().tcMode;
}
template <> bool Options::wasSetByUser(options::tcMode__option_t) const
{
  return theory().tcMode__setByUser__;
}
template <> options::theoryOfMode__option_t::type& Options::ref(
    options::theoryOfMode__option_t)
{
    return theory().theoryOfMode;
}
template <> const options::theoryOfMode__option_t::type& Options::operator[](
    options::theoryOfMode__option_t) const
{
  return theory().theoryOfMode;
}
template <> bool Options::wasSetByUser(options::theoryOfMode__option_t) const
{
  return theory().theoryOfMode__setByUser__;
}

namespace options {

thread_local struct assignFunctionValues__option_t assignFunctionValues;
thread_local struct condenseFunctionValues__option_t condenseFunctionValues;
thread_local struct eeMode__option_t eeMode;
thread_local struct relevanceFilter__option_t relevanceFilter;
thread_local struct tcMode__option_t tcMode;
thread_local struct theoryOfMode__option_t theoryOfMode;


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

EqEngineMode stringToEqEngineMode(const std::string& optarg)
{
  if (optarg == "distributed")
  {
    return EqEngineMode::DISTRIBUTED;
  }
  else if (optarg == "help")
  {
    std::cerr << "Defines mode for managing equalities across theory solvers.\n"
         "Available modes for --ee-mode are:\n"
         "+ distributed (default)\n"
         "  Each theory maintains its own equality engine.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --ee-mode: `") +
                        optarg + "'.  Try --ee-mode=help.");
}

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

TcMode stringToTcMode(const std::string& optarg)
{
  if (optarg == "care-graph")
  {
    return TcMode::CARE_GRAPH;
  }
  else if (optarg == "help")
  {
    std::cerr << "Defines mode for theory combination.\n"
         "Available modes for --tc-mode are:\n"
         "+ care-graph (default)\n"
         "  Use care graphs for theory combination.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --tc-mode: `") +
                        optarg + "'.  Try --tc-mode=help.");
}

std::ostream& operator<<(std::ostream& os, TheoryOfMode mode)
{
  switch(mode) {
    case TheoryOfMode::THEORY_OF_TYPE_BASED:
      return os << "TheoryOfMode::THEORY_OF_TYPE_BASED";
    case TheoryOfMode::THEORY_OF_TERM_BASED:
      return os << "TheoryOfMode::THEORY_OF_TERM_BASED";
    default:
      Unreachable();
  }
  return os;
}

TheoryOfMode stringToTheoryOfMode(const std::string& optarg)
{
  if (optarg == "type")
  {
    return TheoryOfMode::THEORY_OF_TYPE_BASED;
  }
  else if (optarg == "term")
  {
    return TheoryOfMode::THEORY_OF_TERM_BASED;
  }
  else if (optarg == "help")
  {
    std::cerr << "Defines how we associate theories with terms.\n"
         "Available modes for --theoryof-mode are:\n"
         "+ type (default)\n"
         "  Type variables, constants and equalities by type.\n"
         "+ term\n"
         "  Type variables as uninterpreted, type constants by theory, equalities by the\n"
         "  parametric theory.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --theoryof-mode: `") +
                        optarg + "'.  Try --theoryof-mode=help.");
}


}  // 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/theory_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	2	template <> options::assignFunctionValues__option_t::type& Options::ref(
29		options::assignFunctionValues__option_t)
30		{
31	2	return theory().assignFunctionValues;
32		}
33	29116	template <> const options::assignFunctionValues__option_t::type& Options::operator[](
34		options::assignFunctionValues__option_t) const
35		{
36	29116	return theory().assignFunctionValues;
37		}
38		template <> bool Options::wasSetByUser(options::assignFunctionValues__option_t) const
39		{
40		return theory().assignFunctionValues__setByUser__;
41		}
42		template <> options::condenseFunctionValues__option_t::type& Options::ref(
43		options::condenseFunctionValues__option_t)
44		{
45		return theory().condenseFunctionValues;
46		}
47	230522	template <> const options::condenseFunctionValues__option_t::type& Options::operator[](
48		options::condenseFunctionValues__option_t) const
49		{
50	230522	return theory().condenseFunctionValues;
51		}
52		template <> bool Options::wasSetByUser(options::condenseFunctionValues__option_t) const
53		{
54		return theory().condenseFunctionValues__setByUser__;
55		}
56		template <> options::eeMode__option_t::type& Options::ref(
57		options::eeMode__option_t)
58		{
59		return theory().eeMode;
60		}
61	9460	template <> const options::eeMode__option_t::type& Options::operator[](
62		options::eeMode__option_t) const
63		{
64	9460	return theory().eeMode;
65		}
66		template <> bool Options::wasSetByUser(options::eeMode__option_t) const
67		{
68		return theory().eeMode__setByUser__;
69		}
70	22	template <> options::relevanceFilter__option_t::type& Options::ref(
71		options::relevanceFilter__option_t)
72		{
73	22	return theory().relevanceFilter;
74		}
75	9485	template <> const options::relevanceFilter__option_t::type& Options::operator[](
76		options::relevanceFilter__option_t) const
77		{
78	9485	return theory().relevanceFilter;
79		}
80	22	template <> bool Options::wasSetByUser(options::relevanceFilter__option_t) const
81		{
82	22	return theory().relevanceFilter__setByUser__;
83		}
84		template <> options::tcMode__option_t::type& Options::ref(
85		options::tcMode__option_t)
86		{
87		return theory().tcMode;
88		}
89	9460	template <> const options::tcMode__option_t::type& Options::operator[](
90		options::tcMode__option_t) const
91		{
92	9460	return theory().tcMode;
93		}
94		template <> bool Options::wasSetByUser(options::tcMode__option_t) const
95		{
96		return theory().tcMode__setByUser__;
97		}
98	1735	template <> options::theoryOfMode__option_t::type& Options::ref(
99		options::theoryOfMode__option_t)
100		{
101	1735	return theory().theoryOfMode;
102		}
103	160027308	template <> const options::theoryOfMode__option_t::type& Options::operator[](
104		options::theoryOfMode__option_t) const
105		{
106	160027308	return theory().theoryOfMode;
107		}
108	9460	template <> bool Options::wasSetByUser(options::theoryOfMode__option_t) const
109		{
110	9460	return theory().theoryOfMode__setByUser__;
111		}
112
113		namespace options {
114
115		thread_local struct assignFunctionValues__option_t assignFunctionValues;
116		thread_local struct condenseFunctionValues__option_t condenseFunctionValues;
117		thread_local struct eeMode__option_t eeMode;
118		thread_local struct relevanceFilter__option_t relevanceFilter;
119		thread_local struct tcMode__option_t tcMode;
120		thread_local struct theoryOfMode__option_t theoryOfMode;
121
122
123		std::ostream& operator<<(std::ostream& os, EqEngineMode mode)
124		{
125		switch(mode) {
126		case EqEngineMode::DISTRIBUTED:
127		return os << "EqEngineMode::DISTRIBUTED";
128		default:
129		Unreachable();
130		}
131		return os;
132		}
133
134		EqEngineMode stringToEqEngineMode(const std::string& optarg)
135		{
136		if (optarg == "distributed")
137		{
138		return EqEngineMode::DISTRIBUTED;
139		}
140		else if (optarg == "help")
141		{
142		std::cerr << "Defines mode for managing equalities across theory solvers.\n"
143		"Available modes for --ee-mode are:\n"
144		"+ distributed (default)\n"
145		" Each theory maintains its own equality engine.\n";
146		std::exit(1);
147		}
148		throw OptionException(std::string("unknown option for --ee-mode: `") +
149		optarg + "'. Try --ee-mode=help.");
150		}
151
152		std::ostream& operator<<(std::ostream& os, TcMode mode)
153		{
154		switch(mode) {
155		case TcMode::CARE_GRAPH:
156		return os << "TcMode::CARE_GRAPH";
157		default:
158		Unreachable();
159		}
160		return os;
161		}
162
163		TcMode stringToTcMode(const std::string& optarg)
164		{
165		if (optarg == "care-graph")
166		{
167		return TcMode::CARE_GRAPH;
168		}
169		else if (optarg == "help")
170		{
171		std::cerr << "Defines mode for theory combination.\n"
172		"Available modes for --tc-mode are:\n"
173		"+ care-graph (default)\n"
174		" Use care graphs for theory combination.\n";
175		std::exit(1);
176		}
177		throw OptionException(std::string("unknown option for --tc-mode: `") +
178		optarg + "'. Try --tc-mode=help.");
179		}
180
181		std::ostream& operator<<(std::ostream& os, TheoryOfMode mode)
182		{
183		switch(mode) {
184		case TheoryOfMode::THEORY_OF_TYPE_BASED:
185		return os << "TheoryOfMode::THEORY_OF_TYPE_BASED";
186		case TheoryOfMode::THEORY_OF_TERM_BASED:
187		return os << "TheoryOfMode::THEORY_OF_TERM_BASED";
188		default:
189		Unreachable();
190		}
191		return os;
192		}
193
194	5	TheoryOfMode stringToTheoryOfMode(const std::string& optarg)
195		{
196	5	if (optarg == "type")
197		{
198	3	return TheoryOfMode::THEORY_OF_TYPE_BASED;
199		}
200	2	else if (optarg == "term")
201		{
202	2	return TheoryOfMode::THEORY_OF_TERM_BASED;
203		}
204		else if (optarg == "help")
205		{
206		std::cerr << "Defines how we associate theories with terms.\n"
207		"Available modes for --theoryof-mode are:\n"
208		"+ type (default)\n"
209		" Type variables, constants and equalities by type.\n"
210		"+ term\n"
211		" Type variables as uninterpreted, type constants by theory, equalities by the\n"
212		" parametric theory.\n";
213		std::exit(1);
214		}
215		throw OptionException(std::string("unknown option for --theoryof-mode: `") +
216		optarg + "'. Try --theoryof-mode=help.");
217		}
218
219
220		} // namespace options
221	28194	} // namespace cvc5
222		// clang-format on