From: Gereon Kremer Date: Thu, 22 Apr 2021 19:27:54 +0000 (+0200) Subject: Remove unused stuff from options setup (#6422) X-Git-Tag: cvc5-1.0.0~1853 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0869a09f1161480de24c412b12954fc84943bab2;p=cvc5.git Remove unused stuff from options setup (#6422) This PR removes some old stuff from our options setup that has not been used in a long time. Most prominently, this includes the man pages that were still generated, and the alias and links options, which no longer worked anyway. --- diff --git a/CMakeLists.txt b/CMakeLists.txt index 69e028d17..77f9fb566 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -502,7 +502,6 @@ endif() #-----------------------------------------------------------------------------# # Add subdirectories -add_subdirectory(doc) add_subdirectory(src) add_subdirectory(test) diff --git a/doc/CMakeLists.txt b/doc/CMakeLists.txt deleted file mode 100644 index a58303520..000000000 --- a/doc/CMakeLists.txt +++ /dev/null @@ -1,59 +0,0 @@ -############################################################################### -# 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. -# ############################################################################# -# -# The build system configuration. -## - -#-----------------------------------------------------------------------------# -# Set variables required for the documentation *.in files - -string(TIMESTAMP MAN_DATE "%Y-%m-%d") -set(VERSION CVC5_RELEASE_STRING) - -#-----------------------------------------------------------------------------# -# Generate files - -configure_file( - ${CMAKE_CURRENT_SOURCE_DIR}/SmtEngine.3cvc_template.in - ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.3cvc_template) - -configure_file( - ${CMAKE_CURRENT_SOURCE_DIR}/cvc5.1_template.in - ${CMAKE_CURRENT_BINARY_DIR}/cvc5.1_template) - -configure_file( - ${CMAKE_CURRENT_SOURCE_DIR}/cvc5.5.in - ${CMAKE_CURRENT_BINARY_DIR}/cvc5.5) - -configure_file( - ${CMAKE_CURRENT_SOURCE_DIR}/libcvc5.3.in - ${CMAKE_CURRENT_BINARY_DIR}/libcvc5.3) - -configure_file( - ${CMAKE_CURRENT_SOURCE_DIR}/libcvc5parser.3.in - ${CMAKE_CURRENT_BINARY_DIR}/libcvc5parser.3) - -configure_file( - ${CMAKE_CURRENT_SOURCE_DIR}/options.3cvc_template.in - ${CMAKE_CURRENT_BINARY_DIR}/options.3cvc_template) - -#-----------------------------------------------------------------------------# -# Install man pages - -install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc5.1 DESTINATION share/man/man1) -install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc5.5 DESTINATION share/man/man5) -install(FILES - ${CMAKE_CURRENT_BINARY_DIR}/libcvc5.3 - ${CMAKE_CURRENT_BINARY_DIR}/libcvc5parser.3 - ${CMAKE_CURRENT_BINARY_DIR}/options.3cvc - ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.3cvc - DESTINATION share/man/man3) diff --git a/doc/SmtEngine.3cvc_template.in b/doc/SmtEngine.3cvc_template.in deleted file mode 100644 index b34500b50..000000000 --- a/doc/SmtEngine.3cvc_template.in +++ /dev/null @@ -1,54 +0,0 @@ -.\" Process this file with -.\" groff -man -Tascii SmtEngine.3cvc -.\" -.TH SMTENGINE 3cvc "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Library Interfaces" -.SH NAME -SmtEngine \- the primary interface to CVC4's theorem-proving capabilities -.SH DESCRIPTION -.B SmtEngine -is the main entry point into the CVC4 theorem prover API. - -.SH SMTENGINE OPTIONS - -The SmtEngine is in charge of setting and getting information and options. -Numerous options are available via the -.I SmtEngine::setOption() -call. -.I SmtEngine::setOption() -and -.I SmtEngine::getOption() -use the following option keys. - -.ad l - -.RS -.TP 10 -.I "COMMON OPTIONS" -${man_common_smt}$ - -${man_others_smt}$ -.PD -.RE - -.ad b - -.SH VERSION -This manual page refers to -.B CVC4 -version @VERSION@. -.SH BUGS -An issue tracker for the CVC4 project is maintained at -.BR https://github.com/CVC4/CVC4/issues . -.SH AUTHORS -.B CVC4 -is developed by a team of researchers at Stanford University -and the University of Iowa. -See the AUTHORS file in the distribution for a full list of -contributors. -.SH "SEE ALSO" -.BR libcvc4 (3), -.BR libcvc4parser (3) - -Additionally, the CVC4 wiki contains useful information about the -design and internals of CVC4. It is maintained at -.BR http://cvc4.cs.stanford.edu/wiki/ . diff --git a/doc/cvc5.1_template.in b/doc/cvc5.1_template.in deleted file mode 100644 index 042d6cfc1..000000000 --- a/doc/cvc5.1_template.in +++ /dev/null @@ -1,131 +0,0 @@ -.\" Process this file with -.\" groff -man -Tascii cvc4.1 -.\" -.TH CVC4 1 "@MAN_DATE@" "CVC4 release @VERSION@" "User Manuals" -.SH NAME -cvc4, pcvc4 \- an automated theorem prover -.SH SYNOPSIS -.B cvc4 [ -.I options -.B ] [ -.I file -.B ] -.P -.B pcvc4 [ -.I options -.B ] [ -.I file -.B ] -.SH DESCRIPTION -.B cvc4 -is an automated theorem prover for first-order formulas with respect -to background theories of interest. -.B pcvc4 -is CVC4's "portfolio" variant, which is capable of running multiple -CVC4 instances in parallel, configured differently. - -With -.I file -, commands are read from -.I file -and executed. CVC4 supports the SMT-LIB (versions 1.2 and 2.0) input -format, as well as its own native \(lqpresentation language\(rq (see -.BR cvc4 (5) -), which is similar in many respects to CVC3's presentation language, -but not identical. - -If -.I file -is unspecified, standard input is read (and the -.B CVC4 -presentation language is assumed). If -.I file -is unspecified and -.B CVC4 -is connected to a terminal, interactive mode is assumed. - -.SH COMMON OPTIONS - -.IP "Each option marked with [*] has a \-\-no\-OPTIONNAME variant, which reverses the sense of the option." - -${man_common}$ - -${man_others}$ - -.IP "Each option marked with [*] has a \-\-no\-OPTIONNAME variant, which reverses the sense of the option." - -.\".SH FILES -.\".SH ENVIRONMENT -.SH DIAGNOSTICS -.B CVC4 -reports all syntactic and semantic errors on standard error. -.SH HISTORY -The -.B CVC4 -effort is the culmination of fifteen years of theorem proving -research, starting with the -.I Stanford Validity Checker (SVC) -in 1996. - -SVC's successor, the -.I Cooperating Validity Checker (CVC), -had a more optimized internal design, produced proofs, used the -.I Chaff -SAT solver, and featured a number of usability -enhancements. Its name comes from the cooperative nature of -decision procedures in Nelson-Oppen theory combination, -which share amongst each other equalities between shared terms. - -CVC Lite, first made available in 2003, was a rewrite of CVC -that attempted to make CVC -more flexible (hence the \(lqlite\(rq) while extending the feature set: -CVCLite supported quantifiers where its predecessors did not. -CVC3 was a major overhaul of portions of CVC Lite: it added -better decision procedure implementations, added support for using -MiniSat in the core, and had generally better performance. - -CVC4 is the new version, the fifth generation of this validity -checker line that is now celebrating fifteen years of heritage. -It represents a complete re-evaluation of -the core architecture to be both performant and to serve as a cutting-edge research vehicle -for the next several years. Rather than taking CVC3 -and redesigning problem parts, we've taken a clean-room approach, -starting from scratch. Before using any designs from CVC3, we have -thoroughly scrutinized, vetted, and updated them. Many parts of CVC4 -bear only a superficial resemblance, if any, to their correspondent in CVC3. - -However, CVC4 is fundamentally similar to CVC3 and many other -modern SMT solvers: it is a DPLL( -.I T -) solver, -with a SAT solver at its core and a delegation path to different decision -procedure implementations, each in charge of solving formulas in some -background theory. - -The re-evaluation and ground-up rewrite was necessitated, we felt, by -the performance characteristics of CVC3. CVC3 has many useful -features, but some core aspects of the design led to high memory use, and -the use of heavyweight computation (where more nimble engineering -approaches could suffice) makes CVC3 a much slower prover than other tools. -As these designs are central to CVC3, a new version was preferable to a -selective re-engineering, which would have ballooned in short order. -.SH VERSION -This manual page refers to -.B CVC4 -version @VERSION@. -.SH BUGS -An issue tracker for the CVC4 project is maintained at -.BR https://github.com/CVC4/CVC4/issues . -.SH AUTHORS -.B CVC4 -is developed by a team of researchers at Stanford University -and the University of Iowa. -See the AUTHORS file in the distribution for a full list of -contributors. -.SH "SEE ALSO" -.BR libcvc4 (3), -.BR libcvc4parser (3) - -Additionally, the CVC4 wiki contains useful information about the -design and internals of CVC4. It is maintained at -.BR http://cvc4.cs.stanford.edu/wiki/ . diff --git a/doc/cvc5.5.in b/doc/cvc5.5.in deleted file mode 100644 index d66110f63..000000000 --- a/doc/cvc5.5.in +++ /dev/null @@ -1,20 +0,0 @@ -.\" Process this file with -.\" groff -man -Tascii cvc4.5 -.\" -.TH CVC4 5 "@MAN_DATE@" "CVC4 release @VERSION@" "Languages documentation" -.SH NAME -cvc4 \- the native input language for CVC4 -.SH DESCRIPTION -.B cvc4 -is an automated theorem prover for first-order formulas with respect -to background theories of interest. - -.SH HISTORY -.SH "SEE ALSO" -.BR cvc4 (1), -.BR libcvc4 (3), -.BR libcvc4parser (3) - -Additionally, the CVC4 wiki contains useful information about the -design and internals of CVC4. It is maintained at -.BR http://cvc4.cs.stanford.edu/wiki/ . diff --git a/doc/find_public_interface.sh b/doc/find_public_interface.sh deleted file mode 100755 index 4609846f7..000000000 --- a/doc/find_public_interface.sh +++ /dev/null @@ -1,20 +0,0 @@ -#!/bin/bash -# -# Enumerates public interface headers, so that public-only documentation -# can be produced. -# - -cd "$(dirname "$0")" - -echo -n "\"$srcdir/src/include/cvc4.h\" " -echo -n "\"$srcdir/src/include/cvc4_public.h\" " -( (find "$builddir" -name '*.h' | xargs grep -l '^# *include *"cvc4.*_public\.h"'); \ - (find "$srcdir" -name '*.h' | xargs grep -l '^# *include *"cvc4.*_public\.h"'); \ -) | \ -while read f; do - if expr "$f" : ".*_\(template\|private\|test_utils\)\.h$" &>/dev/null; then - continue - fi - echo -n "\"$f\" " -done - diff --git a/doc/libcvc5.3.in b/doc/libcvc5.3.in deleted file mode 100644 index 1db5b3c2d..000000000 --- a/doc/libcvc5.3.in +++ /dev/null @@ -1,64 +0,0 @@ -.\" Process this file with -.\" groff -man -Tascii libcvc4.3 -.\" -.TH LIBCVC4 3 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Library Interfaces" -.SH NAME -libcvc4 \- a library interface for the CVC4 theorem prover -.SH SYNOPSIS - -A small program like: - -.RS -.nf -#include -#include "expr/expr_manager.h" -#include "smt/smt_engine.h" - -using namespace CVC4; - -int main() { - ExprManager em; - SmtEngine smt(&em); - Expr onePlusTwo = em.mkExpr(kind::PLUS, - em.mkConst(Rational(1)), - em.mkConst(Rational(2))); - std::cout << language::SetLanguage(language::output::LANG_CVC4) - << smt.getInfo("name") - << " says that 1 + 2 = " - << smt.simplify(onePlusTwo) - << std::endl; - - return 0; -} -.fi -.RE - -gives the output: - -.RS -"cvc4" says that 1 + 2 = 3 -.RE - -.SH DESCRIPTION - -The main classes of interest in CVC4's API are -.I ExprManager, -.I SmtEngine, -and a few related ones like -.I Expr -and -.I Type. - -The -.I ExprManager -is used to build up expressions and types, and the -.I SmtEngine -is used primarily to make assertions, check satisfiability/validity, and extract models and proofs. - -.SH "SEE ALSO" -.BR cvc4 (1), -.BR libcvc4parser (3) - -Additionally, the CVC4 wiki contains useful information about the -design and internals of CVC4. It is maintained at -.BR http://cvc4.cs.stanford.edu/wiki/ . diff --git a/doc/libcvc5parser.3.in b/doc/libcvc5parser.3.in deleted file mode 100644 index f288daf83..000000000 --- a/doc/libcvc5parser.3.in +++ /dev/null @@ -1,14 +0,0 @@ -.\" Process this file with -.\" groff -man -Tascii libcvc4parser.3 -.\" -.TH LIBCVC4PARSER 3 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Library Interfaces" -.SH NAME -libcvc4parser \- a parser library interface for the CVC4 theorem prover -.SH DESCRIPTION -.SH "SEE ALSO" -.BR cvc4 (1), -.BR libcvc4 (3) - -Additionally, the CVC4 wiki contains useful information about the -design and internals of CVC4. It is maintained at -.BR http://cvc4.cs.stanford.edu/wiki/ . diff --git a/doc/options.3cvc_template.in b/doc/options.3cvc_template.in deleted file mode 100644 index 7eb472a32..000000000 --- a/doc/options.3cvc_template.in +++ /dev/null @@ -1,42 +0,0 @@ -.\" Process this file with -.\" groff -man -Tascii options.3cvc -.\" -.TH OPTIONS 3cvc "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Internals Documentation" -.SH NAME -options \- the options infrastructure - -.SH AVAILABLE INTERNAL OPTIONS - -.ad l - -.RS -.TP 10 -.I "COMMON OPTIONS" -${man_common_internals}$ - -${man_others_internals}$ -.PD -.RE - -.ad b - -.SH VERSION -This manual page refers to -.B CVC4 -version @VERSION@. -.SH BUGS -An issue tracker for the CVC4 project is maintained at -.BR https://github.com/CVC4/CVC4/issues . -.SH AUTHORS -.B CVC4 -is developed by a team of researchers at Stanford University -and the University of Iowa. -See the AUTHORS file in the distribution for a full list of -contributors. -.SH "SEE ALSO" -.BR libcvc4 (3), -.BR libcvc4parser (3) - -Additionally, the CVC4 wiki contains useful information about the -design and internals of CVC4. It is maintained at -.BR http://cvc4.cs.stanford.edu/wiki/ . diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 424f5e0df..df632224c 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -78,7 +78,6 @@ add_custom_command( ${PYTHON_EXECUTABLE} ${CMAKE_CURRENT_LIST_DIR}/mkoptions.py ${CMAKE_CURRENT_LIST_DIR} - ${CMAKE_CURRENT_BINARY_DIR}/../../doc ${CMAKE_CURRENT_BINARY_DIR} ${abs_toml_files} DEPENDS @@ -88,9 +87,6 @@ add_custom_command( module_template.cpp options_holder_template.h options_template.cpp - ${CMAKE_CURRENT_BINARY_DIR}/../../doc/cvc5.1_template - ${CMAKE_CURRENT_BINARY_DIR}/../../doc/SmtEngine.3cvc_template - ${CMAKE_CURRENT_BINARY_DIR}/../../doc/options.3cvc_template ) add_custom_target(gen-options diff --git a/src/options/README b/src/options/README index 8c41a28bb..5467d20c4 100644 --- a/src/options/README +++ b/src/options/README @@ -7,7 +7,7 @@ Modules name ... (string) name of the module (e.g., "Arithmetic Theory") header ... (string) name of the options header to generated (e.g., "options/arith_options.h") - A module defines 0 or more options and/or aliases. + A module defines 0 or more options. In general, each attribute/value pair is required to be in one line. Comments start with # and are not allowed in attribute/value lines. @@ -40,10 +40,7 @@ Options option predicates ... (list) functions that check whether given option value is valid - includes ... (list) header files required by - handler/predicates/notifies - notifies ... (list) notifications to call when option is set - links ... (list) additional options to set after this option is set + includes ... (list) header files required by handler/predicates read_only ... (bool) true: option should not provide a ::set method, false (default): option should provide a ::set method to set the option value @@ -57,7 +54,7 @@ Options to false. This behaviour can be explicitely disabled for options with attribute alternate = false. - More information on how to use handler, predicates and notifies can be found + More information on how to use handler and predicates can be found at the end of the README. @@ -74,74 +71,10 @@ Options handler = "stringToOutputLanguage" predicates = [] includes = ["options/language.h"] - notifies = [] - links = [] read_only = false help = "force output language (default is \"auto\"; see --output-lang help)" - If an alternate option is generated, the linked options defined via attribute - links are not considered. If you want to define links for an alternate option - --no- for an existing option , you can define an alias with long - option no-. This overwrites the default --no- behaviour and - creates the linked options. - - -Aliases -======= - - Aliases can be defined with the [[alias]] tag, which creates a new long - option and binds it to the list of long options specified via the 'links' - attributes. - - - The required attributes are: - - category ... (string) common | expert | regular | undocumented - long ... (string) long option name - links ... (list) list of long options to set - - Optional attributes are: - - help ... (string) documentation (only option for category undocumented) - - - Example: - - [[alias]] - category = "regular" - long = "smtlib-strict" - links = ["--lang=smt2", "--output-lang=smt2", "--strict-parsing", "--expr-depth=-1", "--print-success", "--incremental", "--abstract-values"] - help = "SMT-LIBv2 compliance mode (implies other options)" - - - This example creates a regular option with the long option name - 'smtlib-strict', which links to the long options given as a list 'links'. - Calling - - --smtlib-strict - - is equivalent to specifying the options - - --lang=smt2 --output-lang=smt2 --strict-parsing --expr-depth=-1 --print-success --incremental --abstract-values - - - It's also possible to pass an argument through to another option. - - Example: - - [[alias]] - category = "undocumented" - long = "output-language=L" - links = ["--output-lang=L"] - - This alias makes --output-language synonymous with --output-lang and passes - argument L through to --output-lang. The placeholer name (in this example - 'L') of the argument can be arbitrarily chosen and can be referenced multiple - times in 'links'. - - - Further information (the old option package) ============================================ @@ -150,7 +83,6 @@ Further information (the old option package) - handler to parse an option before setting its value. - predicates to reject bad values for the option. - - notifies for dynamic dispatch after an option is assigned. More details on each class of custom handlers. @@ -169,12 +101,11 @@ Further information (the old option package) T OptionsHandler::custom-option-handler(std::string option, std::string optarg); - The handlers are run before predicates and notifications. + The handlers are run before predicates. Having multiple handlers is considered bad practice and is unsupported. Handlers may have arbitrary side effects, but should call no code inaccessible to liboptions. For side effects that are not required in order - to parse the option, using :predicate is recommended. Use :notify to - achieve dynamic dispatch outside of base/, lib/, and options/. Memory + to parse the option, using :predicate is recommended. Memory management done by a handler needs to either be encapsulated by the type and the destructor for the type or should *always* be owned by handler. More elaborate memory management schemes are not currently supported. @@ -182,8 +113,7 @@ Further information (the old option package) - predicates = [...] Predicates provide support for checking whether or not the value of an - option is acceptable. Predicates are run after handlers and before - notifications. + option is acceptable. Predicates are run after handlers. The signature for a predicate call is: void custom-predicate(std::string option, T value, @@ -195,35 +125,7 @@ Further information (the old option package) void OptionsHandler::custom-predicate(std::string option, T value); - The predicates are run after handlers and before notifications. Multiple + The predicates are run after handlers. Multiple predicates may be defined for the same option, but the order they are run is not guaranteed. Predicates may have arbitrary side effects, but should - call no code inaccessible to liboptions. Use :notify to - achieve dynamic dispatch outside of base/, lib/, and options/. - Predicates are expected to reject bad value for the option by throwing an - OptionsException. - - - notifies = [...] - - This allows for the installation of custom post-processing callbacks using - the Listener infrastructure. custom-option-notification is a C++ function - that is called after the assignment of the option is updated. - The normal usage of an notify is to call a Listener that is registered for - this specific option. This is how dynamic dispatch outside of the - liboptions package should always be done. - The signature of custom-option-notification should take an option name as - well as an OptionsHandler*. - - void custom-notification( - const std::string& option, cvc5::options::OptionsHandler* handler); - - The name is provided so multiple options can use the same notification - implementation. - This is called after all handlers and predicates have been run. - Formally, this is always placed at the end of either the generated - Options::assign or Options::assignBool function for the option. - Because of this :notify cannot be used with void type options. - Users of this feature should *always* check the code generated in - builds/src/options/options.cpp for the correctness of the placement of the - generated code. The Listener notify() function is allowed to throw - an arbitrary std::exception. + call no code inaccessible to liboptions. diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index c28a6f0cf..9c66c6b61 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -18,10 +18,9 @@ has changed (in order to avoid global re-compilation if only single option files changed). - mkoptions.py + + mkoptions.py + location of all *_template.{cpp,h} files - location of all *_template documentation files destination directory for the generated source code files + one or more *_options.toml files @@ -32,14 +31,6 @@ - options_holder_template.h - module_template.h - Directory must contain: - - cvc5.1_template - - options.3cvc_template - - SmtEngine.3cvc_template - These files get generated during autogen.sh from the corresponding *.in - files in doc/. Note that for the generated documentation files tpl-doc is - also the destination directory. - + must be the list of all *.toml option configuration files from the src/options directory. @@ -49,33 +40,26 @@ - /MODULE_options.cpp - /options_holder.h - /options.cpp - - /cvc5.1 - - /options.3 - - /SmtEngine.3 """ -import ast import os import re import sys import textwrap import toml -### Allowed attributes for module/option/alias +### Allowed attributes for module/option MODULE_ATTR_REQ = ['id', 'name', 'header'] -MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['option', 'alias'] +MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['option'] OPTION_ATTR_REQ = ['category', 'type'] OPTION_ATTR_ALL = OPTION_ATTR_REQ + [ 'name', 'help', 'help_mode', 'smt_name', 'short', 'long', 'default', - 'includes', 'handler', 'predicates', 'notifies', 'links', 'read_only', + 'includes', 'handler', 'predicates', 'read_only', 'alternate', 'mode' ] -ALIAS_ATTR_REQ = ['category', 'long', 'links'] -ALIAS_ATTR_ALL = ALIAS_ATTR_REQ + ['help'] - CATEGORY_VALUES = ['common', 'expert', 'regular', 'undocumented'] SUPPORTED_CTYPES = ['int', 'unsigned', 'unsigned long', 'long', 'float', @@ -122,7 +106,6 @@ TPL_IMPL_ASSIGN = TPL_DECL_ASSIGN[:-1] + \ runHandlerAndPredicates(options::{name}, option, value, d_handler); d_holder->{name}__setByUser__ = true; Trace("options") << "user assigned option {name}" << std::endl; - {notifications} }}""" @@ -149,7 +132,6 @@ TPL_IMPL_ASSIGN_BOOL = TPL_DECL_ASSIGN_BOOL[:-1] + \ d_holder->{name} = value; d_holder->{name}__setByUser__ = true; Trace("options") << "user assigned option {name}" << std::endl; - {notifications} }}""" TPL_CALL_ASSIGN_BOOL = \ @@ -314,12 +296,11 @@ class Module(object): """Options module. An options module represents a MODULE_options.toml option configuration - file and contains lists of options and aliases. + file and contains lists of options. """ def __init__(self, d): self.__dict__ = dict((k, None) for k in MODULE_ATTR_ALL) self.options = [] - self.aliases = [] for (attr, val) in d.items(): assert attr in self.__dict__ if val: @@ -336,8 +317,6 @@ class Option(object): self.__dict__ = dict((k, None) for k in OPTION_ATTR_ALL) self.includes = [] self.predicates = [] - self.notifies = [] - self.links = [] self.read_only = False self.alternate = True # add --no- alternative long option for bool self.filename = None @@ -347,39 +326,16 @@ class Option(object): self.__dict__[attr] = val -class Alias(object): - """Module alias. - - An instance of this class corresponds to an alias defined in a - MODULE_options.toml configuration file specified via [[alias]]. - """ - def __init__(self, d): - self.__dict__ = dict((k, None) for k in ALIAS_ATTR_ALL) - self.links = [] - self.filename = None - self.alternate_for = None # replaces a --no- alternative for an option - for (attr, val) in d.items(): - assert attr in self.__dict__ - if val: - self.__dict__[attr] = val - - def die(msg): sys.exit('[error] {}'.format(msg)) -def perr(filename, msg, option_or_alias = None): - msg_suffix = '' - if option_or_alias: - if isinstance(option_or_alias, Option): - msg_suffix = 'option ' - if option_or_alias.name: - msg_suffix = "{} '{}' ".format(msg_suffix, option_or_alias.name) - else: - msg_suffix = "{} '{}' ".format(msg_suffix, option_or_alias.long) +def perr(filename, msg, option = None): + if option: + if option.name: + msg_suffix = "option '{}' ".format(option.name) else: - assert isinstance(option_or_alias, Alias) - msg_suffix = "alias '{}' ".format(option_or_alias.long) + msg_suffix = "option '{}' ".format(option.long) die('parse error in {}: {}{}'.format(filename, msg, msg_suffix)) @@ -423,35 +379,6 @@ def read_tpl(directory, name): die("Could not find '{}'. Aborting.".format(fname)) -def match_option(long_name): - """ - Lookup option by long_name option name. The function returns a tuple of (option, - bool), where the bool indicates the option value (true if not alternate, - false if alternate option). - """ - global g_long_to_opt - val = True - opt = None - long_name = lstrip('--', long_get_option(long_name)) - if long_name.startswith('no-'): - opt = g_long_to_opt.get(lstrip('no-', long_name)) - # Check if we generated an alternative option - if opt and opt.type == 'bool' and opt.alternate: - val = False - else: - opt = g_long_to_opt.get(long_name) - return (opt, val) - - -def long_get_arg(name): - """ - Extract the argument part ARG of a long_name option long_name=ARG. - """ - long_name = name.split('=') - assert len(long_name) <= 2 - return long_name[1] if len(long_name) == 2 else None - - def long_get_option(name): """ Extract the name of a given long option long=ARG @@ -687,24 +614,16 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): def docgen(category, name, smt_name, short_name, long_name, ctype, default, - help_msg, alternate, - help_common, man_common, man_common_smt, man_common_int, - help_others, man_others, man_others_smt, man_others_int): + help_msg, alternate, help_common, help_others): """ - Generate the documentation for --help and all man pages. + Generate the documentation for --help. """ ### Generate documentation if category == 'common': doc_cmd = help_common - doc_man = man_common - doc_smt = man_common_smt - doc_int = man_common_int else: doc_cmd = help_others - doc_man = man_others - doc_smt = man_others_smt - doc_int = man_others_int help_msg = help_msg if help_msg else '[undocumented]' if category == 'expert': @@ -719,60 +638,16 @@ def docgen(category, name, smt_name, short_name, long_name, ctype, default, help_cmd += ' [*]' doc_cmd.extend(help_format(help_cmd, opts)) - # Generate man page documentation for cmdline options - doc_man.append('.IP "{}"'.format(opts.replace('-', '\\-'))) - doc_man.append(help_cmd.replace('-', '\\-')) - - # Escape - with \- for man page documentation - help_msg = help_msg.replace('-', '\\-') - - # Generate man page documentation for smt options - if smt_name or long_name: - smtname = smt_name if smt_name else long_get_option(long_name) - doc_smt.append('.TP\n.B "{}"'.format(smtname)) - if ctype: - doc_smt.append('({}) {}'.format(ctype, help_msg)) - else: - doc_smt.append(help_msg) - - # Generate man page documentation for internal options - if name: - doc_int.append('.TP\n.B "{}"'.format(name)) - if default: - assert ctype - doc_int.append('({}, default = {})'.format( - ctype, - default.replace('-', '\\-'))) - elif ctype: - doc_int.append('({})'.format(ctype)) - doc_int.append('.br\n{}'.format(help_msg)) - - -def docgen_option(option, - help_common, man_common, man_common_smt, man_common_int, - help_others, man_others, man_others_smt, man_others_int): +def docgen_option(option, help_common, help_others): """ Generate documentation for options. """ docgen(option.category, option.name, option.smt_name, option.short, option.long, option.type, option.default, option.help, option.alternate, - help_common, man_common, man_common_smt, man_common_int, - help_others, man_others, man_others_smt, man_others_int) - - -def docgen_alias(alias, - help_common, man_common, man_common_smt, man_common_int, - help_others, man_others, man_others_smt, man_others_int): - """ - Generate documentation for aliases. - """ - docgen(alias.category, None, None, - None, alias.long, None, None, - alias.help, None, - help_common, man_common, man_common_smt, man_common_int, - help_others, man_others, man_others_smt, man_others_int) + help_common, + help_others) def add_getopt_long(long_name, argument_req, getopt_long): @@ -789,8 +664,7 @@ def add_getopt_long(long_name, argument_req, getopt_long): 'required' if argument_req else 'no', value)) -def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, - doc_dir, tpl_man_cvc, tpl_man_smt, tpl_man_int): +def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder): """ Generate code for all option modules (options.cpp, options_holder.h). """ @@ -810,25 +684,13 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, setoption_handlers = [] # handlers for set-option command getoption_handlers = [] # handlers for get-option command - # other documentation - man_common = [] - man_others = [] - man_common_smt = [] - man_others_smt = [] - man_common_int = [] - man_others_int = [] - for module in modules: headers_module.append(format_include(module.header)) macros_module.append(TPL_HOLDER_MACRO_NAME.format(id=module.id)) - if module.options or module.aliases: + if module.options: help_others.append( '"\\nFrom the {} module:\\n"'.format(module.name)) - man_others.append('.SH {} OPTIONS'.format(module.name.upper())) - man_others_smt.append( - '.TP\n.I "{} OPTIONS"'.format(module.name.upper())) - man_others_int.append(man_others_smt[-1]) for option in \ sorted(module.options, key=lambda x: x.long if x.long else x.name): @@ -836,10 +698,7 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, assert option.name or option.smt_name or option.short or option.long argument_req = option.type not in ['bool', 'void'] - docgen_option(option, - help_common, man_common, man_common_smt, - man_common_int, help_others, man_others, - man_others_smt, man_others_int) + docgen_option(option, help_common, help_others) # Generate handler call handler = None @@ -868,11 +727,6 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, ['handler->{}(option, retval);'.format(x) \ for x in option.predicates] - # Generate notification calls - notifications = \ - ['d_handler->{}(option);'.format(x) for x in option.notifies] - - # Generate options_handler and getopt_long cases = [] if option.short: @@ -905,9 +759,6 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, elif handler: cases.append('{};'.format(handler)) - cases.extend( - [TPL_PUSHBACK_PREEMPT.format('"{}"'.format(x)) \ - for x in option.links]) cases.append(' break;\n') options_handler.extend(cases) @@ -915,18 +766,6 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, # Generate handlers for setOption/getOption if option.smt_name or option.long: - smtlinks = [] - for link in option.links: - m = match_option(link) - assert m - smtname = get_smt_name(m[0]) - assert smtname - smtlinks.append( - TPL_CALL_SET_OPTION.format( - smtname=smtname, - value='true' if m[1] else 'false' - )) - # Make smt_name and long name available via set/get-option keys = set() if option.smt_name: @@ -960,8 +799,6 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, setoption_handlers.append( h.format(handler=option.handler, smtname=smtname)) - if smtlinks: - setoption_handlers.append('\n'.join(smtlinks)) setoption_handlers.append('return;') setoption_handlers.append('}') @@ -1056,8 +893,7 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, tpl = TPL_IMPL_ASSIGN if tpl: custom_handlers.append(tpl.format( - name=option.name, - notifications='\n'.join(notifications) + name=option.name )) # Default option values @@ -1068,48 +904,6 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, defaults.append('{}({})'.format(option.name, default)) defaults.append('{}__setByUser__(false)'.format(option.name)) - - for alias in sorted(module.aliases, key=lambda x: x.long): - argument_req = '=' in alias.long - - options_handler.append( - 'case {}:// --{}'.format( - g_getopt_long_start + len(getopt_long), alias.long)) - - # If an alias replaces and alternate --no- option, we have to set - # the corresponding option to false - if alias.alternate_for: - assert alias.alternate_for.name - options_handler.append( - TPL_CALL_ASSIGN_BOOL.format( - name=alias.alternate_for.name, - option='option', value='false')) - - assert alias.links - arg = long_get_arg(alias.long) - for link in alias.links: - arg_link = long_get_arg(link) - if arg == arg_link: - options_handler.append( - TPL_PUSHBACK_PREEMPT.format( - '"{}"'.format(long_get_option(link)))) - if argument_req: - options_handler.append( - TPL_PUSHBACK_PREEMPT.format('optionarg.c_str()')) - else: - options_handler.append( - TPL_PUSHBACK_PREEMPT.format('"{}"'.format(link))) - - options_handler.append(' break;\n') - - add_getopt_long(alias.long, argument_req, getopt_long) - - docgen_alias(alias, - help_common, man_common, man_common_smt, - man_common_int, help_others, man_others, - man_others_smt, man_others_int) - - write_file(dst_dir, 'options_holder.h', tpl_options_holder.format( headers_module='\n'.join(headers_module), macros_module='\n '.join(macros_module) @@ -1133,21 +927,6 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, getoption_handlers='\n'.join(getoption_handlers) )) - write_file(doc_dir, 'cvc5.1', tpl_man_cvc.format( - man_common='\n'.join(man_common), - man_others='\n'.join(man_others) - )) - - write_file(doc_dir, 'SmtEngine.3cvc', tpl_man_smt.format( - man_common_smt='\n'.join(man_common_smt), - man_others_smt='\n'.join(man_others_smt) - )) - - write_file(doc_dir, 'options.3cvc', tpl_man_int.format( - man_common_internals='\n'.join(man_common_int), - man_others_internals='\n'.join(man_others_int) - )) - def lstrip(prefix, s): """ @@ -1156,16 +935,9 @@ def lstrip(prefix, s): return s[len(prefix):] if s.startswith(prefix) else s -def rstrip(suffix, s): - """ - Remove suffix from the end of string s. - """ - return s[:-len(suffix)] if s.endswith(suffix) else s - - def check_attribs(filename, req_attribs, valid_attribs, attribs, ctype): """ - Check if for a given module/option/alias the defined attributes are valid and + Check if for a given module/option the defined attributes are valid and if all required attributes are defined. """ msg_for = "" @@ -1196,7 +968,7 @@ def check_unique(filename, value, cache): cache[value] = filename -def check_long(filename, option_or_alias, long_name, ctype=None): +def check_long(filename, option, long_name, ctype=None): """ Check if given long option name is valid. """ @@ -1204,35 +976,18 @@ def check_long(filename, option_or_alias, long_name, ctype=None): if long_name is None: return if long_name.startswith('--'): - perr(filename, 'remove -- prefix from long', option_or_alias) + perr(filename, 'remove -- prefix from long', option) r = r'^[0-9a-zA-Z\-=]+$' if not re.match(r, long_name): perr(filename, "long '{}' does not match regex criteria '{}'".format( - long_name, r), option_or_alias) + long_name, r), option) name = long_get_option(long_name) check_unique(filename, name, g_long_cache) if ctype == 'bool': check_unique(filename, 'no-{}'.format(name), g_long_cache) -def check_links(filename, option_or_alias): - """ - Check if long options defined in links are valid and correctly used. - """ - global g_long_cache, g_long_arguments - for link in option_or_alias.links: - long_name = lstrip('no-', lstrip('--', long_get_option(link))) - if long_name not in g_long_cache: - perr(filename, - "invalid long option '{}' in links list".format(link), - option_or_alias) - # check if long option requires an argument - if long_name in g_long_arguments and '=' not in link: - perr(filename, - "linked option '{}' requires an argument".format(link), - option_or_alias) - def parse_module(filename, module): """ @@ -1251,7 +1006,6 @@ def parse_module(filename, module): if 'option' in module: for attribs in module['option']: - lineno = 0 check_attribs(filename, OPTION_ATTR_REQ, OPTION_ATTR_ALL, attribs, 'option') option = Option(attribs) @@ -1280,23 +1034,13 @@ def parse_module(filename, module): option.filename = filename res.options.append(option) - if 'alias' in module: - for attribs in module['alias']: - lineno = 0 - check_attribs(filename, - ALIAS_ATTR_REQ, ALIAS_ATTR_ALL, attribs, 'alias') - alias = Alias(attribs) - alias.filename = filename - res.aliases.append(alias) - return res def usage(): - print('mkoptions.py +') + print('mkoptions.py +') print('') print(' location of all *_template.{cpp,h} files') - print(' location of all *_template documentation files') print(' destination directory for the generated files') print(' + one or more *_optios.toml files') print('') @@ -1308,12 +1052,11 @@ def mkoptions_main(): die('missing arguments') src_dir = sys.argv[1] - doc_dir = sys.argv[2] - dst_dir = sys.argv[3] - filenames = sys.argv[4:] + dst_dir = sys.argv[2] + filenames = sys.argv[3:] # Check if given directories exist. - for d in [src_dir, doc_dir, dst_dir]: + for d in [src_dir, dst_dir]: if not os.path.isdir(d): usage() die("'{}' is not a directory".format(d)) @@ -1329,11 +1072,6 @@ def mkoptions_main(): tpl_options = read_tpl(src_dir, 'options_template.cpp') tpl_options_holder = read_tpl(src_dir, 'options_holder_template.h') - # Read documentation template files from documentation directory. - tpl_man_cvc = read_tpl(doc_dir, 'cvc5.1_template') - tpl_man_smt = read_tpl(doc_dir, 'SmtEngine.3cvc_template') - tpl_man_int = read_tpl(doc_dir, 'options.3cvc_template') - # Parse files, check attributes and create module/option objects modules = [] for filename in filenames: @@ -1351,40 +1089,12 @@ def mkoptions_main(): g_long_arguments.add(long_get_option(option.long)) modules.append(module) - # Check if alias.long is unique and check if alias.long defines an alias - # for an alternate (--no-) option for existing option . - for module in modules: - for alias in module.aliases: - # If an alias defines a --no- alternative for an existing boolean - # option, we do not create the alternative for the option, but use - # the alias instead. - if alias.long.startswith('no-'): - m = match_option(alias.long) - if m[0] and m[0].type == 'bool': - m[0].alternate = False - alias.alternate_for = m[0] - del g_long_cache[alias.long] - check_long(alias.filename, alias, alias.long) - # Add long option that requires an argument - if '=' in alias.long: - g_long_arguments.add(long_get_option(alias.long)) - - # Check if long options in links are valid (that needs to be done after all - # long options are available). - for module in modules: - for option in module.options: - check_links(option.filename, option) - for alias in module.aliases: - check_links(alias.filename, alias) - # Create *_options.{h,cpp} in destination directory for module in modules: codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp) # Create options.cpp and options_holder.h in destination directory - codegen_all_modules(modules, - dst_dir, tpl_options, tpl_options_holder, - doc_dir, tpl_man_cvc, tpl_man_smt, tpl_man_int) + codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder)