Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/options/proof_options.cpp	Lines:	1	69	1.4 %
Date:	2021-08-06	Branches:	2	65	3.1 %


/******************************************************************************
 * 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 {



namespace options {

thread_local struct proofEagerChecking__option_t proofEagerChecking;
thread_local struct proofFormatMode__option_t proofFormatMode;
thread_local struct proofGranularityMode__option_t proofGranularityMode;
thread_local struct proofPedantic__option_t proofPedantic;
thread_local struct proofPrintConclusion__option_t proofPrintConclusion;


std::ostream& operator<<(std::ostream& os, ProofFormatMode mode)
{
  switch(mode) {
    case ProofFormatMode::DOT:
      return os << "ProofFormatMode::DOT";
    case ProofFormatMode::NONE:
      return os << "ProofFormatMode::NONE";
    case ProofFormatMode::VERIT:
      return os << "ProofFormatMode::VERIT";
    default:
      Unreachable();
  }
  return os;
}

ProofFormatMode stringToProofFormatMode(const std::string& optarg)
{
  if (optarg == "dot")
  {
    return ProofFormatMode::DOT;
  }
  else if (optarg == "none")
  {
    return ProofFormatMode::NONE;
  }
  else if (optarg == "verit")
  {
    return ProofFormatMode::VERIT;
  }
  else if (optarg == "help")
  {
    std::cerr << "Proof format modes.\n"
         "Available modes for --proof-format-mode are:\n"
         "+ dot\n"
         "  Output DOT proof\n"
         "+ none (default)\n"
         "  Do not translate proof output\n"
         "+ verit\n"
         "  Output veriT proof\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::OFF:
      return os << "ProofGranularityMode::OFF";
    case ProofGranularityMode::DSL_REWRITE:
      return os << "ProofGranularityMode::DSL_REWRITE";
    case ProofGranularityMode::REWRITE:
      return os << "ProofGranularityMode::REWRITE";
    default:
      Unreachable();
  }
  return os;
}

ProofGranularityMode stringToProofGranularityMode(const std::string& optarg)
{
  if (optarg == "theory-rewrite")
  {
    return ProofGranularityMode::THEORY_REWRITE;
  }
  else if (optarg == "off")
  {
    return ProofGranularityMode::OFF;
  }
  else if (optarg == "dsl-rewrite")
  {
    return ProofGranularityMode::DSL_REWRITE;
  }
  else if (optarg == "rewrite")
  {
    return ProofGranularityMode::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"
         "+ 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"
         "+ rewrite\n"
         "  Allow rewrite or substitution steps, expand macros.\n";
    std::exit(1);
  }
  throw OptionException(std::string("unknown option for --proof-granularity: `") +
                        optarg + "'.  Try --proof-granularity=help.");
}



namespace proof
{
// clang-format off
void setDefaultProofEagerChecking(Options& opts, bool value)
{
    if (!opts.proof.proofEagerCheckingWasSetByUser) {
        opts.proof.proofEagerChecking = 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 setDefaultProofPrintConclusion(Options& opts, bool value)
{
    if (!opts.proof.proofPrintConclusionWasSetByUser) {
        opts.proof.proofPrintConclusion = 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/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 {
27
28
29
30		namespace options {
31
32		thread_local struct proofEagerChecking__option_t proofEagerChecking;
33		thread_local struct proofFormatMode__option_t proofFormatMode;
34		thread_local struct proofGranularityMode__option_t proofGranularityMode;
35		thread_local struct proofPedantic__option_t proofPedantic;
36		thread_local struct proofPrintConclusion__option_t proofPrintConclusion;
37
38
39		std::ostream& operator<<(std::ostream& os, ProofFormatMode mode)
40		{
41		switch(mode) {
42		case ProofFormatMode::DOT:
43		return os << "ProofFormatMode::DOT";
44		case ProofFormatMode::NONE:
45		return os << "ProofFormatMode::NONE";
46		case ProofFormatMode::VERIT:
47		return os << "ProofFormatMode::VERIT";
48		default:
49		Unreachable();
50		}
51		return os;
52		}
53
54		ProofFormatMode stringToProofFormatMode(const std::string& optarg)
55		{
56		if (optarg == "dot")
57		{
58		return ProofFormatMode::DOT;
59		}
60		else if (optarg == "none")
61		{
62		return ProofFormatMode::NONE;
63		}
64		else if (optarg == "verit")
65		{
66		return ProofFormatMode::VERIT;
67		}
68		else if (optarg == "help")
69		{
70		std::cerr << "Proof format modes.\n"
71		"Available modes for --proof-format-mode are:\n"
72		"+ dot\n"
73		" Output DOT proof\n"
74		"+ none (default)\n"
75		" Do not translate proof output\n"
76		"+ verit\n"
77		" Output veriT proof\n";
78		std::exit(1);
79		}
80		throw OptionException(std::string("unknown option for --proof-format-mode: `") +
81		optarg + "'. Try --proof-format-mode=help.");
82		}
83
84		std::ostream& operator<<(std::ostream& os, ProofGranularityMode mode)
85		{
86		switch(mode) {
87		case ProofGranularityMode::THEORY_REWRITE:
88		return os << "ProofGranularityMode::THEORY_REWRITE";
89		case ProofGranularityMode::OFF:
90		return os << "ProofGranularityMode::OFF";
91		case ProofGranularityMode::DSL_REWRITE:
92		return os << "ProofGranularityMode::DSL_REWRITE";
93		case ProofGranularityMode::REWRITE:
94		return os << "ProofGranularityMode::REWRITE";
95		default:
96		Unreachable();
97		}
98		return os;
99		}
100
101		ProofGranularityMode stringToProofGranularityMode(const std::string& optarg)
102		{
103		if (optarg == "theory-rewrite")
104		{
105		return ProofGranularityMode::THEORY_REWRITE;
106		}
107		else if (optarg == "off")
108		{
109		return ProofGranularityMode::OFF;
110		}
111		else if (optarg == "dsl-rewrite")
112		{
113		return ProofGranularityMode::DSL_REWRITE;
114		}
115		else if (optarg == "rewrite")
116		{
117		return ProofGranularityMode::REWRITE;
118		}
119		else if (optarg == "help")
120		{
121		std::cerr << "Modes for proof granularity.\n"
122		"Available modes for --proof-granularity are:\n"
123		"+ theory-rewrite (default)\n"
124		" Allow theory rewrite steps, expand macros, rewrite and substitution steps.\n"
125		"+ off\n"
126		" Do not improve the granularity of proofs.\n"
127		"+ dsl-rewrite\n"
128		" Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution,\n"
129		" and theory rewrite steps.\n"
130		"+ rewrite\n"
131		" Allow rewrite or substitution steps, expand macros.\n";
132		std::exit(1);
133		}
134		throw OptionException(std::string("unknown option for --proof-granularity: `") +
135		optarg + "'. Try --proof-granularity=help.");
136		}
137
138
139
140		namespace proof
141		{
142		// clang-format off
143		void setDefaultProofEagerChecking(Options& opts, bool value)
144		{
145		if (!opts.proof.proofEagerCheckingWasSetByUser) {
146		opts.proof.proofEagerChecking = value;
147		}
148		}
149		void setDefaultProofFormatMode(Options& opts, ProofFormatMode value)
150		{
151		if (!opts.proof.proofFormatModeWasSetByUser) {
152		opts.proof.proofFormatMode = value;
153		}
154		}
155		void setDefaultProofGranularityMode(Options& opts, ProofGranularityMode value)
156		{
157		if (!opts.proof.proofGranularityModeWasSetByUser) {
158		opts.proof.proofGranularityMode = value;
159		}
160		}
161		void setDefaultProofPedantic(Options& opts, uint64_t value)
162		{
163		if (!opts.proof.proofPedanticWasSetByUser) {
164		opts.proof.proofPedantic = value;
165		}
166		}
167		void setDefaultProofPrintConclusion(Options& opts, bool value)
168		{
169		if (!opts.proof.proofPrintConclusionWasSetByUser) {
170		opts.proof.proofPrintConclusion = value;
171		}
172		}
173		// clang-format on
174		}
175
176		} // namespace options
177	29322	} // namespace cvc5
178		// clang-format on