+++ /dev/null
-.\" 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/ .
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.
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
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.
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-<long> for an existing option <long>, you can define an alias with long
- option no-<long>. This overwrites the default --no-<long> 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)
============================================
- 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.
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.
- 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,
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.
has changed (in order to avoid global re-compilation if only single option
files changed).
- mkoptions.py <tpl-src> <tpl-doc> <dst> <toml>+
+ mkoptions.py <tpl-src> <dst> <toml>+
<tpl-src> location of all *_template.{cpp,h} files
- <tpl-doc> location of all *_template documentation files
<dst> destination directory for the generated source code files
<toml>+ one or more *_options.toml files
- options_holder_template.h
- module_template.h
- Directory <tpl-doc> 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.
-
<toml>+ must be the list of all *.toml option configuration files from
the src/options directory.
- <dst>/MODULE_options.cpp
- <dst>/options_holder.h
- <dst>/options.cpp
- - <tpl-doc>/cvc5.1
- - <tpl-doc>/options.3
- - <tpl-doc>/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',
runHandlerAndPredicates(options::{name}, option, value, d_handler);
d_holder->{name}__setByUser__ = true;
Trace("options") << "user assigned option {name}" << std::endl;
- {notifications}
}}"""
d_holder->{name} = value;
d_holder->{name}__setByUser__ = true;
Trace("options") << "user assigned option {name}" << std::endl;
- {notifications}
}}"""
TPL_CALL_ASSIGN_BOOL = \
"""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:
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
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))
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
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':
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):
'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).
"""
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):
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
['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:
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)
# 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:
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('}')
tpl = TPL_IMPL_ASSIGN
if tpl:
custom_handlers.append(tpl.format(
- name=option.name,
- notifications='\n'.join(notifications)
+ name=option.name
))
# Default option values
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)
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):
"""
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 = ""
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.
"""
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):
"""
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)
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 <tpl-src> <tpl-doc> <dst> <toml>+')
+ print('mkoptions.py <tpl-src> <dst> <toml>+')
print('')
print(' <tpl-src> location of all *_template.{cpp,h} files')
- print(' <tpl-doc> location of all *_template documentation files')
print(' <dst> destination directory for the generated files')
print(' <toml>+ one or more *_optios.toml files')
print('')
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))
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:
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-<long>) option for existing option <long>.
- 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)
projects / cvc5.git / commitdiff