Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/bv_options.cpp	Lines:	30	185	16.2 %
Date:	2021-08-03	Branches:	26	148	17.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/bv_options.h"

#include <iostream>

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

// clang-format off
namespace cvc5 {



namespace options {

thread_local struct bitvectorAig__option_t bitvectorAig;
thread_local struct bitblastMode__option_t bitblastMode;
thread_local struct bitwiseEq__option_t bitwiseEq;
thread_local struct boolToBitvector__option_t boolToBitvector;
thread_local struct bvAbstraction__option_t bvAbstraction;
thread_local struct bitvectorAigSimplifications__option_t bitvectorAigSimplifications;
thread_local struct bvAlgExtf__option_t bvAlgExtf;
thread_local struct bitvectorAlgebraicBudget__option_t bitvectorAlgebraicBudget;
thread_local struct bitvectorAlgebraicSolver__option_t bitvectorAlgebraicSolver;
thread_local struct bvAssertInput__option_t bvAssertInput;
thread_local struct bvEagerExplanations__option_t bvEagerExplanations;
thread_local struct bitvectorEqualitySolver__option_t bitvectorEqualitySolver;
thread_local struct bvExtractArithRewrite__option_t bvExtractArithRewrite;
thread_local struct bvGaussElim__option_t bvGaussElim;
thread_local struct bitvectorInequalitySolver__option_t bitvectorInequalitySolver;
thread_local struct bvIntroducePow2__option_t bvIntroducePow2;
thread_local struct bvNumFunc__option_t bvNumFunc;
thread_local struct bvPrintConstsAsIndexedSymbols__option_t bvPrintConstsAsIndexedSymbols;
thread_local struct bitvectorPropagate__option_t bitvectorPropagate;
thread_local struct bitvectorQuickXplain__option_t bitvectorQuickXplain;
thread_local struct bvSatSolver__option_t bvSatSolver;
thread_local struct skolemizeArguments__option_t skolemizeArguments;
thread_local struct bvSolver__option_t bvSolver;
thread_local struct bitvectorToBool__option_t bitvectorToBool;


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

BitblastMode stringToBitblastMode(const std::string& optarg)
{
  if (optarg == "lazy")
  {
    return BitblastMode::LAZY;
  }
  else if (optarg == "eager")
  {
    return BitblastMode::EAGER;
  }
  else if (optarg == "help")
  {
    std::cerr << "Bit-blasting modes.\n"
         "Available modes for --bitblast are:\n"
         "+ lazy (default)\n"
         "  Separate boolean structure and term reasoning between the core SAT solver and\n"
         "  the bit-vector SAT solver.\n"
         "+ eager\n"
         "  Bitblast eagerly to bit-vector SAT solver.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --bitblast: `") +
                        optarg + "'.  Try --bitblast=help.");
}

std::ostream& operator<<(std::ostream& os, BoolToBVMode mode)
{
  switch(mode) {
    case BoolToBVMode::OFF:
      return os << "BoolToBVMode::OFF";
    case BoolToBVMode::ALL:
      return os << "BoolToBVMode::ALL";
    case BoolToBVMode::ITE:
      return os << "BoolToBVMode::ITE";
    default:
      Unreachable();
  }
  return os;
}

BoolToBVMode stringToBoolToBVMode(const std::string& optarg)
{
  if (optarg == "off")
  {
    return BoolToBVMode::OFF;
  }
  else if (optarg == "all")
  {
    return BoolToBVMode::ALL;
  }
  else if (optarg == "ite")
  {
    return BoolToBVMode::ITE;
  }
  else if (optarg == "help")
  {
    std::cerr << "BoolToBV preprocessing pass modes.\n"
         "Available modes for --bool-to-bv are:\n"
         "+ off (default)\n"
         "  Don't push any booleans to width one bit-vectors.\n"
         "+ all\n"
         "  Force all booleans to be bit-vectors of width one except at the top level.\n"
         "  Most aggressive mode.\n"
         "+ ite\n"
         "  Try to turn ITEs into BITVECTOR_ITE when possible. It can fail per-formula if\n"
         "  not all sub-formulas can be turned to bit-vectors.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --bool-to-bv: `") +
                        optarg + "'.  Try --bool-to-bv=help.");
}

