Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/datatypes_options.cpp	Lines:	7	107	6.5 %
Date:	2021-08-06	Branches:	6	72	8.3 %


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

#include <iostream>

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

// clang-format off
namespace cvc5 {



namespace options {

thread_local struct cdtBisimilar__option_t cdtBisimilar;
thread_local struct dtBinarySplit__option_t dtBinarySplit;
thread_local struct dtBlastSplits__option_t dtBlastSplits;
thread_local struct dtCyclic__option_t dtCyclic;
thread_local struct dtForceAssignment__option_t dtForceAssignment;
thread_local struct dtInferAsLemmas__option_t dtInferAsLemmas;
thread_local struct dtNestedRec__option_t dtNestedRec;
thread_local struct dtPoliteOptimize__option_t dtPoliteOptimize;
thread_local struct dtRewriteErrorSel__option_t dtRewriteErrorSel;
thread_local struct dtSharedSelectors__option_t dtSharedSelectors;
thread_local struct sygusAbortSize__option_t sygusAbortSize;
thread_local struct sygusFairMax__option_t sygusFairMax;
thread_local struct sygusFair__option_t sygusFair;
thread_local struct sygusSymBreak__option_t sygusSymBreak;
thread_local struct sygusSymBreakAgg__option_t sygusSymBreakAgg;
thread_local struct sygusSymBreakDynamic__option_t sygusSymBreakDynamic;
thread_local struct sygusSymBreakLazy__option_t sygusSymBreakLazy;
thread_local struct sygusSymBreakPbe__option_t sygusSymBreakPbe;
thread_local struct sygusSymBreakRlv__option_t sygusSymBreakRlv;


std::ostream& operator<<(std::ostream& os, SygusFairMode mode)
{
  switch(mode) {
    case SygusFairMode::DT_SIZE:
      return os << "SygusFairMode::DT_SIZE";
    case SygusFairMode::NONE:
      return os << "SygusFairMode::NONE";
    case SygusFairMode::DT_HEIGHT_PRED:
      return os << "SygusFairMode::DT_HEIGHT_PRED";
    case SygusFairMode::DIRECT:
      return os << "SygusFairMode::DIRECT";
    case SygusFairMode::DT_SIZE_PRED:
      return os << "SygusFairMode::DT_SIZE_PRED";
    default:
      Unreachable();
  }
  return os;
}

SygusFairMode stringToSygusFairMode(const std::string& optarg)
{
  if (optarg == "dt-size")
  {
    return SygusFairMode::DT_SIZE;
  }
  else if (optarg == "none")
  {
    return SygusFairMode::NONE;
  }
  else if (optarg == "dt-height-bound")
  {
    return SygusFairMode::DT_HEIGHT_PRED;
  }
  else if (optarg == "direct")
  {
    return SygusFairMode::DIRECT;
  }
  else if (optarg == "dt-size-bound")
  {
    return SygusFairMode::DT_SIZE_PRED;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for enforcing fairness for counterexample guided quantifier instantion.\n"
         "Available modes for --sygus-fair are:\n"
         "+ dt-size (default)\n"
         "  Enforce fairness using size operator.\n"
         "+ none\n"
         "  Do not enforce fairness.\n"
         "+ dt-height-bound\n"
         "  Enforce fairness by height bound predicate.\n"
         "+ direct\n"
         "  Enforce fairness using direct conflict lemmas.\n"
         "+ dt-size-bound\n"
         "  Enforce fairness by size bound predicate.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --sygus-fair: `") +
                        optarg + "'.  Try --sygus-fair=help.");
}



namespace datatypes
{
// clang-format off
void setDefaultCdtBisimilar(Options& opts, bool value)
{
    if (!opts.datatypes.cdtBisimilarWasSetByUser) {
        opts.datatypes.cdtBisimilar = value;
    }
}
void setDefaultDtBinarySplit(Options& opts, bool value)
{
    if (!opts.datatypes.dtBinarySplitWasSetByUser) {
        opts.datatypes.dtBinarySplit = value;
    }
}
void setDefaultDtBlastSplits(Options& opts, bool value)
{
    if (!opts.datatypes.dtBlastSplitsWasSetByUser) {
        opts.datatypes.dtBlastSplits = value;
    }
}
void setDefaultDtCyclic(Options& opts, bool value)
{
    if (!opts.datatypes.dtCyclicWasSetByUser) {
        opts.datatypes.dtCyclic = value;
    }
}
void setDefaultDtForceAssignment(Options& opts, bool value)
{
    if (!opts.datatypes.dtForceAssignmentWasSetByUser) {
        opts.datatypes.dtForceAssignment = value;
    }
}
void setDefaultDtInferAsLemmas(Options& opts, bool value)
{
    if (!opts.datatypes.dtInferAsLemmasWasSetByUser) {
        opts.datatypes.dtInferAsLemmas = value;
    }
}
void setDefaultDtNestedRec(Options& opts, bool value)
{
    if (!opts.datatypes.dtNestedRecWasSetByUser) {
        opts.datatypes.dtNestedRec = value;
    }
}
void setDefaultDtPoliteOptimize(Options& opts, bool value)
{
    if (!opts.datatypes.dtPoliteOptimizeWasSetByUser) {
        opts.datatypes.dtPoliteOptimize = value;
    }
}
void setDefaultDtRewriteErrorSel(Options& opts, bool value)
{
    if (!opts.datatypes.dtRewriteErrorSelWasSetByUser) {
        opts.datatypes.dtRewriteErrorSel = value;
    }
}
void setDefaultDtSharedSelectors(Options& opts, bool value)
{
    if (!opts.datatypes.dtSharedSelectorsWasSetByUser) {
        opts.datatypes.dtSharedSelectors = value;
    }
}
void setDefaultSygusAbortSize(Options& opts, int64_t value)
{
    if (!opts.datatypes.sygusAbortSizeWasSetByUser) {
        opts.datatypes.sygusAbortSize = value;
    }
}
void setDefaultSygusFairMax(Options& opts, bool value)
{
    if (!opts.datatypes.sygusFairMaxWasSetByUser) {
        opts.datatypes.sygusFairMax = value;
    }
}
void setDefaultSygusFair(Options& opts, SygusFairMode value)
{
    if (!opts.datatypes.sygusFairWasSetByUser) {
        opts.datatypes.sygusFair = value;
    }
}
void setDefaultSygusSymBreak(Options& opts, bool value)
{
    if (!opts.datatypes.sygusSymBreakWasSetByUser) {
        opts.datatypes.sygusSymBreak = value;
    }
}
void setDefaultSygusSymBreakAgg(Options& opts, bool value)
{
    if (!opts.datatypes.sygusSymBreakAggWasSetByUser) {
        opts.datatypes.sygusSymBreakAgg = value;
    }
}
void setDefaultSygusSymBreakDynamic(Options& opts, bool value)
{
    if (!opts.datatypes.sygusSymBreakDynamicWasSetByUser) {
        opts.datatypes.sygusSymBreakDynamic = value;
    }
}
void setDefaultSygusSymBreakLazy(Options& opts, bool value)
{
    if (!opts.datatypes.sygusSymBreakLazyWasSetByUser) {
        opts.datatypes.sygusSymBreakLazy = value;
    }
}
void setDefaultSygusSymBreakPbe(Options& opts, bool value)
{
    if (!opts.datatypes.sygusSymBreakPbeWasSetByUser) {
        opts.datatypes.sygusSymBreakPbe = value;
    }
}
void setDefaultSygusSymBreakRlv(Options& opts, bool value)
{
    if (!opts.datatypes.sygusSymBreakRlvWasSetByUser) {
        opts.datatypes.sygusSymBreakRlv = 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/datatypes_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 cdtBisimilar__option_t cdtBisimilar;
33		thread_local struct dtBinarySplit__option_t dtBinarySplit;
34		thread_local struct dtBlastSplits__option_t dtBlastSplits;
35		thread_local struct dtCyclic__option_t dtCyclic;
36		thread_local struct dtForceAssignment__option_t dtForceAssignment;
37		thread_local struct dtInferAsLemmas__option_t dtInferAsLemmas;
38		thread_local struct dtNestedRec__option_t dtNestedRec;
39		thread_local struct dtPoliteOptimize__option_t dtPoliteOptimize;
40		thread_local struct dtRewriteErrorSel__option_t dtRewriteErrorSel;
41		thread_local struct dtSharedSelectors__option_t dtSharedSelectors;
42		thread_local struct sygusAbortSize__option_t sygusAbortSize;
43		thread_local struct sygusFairMax__option_t sygusFairMax;
44		thread_local struct sygusFair__option_t sygusFair;
45		thread_local struct sygusSymBreak__option_t sygusSymBreak;
46		thread_local struct sygusSymBreakAgg__option_t sygusSymBreakAgg;
47		thread_local struct sygusSymBreakDynamic__option_t sygusSymBreakDynamic;
48		thread_local struct sygusSymBreakLazy__option_t sygusSymBreakLazy;
49		thread_local struct sygusSymBreakPbe__option_t sygusSymBreakPbe;
50		thread_local struct sygusSymBreakRlv__option_t sygusSymBreakRlv;
51
52
53		std::ostream& operator<<(std::ostream& os, SygusFairMode mode)
54		{
55		switch(mode) {
56		case SygusFairMode::DT_SIZE:
57		return os << "SygusFairMode::DT_SIZE";
58		case SygusFairMode::NONE:
59		return os << "SygusFairMode::NONE";
60		case SygusFairMode::DT_HEIGHT_PRED:
61		return os << "SygusFairMode::DT_HEIGHT_PRED";
62		case SygusFairMode::DIRECT:
63		return os << "SygusFairMode::DIRECT";
64		case SygusFairMode::DT_SIZE_PRED:
65		return os << "SygusFairMode::DT_SIZE_PRED";
66		default:
67		Unreachable();
68		}
69		return os;
70		}
71
72	2	SygusFairMode stringToSygusFairMode(const std::string& optarg)
73		{
74	2	if (optarg == "dt-size")
75		{
76		return SygusFairMode::DT_SIZE;
77		}
78	2	else if (optarg == "none")
79		{
80		return SygusFairMode::NONE;
81		}
82	2	else if (optarg == "dt-height-bound")
83		{
84		return SygusFairMode::DT_HEIGHT_PRED;
85		}
86	2	else if (optarg == "direct")
87		{
88	2	return SygusFairMode::DIRECT;
89		}
90		else if (optarg == "dt-size-bound")
91		{
92		return SygusFairMode::DT_SIZE_PRED;
93		}
94		else if (optarg == "help")
95		{
96		std::cerr << "Modes for enforcing fairness for counterexample guided quantifier instantion.\n"
97		"Available modes for --sygus-fair are:\n"
98		"+ dt-size (default)\n"
99		" Enforce fairness using size operator.\n"
100		"+ none\n"
101		" Do not enforce fairness.\n"
102		"+ dt-height-bound\n"
103		" Enforce fairness by height bound predicate.\n"
104		"+ direct\n"
105		" Enforce fairness using direct conflict lemmas.\n"
106		"+ dt-size-bound\n"
107		" Enforce fairness by size bound predicate.\n";
108		std::exit(1);
109		}
110		throw OptionException(std::string("unknown option for --sygus-fair: `") +
111		optarg + "'. Try --sygus-fair=help.");
112		}
113
114
115
116		namespace datatypes
117		{
118		// clang-format off
119		void setDefaultCdtBisimilar(Options& opts, bool value)
120		{
121		if (!opts.datatypes.cdtBisimilarWasSetByUser) {
122		opts.datatypes.cdtBisimilar = value;
123		}
124		}
125		void setDefaultDtBinarySplit(Options& opts, bool value)
126		{
127		if (!opts.datatypes.dtBinarySplitWasSetByUser) {
128		opts.datatypes.dtBinarySplit = value;
129		}
130		}
131		void setDefaultDtBlastSplits(Options& opts, bool value)
132		{
133		if (!opts.datatypes.dtBlastSplitsWasSetByUser) {
134		opts.datatypes.dtBlastSplits = value;
135		}
136		}
137		void setDefaultDtCyclic(Options& opts, bool value)
138		{
139		if (!opts.datatypes.dtCyclicWasSetByUser) {
140		opts.datatypes.dtCyclic = value;
141		}
142		}
143		void setDefaultDtForceAssignment(Options& opts, bool value)
144		{
145		if (!opts.datatypes.dtForceAssignmentWasSetByUser) {
146		opts.datatypes.dtForceAssignment = value;
147		}
148		}
149		void setDefaultDtInferAsLemmas(Options& opts, bool value)
150		{
151		if (!opts.datatypes.dtInferAsLemmasWasSetByUser) {
152		opts.datatypes.dtInferAsLemmas = value;
153		}
154		}
155		void setDefaultDtNestedRec(Options& opts, bool value)
156		{
157		if (!opts.datatypes.dtNestedRecWasSetByUser) {
158		opts.datatypes.dtNestedRec = value;
159		}
160		}
161		void setDefaultDtPoliteOptimize(Options& opts, bool value)
162		{
163		if (!opts.datatypes.dtPoliteOptimizeWasSetByUser) {
164		opts.datatypes.dtPoliteOptimize = value;
165		}
166		}
167		void setDefaultDtRewriteErrorSel(Options& opts, bool value)
168		{
169		if (!opts.datatypes.dtRewriteErrorSelWasSetByUser) {
170		opts.datatypes.dtRewriteErrorSel = value;
171		}
172		}
173		void setDefaultDtSharedSelectors(Options& opts, bool value)
174		{
175		if (!opts.datatypes.dtSharedSelectorsWasSetByUser) {
176		opts.datatypes.dtSharedSelectors = value;
177		}
178		}
179		void setDefaultSygusAbortSize(Options& opts, int64_t value)
180		{
181		if (!opts.datatypes.sygusAbortSizeWasSetByUser) {
182		opts.datatypes.sygusAbortSize = value;
183		}
184		}
185		void setDefaultSygusFairMax(Options& opts, bool value)
186		{
187		if (!opts.datatypes.sygusFairMaxWasSetByUser) {
188		opts.datatypes.sygusFairMax = value;
189		}
190		}
191		void setDefaultSygusFair(Options& opts, SygusFairMode value)
192		{
193		if (!opts.datatypes.sygusFairWasSetByUser) {
194		opts.datatypes.sygusFair = value;
195		}
196		}
197		void setDefaultSygusSymBreak(Options& opts, bool value)
198		{
199		if (!opts.datatypes.sygusSymBreakWasSetByUser) {
200		opts.datatypes.sygusSymBreak = value;
201		}
202		}
203		void setDefaultSygusSymBreakAgg(Options& opts, bool value)
204		{
205		if (!opts.datatypes.sygusSymBreakAggWasSetByUser) {
206		opts.datatypes.sygusSymBreakAgg = value;
207		}
208		}
209		void setDefaultSygusSymBreakDynamic(Options& opts, bool value)
210		{
211		if (!opts.datatypes.sygusSymBreakDynamicWasSetByUser) {
212		opts.datatypes.sygusSymBreakDynamic = value;
213		}
214		}
215		void setDefaultSygusSymBreakLazy(Options& opts, bool value)
216		{
217		if (!opts.datatypes.sygusSymBreakLazyWasSetByUser) {
218		opts.datatypes.sygusSymBreakLazy = value;
219		}
220		}
221		void setDefaultSygusSymBreakPbe(Options& opts, bool value)
222		{
223		if (!opts.datatypes.sygusSymBreakPbeWasSetByUser) {
224		opts.datatypes.sygusSymBreakPbe = value;
225		}
226		}
227		void setDefaultSygusSymBreakRlv(Options& opts, bool value)
228		{
229		if (!opts.datatypes.sygusSymBreakRlvWasSetByUser) {
230		opts.datatypes.sygusSymBreakRlv = value;
231		}
232		}
233		// clang-format on
234		}
235
236		} // namespace options
237	29322	} // namespace cvc5
238		// clang-format on