Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/proof_options.cpp	Lines:	7	103	6.8 %
Date:	2021-09-14	Branches:	6	97	6.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/proof_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, ProofCheckMode mode)
{
  switch(mode) {
    case ProofCheckMode::EAGER_SIMPLE:
      return os << "ProofCheckMode::EAGER_SIMPLE";
    case ProofCheckMode::LAZY:
      return os << "ProofCheckMode::LAZY";
    case ProofCheckMode::NONE:
      return os << "ProofCheckMode::NONE";
    case ProofCheckMode::EAGER:
      return os << "ProofCheckMode::EAGER";
    default:
      Unreachable();
  }
  return os;
}
ProofCheckMode stringToProofCheckMode(const std::string& optarg)
{
  if (optarg == "eager-simple")
  {
    return ProofCheckMode::EAGER_SIMPLE;
  }
  else if (optarg == "lazy")
  {
    return ProofCheckMode::LAZY;
  }
  else if (optarg == "none")
  {
    return ProofCheckMode::NONE;
  }
  else if (optarg == "eager")
  {
    return ProofCheckMode::EAGER;
  }
  else if (optarg == "help")
  {
    std::cerr << "Proof checking modes.\n"
         "Available modes for --proof-check are:\n"
         "+ eager-simple\n"
         "  check rule applications during construction\n"
         "+ lazy (default)\n"
         "  check rule applications only during final proof construction\n"
         "+ none\n"
         "  do not check rule applications\n"
         "+ eager\n"
         "  check rule applications and proofs from generators eagerly for local debugging\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --proof-check: `") +
                        optarg + "'.  Try --proof-check=help.");
}
std::ostream& operator<<(std::ostream& os, ProofFormatMode mode)
{
  switch(mode) {
    case ProofFormatMode::NONE:
      return os << "ProofFormatMode::NONE";
    case ProofFormatMode::VERIT:
      return os << "ProofFormatMode::VERIT";
    case ProofFormatMode::DOT:
      return os << "ProofFormatMode::DOT";
    case ProofFormatMode::TPTP:
      return os << "ProofFormatMode::TPTP";
    default:
      Unreachable();
  }
  return os;
}
ProofFormatMode stringToProofFormatMode(const std::string& optarg)
{
  if (optarg == "none")
  {
    return ProofFormatMode::NONE;
  }
  else if (optarg == "verit")
  {
    return ProofFormatMode::VERIT;
  }
  else if (optarg == "dot")
  {
    return ProofFormatMode::DOT;
  }
  else if (optarg == "tptp")
  {
    return ProofFormatMode::TPTP;
  }
  else if (optarg == "help")
  {
    std::cerr << "Proof format modes.\n"
         "Available modes for --proof-format-mode are:\n"
         "+ none (default)\n"
         "  Do not translate proof output\n"
         "+ verit\n"
         "  Output veriT proof\n"
         "+ dot\n"
         "  Output DOT proof\n"
         "+ tptp\n"
         "  Output TPTP proof (work in progress)\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --proof-format-mode: `") +
                        optarg + "'.  Try --proof-format-mode=help.");
}
std::ostream& operator<<(std::ostream& os, ProofGranularityMode mode)
{
  switch(mode) {
    case ProofGranularityMode::THEORY_REWRITE:
      return os << "ProofGranularityMode::THEORY_REWRITE";
    case ProofGranularityMode::REWRITE:
      return os << "ProofGranularityMode::REWRITE";
    case ProofGranularityMode::OFF:
      return os << "ProofGranularityMode::OFF";
    case ProofGranularityMode::DSL_REWRITE:
      return os << "ProofGranularityMode::DSL_REWRITE";
    default:
      Unreachable();
  }
  return os;
}
ProofGranularityMode stringToProofGranularityMode(const std::string& optarg)
{
  if (optarg == "theory-rewrite")
  {
    return ProofGranularityMode::THEORY_REWRITE;
  }
  else if (optarg == "rewrite")
  {
    return ProofGranularityMode::REWRITE;
  }
  else if (optarg == "off")
  {
    return ProofGranularityMode::OFF;
  }
  else if (optarg == "dsl-rewrite")
  {
    return ProofGranularityMode::DSL_REWRITE;
  }
  else if (optarg == "help")
  {
    std::cerr << "Modes for proof granularity.\n"
         "Available modes for --proof-granularity are:\n"
         "+ theory-rewrite (default)\n"
         "  Allow theory rewrite steps, expand macros, rewrite and substitution steps.\n"
         "+ rewrite\n"
         "  Allow rewrite or substitution steps, expand macros.\n"
         "+ off\n"
         "  Do not improve the granularity of proofs.\n"
         "+ dsl-rewrite\n"
         "  Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution,\n"
         "  and theory rewrite steps.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --proof-granularity: `") +
                        optarg + "'.  Try --proof-granularity=help.");
}