std::ostream& operator<<(std::ostream& os, SatSolverMode mode)
{
  switch(mode) {
    case SatSolverMode::CRYPTOMINISAT:
      return os << "SatSolverMode::CRYPTOMINISAT";
    case SatSolverMode::KISSAT:
      return os << "SatSolverMode::KISSAT";
    case SatSolverMode::CADICAL:
      return os << "SatSolverMode::CADICAL";
    case SatSolverMode::MINISAT:
      return os << "SatSolverMode::MINISAT";
    default:
      Unreachable();
  }
  return os;
}

SatSolverMode stringToSatSolverMode(const std::string& optarg)
{
  if (optarg == "cryptominisat")
  {
    return SatSolverMode::CRYPTOMINISAT;
  }
  else if (optarg == "kissat")
  {
    return SatSolverMode::KISSAT;
  }
  else if (optarg == "cadical")
  {
    return SatSolverMode::CADICAL;
  }
  else if (optarg == "minisat")
  {
    return SatSolverMode::MINISAT;
  }
  else if (optarg == "help")
  {
    std::cerr << "SAT solver for bit-blasting backend.\n"
         "Available modes for --bv-sat-solver are:\n"
         "+ cryptominisat\n"
         "+ kissat\n"
         "+ cadical\n"
         "+ minisat (default)\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --bv-sat-solver: `") +
                        optarg + "'.  Try --bv-sat-solver=help.");
}

std::ostream& operator<<(std::ostream& os, BVSolver mode)
{
  switch(mode) {
    case BVSolver::BITBLAST:
      return os << "BVSolver::BITBLAST";
    case BVSolver::LAYERED:
      return os << "BVSolver::LAYERED";
    case BVSolver::BITBLAST_INTERNAL:
      return os << "BVSolver::BITBLAST_INTERNAL";
    default:
      Unreachable();
  }
  return os;
}

BVSolver stringToBVSolver(const std::string& optarg)
{
  if (optarg == "bitblast")
  {
    return BVSolver::BITBLAST;
  }
  else if (optarg == "layered")
  {
    return BVSolver::LAYERED;
  }
  else if (optarg == "bitblast-internal")
  {
    return BVSolver::BITBLAST_INTERNAL;
  }
  else if (optarg == "help")
  {
    std::cerr << "Bit-vector solvers.\n"
         "Available modes for --bv-solver are:\n"
         "+ bitblast (default)\n"
         "  Enables bitblasting solver.\n"
         "+ layered\n"
         "  Enables the layered BV solver.\n"
         "+ bitblast-internal\n"
         "  Enables bitblasting to internal SAT solver with proof support.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --bv-solver: `") +
                        optarg + "'.  Try --bv-solver=help.");
}



