/* special cases */
case UNDEFINED_KIND: return "UNDEFINED_KIND";
case NULL_EXPR: return "NULL";
+ // clang-format off
${kind_printers}
+ // clang-format on
case LAST_KIND: return "LAST_KIND";
default: return "?";
}
{
switch (tc)
{
+ // clang-format off
${type_constant_descriptions}
+ // clang-format on
default: return "UNKNOWN_TYPE_CONSTANT";
}
}
TheoryId kindToTheoryId(::cvc5::Kind k)
{
- switch(k) {
- case kind::UNDEFINED_KIND:
- case kind::NULL_EXPR:
- break;
+ switch (k)
+ {
+ case kind::UNDEFINED_KIND:
+ case kind::NULL_EXPR:
+ break;
+ // clang-format off
${kind_to_theory_id}
- case kind::LAST_KIND:
- break;
+ // clang-format on
+ case kind::LAST_KIND: break;
}
throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind");
}
{
switch (typeConstant)
{
+ // clang-format off
${type_constant_to_theory_id}
+ // clang-format on
case LAST_TYPE: break;
}
throw IllegalArgumentException(
enum Kind_t
{
- UNDEFINED_KIND = -1, /**< undefined */
- NULL_EXPR, /**< Null kind */
+ UNDEFINED_KIND = -1, /**< undefined */
+ NULL_EXPR, /**< Null kind */
+ // clang-format off
${kind_decls} LAST_KIND /**< marks the upper-bound of this enumeration */
+ // clang-format on
}; /* enum Kind_t */
bool isAssociative(::cvc5::Kind k);
std::string kindToString(::cvc5::Kind k);
-struct KindHashFunction {
+struct KindHashFunction
+{
inline size_t operator()(::cvc5::Kind k) const { return k; }
-};/* struct KindHashFunction */
+}; /* struct KindHashFunction */
} // namespace kind
*/
enum TypeConstant
{
+ // clang-format off
${type_constant_list} LAST_TYPE
+ // clang-format on
}; /* enum TypeConstant */
/**
* We hash the constants with their values.
*/
-struct TypeConstantHashFunction {
- inline size_t operator()(TypeConstant tc) const {
- return tc;
- }
-};/* struct TypeConstantHashFunction */
+struct TypeConstantHashFunction
+{
+ inline size_t operator()(TypeConstant tc) const { return tc; }
+}; /* struct TypeConstantHashFunction */
const char* toString(TypeConstant tc);
std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant);
/**
* Get the metakind for a particular kind.
*/
-MetaKind metaKindOf(Kind k) {
+MetaKind metaKindOf(Kind k)
+{
static const MetaKind metaKinds[] = {
- metakind::INVALID, /* UNDEFINED_KIND */
- metakind::INVALID, /* NULL_EXPR */
-// clang-format off
-${metakind_kinds}
-// clang-format on
- metakind::INVALID /* LAST_KIND */
- };/* metaKinds[] */
+ metakind::INVALID, /* UNDEFINED_KIND */
+ metakind::INVALID, /* NULL_EXPR */
+ // clang-format off
+${metakind_kinds} // clang-format on
+ metakind::INVALID /* LAST_KIND */
+ }; /* metaKinds[] */
Assert(k >= kind::NULL_EXPR && k < kind::LAST_KIND);
// handle the UNDEFINED_KIND (-1) case. If we don't, the compiler
// emits warnings for non-assertion builds, since the check isn't done.
return metaKinds[k + 1];
-}/* metaKindOf(k) */
+} /* metaKindOf(k) */
} // namespace kind
switch (nv->d_kind)
{
// clang-format off
-${metakind_constHashes}
+ ${metakind_constHashes}
// clang-format on
default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv->d_kind);
}
#endif /* CVC5__KIND__METAKIND_H */
+// clang-format off
${metakind_includes}
+// clang-format on
#ifdef CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP
namespace cvc5 {
namespace expr {
+// clang-format off
${metakind_getConst_decls}
+// clang-format on
} // namespace expr
namespace kind {
return nv->getConst<T>().hash();
}
+// clang-format off
${metakind_constantMaps_decls}
+// clang-format on
-struct NodeValueConstPrinter {
+struct NodeValueConstPrinter
+{
static void toStream(std::ostream& out, const ::cvc5::expr::NodeValue* nv);
static void toStream(std::ostream& out, TNode n);
};
#include "expr/type_checker.h"
#include "expr/type_checker_util.h"
+// clang-format off
${typechecker_includes}
+// clang-format on
namespace cvc5 {
namespace expr {
TypeNode typeNode;
// Infer the type
- switch(n.getKind()) {
- case kind::VARIABLE:
- case kind::SKOLEM:
- typeNode = nodeManager->getAttribute(n, TypeAttr());
- break;
- case kind::BUILTIN:
- typeNode = nodeManager->builtinOperatorType();
- break;
-
+ switch (n.getKind())
+ {
+ case kind::VARIABLE:
+ case kind::SKOLEM:
+ typeNode = nodeManager->getAttribute(n, TypeAttr());
+ break;
+ case kind::BUILTIN:
+ typeNode = nodeManager->builtinOperatorType();
+ break;
+
+ // clang-format off
${typerules}
+ // clang-format on
- default:
- Debug("getType") << "FAILURE" << std::endl;
- Unhandled() << " " << n.getKind();
+ default:
+ Debug("getType") << "FAILURE" << std::endl;
+ Unhandled() << " " << n.getKind();
}
nodeManager->setAttribute(n, TypeAttr(), typeNode);
|| n.getMetaKind() == kind::metakind::PARAMETERIZED
|| n.getMetaKind() == kind::metakind::NULLARY_OPERATOR);
- switch(n.getKind()) {
+ switch (n.getKind())
+ {
+ // clang-format off
${construles}
+ // clang-format on
default:;
}
#include "expr/type_node.h"
#include "options/language.h"
+// clang-format off
${type_properties_includes}
+// clang-format on
namespace cvc5 {
namespace kind {
{
switch (tc)
{
+ // clang-format off
${type_constant_cardinalities}
+ // clang-format on
default: InternalError() << "No cardinality known for type constant " << tc;
}
} /* getCardinality(TypeConstant) */
switch(Kind k = typeNode.getKind()) {
case TYPE_CONSTANT:
return getCardinality(typeNode.getConst<TypeConstant>());
+ // clang-format off
${type_cardinalities}
+ // clang-format on
default:
InternalError() << "A theory kinds file did not provide a cardinality "
<< "or cardinality computer for type:\n"
inline bool isWellFounded(TypeConstant tc) {
switch(tc) {
+ // clang-format off
${type_constant_wellfoundednesses}
-default:
- InternalError() << "No well-foundedness status known for type constant: "
- << tc;
+ // clang-format on
+ default:
+ InternalError() << "No well-foundedness status known for type constant: "
+ << tc;
}
}/* isWellFounded(TypeConstant) */
switch(Kind k = typeNode.getKind()) {
case TYPE_CONSTANT:
return isWellFounded(typeNode.getConst<TypeConstant>());
+ // clang-format off
${type_wellfoundednesses}
+ // clang-format on
default:
InternalError() << "A theory kinds file did not provide a well-foundedness "
<< "or well-foundedness computer for type:\n"
{
switch (tc)
{
+ // clang-format off
${type_constant_groundterms}
+ // clang-format on
default:
InternalError() << "No ground term known for type constant: " << tc;
}
{
case TYPE_CONSTANT:
return mkGroundTerm(typeNode.getConst<TypeConstant>());
+ // clang-format off
${type_groundterms}
+ // clang-format on
default:
InternalError() << "A theory kinds file did not provide a ground term "
<< "or ground term computer for type:\n"
using namespace cvc5;
using namespace cvc5::options;
+// clang-format on
namespace cvc5 {
void Options::setListener(OptionsListener* ol) { d_olisten = ol; }
+// clang-format off
${custom_handlers}$
+// clang-format on
#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)
# define DO_SEMANTIC_CHECKS_BY_DEFAULT false
# define DO_SEMANTIC_CHECKS_BY_DEFAULT true
#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
+// clang-format off
options::OptionsHolder::OptionsHolder() :
${module_defaults}$
{
}
+// clang-format on
-
-static const std::string mostCommonOptionsDescription = "\
+static const std::string mostCommonOptionsDescription =
+ "\
Most commonly-used cvc5 options:\n"
-${help_common}$;
-
+ // clang-format off
+${help_common}$
+ // clang-format on
+ ;
-static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
-\n\
-Additional cvc5 options:\n"
+// clang-format off
+static const std::string optionsDescription =
+ mostCommonOptionsDescription + "\n\nAdditional cvc5 options:\n"
${help_others}$;
-
+// clang-format on
static const std::string optionsFootnote = "\n\
[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
* If you add something that has a short option equivalent, you should
* add it to the getopt_long() call in parseOptions().
*/
+// clang-format off
static struct option cmdlineOptions[] = {
${cmdline_options}$
- { NULL, no_argument, NULL, '\0' }
-};/* cmdlineOptions */
+ {nullptr, no_argument, nullptr, '\0'}};
+// clang-format on
namespace options {
Debug("options") << "[ before, optind == " << optind << " ]" << std::endl;
Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]"
<< std::endl;
+ // clang-format off
int c = getopt_long(argc, argv,
"+:${options_short}$",
cmdlineOptions, NULL);
+ // clang-format on
main_optind = optind;
Debug("preemptGetopt") << "processing option " << c
<< " (`" << char(c) << "'), " << option << std::endl;
+ // clang-format off
switch(c)
{
${options_handler}$
-
- case ':':
+ case ':' :
// This can be a long or short option, and the way to get at the
// name of it is different.
- throw OptionException(std::string("option `") + option +
- "' missing its required argument");
+ throw OptionException(std::string("option `") + option
+ + "' missing its required argument");
- case '?':
- default:
- throw OptionException(std::string("can't understand option `") + option +
- "'" + suggestCommandLineOptions(option));
+ case '?':
+ default:
+ throw OptionException(std::string("can't understand option `") + option
+ + "'" + suggestCommandLineOptions(option));
}
}
+ // clang-format on
Debug("options") << "got " << nonoptions->size()
<< " non-option arguments." << std::endl;
return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('=')));
}
+// clang-format off
static const char* smtOptions[] = {
${options_smt}$
- NULL
-};/* smtOptions[] */
+ nullptr};
+// clang-format on
std::vector<std::string> Options::suggestSmtOptions(
const std::string& optionName)
return suggestions;
}
+// clang-format off
std::vector<std::vector<std::string> > Options::getOptions() const
{
std::vector< std::vector<std::string> > opts;
${options_getoptions}$
-
return opts;
}
+// clang-format on
void Options::setOption(const std::string& key, const std::string& optionarg)
{
}
}
+// clang-format off
void Options::setOptionInternal(const std::string& key,
const std::string& optionarg)
{
${setoption_handlers}$
throw UnrecognizedOptionException(key);
}
+// clang-format on
+// clang-format off
std::string Options::getOption(const std::string& key) const
{
Trace("options") << "Options::getOption(" << key << ")" << std::endl;
throw UnrecognizedOptionException(key);
}
+// clang-format on
#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
#pragma once
+#include "expr/attribute.h"
+#include "expr/attribute_unique_id.h"
#include "theory/rewriter.h"
#include "theory/rewriter_attributes.h"
-#include "expr/attribute_unique_id.h"
-#include "expr/attribute.h"
+// clang-format off
${rewriter_includes}
+// clang-format on
namespace cvc5 {
namespace theory {
-Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) {
- switch(theoryId) {
+Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node)
+{
+ switch (theoryId)
+ {
+ // clang-format off
${pre_rewrite_get_cache}
- default:
- Unreachable();
+ // clang-format on
+ default: Unreachable();
}
}
-Node Rewriter::getPostRewriteCache(theory::TheoryId theoryId, TNode node) {
- switch(theoryId) {
+Node Rewriter::getPostRewriteCache(theory::TheoryId theoryId, TNode node)
+{
+ switch (theoryId)
+ {
+ // clang-format off
${post_rewrite_get_cache}
- default:
- Unreachable();
+ // clang-format on
+ default: Unreachable();
}
}
-void Rewriter::setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache) {
- switch(theoryId) {
+void Rewriter::setPreRewriteCache(theory::TheoryId theoryId,
+ TNode node,
+ TNode cache)
+{
+ switch (theoryId)
+ {
+ // clang-format off
${pre_rewrite_set_cache}
- default:
- Unreachable();
+ // clang-format on
+ default: Unreachable();
}
}
-void Rewriter::setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache) {
- switch(theoryId) {
+void Rewriter::setPostRewriteCache(theory::TheoryId theoryId,
+ TNode node,
+ TNode cache)
+{
+ switch (theoryId)
+ {
+ // clang-format off
${post_rewrite_set_cache}
- default:
- Unreachable();
+ // clang-format on
+ default: Unreachable();
}
}
Rewriter::Rewriter() : d_tpg(nullptr)
{
-for (size_t i = 0; i < kind::LAST_KIND; ++i)
-{
- d_preRewriters[i] = nullptr;
- d_postRewriters[i] = nullptr;
-}
+ for (size_t i = 0; i < kind::LAST_KIND; ++i)
+ {
+ d_preRewriters[i] = nullptr;
+ d_postRewriters[i] = nullptr;
+ }
-for (size_t i = 0; i < theory::THEORY_LAST; ++i)
-{
- d_preRewritersEqual[i] = nullptr;
- d_postRewritersEqual[i] = nullptr;
-}
+ for (size_t i = 0; i < theory::THEORY_LAST; ++i)
+ {
+ d_preRewritersEqual[i] = nullptr;
+ d_postRewritersEqual[i] = nullptr;
+ }
}
-void Rewriter::clearCachesInternal() {
+void Rewriter::clearCachesInternal()
+{
typedef cvc5::expr::attr::AttributeUniqueId AttributeUniqueId;
std::vector<AttributeUniqueId> preids;
- ${pre_rewrite_attribute_ids}
+ // clang-format off
+ ${pre_rewrite_attribute_ids} // clang-format on
- std::vector<AttributeUniqueId> postids;
- ${post_rewrite_attribute_ids}
+ std::vector<AttributeUniqueId>
+ postids;
+ // clang-format off
+ ${post_rewrite_attribute_ids} // clang-format on
- std::vector<const AttributeUniqueId*> allids;
- for(unsigned i = 0; i < preids.size(); ++i){
+ std::vector<const AttributeUniqueId*>
+ allids;
+ for (size_t i = 0, size = preids.size(); i < size; ++i)
+ {
allids.push_back(&preids[i]);
}
- for(unsigned i = 0; i < postids.size(); ++i){
+ for (size_t i = 0, size = postids.size(); i < size; ++i)
+ {
allids.push_back(&postids[i]);
}
NodeManager::currentNM()->deleteAttributes(allids);
#include "options/theory_options.h"
#include "theory/theory.h"
+// clang-format off
${theory_includes}
+// clang-format on
namespace cvc5 {
namespace theory {
template <TheoryId theoryId>
struct TheoryTraits;
+// clang-format off
${theory_traits}
-
-struct TheoryConstructor {
- static void addTheory(TheoryEngine* engine, TheoryId id) {
- switch(id) {
-
+// clang-format on
+
+struct TheoryConstructor
+{
+ static void addTheory(TheoryEngine* engine, TheoryId id)
+ {
+ switch (id)
+ {
+ // clang-format off
${theory_constructors}
+ // clang-format on
-default: Unhandled() << id;
+ default: Unhandled() << id;
}
}
}; /* struct cvc5::theory::TheoryConstructor */
#include "expr/kind.h"
#include "theory/type_enumerator.h"
-
+// clang-format off
${type_enumerator_includes}
+// clang-format on
using namespace std;
case kind::TYPE_CONSTANT:
switch (type.getConst<TypeConstant>())
{
+ // clang-format off
${mk_type_enumerator_type_constant_cases}
+ // clang-format on
default: Unhandled() << "No type enumerator for type `" << type << "'";
}
Unreachable();
+ // clang-format off
${mk_type_enumerator_cases}
+ // clang-format on
default: Unhandled() << "No type enumerator for type `" << type << "'";
}
Unreachable();