Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/bv_options.cpp	Lines:	30	185	16.2 %
Date:	2021-09-14	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::options {

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