namespace bv
{
// clang-format off
void setDefaultBitvectorAig(Options& opts, bool value)
{
    if (!opts.bv.bitvectorAigWasSetByUser) {
        opts.bv.bitvectorAig = value;
    }
}
void setDefaultBitblastMode(Options& opts, BitblastMode value)
{
    if (!opts.bv.bitblastModeWasSetByUser) {
        opts.bv.bitblastMode = value;
    }
}
void setDefaultBitwiseEq(Options& opts, bool value)
{
    if (!opts.bv.bitwiseEqWasSetByUser) {
        opts.bv.bitwiseEq = value;
    }
}
void setDefaultBoolToBitvector(Options& opts, BoolToBVMode value)
{
    if (!opts.bv.boolToBitvectorWasSetByUser) {
        opts.bv.boolToBitvector = value;
    }
}
void setDefaultBvAbstraction(Options& opts, bool value)
{
    if (!opts.bv.bvAbstractionWasSetByUser) {
        opts.bv.bvAbstraction = value;
    }
}
void setDefaultBitvectorAigSimplifications(Options& opts, std::string value)
{
    if (!opts.bv.bitvectorAigSimplificationsWasSetByUser) {
        opts.bv.bitvectorAigSimplifications = value;
    }
}
void setDefaultBvAlgExtf(Options& opts, bool value)
{
    if (!opts.bv.bvAlgExtfWasSetByUser) {
        opts.bv.bvAlgExtf = value;
    }
}
void setDefaultBitvectorAlgebraicBudget(Options& opts, unsigned value)
{
    if (!opts.bv.bitvectorAlgebraicBudgetWasSetByUser) {
        opts.bv.bitvectorAlgebraicBudget = value;
    }
}
void setDefaultBitvectorAlgebraicSolver(Options& opts, bool value)
{
    if (!opts.bv.bitvectorAlgebraicSolverWasSetByUser) {
        opts.bv.bitvectorAlgebraicSolver = value;
    }
}
void setDefaultBvAssertInput(Options& opts, bool value)
{
    if (!opts.bv.bvAssertInputWasSetByUser) {
        opts.bv.bvAssertInput = value;
    }
}
void setDefaultBvEagerExplanations(Options& opts, bool value)
{
    if (!opts.bv.bvEagerExplanationsWasSetByUser) {
        opts.bv.bvEagerExplanations = value;
    }
}
void setDefaultBitvectorEqualitySolver(Options& opts, bool value)
{
    if (!opts.bv.bitvectorEqualitySolverWasSetByUser) {
        opts.bv.bitvectorEqualitySolver = value;
    }
}
void setDefaultBvExtractArithRewrite(Options& opts, bool value)
{
    if (!opts.bv.bvExtractArithRewriteWasSetByUser) {
        opts.bv.bvExtractArithRewrite = value;
    }
}
void setDefaultBvGaussElim(Options& opts, bool value)
{
    if (!opts.bv.bvGaussElimWasSetByUser) {
        opts.bv.bvGaussElim = value;
    }
}
void setDefaultBitvectorInequalitySolver(Options& opts, bool value)
{
    if (!opts.bv.bitvectorInequalitySolverWasSetByUser) {
        opts.bv.bitvectorInequalitySolver = value;
    }
}
void setDefaultBvIntroducePow2(Options& opts, bool value)
{
    if (!opts.bv.bvIntroducePow2WasSetByUser) {
        opts.bv.bvIntroducePow2 = value;
    }
}
void setDefaultBvNumFunc(Options& opts, unsigned value)
{
    if (!opts.bv.bvNumFuncWasSetByUser) {
        opts.bv.bvNumFunc = value;
    }
}
void setDefaultBvPrintConstsAsIndexedSymbols(Options& opts, bool value)
{
    if (!opts.bv.bvPrintConstsAsIndexedSymbolsWasSetByUser) {
        opts.bv.bvPrintConstsAsIndexedSymbols = value;
    }
}
void setDefaultBitvectorPropagate(Options& opts, bool value)
{
    if (!opts.bv.bitvectorPropagateWasSetByUser) {
        opts.bv.bitvectorPropagate = value;
    }
}
void setDefaultBitvectorQuickXplain(Options& opts, bool value)
{
    if (!opts.bv.bitvectorQuickXplainWasSetByUser) {
        opts.bv.bitvectorQuickXplain = value;
    }
}
void setDefaultBvSatSolver(Options& opts, SatSolverMode value)
{
    if (!opts.bv.bvSatSolverWasSetByUser) {
        opts.bv.bvSatSolver = value;
    }
}
void setDefaultSkolemizeArguments(Options& opts, bool value)
{
    if (!opts.bv.skolemizeArgumentsWasSetByUser) {
        opts.bv.skolemizeArguments = value;
    }
}
void setDefaultBvSolver(Options& opts, BVSolver value)
{
    if (!opts.bv.bvSolverWasSetByUser) {
        opts.bv.bvSolver = value;
    }
}
void setDefaultBitvectorToBool(Options& opts, bool value)
{
    if (!opts.bv.bitvectorToBoolWasSetByUser) {
        opts.bv.bitvectorToBool = 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/bv_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 bitvectorAig__option_t bitvectorAig;
33		thread_local struct bitblastMode__option_t bitblastMode;
34		thread_local struct bitwiseEq__option_t bitwiseEq;
35		thread_local struct boolToBitvector__option_t boolToBitvector;
36		thread_local struct bvAbstraction__option_t bvAbstraction;
37		thread_local struct bitvectorAigSimplifications__option_t bitvectorAigSimplifications;
38		thread_local struct bvAlgExtf__option_t bvAlgExtf;
39		thread_local struct bitvectorAlgebraicBudget__option_t bitvectorAlgebraicBudget;
40		thread_local struct bitvectorAlgebraicSolver__option_t bitvectorAlgebraicSolver;
41		thread_local struct bvAssertInput__option_t bvAssertInput;
42		thread_local struct bvEagerExplanations__option_t bvEagerExplanations;
43		thread_local struct bitvectorEqualitySolver__option_t bitvectorEqualitySolver;
44		thread_local struct bvExtractArithRewrite__option_t bvExtractArithRewrite;
45		thread_local struct bvGaussElim__option_t bvGaussElim;
46		thread_local struct bitvectorInequalitySolver__option_t bitvectorInequalitySolver;
47		thread_local struct bvIntroducePow2__option_t bvIntroducePow2;
48		thread_local struct bvNumFunc__option_t bvNumFunc;
49		thread_local struct bvPrintConstsAsIndexedSymbols__option_t bvPrintConstsAsIndexedSymbols;
50		thread_local struct bitvectorPropagate__option_t bitvectorPropagate;
51		thread_local struct bitvectorQuickXplain__option_t bitvectorQuickXplain;
52		thread_local struct bvSatSolver__option_t bvSatSolver;
53		thread_local struct skolemizeArguments__option_t skolemizeArguments;
54		thread_local struct bvSolver__option_t bvSolver;
55		thread_local struct bitvectorToBool__option_t bitvectorToBool;
56
57
58		std::ostream& operator<<(std::ostream& os, BitblastMode mode)
59		{
60		switch(mode) {
61		case BitblastMode::LAZY:
62		return os << "BitblastMode::LAZY";
63		case BitblastMode::EAGER:
64		return os << "BitblastMode::EAGER";
65		default:
66		Unreachable();
67		}
68		return os;
69		}
70
71	40	BitblastMode stringToBitblastMode(const std::string& optarg)
72		{
73	40	if (optarg == "lazy")
74		{
75	2	return BitblastMode::LAZY;
76		}
77	38	else if (optarg == "eager")
78		{
79	38	return BitblastMode::EAGER;
80		}
81		else if (optarg == "help")
82		{
83		std::cerr << "Bit-blasting modes.\n"
84		"Available modes for --bitblast are:\n"
85		"+ lazy (default)\n"
86		" Separate boolean structure and term reasoning between the core SAT solver and\n"
87		" the bit-vector SAT solver.\n"
88		"+ eager\n"
89		" Bitblast eagerly to bit-vector SAT solver.\n";
90		std::exit(1);
91		}
92		throw OptionException(std::string("unknown option for --bitblast: `") +
93		optarg + "'. Try --bitblast=help.");
94		}
95
96		std::ostream& operator<<(std::ostream& os, BoolToBVMode mode)
97		{
98		switch(mode) {
99		case BoolToBVMode::OFF:
100		return os << "BoolToBVMode::OFF";
101		case BoolToBVMode::ALL:
102		return os << "BoolToBVMode::ALL";
103		case BoolToBVMode::ITE:
104		return os << "BoolToBVMode::ITE";
105		default:
106		Unreachable();
107		}
108		return os;
109		}
110
111	12	BoolToBVMode stringToBoolToBVMode(const std::string& optarg)
112		{
113	12	if (optarg == "off")
114		{
115		return BoolToBVMode::OFF;
116		}
117	12	else if (optarg == "all")
118		{
119	8	return BoolToBVMode::ALL;
120		}
121	4	else if (optarg == "ite")
122		{
123	4	return BoolToBVMode::ITE;
124		}
125		else if (optarg == "help")
126		{
127		std::cerr << "BoolToBV preprocessing pass modes.\n"
128		"Available modes for --bool-to-bv are:\n"
129		"+ off (default)\n"
130		" Don't push any booleans to width one bit-vectors.\n"
131		"+ all\n"
132		" Force all booleans to be bit-vectors of width one except at the top level.\n"
133		" Most aggressive mode.\n"
134		"+ ite\n"
135		" Try to turn ITEs into BITVECTOR_ITE when possible. It can fail per-formula if\n"
136		" not all sub-formulas can be turned to bit-vectors.\n";
137		std::exit(1);
138		}
139		throw OptionException(std::string("unknown option for --bool-to-bv: `") +
140		optarg + "'. Try --bool-to-bv=help.");
141		}
142
143		std::ostream& operator<<(std::ostream& os, SatSolverMode mode)
144		{
145		switch(mode) {
146		case SatSolverMode::CRYPTOMINISAT:
147		return os << "SatSolverMode::CRYPTOMINISAT";
148		case SatSolverMode::KISSAT:
149		return os << "SatSolverMode::KISSAT";
150		case SatSolverMode::CADICAL:
151		return os << "SatSolverMode::CADICAL";
152		case SatSolverMode::MINISAT:
153		return os << "SatSolverMode::MINISAT";
154		default:
155		Unreachable();
156		}
157		return os;
158		}
159
160	18	SatSolverMode stringToSatSolverMode(const std::string& optarg)
161		{
162	18	if (optarg == "cryptominisat")
163		{
164	10	return SatSolverMode::CRYPTOMINISAT;
165		}
166	8	else if (optarg == "kissat")
167		{
168		return SatSolverMode::KISSAT;
169		}
170	8	else if (optarg == "cadical")
171		{
172	4	return SatSolverMode::CADICAL;
173		}
174	4	else if (optarg == "minisat")
175		{
176	2	return SatSolverMode::MINISAT;
177		}
178	2	else if (optarg == "help")
179		{
180		std::cerr << "SAT solver for bit-blasting backend.\n"
181		"Available modes for --bv-sat-solver are:\n"
182		"+ cryptominisat\n"
183		"+ kissat\n"
184		"+ cadical\n"
185		"+ minisat (default)\n";
186		std::exit(1);
187		}
188	4	throw OptionException(std::string("unknown option for --bv-sat-solver: `") +
189	6	optarg + "'. Try --bv-sat-solver=help.");
190		}
191
192		std::ostream& operator<<(std::ostream& os, BVSolver mode)
193		{
194		switch(mode) {
195		case BVSolver::BITBLAST:
196		return os << "BVSolver::BITBLAST";
197		case BVSolver::LAYERED:
198		return os << "BVSolver::LAYERED";
199		case BVSolver::BITBLAST_INTERNAL:
200		return os << "BVSolver::BITBLAST_INTERNAL";
201		default:
202		Unreachable();
203		}
204		return os;
205		}
206
207	46	BVSolver stringToBVSolver(const std::string& optarg)
208		{
209	46	if (optarg == "bitblast")
210		{
211	24	return BVSolver::BITBLAST;
212		}
213	22	else if (optarg == "layered")
214		{
215	2	return BVSolver::LAYERED;
216		}
217	20	else if (optarg == "bitblast-internal")
218		{
219	20	return BVSolver::BITBLAST_INTERNAL;
220		}
221		else if (optarg == "help")
222		{
223		std::cerr << "Bit-vector solvers.\n"
224		"Available modes for --bv-solver are:\n"
225		"+ bitblast (default)\n"
226		" Enables bitblasting solver.\n"
227		"+ layered\n"
228		" Enables the layered BV solver.\n"
229		"+ bitblast-internal\n"
230		" Enables bitblasting to internal SAT solver with proof support.\n";
231		std::exit(1);
232		}
233		throw OptionException(std::string("unknown option for --bv-solver: `") +
234		optarg + "'. Try --bv-solver=help.");
235		}
236
237
238
239		namespace bv
240		{
241		// clang-format off
242		void setDefaultBitvectorAig(Options& opts, bool value)
243		{
244		if (!opts.bv.bitvectorAigWasSetByUser) {
245		opts.bv.bitvectorAig = value;
246		}
247		}
248		void setDefaultBitblastMode(Options& opts, BitblastMode value)
249		{
250		if (!opts.bv.bitblastModeWasSetByUser) {
251		opts.bv.bitblastMode = value;
252		}
253		}
254		void setDefaultBitwiseEq(Options& opts, bool value)
255		{
256		if (!opts.bv.bitwiseEqWasSetByUser) {
257		opts.bv.bitwiseEq = value;
258		}
259		}
260		void setDefaultBoolToBitvector(Options& opts, BoolToBVMode value)
261		{
262		if (!opts.bv.boolToBitvectorWasSetByUser) {
263		opts.bv.boolToBitvector = value;
264		}
265		}
266		void setDefaultBvAbstraction(Options& opts, bool value)
267		{
268		if (!opts.bv.bvAbstractionWasSetByUser) {
269		opts.bv.bvAbstraction = value;
270		}
271		}
272		void setDefaultBitvectorAigSimplifications(Options& opts, std::string value)
273		{
274		if (!opts.bv.bitvectorAigSimplificationsWasSetByUser) {
275		opts.bv.bitvectorAigSimplifications = value;
276		}
277		}
278		void setDefaultBvAlgExtf(Options& opts, bool value)
279		{
280		if (!opts.bv.bvAlgExtfWasSetByUser) {
281		opts.bv.bvAlgExtf = value;
282		}
283		}
284		void setDefaultBitvectorAlgebraicBudget(Options& opts, unsigned value)
285		{
286		if (!opts.bv.bitvectorAlgebraicBudgetWasSetByUser) {
287		opts.bv.bitvectorAlgebraicBudget = value;
288		}
289		}
290		void setDefaultBitvectorAlgebraicSolver(Options& opts, bool value)
291		{
292		if (!opts.bv.bitvectorAlgebraicSolverWasSetByUser) {
293		opts.bv.bitvectorAlgebraicSolver = value;
294		}
295		}
296		void setDefaultBvAssertInput(Options& opts, bool value)
297		{
298		if (!opts.bv.bvAssertInputWasSetByUser) {
299		opts.bv.bvAssertInput = value;
300		}
301		}
302		void setDefaultBvEagerExplanations(Options& opts, bool value)
303		{
304		if (!opts.bv.bvEagerExplanationsWasSetByUser) {
305		opts.bv.bvEagerExplanations = value;
306		}
307		}
308		void setDefaultBitvectorEqualitySolver(Options& opts, bool value)
309		{
310		if (!opts.bv.bitvectorEqualitySolverWasSetByUser) {
311		opts.bv.bitvectorEqualitySolver = value;
312		}
313		}
314		void setDefaultBvExtractArithRewrite(Options& opts, bool value)
315		{
316		if (!opts.bv.bvExtractArithRewriteWasSetByUser) {
317		opts.bv.bvExtractArithRewrite = value;
318		}
319		}
320		void setDefaultBvGaussElim(Options& opts, bool value)
321		{
322		if (!opts.bv.bvGaussElimWasSetByUser) {
323		opts.bv.bvGaussElim = value;
324		}
325		}
326		void setDefaultBitvectorInequalitySolver(Options& opts, bool value)
327		{
328		if (!opts.bv.bitvectorInequalitySolverWasSetByUser) {
329		opts.bv.bitvectorInequalitySolver = value;
330		}
331		}
332		void setDefaultBvIntroducePow2(Options& opts, bool value)
333		{
334		if (!opts.bv.bvIntroducePow2WasSetByUser) {
335		opts.bv.bvIntroducePow2 = value;
336		}
337		}
338		void setDefaultBvNumFunc(Options& opts, unsigned value)
339		{
340		if (!opts.bv.bvNumFuncWasSetByUser) {
341		opts.bv.bvNumFunc = value;
342		}
343		}
344		void setDefaultBvPrintConstsAsIndexedSymbols(Options& opts, bool value)
345		{
346		if (!opts.bv.bvPrintConstsAsIndexedSymbolsWasSetByUser) {
347		opts.bv.bvPrintConstsAsIndexedSymbols = value;
348		}
349		}
350		void setDefaultBitvectorPropagate(Options& opts, bool value)
351		{
352		if (!opts.bv.bitvectorPropagateWasSetByUser) {
353		opts.bv.bitvectorPropagate = value;
354		}
355		}
356		void setDefaultBitvectorQuickXplain(Options& opts, bool value)
357		{
358		if (!opts.bv.bitvectorQuickXplainWasSetByUser) {
359		opts.bv.bitvectorQuickXplain = value;
360		}
361		}
362		void setDefaultBvSatSolver(Options& opts, SatSolverMode value)
363		{
364		if (!opts.bv.bvSatSolverWasSetByUser) {
365		opts.bv.bvSatSolver = value;
366		}
367		}
368		void setDefaultSkolemizeArguments(Options& opts, bool value)
369		{
370		if (!opts.bv.skolemizeArgumentsWasSetByUser) {
371		opts.bv.skolemizeArguments = value;
372		}
373		}
374		void setDefaultBvSolver(Options& opts, BVSolver value)
375		{
376		if (!opts.bv.bvSolverWasSetByUser) {
377		opts.bv.bvSolver = value;
378		}
379		}
380		void setDefaultBitvectorToBool(Options& opts, bool value)
381		{
382		if (!opts.bv.bitvectorToBoolWasSetByUser) {
383		opts.bv.bitvectorToBool = value;
384		}
385		}
386		// clang-format on
387		}
388
389		} // namespace options
390	29286	} // namespace cvc5
391		// clang-format on