namespace proof
{
// clang-format off
void setDefaultProofCheck(Options& opts, ProofCheckMode value)
{
    if (!opts.proof.proofCheckWasSetByUser) {
        opts.proof.proofCheck = value;
    }
}
void setDefaultProofFormatMode(Options& opts, ProofFormatMode value)
{
    if (!opts.proof.proofFormatModeWasSetByUser) {
        opts.proof.proofFormatMode = value;
    }
}
void setDefaultProofGranularityMode(Options& opts, ProofGranularityMode value)
{
    if (!opts.proof.proofGranularityModeWasSetByUser) {
        opts.proof.proofGranularityMode = value;
    }
}
void setDefaultProofPedantic(Options& opts, uint64_t value)
{
    if (!opts.proof.proofPedanticWasSetByUser) {
        opts.proof.proofPedantic = value;
    }
}
void setDefaultProofPpMerge(Options& opts, bool value)
{
    if (!opts.proof.proofPpMergeWasSetByUser) {
        opts.proof.proofPpMerge = value;
    }
}
void setDefaultProofPrintConclusion(Options& opts, bool value)
{
    if (!opts.proof.proofPrintConclusionWasSetByUser) {
        opts.proof.proofPrintConclusion = 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/proof_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, ProofCheckMode mode)
29		{
30		switch(mode) {
31		case ProofCheckMode::EAGER_SIMPLE:
32		return os << "ProofCheckMode::EAGER_SIMPLE";
33		case ProofCheckMode::LAZY:
34		return os << "ProofCheckMode::LAZY";
35		case ProofCheckMode::NONE:
36		return os << "ProofCheckMode::NONE";
37		case ProofCheckMode::EAGER:
38		return os << "ProofCheckMode::EAGER";
39		default:
40		Unreachable();
41		}
42		return os;
43		}
44	2	ProofCheckMode stringToProofCheckMode(const std::string& optarg)
45		{
46	2	if (optarg == "eager-simple")
47		{
48		return ProofCheckMode::EAGER_SIMPLE;
49		}
50	2	else if (optarg == "lazy")
51		{
52		return ProofCheckMode::LAZY;
53		}
54	2	else if (optarg == "none")
55		{
56		return ProofCheckMode::NONE;
57		}
58	2	else if (optarg == "eager")
59		{
60	2	return ProofCheckMode::EAGER;
61		}
62		else if (optarg == "help")
63		{
64		std::cerr << "Proof checking modes.\n"
65		"Available modes for --proof-check are:\n"
66		"+ eager-simple\n"
67		" check rule applications during construction\n"
68		"+ lazy (default)\n"
69		" check rule applications only during final proof construction\n"
70		"+ none\n"
71		" do not check rule applications\n"
72		"+ eager\n"
73		" check rule applications and proofs from generators eagerly for local debugging\n";
74		std::exit(1);
75		}
76		throw OptionException(std::string("unknown option for --proof-check: `") +
77		optarg + "'. Try --proof-check=help.");
78		}
79		std::ostream& operator<<(std::ostream& os, ProofFormatMode mode)
80		{
81		switch(mode) {
82		case ProofFormatMode::NONE:
83		return os << "ProofFormatMode::NONE";
84		case ProofFormatMode::VERIT:
85		return os << "ProofFormatMode::VERIT";
86		case ProofFormatMode::DOT:
87		return os << "ProofFormatMode::DOT";
88		case ProofFormatMode::TPTP:
89		return os << "ProofFormatMode::TPTP";
90		default:
91		Unreachable();
92		}
93		return os;
94		}
95		ProofFormatMode stringToProofFormatMode(const std::string& optarg)
96		{
97		if (optarg == "none")
98		{
99		return ProofFormatMode::NONE;
100		}
101		else if (optarg == "verit")
102		{
103		return ProofFormatMode::VERIT;
104		}
105		else if (optarg == "dot")
106		{
107		return ProofFormatMode::DOT;
108		}
109		else if (optarg == "tptp")
110		{
111		return ProofFormatMode::TPTP;
112		}
113		else if (optarg == "help")
114		{
115		std::cerr << "Proof format modes.\n"
116		"Available modes for --proof-format-mode are:\n"
117		"+ none (default)\n"
118		" Do not translate proof output\n"
119		"+ verit\n"
120		" Output veriT proof\n"
121		"+ dot\n"
122		" Output DOT proof\n"
123		"+ tptp\n"
124		" Output TPTP proof (work in progress)\n";
125		std::exit(1);
126		}
127		throw OptionException(std::string("unknown option for --proof-format-mode: `") +
128		optarg + "'. Try --proof-format-mode=help.");
129		}
130		std::ostream& operator<<(std::ostream& os, ProofGranularityMode mode)
131		{
132		switch(mode) {
133		case ProofGranularityMode::THEORY_REWRITE:
134		return os << "ProofGranularityMode::THEORY_REWRITE";
135		case ProofGranularityMode::REWRITE:
136		return os << "ProofGranularityMode::REWRITE";
137		case ProofGranularityMode::OFF:
138		return os << "ProofGranularityMode::OFF";
139		case ProofGranularityMode::DSL_REWRITE:
140		return os << "ProofGranularityMode::DSL_REWRITE";
141		default:
142		Unreachable();
143		}
144		return os;
145		}
146		ProofGranularityMode stringToProofGranularityMode(const std::string& optarg)
147		{
148		if (optarg == "theory-rewrite")
149		{
150		return ProofGranularityMode::THEORY_REWRITE;
151		}
152		else if (optarg == "rewrite")
153		{
154		return ProofGranularityMode::REWRITE;
155		}
156		else if (optarg == "off")
157		{
158		return ProofGranularityMode::OFF;
159		}
160		else if (optarg == "dsl-rewrite")
161		{
162		return ProofGranularityMode::DSL_REWRITE;
163		}
164		else if (optarg == "help")
165		{
166		std::cerr << "Modes for proof granularity.\n"
167		"Available modes for --proof-granularity are:\n"
168		"+ theory-rewrite (default)\n"
169		" Allow theory rewrite steps, expand macros, rewrite and substitution steps.\n"
170		"+ rewrite\n"
171		" Allow rewrite or substitution steps, expand macros.\n"
172		"+ off\n"
173		" Do not improve the granularity of proofs.\n"
174		"+ dsl-rewrite\n"
175		" Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution,\n"
176		" and theory rewrite steps.\n";
177		std::exit(1);
178		}
179		throw OptionException(std::string("unknown option for --proof-granularity: `") +
180		optarg + "'. Try --proof-granularity=help.");
181		}
182
183		namespace proof
184		{
185		// clang-format off
186		void setDefaultProofCheck(Options& opts, ProofCheckMode value)
187		{
188		if (!opts.proof.proofCheckWasSetByUser) {
189		opts.proof.proofCheck = value;
190		}
191		}
192		void setDefaultProofFormatMode(Options& opts, ProofFormatMode value)
193		{
194		if (!opts.proof.proofFormatModeWasSetByUser) {
195		opts.proof.proofFormatMode = value;
196		}
197		}
198		void setDefaultProofGranularityMode(Options& opts, ProofGranularityMode value)
199		{
200		if (!opts.proof.proofGranularityModeWasSetByUser) {
201		opts.proof.proofGranularityMode = value;
202		}
203		}
204		void setDefaultProofPedantic(Options& opts, uint64_t value)
205		{
206		if (!opts.proof.proofPedanticWasSetByUser) {
207		opts.proof.proofPedantic = value;
208		}
209		}
210		void setDefaultProofPpMerge(Options& opts, bool value)
211		{
212		if (!opts.proof.proofPpMergeWasSetByUser) {
213		opts.proof.proofPpMerge = value;
214		}
215		}
216		void setDefaultProofPrintConclusion(Options& opts, bool value)
217		{
218		if (!opts.proof.proofPrintConclusionWasSetByUser) {
219		opts.proof.proofPrintConclusion = value;
220		}
221		}
222		// clang-format on
223		}
224
225	29517	} // namespace cvc5::options
226		// clang-format on