Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/bv_options.cpp	Lines:	29	185	15.7 %
Date:	2021-08-17	Branches:	25	148	16.9 %


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