diff options
Diffstat (limited to 'src')
196 files changed, 2184 insertions, 1225 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ba88080b8..ecfef1c22 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -182,6 +182,8 @@ libcvc5_add_sources( proof/lfsc/lfsc_list_sc_node_converter.h proof/lfsc/lfsc_node_converter.cpp proof/lfsc/lfsc_node_converter.h + proof/lfsc/lfsc_print_channel.cpp + proof/lfsc/lfsc_print_channel.h proof/lfsc/lfsc_util.cpp proof/lfsc/lfsc_util.h proof/method_id.cpp @@ -292,6 +294,8 @@ libcvc5_add_sources( smt/check_models.h smt/command.cpp smt/command.h + smt/difficulty_post_processor.cpp + smt/difficulty_post_processor.h smt/dump.cpp smt/dump.h smt/dump_manager.cpp @@ -686,6 +690,8 @@ libcvc5_add_sources( theory/decision_manager.h theory/decision_strategy.cpp theory/decision_strategy.h + theory/difficulty_manager.cpp + theory/difficulty_manager.h theory/ee_manager.cpp theory/ee_manager.h theory/ee_manager_central.cpp @@ -855,6 +861,8 @@ libcvc5_add_sources( theory/quantifiers/quantifiers_macros.h theory/quantifiers/quantifiers_modules.cpp theory/quantifiers/quantifiers_modules.h + theory/quantifiers/quantifiers_preprocess.cpp + theory/quantifiers/quantifiers_preprocess.h theory/quantifiers/quantifiers_registry.cpp theory/quantifiers/quantifiers_registry.h theory/quantifiers/quantifiers_rewriter.cpp diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index d41af938a..b1fb80336 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -60,6 +60,7 @@ #include "options/option_exception.h" #include "options/options.h" #include "options/options_public.h" +#include "options/outputc.h" #include "options/smt_options.h" #include "proof/unsat_core.h" #include "smt/model.h" @@ -7937,6 +7938,21 @@ Statistics Solver::getStatistics() const return Statistics(d_smtEngine->getStatisticsRegistry()); } +std::ostream& Solver::getOutput(const std::string& tag) const +{ + // `Output(tag)` may raise an `OptionException`, which we do not want to + // forward as such. We thus do not use the standard exception handling macros + // here but roll our own. + try + { + return Output(tag); + } + catch (const cvc5::Exception& e) + { + throw CVC5ApiException("Invalid output tag " + tag); + } +} + } // namespace api } // namespace cvc5 diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index a221f3711..e02506d9c 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4352,6 +4352,13 @@ class CVC5_EXPORT Solver */ Statistics getStatistics() const; + /** + * Returns an output stream for the given tag. Tags can be enabled with the + * `output` option (and `-o <tag>` on the command line). Raises an exception + * when an invalid tag is given. + */ + std::ostream& getOutput(const std::string& tag) const; + private: /** @return the node manager of this solver */ NodeManager* getNodeManager(void) const; diff --git a/src/main/options_template.cpp b/src/main/options_template.cpp index 87a5fc158..dfd93843e 100644 --- a/src/main/options_template.cpp +++ b/src/main/options_template.cpp @@ -48,13 +48,14 @@ namespace cvc5::main { // clang-format off static const std::string commonOptionsDescription = - "Most commonly-used cvc5 options:\n" +R"FOOBAR(Most commonly-used cvc5 options: ${help_common}$ - ; +)FOOBAR"; static const std::string additionalOptionsDescription = - "Additional cvc5 options:\n" -${help_others}$; +R"FOOBAR(Additional cvc5 options: +${help_others}$ +)FOOBAR"; static const std::string optionsFootnote = "\n\ [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\ diff --git a/src/options/managed_streams.cpp b/src/options/managed_streams.cpp index 5053db9a8..81bb242cf 100644 --- a/src/options/managed_streams.cpp +++ b/src/options/managed_streams.cpp @@ -29,8 +29,6 @@ namespace cvc5 { -namespace detail { - std::string cvc5_errno_failreason() { #if HAVE_STRERROR_R @@ -72,6 +70,8 @@ std::string cvc5_errno_failreason() #endif /* HAVE_STRERROR_R */ } +namespace detail { + std::ostream* openOStream(const std::string& filename) { errno = 0; diff --git a/src/options/managed_streams.h b/src/options/managed_streams.h index f6fddc064..56bb21c2e 100644 --- a/src/options/managed_streams.h +++ b/src/options/managed_streams.h @@ -24,8 +24,6 @@ #include <memory> #include <ostream> -#include "options/options_public.h" - namespace cvc5 { namespace detail { diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 55e047047..f277a1967 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -11,34 +11,39 @@ # directory for licensing information. # ############################################################################# ## - """ Generate option handling code and documentation in one pass. The generated files are only written to the destination file if the contents of the file has changed (in order to avoid global re-compilation if only single option files changed). - mkoptions.py <tpl-src> <dst> <toml>+ + mkoptions.py <src> <build> <dst> <toml>+ - <tpl-src> location of all *_template.{cpp,h} files - <dst> destination directory for the generated source code files + <src> base source directory of all toml files + <build> build directory to write the generated sphinx docs + <dst> base destination directory for all generated files <toml>+ one or more *_options.toml files - Directory <tpl-src> must contain: - - options_template.cpp - - options_public_template.cpp - - module_template.cpp - - module_template.h + This script expects the following files (within <src>): + + - <src>/main/options_template.cpp + - <src>/options/module_template.cpp + - <src>/options/module_template.h + - <src>/options/options_public_template.cpp + - <src>/options/options_template.cpp + - <src>/options/options_template.h - <toml>+ must be the list of all *.toml option configuration files from - the src/options directory. + <toml>+ must be the list of all *.toml option configuration files. - The script generates the following files: - - <dst>/MODULE_options.h - - <dst>/MODULE_options.cpp - - <dst>/options.cpp + This script generates the following files: + - <dst>/main/options.cpp + - <dst>/options/<module>_options.cpp (for every toml file) + - <dst>/options/<module>_options.h (for every toml file) + - <dst>/options/options_public.cpp + - <dst>/options/options.cpp + - <dst>/options/options.h """ import os @@ -54,10 +59,9 @@ MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['option'] OPTION_ATTR_REQ = ['category', 'type'] OPTION_ATTR_ALL = OPTION_ATTR_REQ + [ - 'name', 'short', 'long', 'alias', - 'default', 'alternate', 'mode', - 'handler', 'predicates', 'includes', 'minimum', 'maximum', - 'help', 'help_mode' + 'name', 'short', 'long', 'alias', 'default', 'alternate', 'mode', + 'handler', 'predicates', 'includes', 'minimum', 'maximum', 'help', + 'help_mode' ] CATEGORY_VALUES = ['common', 'expert', 'regular', 'undocumented'] @@ -100,13 +104,6 @@ g_getopt_long_start = 256 ### Source code templates -TPL_ASSIGN = ''' opts.{module}.{name} = {handler}; - opts.{module}.{name}WasSetByUser = true;''' -TPL_ASSIGN_PRED = ''' auto value = {handler}; - {predicates} - opts.{module}.{name} = value; - opts.{module}.{name}WasSetByUser = true;''' - TPL_CALL_SET_OPTION = 'setOption(std::string("{smtname}"), ("{value}"));' TPL_GETOPT_LONG = '{{ "{}", {}_argument, nullptr, {} }},' @@ -176,41 +173,6 @@ TPL_MODE_HANDLER_CASE = \ }}""" -def get_module_headers(modules): - """Render includes for module headers""" - return concat_format('#include "{header}"', modules) - - -def get_holder_fwd_decls(modules): - """Render forward declaration of holder structs""" - return concat_format(' struct Holder{id_cap};', modules) - - -def get_holder_mem_decls(modules): - """Render declarations of holder members of the Option class""" - return concat_format(' std::unique_ptr<options::Holder{id_cap}> d_{id};', modules) - - -def get_holder_mem_inits(modules): - """Render initializations of holder members of the Option class""" - return concat_format(' d_{id}(std::make_unique<options::Holder{id_cap}>()),', modules) - - -def get_holder_ref_inits(modules): - """Render initializations of holder references of the Option class""" - return concat_format(' {id}(*d_{id}),', modules) - - -def get_holder_mem_copy(modules): - """Render copy operation of holder members of the Option class""" - return concat_format(' *d_{id} = *options.d_{id};', modules) - - -def get_holder_ref_decls(modules): - """Render reference declarations for holder members of the Option class""" - return concat_format(' options::Holder{id_cap}& {id};', modules) - - def get_handler(option): """Render handler call for assignment functions""" optname = option.long_name if option.long else "" @@ -241,11 +203,7 @@ def get_predicates(option): class Module(object): - """Options module. - - An options module represents a MODULE_options.toml option configuration - file and contains lists of options. - """ + """Represents one options module from one <module>_options.toml file.""" def __init__(self, d, filename): self.__dict__ = {k: d.get(k, None) for k in MODULE_ATTR_ALL} self.options = [] @@ -329,14 +287,207 @@ def generate_get_impl(modules): res.append('if ({}) {}'.format(cond, ret)) return '\n '.join(res) - def __lt__(self, other): - if self.long_name and other.long_name: - return self.long_name < other.long_name - if self.long_name: return True - return False - def __str__(self): - return self.long_name if self.long_name else self.name +def _set_handlers(option): + """Render handler call for options::set().""" + optname = option.long_name if option.long else "" + if option.handler: + if option.type == 'void': + return 'opts.handler().{}("{}", name)'.format( + option.handler, optname) + else: + return 'opts.handler().{}("{}", name, optionarg)'.format( + option.handler, optname) + elif option.mode: + return 'stringTo{}(optionarg)'.format(option.type) + return 'handlers::handleOption<{}>("{}", name, optionarg)'.format( + option.type, optname) + + +def _set_predicates(option): + """Render predicate calls for options::set().""" + if option.type == 'void': + return [] + optname = option.long_name if option.long else "" + assert option.type != 'void' + res = [] + if option.minimum: + res.append( + 'opts.handler().checkMinimum("{}", name, value, static_cast<{}>({}));' + .format(optname, option.type, option.minimum)) + if option.maximum: + res.append( + 'opts.handler().checkMaximum("{}", name, value, static_cast<{}>({}));' + .format(optname, option.type, option.maximum)) + res += [ + 'opts.handler().{}("{}", name, value);'.format(x, optname) + for x in option.predicates + ] + return res + + +TPL_SET = ''' opts.{module}.{name} = {handler}; + opts.{module}.{name}WasSetByUser = true;''' +TPL_SET_PRED = ''' auto value = {handler}; + {predicates} + opts.{module}.{name} = value; + opts.{module}.{name}WasSetByUser = true;''' + + +def generate_set_impl(modules): + """Generates the implementation for options::set().""" + res = [] + for module, option in all_options(modules, True): + if not option.long: + continue + cond = ' || '.join(['name == "{}"'.format(x) for x in option.names]) + predicates = _set_predicates(option) + if res: + res.append(' }} else if ({}) {{'.format(cond)) + else: + res.append('if ({}) {{'.format(cond)) + if option.name and not (option.handler and option.mode): + if predicates: + res.append( + TPL_SET_PRED.format(module=module.id, + name=option.name, + handler=_set_handlers(option), + predicates='\n '.join(predicates))) + else: + res.append( + TPL_SET.format(module=module.id, + name=option.name, + handler=_set_handlers(option))) + elif option.handler: + h = ' opts.handler().{handler}("{smtname}", name' + if option.type not in ['bool', 'void']: + h += ', optionarg' + h += ');' + res.append( + h.format(handler=option.handler, smtname=option.long_name)) + return '\n'.join(res) + + +################################################################################ +################################################################################ +# code generation functions + +################################################################################ +# for options/options.h + + +def generate_holder_fwd_decls(modules): + """Render forward declaration of holder structs""" + return concat_format(' struct Holder{id_cap};', modules) + + +def generate_holder_mem_decls(modules): + """Render declarations of holder members of the Option class""" + return concat_format( + ' std::unique_ptr<options::Holder{id_cap}> d_{id};', modules) + + +def generate_holder_ref_decls(modules): + """Render reference declarations for holder members of the Option class""" + return concat_format(' options::Holder{id_cap}& {id};', modules) + + +################################################################################ +# for options/options.cpp + + +def generate_module_headers(modules): + """Render includes for module headers""" + return concat_format('#include "{header}"', modules) + + +def generate_holder_mem_inits(modules): + """Render initializations of holder members of the Option class""" + return concat_format( + ' d_{id}(std::make_unique<options::Holder{id_cap}>()),', + modules) + + +def generate_holder_ref_inits(modules): + """Render initializations of holder references of the Option class""" + return concat_format(' {id}(*d_{id}),', modules) + + +def generate_holder_mem_copy(modules): + """Render copy operation of holder members of the Option class""" + return concat_format(' *d_{id} = *options.d_{id};', modules) + + +################################################################################ +# stuff for main/options.cpp + + +def _cli_help_format_options(option): + """ + Format short and long options for the cmdline documentation + (--long | --alias | -short). + """ + opts = [] + if option.long: + if option.long_opt: + opts.append('--{}={}'.format(option.long_name, option.long_opt)) + else: + opts.append('--{}'.format(option.long_name)) + + if option.alias: + if option.long_opt: + opts.extend( + ['--{}={}'.format(a, option.long_opt) for a in option.alias]) + else: + opts.extend(['--{}'.format(a) for a in option.alias]) + + if option.short: + if option.long_opt: + opts.append('-{} {}'.format(option.short, option.long_opt)) + else: + opts.append('-{}'.format(option.short)) + + return ' | '.join(opts) + + +def _cli_help_wrap(help_msg, opts): + """Format cmdline documentation (--help) to be 80 chars wide.""" + width_opt = 25 + text = textwrap.wrap(help_msg, 80 - width_opt, break_on_hyphens=False) + if len(opts) > width_opt - 3: + lines = [' {}'.format(opts), ' ' * width_opt + text[0]] + else: + lines = [' {}{}'.format(opts.ljust(width_opt - 2), text[0])] + lines.extend([' ' * width_opt + l for l in text[1:]]) + return lines + + +def generate_cli_help(modules): + """Generate the output for --help.""" + common = [] + others = [] + for module in modules: + if not module.options: + continue + others.append('') + others.append('From the {} module:'.format(module.name)) + for option in module.options: + if option.category == 'undocumented': + continue + msg = option.help + if option.category == 'expert': + msg += ' (EXPERTS only)' + opts = _cli_help_format_options(option) + if opts: + if option.alternate: + msg += ' [*]' + res = _cli_help_wrap(msg, opts) + + if option.category == 'common': + common.extend(res) + else: + others.extend(res) + return '\n'.join(common), '\n'.join(others) class SphinxGenerator: @@ -355,7 +506,7 @@ class SphinxGenerator: names.append('--{}={}'.format(option.long_name, option.long_opt)) else: names.append('--{}'.format(option.long_name)) - + if option.alias: if option.long_opt: names.extend(['--{}={}'.format(a, option.long_opt) for a in option.alias]) @@ -367,7 +518,7 @@ class SphinxGenerator: names.append('-{} {}'.format(option.short, option.long_opt)) else: names.append('-{}'.format(option.short)) - + modes = None if option.mode: modes = {} @@ -391,7 +542,7 @@ class SphinxGenerator: if module.name not in self.others: self.others[module.name] = [] self.others[module.name].append(data) - + def __render_option(self, res, opt): desc = '``{}``' val = ' {}' @@ -506,50 +657,6 @@ def format_include(include): return '#include "{}"'.format(include) -def help_format_options(option): - """ - Format short and long options for the cmdline documentation - (--long | --alias | -short). - """ - opts = [] - if option.long: - if option.long_opt: - opts.append('--{}={}'.format(option.long_name, option.long_opt)) - else: - opts.append('--{}'.format(option.long_name)) - - if option.alias: - if option.long_opt: - opts.extend(['--{}={}'.format(a, option.long_opt) for a in option.alias]) - else: - opts.extend(['--{}'.format(a) for a in option.alias]) - - if option.short: - if option.long_opt: - opts.append('-{} {}'.format(option.short, option.long_opt)) - else: - opts.append('-{}'.format(option.short)) - - return ' | '.join(opts) - - -def help_format(help_msg, opts): - """ - Format cmdline documentation (--help) to be 80 chars wide. - """ - width = 80 - width_opt = 25 - wrapper = \ - textwrap.TextWrapper(width=width - width_opt, break_on_hyphens=False) - text = wrapper.wrap(help_msg.replace('"', '\\"')) - if len(opts) > width_opt - 3: - lines = [' {}'.format(opts)] - lines.append(' ' * width_opt + text[0]) - else: - lines = [' {}{}'.format(opts.ljust(width_opt - 2), text[0])] - lines.extend([' ' * width_opt + l for l in text[1:]]) - return ['"{}\\n"'.format(x) for x in lines] - def help_mode_format(option): """ Format help message for mode options. @@ -702,34 +809,6 @@ def codegen_module(module, dst_dir, tpls): write_file(dst_dir, filename, tpl['content'].format(**data)) -def docgen_option(option, help_common, help_others): - """ - Generate documentation for options. - """ - - if option.category == 'undocumented': - return - - help_msg = option.help - if option.category == 'expert': - help_msg += ' (EXPERTS only)' - - opts = help_format_options(option) - - # Generate documentation for cmdline options - if opts and option.category != 'undocumented': - help_cmd = help_msg - if option.alternate: - help_cmd += ' [*]' - - res = help_format(help_cmd, opts) - - if option.category == 'common': - help_common.extend(res) - else: - help_others.extend(res) - - def add_getopt_long(long_name, argument_req, getopt_long): """ For each long option we need to add an instance of the option struct in @@ -745,31 +824,19 @@ def add_getopt_long(long_name, argument_req, getopt_long): def codegen_all_modules(modules, build_dir, dst_dir, tpls): - """ - Generate code for all option modules (options.cpp). - """ + """Generate code for all option modules.""" headers_module = [] # generated *_options.h header includes - headers_handler = set() # option includes (for handlers, predicates, ...) getopt_short = [] # short options for getopt_long getopt_long = [] # long options for getopt_long options_get_info = [] # code for getOptionInfo() options_handler = [] # option handler calls - help_common = [] # help text for all common options - help_others = [] # help text for all non-common options - setoption_handlers = [] # handlers for set-option command - - assign_impls = [] sphinxgen = SphinxGenerator() for module in modules: headers_module.append(format_include(module.header)) - if module.options: - help_others.append( - '"\\nFrom the {} module:\\n"'.format(module.name)) - for option in \ sorted(module.options, key=lambda x: x.long if x.long else x.name): assert option.type != 'void' or option.name is None @@ -777,16 +844,8 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls): mode_handler = option.handler and option.mode argument_req = option.type not in ['bool', 'void'] - docgen_option(option, help_common, help_others) - sphinxgen.add(module, option) - # Generate handler call - handler = get_handler(option) - - # Generate predicate calls - predicates = get_predicates(option) - # Generate options_handler and getopt_long cases = [] if option.short: @@ -868,32 +927,6 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls): else: options_get_info.append('if ({}) return OptionInfo{{"{}", {{{alias}}}, false, OptionInfo::VoidInfo{{}}}};'.format(cond, long_get_option(option.long), alias=alias)) - if setoption_handlers: - setoption_handlers.append(' }} else if ({}) {{'.format(cond)) - else: - setoption_handlers.append(' if ({}) {{'.format(cond)) - if option.name and not mode_handler: - if predicates: - setoption_handlers.append( - TPL_ASSIGN_PRED.format( - module=module.id, - name=option.name, - handler=handler, - predicates='\n '.join(predicates))) - else: - setoption_handlers.append( - TPL_ASSIGN.format( - module=module.id, - name=option.name, - handler=handler)) - elif option.handler: - h = ' opts.handler().{handler}("{smtname}", name' - if argument_req: - h += ', optionarg' - h += ');' - setoption_handlers.append( - h.format(handler=option.handler, smtname=option.long_name)) - # Add --no- alternative options for boolean options if option.long and option.alternate: cases = [] @@ -919,26 +952,29 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls): cases.append(' break;') options_handler.extend(cases) + help_common, help_others = generate_cli_help(modules) + data = { - 'holder_fwd_decls': get_holder_fwd_decls(modules), - 'holder_mem_decls': get_holder_mem_decls(modules), - 'holder_ref_decls': get_holder_ref_decls(modules), - 'headers_module': get_module_headers(modules), - 'headers_handler': '\n'.join(sorted(list(headers_handler))), - 'holder_mem_inits': get_holder_mem_inits(modules), - 'holder_ref_inits': get_holder_ref_inits(modules), - 'holder_mem_copy': get_holder_mem_copy(modules), + # options/options.h + 'holder_fwd_decls': generate_holder_fwd_decls(modules), + 'holder_mem_decls': generate_holder_mem_decls(modules), + 'holder_ref_decls': generate_holder_ref_decls(modules), + # options/options.cpp + 'headers_module': generate_module_headers(modules), + 'holder_mem_inits': generate_holder_mem_inits(modules), + 'holder_ref_inits': generate_holder_ref_inits(modules), + 'holder_mem_copy': generate_holder_mem_copy(modules), # options/options_public.cpp 'options_includes': generate_public_includes(modules), 'getnames_impl': generate_getnames_impl(modules), 'get_impl': generate_get_impl(modules), + 'set_impl': generate_set_impl(modules), 'cmdline_options': '\n '.join(getopt_long), - 'help_common': '\n'.join(help_common), - 'help_others': '\n'.join(help_others), + 'help_common': help_common, + 'help_others': help_others, 'options_handler': '\n '.join(options_handler), 'options_short': ''.join(getopt_short), 'options_get_info': '\n '.join(sorted(options_get_info)), - 'setoption_handlers': '\n'.join(setoption_handlers), } for tpl in tpls: write_file(dst_dir, tpl['output'], tpl['content'].format(**data)) @@ -1075,7 +1111,7 @@ def mkoptions_main(): for file in filenames: if not os.path.exists(file): die("configuration file '{}' does not exist".format(file)) - + module_tpls = [ {'input': 'options/module_template.h'}, {'input': 'options/module_template.cpp'}, diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp index 5b56933b5..4bd5239f6 100644 --- a/src/options/options_public_template.cpp +++ b/src/options/options_public_template.cpp @@ -211,27 +211,19 @@ namespace cvc5::options throw OptionException("Unrecognized option key or setting: " + name); } -void setInternal(Options & opts, const std::string& name, - const std::string& optionarg) -{ - // clang-format off -${setoption_handlers}$ - // clang-format on + void set( + Options & opts, const std::string& name, const std::string& optionarg) + { + Trace("options") << "set option " << name << " = " << optionarg + << std::endl; + // clang-format off + ${set_impl}$ + // clang-format on } else { throw OptionException("Unrecognized option key or setting: " + name); } - Trace("options") << "user assigned option " << name << " = " << optionarg << std::endl; -} - -void set(Options& opts, const std::string& name, const std::string& optionarg) -{ - - Trace("options") << "setOption(" << name << ", " << optionarg << ")" - << std::endl; - // first update this object - setInternal(opts, name, optionarg); } #if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE) diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 06a423438..c6f24a41d 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -16,21 +16,12 @@ #include "options/options.h" #include "base/check.h" -#include "base/exception.h" -#include "base/output.h" -#include "options/language.h" +#include "base/cvc5config.h" #include "options/options_handler.h" #include "options/options_listener.h" // clang-format off ${headers_module}$ - -#include "base/cvc5config.h" - -${headers_handler}$ - -using namespace cvc5; -using namespace cvc5::options; // clang-format on namespace cvc5 @@ -49,13 +40,15 @@ ${holder_ref_inits}$ Options::~Options() {} -void Options::copyValues(const Options& options){ - if(this != &options) { + void Options::copyValues(const Options& options) + { + if (this != &options) + { // clang-format off ${holder_mem_copy}$ // clang-format on + } } -} } // namespace cvc5 diff --git a/src/options/outputc.cpp b/src/options/outputc.cpp index e14519123..43c9ced97 100644 --- a/src/options/outputc.cpp +++ b/src/options/outputc.cpp @@ -18,6 +18,11 @@ Cvc5ostream OutputC::operator()(const options::OutputTag tag) const } } +Cvc5ostream OutputC::operator()(const std::string& tag) const +{ + return (*this)(options::stringToOutputTag(tag)); +} + bool OutputC::isOn(const options::OutputTag tag) const { return options::outputTagHolder()[static_cast<size_t>(tag)]; diff --git a/src/options/outputc.h b/src/options/outputc.h index 647b891db..d96468e40 100644 --- a/src/options/outputc.h +++ b/src/options/outputc.h @@ -17,6 +17,7 @@ class OutputC explicit OutputC(std::ostream* os) : d_os(os) {} Cvc5ostream operator()(const options::OutputTag tag) const; + Cvc5ostream operator()(const std::string& tag) const; bool isOn(const options::OutputTag tag) const; diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 40a37fa7b..7d0dab720 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -221,6 +221,21 @@ name = "SMT Layer" help = "turn on unsat assumptions generation" [[option]] + name = "difficultyMode" + category = "regular" + long = "difficulty-mode=MODE" + type = "DifficultyMode" + default = "LEMMA_LITERAL" + help = "choose output mode for get-difficulty, see --difficulty-mode=help" + help_mode = "difficulty output modes." +[[option.mode.LEMMA_LITERAL]] + name = "lemma-literal" + help = "Difficulty of an assertion is how many lemmas use a literal that the assertion depends on to be satisfied." +[[option.mode.MODEL_CHECK]] + name = "model-check" + help = "Difficulty of an assertion is how many times it was not satisfied in a candidate model." + +[[option]] name = "checkSynthSol" category = "regular" long = "check-synth-sol" diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index 7f3d778fd..57469ab11 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -308,7 +308,7 @@ Ackermann::Ackermann(PreprocessingPassContext* preprocContext) PreprocessingPassResult Ackermann::applyInternal( AssertionPipeline* assertionsToPreprocess) { - AlwaysAssert(!options::incrementalSolving()); + AlwaysAssert(!options().base.incrementalSolving); /* collect all function applications and generate consistency lemmas * accordingly */ diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index a789a0d0b..206f12a3f 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -20,6 +20,7 @@ #include "base/map_util.h" #include "expr/node.h" +#include "options/bv_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_statistics_registry.h" @@ -35,7 +36,7 @@ using namespace cvc5::theory; BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics() { - d_boolToBVMode = options::boolToBitvector(); + d_boolToBVMode = options().bv.boolToBitvector; }; PreprocessingPassResult BoolToBV::applyInternal( @@ -50,7 +51,7 @@ PreprocessingPassResult BoolToBV::applyInternal( for (size_t i = 0; i < size; ++i) { Node newAssertion = lowerAssertion((*assertionsToPreprocess)[i], true); - assertionsToPreprocess->replace(i, Rewriter::rewrite(newAssertion)); + assertionsToPreprocess->replace(i, rewrite(newAssertion)); } } else @@ -59,7 +60,7 @@ PreprocessingPassResult BoolToBV::applyInternal( for (size_t i = 0; i < size; ++i) { assertionsToPreprocess->replace( - i, Rewriter::rewrite(lowerIte((*assertionsToPreprocess)[i]))); + i, rewrite(lowerIte((*assertionsToPreprocess)[i]))); } } diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp index 597481678..cea5bf37c 100644 --- a/src/preprocessing/passes/bv_abstraction.cpp +++ b/src/preprocessing/passes/bv_abstraction.cpp @@ -53,7 +53,7 @@ PreprocessingPassResult BvAbstraction::applyInternal( bv_theory->applyAbstraction(assertions, new_assertions); for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { - assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i])); + assertionsToPreprocess->replace(i, rewrite(new_assertions[i])); } return PreprocessingPassResult::NO_CONFLICT; } diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index b3c34087d..e49cc5c44 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -37,28 +37,24 @@ namespace cvc5 { namespace preprocessing { namespace passes { -namespace { - -bool is_bv_const(Node n) +bool BVGauss::is_bv_const(Node n) { if (n.isConst()) { return true; } - return Rewriter::rewrite(n).getKind() == kind::CONST_BITVECTOR; + return rewrite(n).getKind() == kind::CONST_BITVECTOR; } -Node get_bv_const(Node n) +Node BVGauss::get_bv_const(Node n) { Assert(is_bv_const(n)); - return Rewriter::rewrite(n); + return rewrite(n); } -Integer get_bv_const_value(Node n) +Integer BVGauss::get_bv_const_value(Node n) { Assert(is_bv_const(n)); return get_bv_const(n).getConst<BitVector>().getValue(); } -} // namespace - /** * Determines if an overflow may occur in given 'expr'. * @@ -75,7 +71,7 @@ Integer get_bv_const_value(Node n) * will be handled via the default case, which is not incorrect but also not * necessarily the minimum. */ -unsigned BVGauss::getMinBwExpr(Node expr) +uint32_t BVGauss::getMinBwExpr(Node expr) { std::vector<Node> visit; /* Maps visited nodes to the determined minimum bit-width required. */ @@ -454,7 +450,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( Assert(is_bv_const(eq[0])); eqrhs = eq[0]; } - if (getMinBwExpr(Rewriter::rewrite(urem[0])) == 0) + if (getMinBwExpr(rewrite(urem[0])) == 0) { Trace("bv-gauss-elim") << "Minimum required bit-width exceeds given bit-width, " @@ -504,7 +500,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( NodeBuilder nb_nonconsts(NodeManager::currentNM(), k); for (const Node& nn : n) { - Node nnrw = Rewriter::rewrite(nn); + Node nnrw = rewrite(nn); if (is_bv_const(nnrw)) { nb_consts << nnrw; @@ -519,7 +515,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( unsigned nc = nb_consts.getNumChildren(); if (nc > 1) { - n0 = Rewriter::rewrite(nb_consts.constructNode()); + n0 = rewrite(nb_consts.constructNode()); } else if (nc == 1) { @@ -532,7 +528,7 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( /* n1 is a mult with non-const operands */ if (nb_nonconsts.getNumChildren() > 1) { - n1 = Rewriter::rewrite(nb_nonconsts.constructNode()); + n1 = rewrite(nb_nonconsts.constructNode()); } else { diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h index 8fafcb741..0078770fb 100644 --- a/src/preprocessing/passes/bv_gauss.h +++ b/src/preprocessing/passes/bv_gauss.h @@ -93,14 +93,29 @@ class BVGauss : public PreprocessingPass NONE }; - static Result gaussElim(Integer prime, - std::vector<Integer>& rhs, - std::vector<std::vector<Integer>>& lhs); + Result gaussElim(Integer prime, + std::vector<Integer>& rhs, + std::vector<std::vector<Integer>>& lhs); - static Result gaussElimRewriteForUrem(const std::vector<Node>& equations, - std::unordered_map<Node, Node>& res); + Result gaussElimRewriteForUrem(const std::vector<Node>& equations, + std::unordered_map<Node, Node>& res); - static unsigned getMinBwExpr(Node expr); + uint32_t getMinBwExpr(Node expr); + + /** + * Return true if given node is a bit-vector value (after rewriting). + */ + bool is_bv_const(Node n); + /** + * Return the bit-vector value resulting from rewriting node 'n'. + * Asserts that given node can be rewritten to a bit-vector value. + */ + Node get_bv_const(Node n); + /** + * Return the Integer value representing the given bit-vector value. + * Asserts that given node can be rewritten to a bit-vector value. + */ + Integer get_bv_const_value(Node n); }; } // namespace passes diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp index 45df7478c..ff0657dcd 100644 --- a/src/preprocessing/passes/bv_intro_pow2.cpp +++ b/src/preprocessing/passes/bv_intro_pow2.cpp @@ -94,7 +94,7 @@ PreprocessingPassResult BvIntroPow2::applyInternal( Node res = pow2Rewrite(cur, cache); if (res != cur) { - res = Rewriter::rewrite(res); + res = rewrite(res); assertionsToPreprocess->replace(i, res); } } diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp index cd58a3faf..0d0131e3e 100644 --- a/src/preprocessing/passes/bv_to_bool.cpp +++ b/src/preprocessing/passes/bv_to_bool.cpp @@ -53,7 +53,7 @@ PreprocessingPassResult BVToBool::applyInternal( liftBvToBool(assertionsToPreprocess->ref(), new_assertions); for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { - assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i])); + assertionsToPreprocess->replace(i, rewrite(new_assertions[i])); } return PreprocessingPassResult::NO_CONFLICT; } @@ -281,7 +281,7 @@ void BVToBool::liftBvToBool(const std::vector<Node>& assertions, for (unsigned i = 0; i < assertions.size(); ++i) { Node new_assertion = liftNode(assertions[i]); - new_assertions.push_back(Rewriter::rewrite(new_assertion)); + new_assertions.push_back(rewrite(new_assertion)); Trace("bv-to-bool") << " " << assertions[i] << " => " << new_assertions[i] << "\n"; } diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 65c9bb012..f6a65f90a 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -60,7 +60,7 @@ Node BVToInt::mkRangeConstraint(Node newVar, uint64_t k) Node lower = d_nm->mkNode(kind::LEQ, d_zero, newVar); Node upper = d_nm->mkNode(kind::LT, newVar, pow2(k)); Node result = d_nm->mkNode(kind::AND, lower, upper); - return Rewriter::rewrite(result); + return rewrite(result); } Node BVToInt::maxInt(uint64_t k) @@ -256,7 +256,7 @@ Node BVToInt::eliminationPass(Node n) Node BVToInt::bvToInt(Node n) { // make sure the node is re-written before processing it. - n = Rewriter::rewrite(n); + n = rewrite(n); n = makeBinary(n); n = eliminationPass(n); // binarize again, in case the elimination pass introduced @@ -424,13 +424,13 @@ Node BVToInt::translateWithChildren(Node original, // operators) // 3. translating into a sum uint64_t bvsize = original[0].getType().getBitVectorSize(); - if (options::solveBVAsInt() == options::SolveBVAsIntMode::IAND) + if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::IAND) { Node iAndOp = d_nm->mkConst(IntAnd(bvsize)); returnNode = d_nm->mkNode( kind::IAND, iAndOp, translated_children[0], translated_children[1]); } - else if (options::solveBVAsInt() == options::SolveBVAsIntMode::BV) + else if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::BV) { // translate the children back to BV Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize)); @@ -445,14 +445,14 @@ Node BVToInt::translateWithChildren(Node original, } else { - Assert(options::solveBVAsInt() == options::SolveBVAsIntMode::SUM); + Assert(options().smt.solveBVAsInt == options::SolveBVAsIntMode::SUM); // Construct a sum of ites, based on granularity. Assert(translated_children.size() == 2); returnNode = d_iandUtils.createSumNode(translated_children[0], translated_children[1], bvsize, - options::BVAndIntegerGranularity()); + options().smt.BVAndIntegerGranularity); } break; } @@ -657,7 +657,7 @@ Node BVToInt::translateWithChildren(Node original, * of the bounds that were relevant for the original * bit-vectors. */ - if (childrenTypesChanged(original) && options::ufHo()) + if (childrenTypesChanged(original) && options().uf.ufHo) { throw TypeCheckingExceptionPrivate( original, @@ -946,7 +946,7 @@ PreprocessingPassResult BVToInt::applyInternal( { Node bvNode = (*assertionsToPreprocess)[i]; Node intNode = bvToInt(bvNode); - Node rwNode = Rewriter::rewrite(intNode); + Node rwNode = rewrite(intNode); Trace("bv-to-int-debug") << "bv node: " << bvNode << std::endl; Trace("bv-to-int-debug") << "int node: " << intNode << std::endl; Trace("bv-to-int-debug") << "rw node: " << rwNode << std::endl; @@ -966,7 +966,7 @@ void BVToInt::addFinalizeRangeAssertions( vec_range.assign(d_rangeAssertions.key_begin(), d_rangeAssertions.key_end()); // conjoin all range assertions and add the conjunction // as a new assertion - Node rangeAssertions = Rewriter::rewrite(d_nm->mkAnd(vec_range)); + Node rangeAssertions = rewrite(d_nm->mkAnd(vec_range)); assertionsToPreprocess->push_back(rangeAssertions); Trace("bv-to-int-debug") << "range constraints: " << rangeAssertions.toString() << std::endl; diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp index a36388c26..06b4f0ba1 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.cpp +++ b/src/preprocessing/passes/extended_rewriter_pass.cpp @@ -20,7 +20,6 @@ #include "options/smt_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" -#include "theory/quantifiers/extended_rewrite.h" namespace cvc5 { namespace preprocessing { @@ -32,11 +31,12 @@ ExtRewPre::ExtRewPre(PreprocessingPassContext* preprocContext) PreprocessingPassResult ExtRewPre::applyInternal( AssertionPipeline* assertionsToPreprocess) { - theory::quantifiers::ExtendedRewriter extr(options::extRewPrepAgg()); for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { assertionsToPreprocess->replace( - i, extr.extendedRewrite((*assertionsToPreprocess)[i])); + i, + extendedRewrite((*assertionsToPreprocess)[i], + options().smt.extRewPrepAgg)); } return PreprocessingPassResult::NO_CONFLICT; } diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp index 6040b3669..24edf1509 100644 --- a/src/preprocessing/passes/foreign_theory_rewrite.cpp +++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp @@ -36,7 +36,7 @@ ForeignTheoryRewrite::ForeignTheoryRewrite( Node ForeignTheoryRewrite::simplify(Node n) { std::vector<Node> toVisit; - n = Rewriter::rewrite(n); + n = rewrite(n); toVisit.push_back(n); // traverse n and rewrite until fixpoint while (!toVisit.empty()) @@ -143,7 +143,7 @@ PreprocessingPassResult ForeignTheoryRewrite::applyInternal( for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { assertionsToPreprocess->replace( - i, Rewriter::rewrite(simplify((*assertionsToPreprocess)[i]))); + i, rewrite(simplify((*assertionsToPreprocess)[i]))); } return PreprocessingPassResult::NO_CONFLICT; diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp index 2405702b0..7e8f3ffab 100644 --- a/src/preprocessing/passes/fun_def_fmf.cpp +++ b/src/preprocessing/passes/fun_def_fmf.cpp @@ -153,7 +153,7 @@ void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess) << "FMF fun def: FUNCTION : rewrite " << assertions[i] << std::endl; Trace("fmf-fun-def") << " to " << std::endl; Node new_q = nm->mkNode(FORALL, bvl, bd); - new_q = Rewriter::rewrite(new_q); + new_q = rewrite(new_q); assertionsToPreprocess->replace(i, new_q); Trace("fmf-fun-def") << " " << assertions[i] << std::endl; fd_assertions.push_back(i); @@ -187,7 +187,7 @@ void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess) Assert(constraints.empty()); if (n != assertions[i]) { - n = Rewriter::rewrite(n); + n = rewrite(n); Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << std::endl; Trace("fmf-fun-def-rewrite") << " to " << std::endl; @@ -232,7 +232,7 @@ Node FunDefFmf::simplifyFormula( for (unsigned i = 0; i < constraints.size(); i++) { constraints[i] = nm->mkNode(FORALL, n[0], constraints[i]); - constraints[i] = Rewriter::rewrite(constraints[i]); + constraints[i] = rewrite(constraints[i]); } if (c != n[1]) { @@ -365,7 +365,7 @@ Node FunDefFmf::simplifyFormula( if (constraints.size() > 1) { cons = nm->mkNode(AND, constraints); - cons = Rewriter::rewrite(cons); + cons = rewrite(cons); constraints.clear(); constraints.push_back(cons); } diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp index e990f8868..cd8ecc73f 100644 --- a/src/preprocessing/passes/global_negate.cpp +++ b/src/preprocessing/passes/global_negate.cpp @@ -94,7 +94,7 @@ Node GlobalNegate::simplify(const std::vector<Node>& assertions, } Trace("cegqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl; - body = Rewriter::rewrite(body); + body = rewrite(body); Trace("cegqi-gn") << "...got (post-rewrite) : " << body << std::endl; return body; } diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp index 27dcf651b..d3372a28e 100644 --- a/src/preprocessing/passes/ho_elim.cpp +++ b/src/preprocessing/passes/ho_elim.cpp @@ -180,7 +180,7 @@ Node HoElim::eliminateHo(Node n) if (cur.isVar()) { Node ret = cur; - if (options::hoElim()) + if (options().quantifiers.hoElim) { if (tn.isFunction()) { @@ -203,7 +203,7 @@ Node HoElim::eliminateHo(Node n) else { d_visited[cur] = Node::null(); - if (cur.getKind() == APPLY_UF && options::hoElim()) + if (cur.getKind() == APPLY_UF && options().quantifiers.hoElim) { Node op = cur.getOperator(); // convert apply uf with variable arguments eagerly to ho apply @@ -275,7 +275,7 @@ Node HoElim::eliminateHo(Node n) children.insert(children.begin(), retOp); } // process ho apply - if (ret.getKind() == HO_APPLY && options::hoElim()) + if (ret.getKind() == HO_APPLY && options().quantifiers.hoElim) { TypeNode tnr = ret.getType(); tnr = getUSort(tnr); @@ -315,7 +315,7 @@ PreprocessingPassResult HoElim::applyInternal( Node res = eliminateLambdaComplete(prev, newLambda); if (res != prev) { - res = theory::Rewriter::rewrite(res); + res = rewrite(res); Assert(!expr::hasFreeVar(res)); assertionsToPreprocess->replace(i, res); } @@ -361,7 +361,7 @@ PreprocessingPassResult HoElim::applyInternal( if (!axioms.empty()) { Node conj = nm->mkAnd(axioms); - conj = theory::Rewriter::rewrite(conj); + conj = rewrite(conj); Assert(!expr::hasFreeVar(conj)); assertionsToPreprocess->conjoin(0, conj); } @@ -374,7 +374,7 @@ PreprocessingPassResult HoElim::applyInternal( Node res = eliminateHo(prev); if (res != prev) { - res = theory::Rewriter::rewrite(res); + res = rewrite(res); Assert(!expr::hasFreeVar(res)); assertionsToPreprocess->replace(i, res); } @@ -382,7 +382,7 @@ PreprocessingPassResult HoElim::applyInternal( // extensionality: process all function types for (const TypeNode& ftn : d_funTypes) { - if (options::hoElim()) + if (options().quantifiers.hoElim) { Node h = getHoApplyUf(ftn); Trace("ho-elim-ax") << "Make extensionality for " << h << std::endl; @@ -406,7 +406,7 @@ PreprocessingPassResult HoElim::applyInternal( // exists another function that acts like the "store" operator for // arrays, e.g. it is the same function with one I/O pair updated. // Without this axiom, the translation is model unsound. - if (options::hoElimStoreAx()) + if (options().quantifiers.hoElimStoreAx) { Node u = nm->mkBoundVar("u", uf); Node v = nm->mkBoundVar("v", uf); @@ -428,7 +428,7 @@ PreprocessingPassResult HoElim::applyInternal( Trace("ho-elim-ax") << "...store axiom : " << store << std::endl; } } - else if (options::hoElimStoreAx()) + else if (options().quantifiers.hoElimStoreAx) { Node u = nm->mkBoundVar("u", ftn); Node v = nm->mkBoundVar("v", ftn); @@ -456,7 +456,7 @@ PreprocessingPassResult HoElim::applyInternal( if (!axioms.empty()) { Node conj = nm->mkAnd(axioms); - conj = theory::Rewriter::rewrite(conj); + conj = rewrite(conj); Assert(!expr::hasFreeVar(conj)); assertionsToPreprocess->conjoin(0, conj); } diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h index 8b8dc08c2..80f8cda70 100644 --- a/src/preprocessing/passes/ho_elim.h +++ b/src/preprocessing/passes/ho_elim.h @@ -73,10 +73,10 @@ namespace passes { * * Based on options, this preprocessing pass may apply a subset o the above * steps. In particular: - * * If options::hoElim() is true, then step [2] is taken and extensionality + * * If hoElim is true, then step [2] is taken and extensionality * axioms are added in step [3]. - * * If options::hoElimStoreAx() is true, then store axioms are added in step 3. - * The form of these axioms depends on whether options::hoElim() is true. If it + * * If hoElimStoreAx is true, then store axioms are added in step 3. + * The form of these axioms depends on whether hoElim is true. If it * is true, the axiom is given in terms of the uninterpreted functions that * encode function sorts. If it is false, then the store axiom is given in terms * of the original function sorts. diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 41d52d1ae..e6b5a4bca 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -105,9 +105,9 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache) Node IntToBV::intToBV(TNode n, NodeMap& cache) { - int size = options::solveIntAsBV(); + int size = options().smt.solveIntAsBV; AlwaysAssert(size > 0); - AlwaysAssert(!options::incrementalSolving()); + AlwaysAssert(!options().base.incrementalSolving); NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); @@ -203,7 +203,7 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache) // Mark the substitution and continue Node result = builder; - result = Rewriter::rewrite(result); + result = rewrite(result); cache[current] = result; } else diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index 7578bcad6..97e56c58c 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -64,7 +64,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) } for (unsigned i = 0, size = assertions->size(); i < size; ++i) { - assertions->replace(i, Rewriter::rewrite((*assertions)[i])); + assertions->replace(i, rewrite((*assertions)[i])); } return PreprocessingPassResult::NO_CONFLICT; diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 434256d28..5f9b4fb1d 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -97,7 +97,7 @@ Node ITESimp::simpITE(util::ITEUtilities* ite_utils, TNode assertion) Node result = ite_utils->simpITE(assertion); Node res_rewritten = rewrite(result); - if (options::simplifyWithCareEnabled()) + if (options().smt.simplifyWithCareEnabled) { Chat() << "starting simplifyWithCare()" << endl; Node postSimpWithCare = ite_utils->simplifyWithCare(res_rewritten); @@ -119,7 +119,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic(); if (simpDidALotOfWork) { - if (options::compressItes()) + if (options().smt.compressItes) { result = d_iteUtilities.compress(assertionsToPreprocess); } @@ -128,7 +128,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) { // if false, don't bother to reclaim memory here. NodeManager* nm = NodeManager::currentNM(); - if (nm->poolSize() >= options::zombieHuntThreshold()) + if (nm->poolSize() >= options().smt.zombieHuntThreshold) { Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl; @@ -136,7 +136,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) << " nodes before cleanup" << endl; d_iteUtilities.clear(); d_env.getRewriter()->clearCaches(); - nm->reclaimZombiesUntil(options::zombieHuntThreshold()); + nm->reclaimZombiesUntil(options().smt.zombieHuntThreshold); Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl; } @@ -145,7 +145,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) // Do theory specific preprocessing passes if (logicInfo().isTheoryEnabled(theory::THEORY_ARITH) - && !options::incrementalSolving()) + && !options().base.incrementalSolving) { if (!simpDidALotOfWork) { diff --git a/src/preprocessing/passes/learned_rewrite.cpp b/src/preprocessing/passes/learned_rewrite.cpp index 81fbf1ea1..c2693e927 100644 --- a/src/preprocessing/passes/learned_rewrite.cpp +++ b/src/preprocessing/passes/learned_rewrite.cpp @@ -233,7 +233,7 @@ Node LearnedRewrite::rewriteLearned(Node n, { NodeManager* nm = NodeManager::currentNM(); Trace("learned-rewrite-rr-debug") << "Rewrite " << n << std::endl; - Node nr = Rewriter::rewrite(n); + Node nr = rewrite(n); Kind k = nr.getKind(); if (k == INTS_DIVISION || k == INTS_MODULUS || k == DIVISION) { @@ -278,7 +278,7 @@ Node LearnedRewrite::rewriteLearned(Node n, children.insert(children.end(), n.begin(), n.end()); Node ret = nm->mkNode(nk, children); nr = returnRewriteLearned(nr, ret, LearnedRewriteId::NON_ZERO_DEN); - nr = Rewriter::rewrite(nr); + nr = rewrite(nr); k = nr.getKind(); } } diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index a5720e758..c40a65bc1 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -43,11 +43,58 @@ using namespace cvc5::theory; namespace { /** + * Trace nodes back to their assertions using CircuitPropagator's + * BackEdgesMap. + */ +void traceBackToAssertions(booleans::CircuitPropagator* propagator, + const std::vector<Node>& nodes, + std::vector<TNode>& assertions) +{ + const booleans::CircuitPropagator::BackEdgesMap& backEdges = + propagator->getBackEdges(); + for (vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i) + { + booleans::CircuitPropagator::BackEdgesMap::const_iterator j = + backEdges.find(*i); + // term must appear in map, otherwise how did we get here?! + Assert(j != backEdges.end()); + // if term maps to empty, that means it's a top-level assertion + if (!(*j).second.empty()) + { + traceBackToAssertions(propagator, (*j).second, assertions); + } + else + { + assertions.push_back(*i); + } + } +} + +} // namespace + +MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "miplib-trick") +{ + if (!options().base.incrementalSolving) + { + NodeManager::currentNM()->subscribeEvents(this); + } +} + +MipLibTrick::~MipLibTrick() +{ + if (!options().base.incrementalSolving) + { + NodeManager::currentNM()->unsubscribeEvents(this); + } +} + +/** * Remove conjuncts in toRemove from conjunction n. Return # of removed * conjuncts. */ -size_t removeFromConjunction(Node& n, - const std::unordered_set<unsigned long>& toRemove) +size_t MipLibTrick::removeFromConjunction( + Node& n, const std::unordered_set<unsigned long>& toRemove) { Assert(n.getKind() == kind::AND); Node trueNode = NodeManager::currentNM()->mkConst(true); @@ -109,7 +156,7 @@ size_t removeFromConjunction(Node& n, { n = b; } - n = Rewriter::rewrite(n); + n = rewrite(n); return removals; } } @@ -118,53 +165,6 @@ size_t removeFromConjunction(Node& n, return 0; } -/** - * Trace nodes back to their assertions using CircuitPropagator's - * BackEdgesMap. - */ -void traceBackToAssertions(booleans::CircuitPropagator* propagator, - const std::vector<Node>& nodes, - std::vector<TNode>& assertions) -{ - const booleans::CircuitPropagator::BackEdgesMap& backEdges = - propagator->getBackEdges(); - for (vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i) - { - booleans::CircuitPropagator::BackEdgesMap::const_iterator j = - backEdges.find(*i); - // term must appear in map, otherwise how did we get here?! - Assert(j != backEdges.end()); - // if term maps to empty, that means it's a top-level assertion - if (!(*j).second.empty()) - { - traceBackToAssertions(propagator, (*j).second, assertions); - } - else - { - assertions.push_back(*i); - } - } -} - -} // namespace - -MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "miplib-trick") -{ - if (!options::incrementalSolving()) - { - NodeManager::currentNM()->subscribeEvents(this); - } -} - -MipLibTrick::~MipLibTrick() -{ - if (!options::incrementalSolving()) - { - NodeManager::currentNM()->unsubscribeEvents(this); - } -} - void MipLibTrick::nmNotifyNewVar(TNode n) { if (n.getType().isBoolean()) @@ -188,7 +188,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( { Assert(assertionsToPreprocess->getRealAssertionsEnd() == assertionsToPreprocess->size()); - Assert(!options::incrementalSolving()); + Assert(!options().base.incrementalSolving); context::Context fakeContext; TheoryEngine* te = d_preprocContext->getTheoryEngine(); @@ -530,12 +530,12 @@ PreprocessingPassResult MipLibTrick::applyInternal( nm->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME); - Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero)); - Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one)); + Node geq = rewrite(nm->mkNode(kind::GEQ, newVar, zero)); + Node leq = rewrite(nm->mkNode(kind::LEQ, newVar, one)); TrustNode tgeq = TrustNode::mkTrustLemma(geq, nullptr); TrustNode tleq = TrustNode::mkTrustLemma(leq, nullptr); - Node n = Rewriter::rewrite(geq.andNode(leq)); + Node n = rewrite(geq.andNode(leq)); assertionsToPreprocess->push_back(n); TrustSubstitutionMap tnullMap(&fakeContext, nullptr); CVC5_UNUSED SubstitutionMap& nullMap = tnullMap.get(); @@ -575,8 +575,8 @@ PreprocessingPassResult MipLibTrick::applyInternal( kind::MULT, nm->mkConst(coef[pos_var][0]), newVars[0]); } Debug("miplib") << "vars[] " << var << endl - << " eq " << Rewriter::rewrite(sum) << endl; - Node newAssertion = var.eqNode(Rewriter::rewrite(sum)); + << " eq " << rewrite(sum) << endl; + Node newAssertion = var.eqNode(rewrite(sum)); if (top_level_substs.hasSubstitution(newAssertion[0])) { // Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl; @@ -586,7 +586,8 @@ PreprocessingPassResult MipLibTrick::applyInternal( Assert(top_level_substs.getSubstitution(newAssertion[0]) == newAssertion[1]); } - else if (pos.getNumChildren() <= options::arithMLTrickSubstitutions()) + else if (pos.getNumChildren() + <= options().arith.arithMLTrickSubstitutions) { top_level_substs.addSubstitution(newAssertion[0], newAssertion[1]); Debug("miplib") << "addSubs: " << newAssertion[0] << " to " @@ -596,10 +597,10 @@ PreprocessingPassResult MipLibTrick::applyInternal( { Debug("miplib") << "skipSubs: " << newAssertion[0] << " to " << newAssertion[1] - << " (threshold is " << options::arithMLTrickSubstitutions() - << ")" << endl; + << " (threshold is " + << options().arith.arithMLTrickSubstitutions << ")" << endl; } - newAssertion = Rewriter::rewrite(newAssertion); + newAssertion = rewrite(newAssertion); Debug("miplib") << " " << newAssertion << endl; assertionsToPreprocess->push_back(newAssertion); @@ -642,7 +643,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( } Debug("miplib") << "had: " << assertion[i] << endl; assertionsToPreprocess->replace( - i, Rewriter::rewrite(top_level_substs.apply(assertion))); + i, rewrite(top_level_substs.apply(assertion))); Debug("miplib") << "now: " << assertion << endl; } } diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h index c63885cf0..537d27a0a 100644 --- a/src/preprocessing/passes/miplib_trick.h +++ b/src/preprocessing/passes/miplib_trick.h @@ -49,6 +49,9 @@ class MipLibTrick : public PreprocessingPass, public NodeManagerListener Statistics(); }; + size_t removeFromConjunction( + Node& n, const std::unordered_set<unsigned long>& toRemove); + Statistics d_statistics; std::vector<Node> d_boolVars; diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp index afd21fb7a..27f34f177 100644 --- a/src/preprocessing/passes/nl_ext_purify.cpp +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -64,7 +64,7 @@ Node NlExtPurify::purifyNlTerms(TNode n, && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS)) { // don't do it if it rewrites to a constant - Node nr = Rewriter::rewrite(n); + Node nr = rewrite(n); if (nr.isConst()) { // return the rewritten constant diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp index ca61c9197..6c93eba15 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.cpp +++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp @@ -210,7 +210,7 @@ void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion, Node orig) { Assert(assertion.getKind() == kind::GEQ); - Assert(assertion == Rewriter::rewrite(assertion)); + Assert(assertion == rewrite(assertion)); // assume assertion is rewritten Node l = assertion[0]; @@ -264,7 +264,7 @@ void PseudoBooleanProcessor::learnInternal(Node assertion, case kind::LEQ: case kind::LT: { - Node rw = Rewriter::rewrite(assertion); + Node rw = rewrite(assertion); if (assertion == rw) { if (assertion.getKind() == kind::GEQ) @@ -320,7 +320,7 @@ void PseudoBooleanProcessor::addSub(Node from, Node to) { if (!d_subCache.hasSubstitution(from)) { - Node rw_to = Rewriter::rewrite(to); + Node rw_to = rewrite(to); d_subCache.addSubstitution(from, rw_to); } } @@ -386,7 +386,7 @@ void PseudoBooleanProcessor::learnGeqSub(Node geq) Node PseudoBooleanProcessor::applyReplacements(Node pre) { - Node assertion = Rewriter::rewrite(pre); + Node assertion = rewrite(pre); Node result = d_subCache.apply(assertion); if (Debug.isOn("pbs::rewrites") && result != assertion) diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp index a9363c549..f80c4383c 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.cpp +++ b/src/preprocessing/passes/quantifiers_preprocess.cpp @@ -20,7 +20,7 @@ #include "base/output.h" #include "preprocessing/assertion_pipeline.h" -#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/quantifiers_preprocess.h" #include "theory/rewriter.h" namespace cvc5 { @@ -37,14 +37,15 @@ PreprocessingPassResult QuantifiersPreprocess::applyInternal( AssertionPipeline* assertionsToPreprocess) { size_t size = assertionsToPreprocess->size(); + quantifiers::QuantifiersPreprocess qp(d_env); for (size_t i = 0; i < size; ++i) { Node prev = (*assertionsToPreprocess)[i]; - TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(prev); + TrustNode trn = qp.preprocess(prev); if (!trn.isNull()) { Node next = trn.getNode(); - assertionsToPreprocess->replace(i, Rewriter::rewrite(next)); + assertionsToPreprocess->replace(i, rewrite(next)); Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl; Trace("quantifiers-preprocess") << " ...got " << (*assertionsToPreprocess)[i] << endl; diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index 3cfc29ed6..9e2170ffd 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -57,7 +57,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va || n.getKind() == kind::GEQ || n.getKind() == kind::LT || n.getKind() == kind::GT || n.getKind() == kind::LEQ) { - ret = Rewriter::rewrite(n); + ret = rewrite(n); Trace("real-as-int-debug") << "Now looking at : " << ret << std::endl; if (!ret.isConst()) { @@ -81,13 +81,12 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va Rational(c.getConst<Rational>().getDenominator()))); } } - Node cc = - coeffs.empty() - ? Node::null() - : (coeffs.size() == 1 - ? coeffs[0] - : Rewriter::rewrite(NodeManager::currentNM()->mkNode( - kind::MULT, coeffs))); + Node cc = coeffs.empty() + ? Node::null() + : (coeffs.size() == 1 + ? coeffs[0] + : rewrite(NodeManager::currentNM()->mkNode( + kind::MULT, coeffs))); std::vector<Node> sum; for (std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end(); @@ -105,7 +104,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va { if (!cc.isNull()) { - c = Rewriter::rewrite( + c = rewrite( NodeManager::currentNM()->mkNode(kind::MULT, c, cc)); } } diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp index 4704f1cb5..0e7aafcc3 100644 --- a/src/preprocessing/passes/rewrite.cpp +++ b/src/preprocessing/passes/rewrite.cpp @@ -34,7 +34,7 @@ PreprocessingPassResult Rewrite::applyInternal( AssertionPipeline* assertionsToPreprocess) { for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { - assertionsToPreprocess->replace(i, Rewriter::rewrite((*assertionsToPreprocess)[i])); + assertionsToPreprocess->replace(i, rewrite((*assertionsToPreprocess)[i])); } return PreprocessingPassResult::NO_CONFLICT; diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp index 4322e60d5..37bf0fd8b 100644 --- a/src/preprocessing/passes/sep_skolem_emp.cpp +++ b/src/preprocessing/passes/sep_skolem_emp.cpp @@ -113,7 +113,7 @@ PreprocessingPassResult SepSkolemEmp::applyInternal( Node next = preSkolemEmp(prev, pol, visited); if (next != prev) { - assertionsToPreprocess->replace(i, Rewriter::rewrite(next)); + assertionsToPreprocess->replace(i, rewrite(next)); Trace("sep-preprocess") << "*** Preprocess sep " << prev << endl; Trace("sep-preprocess") << " ...got " << (*assertionsToPreprocess)[i] << endl; diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index 7b93f43cf..68fb89e1f 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -41,7 +41,7 @@ PreprocessingPassResult SortInferencePass::applyInternal( theory::SortInference* si = d_preprocContext->getTheoryEngine()->getSortInference(); - if (options::sortInference()) + if (options().smt.sortInference) { si->initialize(assertionsToPreprocess->ref()); std::map<Node, Node> model_replace_f; @@ -52,7 +52,7 @@ PreprocessingPassResult SortInferencePass::applyInternal( Node next = si->simplify(prev, model_replace_f, visited); if (next != prev) { - next = theory::Rewriter::rewrite(next); + next = rewrite(next); assertionsToPreprocess->replace(i, next); Trace("sort-infer-preprocess") << "*** Preprocess SortInferencePass " << prev << endl; @@ -64,7 +64,7 @@ PreprocessingPassResult SortInferencePass::applyInternal( si->getNewAssertions(newAsserts); for (const Node& na : newAsserts) { - Node nar = theory::Rewriter::rewrite(na); + Node nar = rewrite(na); Trace("sort-infer-preprocess") << "*** Preprocess SortInferencePass : new constraint " << nar << endl; @@ -80,7 +80,7 @@ PreprocessingPassResult SortInferencePass::applyInternal( } // only need to compute monotonicity on the resulting formula if we are // using this option - if (options::ufssFairnessMonotone()) + if (options().uf.ufssFairnessMonotone) { si->computeMonotonicity(assertionsToPreprocess->ref()); } diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp index 09d24d900..24d25e354 100644 --- a/src/preprocessing/passes/static_learning.cpp +++ b/src/preprocessing/passes/static_learning.cpp @@ -47,8 +47,7 @@ PreprocessingPassResult StaticLearning::applyInternal( } else { - assertionsToPreprocess->replace( - i, theory::Rewriter::rewrite(learned.constructNode())); + assertionsToPreprocess->replace(i, rewrite(learned.constructNode())); } } return PreprocessingPassResult::NO_CONFLICT; diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp index 6ab3a9bd2..80d6dd0e8 100644 --- a/src/preprocessing/passes/strings_eager_pp.cpp +++ b/src/preprocessing/passes/strings_eager_pp.cpp @@ -49,7 +49,7 @@ PreprocessingPassResult StringsEagerPp::applyInternal( } if (prev != rew) { - assertionsToPreprocess->replace(i, theory::Rewriter::rewrite(rew)); + assertionsToPreprocess->replace(i, rewrite(rew)); } } diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index d105c436a..8abd77a27 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -21,7 +21,7 @@ #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/quantifiers_preprocess.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_utils.h" #include "theory/rewriter.h" @@ -65,7 +65,7 @@ PreprocessingPassResult SygusInference::applyInternal( prev.substitute(funs.begin(), funs.end(), sols.begin(), sols.end()); if (curr != prev) { - curr = theory::Rewriter::rewrite(curr); + curr = rewrite(curr); Trace("sygus-infer-debug") << "...rewrote " << prev << " to " << curr << std::endl; assertionsToPreprocess->replace(i, curr); @@ -118,6 +118,7 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions, // process eassertions std::vector<Node> processed_assertions; + quantifiers::QuantifiersPreprocess qp(d_env); for (const Node& as : eassertions) { // substitution for this assertion @@ -126,12 +127,12 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions, std::map<TypeNode, unsigned> type_count; Node pas = as; // rewrite - pas = theory::Rewriter::rewrite(pas); + pas = rewrite(pas); Trace("sygus-infer") << "assertion : " << pas << std::endl; if (pas.getKind() == FORALL) { // preprocess the quantified formula - TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(pas); + TrustNode trn = qp.preprocess(pas); if (!trn.isNull()) { pas = trn.getNode(); diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index 81d5cae84..a54d220e5 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -146,7 +146,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( Trace("srs-input") << "Make synth variables for types..." << std::endl; // We will generate a fixed number of variables per type. These are the // variables that appear as free variables in the rewrites we generate. - unsigned nvars = options::sygusRewSynthInputNVars(); + unsigned nvars = options().quantifiers.sygusRewSynthInputNVars; // must have at least one variable per type nvars = nvars < 1 ? 1 : nvars; std::map<TypeNode, std::vector<Node> > tvars; @@ -162,7 +162,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( // our input does not contain a Boolean variable, we need not allocate any // Boolean variables here. unsigned useNVars = - (options::sygusRewSynthInputUseBool() || !tn.isBoolean()) + (options().quantifiers.sygusRewSynthInputUseBool || !tn.isBoolean()) ? nvars : (hasBoolVar ? 1 : 0); for (unsigned i = 0; i < useNVars; i++) @@ -276,7 +276,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( // we add variable constructors if we are not Boolean, we are interested // in purely propositional rewrites (via the option), or this term is // a Boolean variable. - if (!ctt.isBoolean() || options::sygusRewSynthInputUseBool() + if (!ctt.isBoolean() || options().quantifiers.sygusRewSynthInputUseBool || ct.getKind() == BOUND_VARIABLE) { for (const Node& v : tvars[ctt]) diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index c8ddfc2fa..c59aa86ef 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -231,7 +231,7 @@ void UnconstrainedSimplifier::processUnconstrained() // Special case: condition is unconstrained, then and else are // different, and total cardinality of the type is 2, then the // result is unconstrained - Node test = Rewriter::rewrite(parent[1].eqNode(parent[2])); + Node test = rewrite(parent[1].eqNode(parent[2])); if (test == nm->mkConst<bool>(false)) { ++d_numUnconstrainedElim; @@ -530,7 +530,7 @@ void UnconstrainedSimplifier::processUnconstrained() { // TODO(#2377): could build ITE here Node test = other.eqNode(nm->mkConst<Rational>(0)); - if (Rewriter::rewrite(test) != nm->mkConst<bool>(false)) + if (rewrite(test) != nm->mkConst<bool>(false)) { break; } @@ -573,7 +573,7 @@ void UnconstrainedSimplifier::processUnconstrained() Node test = nm->mkNode(extractOp, children); BitVector one(1, unsigned(1)); test = test.eqNode(nm->mkConst<BitVector>(one)); - if (Rewriter::rewrite(test) != nm->mkConst<bool>(true)) + if (rewrite(test) != nm->mkConst<bool>(true)) { done = true; break; @@ -753,8 +753,7 @@ void UnconstrainedSimplifier::processUnconstrained() } currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; - Node test = - Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv))); + Node test = rewrite(other.eqNode(nm->mkConst<BitVector>(bv))); if (test == nm->mkConst<bool>(false)) { break; @@ -861,7 +860,7 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal( for (size_t i = 0, asize = assertions.size(); i < asize; ++i) { Node a = assertions[i]; - Node as = Rewriter::rewrite(d_substitutions.apply(a)); + Node as = rewrite(d_substitutions.apply(a)); // replace the assertion assertionsToPreprocess->replace(i, as); } diff --git a/src/proof/lfsc/lfsc_print_channel.cpp b/src/proof/lfsc/lfsc_print_channel.cpp new file mode 100644 index 000000000..36fd8831b --- /dev/null +++ b/src/proof/lfsc/lfsc_print_channel.cpp @@ -0,0 +1,161 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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. + * **************************************************************************** + * + * Print channels for LFSC proofs. + */ + +#include "proof/lfsc/lfsc_print_channel.h" + +#include <sstream> + +#include "proof/lfsc/lfsc_util.h" + +namespace cvc5 { +namespace proof { + +LfscPrintChannelOut::LfscPrintChannelOut(std::ostream& out) : d_out(out) {} +void LfscPrintChannelOut::printNode(TNode n) +{ + d_out << " "; + printNodeInternal(d_out, n); +} + +void LfscPrintChannelOut::printTypeNode(TypeNode tn) +{ + d_out << " "; + printTypeNodeInternal(d_out, tn); +} + +void LfscPrintChannelOut::printHole() { d_out << " _ "; } +void LfscPrintChannelOut::printTrust(TNode res, PfRule src) +{ + d_out << std::endl << "(trust "; + printNodeInternal(d_out, res); + d_out << ") ; from " << src << std::endl; +} + +void LfscPrintChannelOut::printOpenRule(const ProofNode* pn) +{ + d_out << std::endl << "("; + printRule(d_out, pn); +} + +void LfscPrintChannelOut::printOpenLfscRule(LfscRule lr) +{ + d_out << std::endl << "(" << lr; +} + +void LfscPrintChannelOut::printCloseRule(size_t nparen) +{ + for (size_t i = 0; i < nparen; i++) + { + d_out << ")"; + } +} + +void LfscPrintChannelOut::printProofId(size_t id) +{ + d_out << " "; + printProofId(d_out, id); +} +void LfscPrintChannelOut::printAssumeId(size_t id) +{ + d_out << " "; + printAssumeId(d_out, id); +} + +void LfscPrintChannelOut::printEndLine() { d_out << std::endl; } + +void LfscPrintChannelOut::printNodeInternal(std::ostream& out, Node n) +{ + // due to use of special names in the node converter, we must clean symbols + std::stringstream ss; + n.toStream(ss, -1, 0, Language::LANG_SMTLIB_V2_6); + std::string s = ss.str(); + cleanSymbols(s); + out << s; +} + +void LfscPrintChannelOut::printTypeNodeInternal(std::ostream& out, TypeNode tn) +{ + // due to use of special names in the node converter, we must clean symbols + std::stringstream ss; + tn.toStream(ss, Language::LANG_SMTLIB_V2_6); + std::string s = ss.str(); + cleanSymbols(s); + out << s; +} + +void LfscPrintChannelOut::printRule(std::ostream& out, const ProofNode* pn) +{ + if (pn->getRule() == PfRule::LFSC_RULE) + { + const std::vector<Node>& args = pn->getArguments(); + out << getLfscRule(args[0]); + return; + } + // Otherwise, convert to lower case + std::stringstream ss; + ss << pn->getRule(); + std::string rname = ss.str(); + std::transform( + rname.begin(), rname.end(), rname.begin(), [](unsigned char c) { + return std::tolower(c); + }); + out << rname; +} + +void LfscPrintChannelOut::printId(std::ostream& out, size_t id) +{ + out << "__t" << id; +} + +void LfscPrintChannelOut::printProofId(std::ostream& out, size_t id) +{ + out << "__p" << id; +} + +void LfscPrintChannelOut::printAssumeId(std::ostream& out, size_t id) +{ + out << "__a" << id; +} + +void LfscPrintChannelOut::cleanSymbols(std::string& s) +{ + size_t start_pos = 0; + while ((start_pos = s.find("(_ ", start_pos)) != std::string::npos) + { + s.replace(start_pos, 3, "("); + start_pos += 1; + } + start_pos = 0; + while ((start_pos = s.find("__LFSC_TMP", start_pos)) != std::string::npos) + { + s.replace(start_pos, 10, ""); + } +} + +LfscPrintChannelPre::LfscPrintChannelPre(LetBinding& lbind) : d_lbind(lbind) {} + +void LfscPrintChannelPre::printNode(TNode n) { d_lbind.process(n); } +void LfscPrintChannelPre::printTrust(TNode res, PfRule src) +{ + d_lbind.process(res); +} + +void LfscPrintChannelPre::printOpenRule(const ProofNode* pn) +{ + +} + +} // namespace proof +} // namespace cvc5 diff --git a/src/proof/lfsc/lfsc_print_channel.h b/src/proof/lfsc/lfsc_print_channel.h new file mode 100644 index 000000000..655fa192c --- /dev/null +++ b/src/proof/lfsc/lfsc_print_channel.h @@ -0,0 +1,128 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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. + * **************************************************************************** + * + * Print channels for LFSC proofs. + */ + +#include "cvc5_private.h" + +#ifndef CVC4__PROOF__LFSC__LFSC_PRINT_CHANNEL_H +#define CVC4__PROOF__LFSC__LFSC_PRINT_CHANNEL_H + +#include <iostream> +#include <map> + +#include "expr/node.h" +#include "printer/let_binding.h" +#include "proof/lfsc/lfsc_util.h" +#include "proof/proof_node.h" + +namespace cvc5 { +namespace proof { + +/** + * LFSC proofs are printed in two phases: the first phase computes the + * letification of terms in the proof as well as other information that is + * required for printing the preamble of the proof. The second phase prints the + * proof to an output stream. This is the base class for these two phases. + */ +class LfscPrintChannel +{ + public: + LfscPrintChannel() {} + virtual ~LfscPrintChannel() {} + /** Print node n */ + virtual void printNode(TNode n) {} + /** Print type node n */ + virtual void printTypeNode(TypeNode tn) {} + /** Print a hole */ + virtual void printHole() {} + /** + * Print an application of the trusting the result res, whose source is the + * given proof rule. + */ + virtual void printTrust(TNode res, PfRule src) {} + /** Print the opening of the rule of proof rule pn, e.g. "(and_elim ". */ + virtual void printOpenRule(const ProofNode* pn) {} + /** Print the opening of LFSC rule lr, e.g. "(cong " */ + virtual void printOpenLfscRule(LfscRule lr) {} + /** Print the closing of # nparen proof rules */ + virtual void printCloseRule(size_t nparen = 1) {} + /** Print a letified proof with the given identifier */ + virtual void printProofId(size_t id) {} + /** Print a proof assumption with the given identifier */ + virtual void printAssumeId(size_t id) {} + /** Print an end line */ + virtual void printEndLine() {} +}; + +/** Prints the proof to output stream d_out */ +class LfscPrintChannelOut : public LfscPrintChannel +{ + public: + LfscPrintChannelOut(std::ostream& out); + void printNode(TNode n) override; + void printTypeNode(TypeNode tn) override; + void printHole() override; + void printTrust(TNode res, PfRule src) override; + void printOpenRule(const ProofNode* pn) override; + void printOpenLfscRule(LfscRule lr) override; + void printCloseRule(size_t nparen = 1) override; + void printProofId(size_t id) override; + void printAssumeId(size_t id) override; + void printEndLine() override; + //------------------- helper methods + /** + * Print node to stream in the expected format of LFSC. + */ + static void printNodeInternal(std::ostream& out, Node n); + /** + * Print type node to stream in the expected format of LFSC. + */ + static void printTypeNodeInternal(std::ostream& out, TypeNode tn); + static void printRule(std::ostream& out, const ProofNode* pn); + static void printId(std::ostream& out, size_t id); + static void printProofId(std::ostream& out, size_t id); + static void printAssumeId(std::ostream& out, size_t id); + //------------------- end helper methods + private: + /** + * Replaces "(_ " with "(" to eliminate indexed symbols + * Replaces "__LFSC_TMP" with "" + */ + static void cleanSymbols(std::string& s); + /** The output stream */ + std::ostream& d_out; +}; + +/** + * Run on the proof before it is printed, and does two preparation steps: + * - Computes the letification of nodes that appear in the proof. + * - Computes the set of DSL rules that appear in the proof. + */ +class LfscPrintChannelPre : public LfscPrintChannel +{ + public: + LfscPrintChannelPre(LetBinding& lbind); + void printNode(TNode n) override; + void printTrust(TNode res, PfRule src) override; + void printOpenRule(const ProofNode* pn) override; + + private: + /** The let binding */ + LetBinding& d_lbind; +}; + +} // namespace proof +} // namespace cvc5 + +#endif diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index bc2b6437b..7b93e3a55 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -840,7 +840,7 @@ enum class PfRule : uint32_t // Arguments: (F) // --------------------------------------------------------------- // Conclusion: F - // where F is an equality of the form t = QuantifiersRewriter::preprocess(t) + // where F is an equality of the form t = QuantifiersPreprocess::preprocess(t) QUANTIFIERS_PREPROCESS, //================================================= String rules diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 008d7a6d8..522c38040 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -275,10 +275,6 @@ TypeNode Command::grammarToTypeNode(api::Grammar* grammar) : sortToTypeNode(grammar->resolve()); } -Options& Command::getOriginalOptionsFrom(api::Solver* s) -{ - return *s->d_originalOptions.get(); -} /* -------------------------------------------------------------------------- */ /* class EmptyCommand */ diff --git a/src/smt/command.h b/src/smt/command.h index 627cb13c9..7d2d9cfc4 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -299,8 +299,6 @@ class CVC5_EXPORT Command const std::vector<api::Sort>& sorts); /** Helper to convert a Grammar to an internal TypeNode */ static TypeNode grammarToTypeNode(api::Grammar* grammar); - /** Get original options from the solver (for ResetCommand) */ - Options& getOriginalOptionsFrom(api::Solver* s); }; /* class Command */ /** diff --git a/src/smt/difficulty_post_processor.cpp b/src/smt/difficulty_post_processor.cpp new file mode 100644 index 000000000..748092238 --- /dev/null +++ b/src/smt/difficulty_post_processor.cpp @@ -0,0 +1,77 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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. + * **************************************************************************** + * + * Implementation of module for processing the difficulty of input assumptions + * based on proof nodes. + */ + +#include "smt/difficulty_post_processor.h" + +#include "smt/env.h" +#include "util/rational.h" + +using namespace cvc5::kind; +using namespace cvc5::theory; + +namespace cvc5 { +namespace smt { + +DifficultyPostprocessCallback::DifficultyPostprocessCallback() + : d_currDifficulty(0) +{ +} + +bool DifficultyPostprocessCallback::setCurrentDifficulty(Node d) +{ + if (d.isConst() && d.getType().isInteger() + && d.getConst<Rational>().sgn() >= 0 + && d.getConst<Rational>().getNumerator().fitsUnsignedInt()) + { + d_currDifficulty = d.getConst<Rational>().getNumerator().toUnsignedInt(); + return true; + } + return false; +} + +bool DifficultyPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn, + const std::vector<Node>& fa, + bool& continueUpdate) +{ + PfRule r = pn->getRule(); + if (r == PfRule::ASSUME) + { + Trace("difficulty-debug") + << " found assume: " << pn->getResult() << std::endl; + d_accMap[pn->getResult()] += d_currDifficulty; + } + else if (r == PfRule::MACRO_SR_EQ_INTRO || r == PfRule::MACRO_SR_PRED_INTRO) + { + // premise is just a substitution, ignore + continueUpdate = false; + return false; + } + return true; +} + +void DifficultyPostprocessCallback::getDifficultyMap( + std::map<Node, Node>& dmap) const +{ + Assert(dmap.empty()); + NodeManager* nm = NodeManager::currentNM(); + for (const std::pair<const Node, uint64_t>& d : d_accMap) + { + dmap[d.first] = nm->mkConst(Rational(d.second)); + } +} + +} // namespace smt +} // namespace cvc5 diff --git a/src/smt/difficulty_post_processor.h b/src/smt/difficulty_post_processor.h new file mode 100644 index 000000000..ef1c9a9ea --- /dev/null +++ b/src/smt/difficulty_post_processor.h @@ -0,0 +1,88 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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. + * **************************************************************************** + * + * Implementation of module for processing the difficulty of input assumptions + * based on proof nodes. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__SMT__DIFFICULTY_POST_PROCESSOR_H +#define CVC5__SMT__DIFFICULTY_POST_PROCESSOR_H + +#include <map> + +#include "proof/proof_node_updater.h" + +namespace cvc5 { +namespace smt { + +/** + * A postprocess callback that computes difficulty based on the structure + * of the proof. In particular, this class assesses what the source of an + * assertion was by considering the shape of the proof. For instance, if + * assertion A entails x=t, and this was used to derive a substitution + * { x -> t } to assertion B, then B is the source of B*{ x -> t }. The + * difficulty of this assertion is carried to B and not A. The reason is that + * A can be understood as a definition, and is eliminated, whereas B was + * persistent if B*{ x -> t } was a prepreprocessed assertion. + * + * Note that this postprocess callback is intended to be run on the proof + * of a single preprocessed assertion C. If C was derived by proof with + * free assumptions A_1, ..., A_n, then for each A_i that is a "source" as + * described above, we increment the difficulty of A_i by the difficulty value + * assigned to C. + * + * This means that the user of this method should: + * (1) assign the current difficulty we are incrementing (setCurrentDifficulty), + * (2) process the proof using a proof node updater with this callback. + * The final difficulty map is accumulated in d_accMap, which can be accessed + * at any time via getDifficultyMap. + */ +class DifficultyPostprocessCallback : public ProofNodeUpdaterCallback +{ + public: + DifficultyPostprocessCallback(); + ~DifficultyPostprocessCallback() {} + /** + * Set current difficulty of the next proof to process to the (integer) + * value stored in Node d. This value will be assigned to all the free + * assumptions of the proof we traverse next. This value is stored in + * d_currDifficulty. + * + * @return true if the difficulty value was successfully extracted + */ + bool setCurrentDifficulty(Node d); + /** + * Should proof pn be updated? This is used to selectively traverse to e.g. + * the source of an assertion. + */ + bool shouldUpdate(std::shared_ptr<ProofNode> pn, + const std::vector<Node>& fa, + bool& continueUpdate) override; + /** Get the (acculumated) difficulty map for the last processed proof node */ + void getDifficultyMap(std::map<Node, Node>& dmap) const; + + private: + /** + * The current difficulty of the assertion whose proof of preprocessing + * we are considering. + */ + uint64_t d_currDifficulty; + /** The current accumulated difficulty map */ + std::map<Node, uint64_t> d_accMap; +}; + +} // namespace smt +} // namespace cvc5 + +#endif diff --git a/src/smt/env_obj.cpp b/src/smt/env_obj.cpp index acc3ab038..32c6e4b02 100644 --- a/src/smt/env_obj.cpp +++ b/src/smt/env_obj.cpp @@ -24,7 +24,15 @@ namespace cvc5 { EnvObj::EnvObj(Env& env) : d_env(env) {} -Node EnvObj::rewrite(TNode node) { return d_env.getRewriter()->rewrite(node); } +Node EnvObj::rewrite(TNode node) const +{ + return d_env.getRewriter()->rewrite(node); +} + +Node EnvObj::extendedRewrite(TNode node, bool aggr) const +{ + return d_env.getRewriter()->extendedRewrite(node, aggr); +} const LogicInfo& EnvObj::logicInfo() const { return d_env.getLogicInfo(); } diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h index d1c882b96..4b907c27b 100644 --- a/src/smt/env_obj.h +++ b/src/smt/env_obj.h @@ -48,7 +48,12 @@ class EnvObj * Rewrite a node. * This is a wrapper around theory::Rewriter::rewrite via Env. */ - Node rewrite(TNode node); + Node rewrite(TNode node) const; + /** + * Extended rewrite a node. + * This is a wrapper around theory::Rewriter::extendedRewrite via Env. + */ + Node extendedRewrite(TNode node, bool aggr = true) const; /** Get the current logic information. */ const LogicInfo& logicInfo() const; diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 1e322ccd3..e2730151e 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -180,8 +180,7 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f) if (!proofStepProcessed) { // maybe its just an (extended) rewrite? - theory::quantifiers::ExtendedRewriter extr(true); - Node pr = extr.extendedRewrite(proven[0]); + Node pr = theory::Rewriter::callExtendedRewrite(proven[0]); if (proven[1] == pr) { Node idr = mkMethodId(MethodId::RW_EXT_REWRITE); diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 087aa0e06..08ba5b416 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -20,9 +20,7 @@ #include "expr/subs.h" #include "smt/smt_solver.h" #include "theory/quantifiers/cegqi/nested_qe.h" -#include "theory/quantifiers/extended_rewrite.h" #include "theory/quantifiers_engine.h" -#include "theory/rewriter.h" #include "theory/theory_engine.h" #include "util/string.h" @@ -33,7 +31,7 @@ namespace cvc5 { namespace smt { QuantElimSolver::QuantElimSolver(Env& env, SmtSolver& sms) - : d_env(env), d_smtSolver(sms) + : EnvObj(env), d_smtSolver(sms) { } @@ -52,7 +50,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, } NodeManager* nm = NodeManager::currentNM(); // ensure the body is rewritten - q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1])); + q = nm->mkNode(q.getKind(), q[0], rewrite(q[1])); // do nested quantifier elimination if necessary q = quantifiers::NestedQe::doNestedQe(d_env, q, true); Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : " @@ -110,7 +108,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl; if (q.getKind() == EXISTS) { - ret = Rewriter::rewrite(ret.negate()); + ret = rewrite(ret.negate()); } } else @@ -118,8 +116,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, ret = nm->mkConst(q.getKind() != EXISTS); } // do extended rewrite to minimize the size of the formula aggressively - theory::quantifiers::ExtendedRewriter extr(true); - ret = extr.extendedRewrite(ret); + ret = extendedRewrite(ret); // if we are not an internal subsolver, convert to witness form, since // internally generated skolems should not escape if (!isInternalSubsolver) diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h index f890deba0..a0b43d09d 100644 --- a/src/smt/quant_elim_solver.h +++ b/src/smt/quant_elim_solver.h @@ -20,10 +20,9 @@ #include "expr/node.h" #include "smt/assertions.h" +#include "smt/env_obj.h" namespace cvc5 { -class Env; - namespace smt { class SmtSolver; @@ -36,7 +35,7 @@ class SmtSolver; * quantifier instantiations used for unsat which are in turn used for * constructing the solution for the quantifier elimination query. */ -class QuantElimSolver +class QuantElimSolver : protected EnvObj { public: QuantElimSolver(Env& env, SmtSolver& sms); @@ -97,8 +96,6 @@ class QuantElimSolver bool isInternalSubsolver); private: - /** Reference to the env */ - Env& d_env; /** The SMT solver, which is used during doQuantifierElimination. */ SmtSolver& d_smtSolver; }; diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 3c35c2961..6e7939ff7 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -131,6 +131,17 @@ void SetDefaults::setDefaultsPre(Options& opts) Assert(opts.smt.unsatCores == (opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF)); + // new unsat core specific restrictions for proofs + if (opts.smt.unsatCores + && opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF) + { + // no fine-graininess + if (!opts.proof.proofGranularityModeWasSetByUser) + { + opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF; + } + } + if (opts.bv.bitvectorAigSimplificationsWasSetByUser) { Notice() << "SmtEngine: setting bitvectorAig" << std::endl; @@ -141,6 +152,21 @@ void SetDefaults::setDefaultsPre(Options& opts) Notice() << "SmtEngine: setting bitvectorAlgebraicSolver" << std::endl; opts.bv.bitvectorAlgebraicSolver = true; } + + // if we requiring disabling proofs, disable them now + if (opts.smt.produceProofs) + { + std::stringstream reasonNoProofs; + if (incompatibleWithProofs(opts, reasonNoProofs)) + { + opts.smt.unsatCores = false; + opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF; + Notice() << "SmtEngine: turning off produce-proofs due to " + << reasonNoProofs.str() << "." << std::endl; + opts.smt.produceProofs = false; + opts.smt.checkProofs = false; + } + } } void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const @@ -185,12 +211,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const } } - /* Disable bit-level propagation by default for the BITBLAST solver. */ - if (opts.bv.bvSolver == options::BVSolver::BITBLAST) - { - opts.bv.bitvectorPropagate = false; - } - if (opts.smt.solveIntAsBV > 0) { // Int to BV currently always eliminates arithmetic completely (or otherwise @@ -260,18 +280,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const } } - // --ite-simp is an experimental option designed for QF_LIA/nec. This - // technique is experimental. This benchmark set also requires removing ITEs - // during preprocessing, before repeating simplification. Hence, we enable - // this by default. - if (opts.smt.doITESimp) - { - if (!opts.smt.earlyIteRemovalWasSetByUser) - { - opts.smt.earlyIteRemoval = true; - } - } - // Set default options associated with strings-exp. We also set these options // if we are using eager string preprocessing, which may introduce quantified // formulas at preprocess time. @@ -303,17 +311,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const // quantifiers (those marked with InternalQuantAttribute). } - // new unsat core specific restrictions for proofs - if (opts.smt.unsatCores - && opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF) - { - // no fine-graininess - if (!opts.proof.proofGranularityModeWasSetByUser) - { - opts.proof.proofGranularityMode = options::ProofGranularityMode::OFF; - } - } - if (opts.arrays.arraysExp) { if (!logic.isQuantified()) @@ -322,12 +319,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const logic.enableQuantifiers(); logic.lock(); } - // Allows to answer sat more often by default. - if (!opts.quantifiers.fmfBoundWasSetByUser) - { - opts.quantifiers.fmfBound = true; - Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl; - } } // We now know whether the input uses sygus. Update the logic to incorporate @@ -339,20 +330,24 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const logic.lock(); } - // if we requiring disabling proofs, disable them now - if (opts.smt.produceProofs) + // widen the logic + widenLogic(logic, opts); + + // check if we have any options that are not supported with quantified logics + if (logic.isQuantified()) { - std::stringstream reasonNoProofs; - if (incompatibleWithProofs(opts, reasonNoProofs)) + std::stringstream reasonNoQuant; + if (incompatibleWithQuantifiers(opts, reasonNoQuant)) { - opts.smt.unsatCores = false; - opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF; - Notice() << "SmtEngine: turning off produce-proofs due to " - << reasonNoProofs.str() << "." << std::endl; - opts.smt.produceProofs = false; - opts.smt.checkProofs = false; + std::stringstream ss; + ss << reasonNoQuant.str() << " not supported in quantified logics."; + throw OptionException(ss.str()); } } +} + +void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const +{ // sygus core connective requires unsat cores if (opts.quantifiers.sygusCoreConnective) @@ -473,25 +468,19 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const Notice() << "SmtEngine: turning on produce-models" << std::endl; opts.smt.produceModels = true; } - - // widen the logic - widenLogic(logic, opts); - - // check if we have any options that are not supported with quantified logics - if (logic.isQuantified()) + + // --ite-simp is an experimental option designed for QF_LIA/nec. This + // technique is experimental. This benchmark set also requires removing ITEs + // during preprocessing, before repeating simplification. Hence, we enable + // this by default. + if (opts.smt.doITESimp) { - std::stringstream reasonNoQuant; - if (incompatibleWithQuantifiers(opts, reasonNoQuant)) + if (!opts.smt.earlyIteRemovalWasSetByUser) { - std::stringstream ss; - ss << reasonNoQuant.str() << " not supported in quantified logics."; - throw OptionException(ss.str()); + opts.smt.earlyIteRemoval = true; } } -} - -void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const -{ + // Set the options for the theoryOf if (!opts.theory.theoryOfModeWasSetByUser) { @@ -566,7 +555,13 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const << std::endl; opts.smt.repeatSimp = repeatSimp; } - + + /* Disable bit-level propagation by default for the BITBLAST solver. */ + if (opts.bv.bvSolver == options::BVSolver::BITBLAST) + { + opts.bv.bitvectorPropagate = false; + } + if (opts.bv.boolToBitvector == options::BoolToBVMode::ALL && !logic.isTheoryEnabled(THEORY_BV)) { @@ -678,17 +673,6 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const } } - if (opts.base.incrementalSolving) - { - // disable modes not supported by incremental - opts.smt.sortInference = false; - opts.uf.ufssFairnessMonotone = false; - opts.quantifiers.globalNegate = false; - opts.quantifiers.cegqiNestedQE = false; - opts.bv.bvAbstraction = false; - opts.arith.arithMLTrick = false; - } - if (logic.isHigherOrder()) { opts.uf.ufHo = true; @@ -702,6 +686,16 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const // set all defaults in the quantifiers theory, which includes sygus setDefaultsQuantifiers(logic, opts); + // shared selectors are generally not good to combine with standard + // quantifier techniques e.g. E-matching + if (!opts.datatypes.dtSharedSelectorsWasSetByUser) + { + if (logic.isQuantified() && !usesSygus(opts)) + { + opts.datatypes.dtSharedSelectors = false; + } + } + // until bugs 371,431 are fixed if (!opts.prop.minisatUseElimWasSetByUser) { @@ -986,6 +980,15 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic, reason << "solveIntAsBV"; return true; } + + // disable modes not supported by incremental + opts.smt.sortInference = false; + opts.uf.ufssFairnessMonotone = false; + opts.quantifiers.globalNegate = false; + opts.quantifiers.cegqiNestedQE = false; + opts.bv.bvAbstraction = false; + opts.arith.arithMLTrick = false; + return false; } @@ -1163,7 +1166,7 @@ bool SetDefaults::incompatibleWithQuantifiers(Options& opts, return false; } -void SetDefaults::widenLogic(LogicInfo& logic, Options& opts) const +void SetDefaults::widenLogic(LogicInfo& logic, const Options& opts) const { bool needsUf = false; // strings require LIA, UF; widen the logic @@ -1254,6 +1257,15 @@ void SetDefaults::widenLogic(LogicInfo& logic, Options& opts) const void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic, Options& opts) const { + if (opts.arrays.arraysExp) + { + // Allows to answer sat more often by default. + if (!opts.quantifiers.fmfBoundWasSetByUser) + { + opts.quantifiers.fmfBound = true; + Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl; + } + } if (logic.hasCardinalityConstraints()) { // must have finite model finding on diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h index 293f1398d..4d1bf5bcb 100644 --- a/src/smt/set_defaults.h +++ b/src/smt/set_defaults.h @@ -115,7 +115,7 @@ class SetDefaults * use of other theories to handle certain operators, e.g. UF to handle * partial functions. */ - void widenLogic(LogicInfo& logic, Options& opts) const; + void widenLogic(LogicInfo& logic, const Options& opts) const; //------------------------- options setting, post finalization of logic /** * Set all default options, after we have finalized the logic. diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp index 6ab399348..ba2de9fdf 100644 --- a/src/theory/arith/arith_preprocess.cpp +++ b/src/theory/arith/arith_preprocess.cpp @@ -23,11 +23,12 @@ namespace cvc5 { namespace theory { namespace arith { -ArithPreprocess::ArithPreprocess(ArithState& state, +ArithPreprocess::ArithPreprocess(Env& env, + ArithState& state, InferenceManager& im, ProofNodeManager* pnm, OperatorElim& oe) - : d_im(im), d_opElim(oe), d_reduced(state.getUserContext()) + : EnvObj(env), d_im(im), d_opElim(oe), d_reduced(userContext()) { } TrustNode ArithPreprocess::eliminate(TNode n, diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h index a537c33c7..939306a6e 100644 --- a/src/theory/arith/arith_preprocess.h +++ b/src/theory/arith/arith_preprocess.h @@ -19,6 +19,7 @@ #define CVC5__THEORY__ARITH__ARITH_PREPROCESS_H #include "context/cdhashmap.h" +#include "smt/env_obj.h" #include "theory/arith/operator_elim.h" #include "theory/logic_info.h" @@ -40,10 +41,11 @@ class OperatorElim; * extends that utility with the ability to generate lemmas on demand via * the provided inference manager. */ -class ArithPreprocess +class ArithPreprocess : protected EnvObj { public: - ArithPreprocess(ArithState& state, + ArithPreprocess(Env& env, + ArithState& state, InferenceManager& im, ProofNodeManager* pnm, OperatorElim& oe); diff --git a/src/theory/arith/branch_and_bound.cpp b/src/theory/arith/branch_and_bound.cpp index ca1a2fa6f..31017dea6 100644 --- a/src/theory/arith/branch_and_bound.cpp +++ b/src/theory/arith/branch_and_bound.cpp @@ -28,14 +28,16 @@ namespace cvc5 { namespace theory { namespace arith { -BranchAndBound::BranchAndBound(ArithState& s, +BranchAndBound::BranchAndBound(Env& env, + ArithState& s, InferenceManager& im, PreprocessRewriteEq& ppre, ProofNodeManager* pnm) - : d_astate(s), + : EnvObj(env), + d_astate(s), d_im(im), d_ppre(ppre), - d_pfGen(new EagerProofGenerator(pnm, s.getUserContext())), + d_pfGen(new EagerProofGenerator(pnm, userContext())), d_pnm(pnm) { } @@ -45,7 +47,7 @@ TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value) TrustNode lem = TrustNode::null(); NodeManager* nm = NodeManager::currentNM(); Integer floor = value.floor(); - if (d_astate.options().arith.brabTest) + if (options().arith.brabTest) { Trace("integers") << "branch-round-and-bound enabled" << std::endl; Integer ceil = value.ceiling(); diff --git a/src/theory/arith/branch_and_bound.h b/src/theory/arith/branch_and_bound.h index 4281ba678..52acf6aae 100644 --- a/src/theory/arith/branch_and_bound.h +++ b/src/theory/arith/branch_and_bound.h @@ -23,6 +23,7 @@ #include "expr/node.h" #include "proof/proof_node_manager.h" #include "proof/trust_node.h" +#include "smt/env_obj.h" #include "theory/arith/arith_state.h" #include "theory/arith/inference_manager.h" #include "theory/arith/pp_rewrite_eq.h" @@ -37,10 +38,11 @@ namespace arith { * agnostic to the state of solver; instead is simply given (variable, value) * pairs in branchIntegerVariable below and constructs the appropriate lemma. */ -class BranchAndBound +class BranchAndBound : protected EnvObj { public: - BranchAndBound(ArithState& s, + BranchAndBound(Env& env, + ArithState& s, InferenceManager& im, PreprocessRewriteEq& ppre, ProofNodeManager* pnm); diff --git a/src/theory/arith/equality_solver.cpp b/src/theory/arith/equality_solver.cpp index 8b4e1b8dd..8e5cc9a28 100644 --- a/src/theory/arith/equality_solver.cpp +++ b/src/theory/arith/equality_solver.cpp @@ -23,12 +23,15 @@ namespace cvc5 { namespace theory { namespace arith { -EqualitySolver::EqualitySolver(ArithState& astate, InferenceManager& aim) - : d_astate(astate), +EqualitySolver::EqualitySolver(Env& env, + ArithState& astate, + InferenceManager& aim) + : EnvObj(env), + d_astate(astate), d_aim(aim), d_notify(*this), d_ee(nullptr), - d_propLits(astate.getSatContext()) + d_propLits(context()) { } diff --git a/src/theory/arith/equality_solver.h b/src/theory/arith/equality_solver.h index bce30e697..8528650f0 100644 --- a/src/theory/arith/equality_solver.h +++ b/src/theory/arith/equality_solver.h @@ -21,6 +21,7 @@ #include "context/cdhashset.h" #include "expr/node.h" #include "proof/trust_node.h" +#include "smt/env_obj.h" #include "theory/arith/arith_state.h" #include "theory/ee_setup_info.h" #include "theory/uf/equality_engine.h" @@ -39,12 +40,12 @@ class InferenceManager; * the literals that it propagates and only explains the literals that * originated from this class. */ -class EqualitySolver +class EqualitySolver : protected EnvObj { using NodeSet = context::CDHashSet<Node>; public: - EqualitySolver(ArithState& astate, InferenceManager& aim); + EqualitySolver(Env& env, ArithState& astate, InferenceManager& aim); ~EqualitySolver() {} //--------------------------------- initialization /** diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index 5ab606f96..0c6b18893 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -30,7 +30,7 @@ InferenceManager::InferenceManager(Env& env, ProofNodeManager* pnm) : InferenceManagerBuffered(env, ta, astate, pnm, "theory::arith::"), // currently must track propagated literals if using the equality solver - d_trackPropLits(astate.options().arith.arithEqSolver), + d_trackPropLits(options().arith.arithEqSolver), d_propLits(context()) { } @@ -128,7 +128,7 @@ bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p) bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem) { - if (d_theoryState.options().arith.nlExtEntailConflicts) + if (options().arith.nlExtEntailConflicts) { Node ch_lemma = lem.d_node.negate(); ch_lemma = Rewriter::rewrite(ch_lemma); diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index 9b37a135f..9b7678388 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -23,7 +23,7 @@ #include "theory/arith/nl/cad/projections.h" #include "theory/arith/nl/cad/variable_ordering.h" #include "theory/arith/nl/nl_model.h" -#include "theory/quantifiers/extended_rewrite.h" +#include "theory/rewriter.h" namespace std { /** Generic streaming operator for std::vector. */ @@ -42,7 +42,7 @@ namespace nl { namespace cad { CDCAC::CDCAC(Env& env, const std::vector<poly::Variable>& ordering) - : d_env(env), d_variableOrdering(ordering) + : EnvObj(env), d_variableOrdering(ordering) { if (d_env.isTheoryProofProducing()) { @@ -276,9 +276,8 @@ PolyVector requiredCoefficientsLazardModified( Kind::EQUAL, nl::as_cvc_polynomial(coeff, vm), zero)); } // if phi is false (i.e. p can not vanish) - quantifiers::ExtendedRewriter rew; - Node rewritten = - rew.extendedRewrite(NodeManager::currentNM()->mkAnd(conditions)); + Node rewritten = Rewriter::callExtendedRewrite( + NodeManager::currentNM()->mkAnd(conditions)); if (rewritten.isConst()) { Assert(rewritten.getKind() == Kind::CONST_BOOLEAN); diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index b504998d8..be72e4063 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -26,6 +26,7 @@ #include <vector> #include "smt/env.h" +#include "smt/env_obj.h" #include "theory/arith/nl/cad/cdcac_utils.h" #include "theory/arith/nl/cad/constraints.h" #include "theory/arith/nl/cad/proof_generator.h" @@ -44,7 +45,7 @@ namespace cad { * This class implements Cylindrical Algebraic Coverings as presented in * https://arxiv.org/pdf/2003.05633.pdf */ -class CDCAC +class CDCAC : protected EnvObj { public: /** Initialize this method with the given variable ordering. */ @@ -184,9 +185,6 @@ class CDCAC */ void pruneRedundantIntervals(std::vector<CACInterval>& intervals); - /** A reference to the environment */ - Env& d_env; - /** * The current assignment. When the method terminates with SAT, it contains a * model for the input constraints. diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index eb5620a82..76d964934 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -34,11 +34,15 @@ namespace theory { namespace arith { namespace nl { -IAndSolver::IAndSolver(InferenceManager& im, ArithState& state, NlModel& model) - : d_im(im), +IAndSolver::IAndSolver(Env& env, + InferenceManager& im, + ArithState& state, + NlModel& model) + : EnvObj(env), + d_im(im), d_model(model), d_astate(state), - d_initRefine(state.getUserContext()) + d_initRefine(userContext()) { NodeManager* nm = NodeManager::currentNM(); d_false = nm->mkConst(false); @@ -152,7 +156,7 @@ void IAndSolver::checkFullRefine() } // ************* additional lemma schemas go here - if (d_astate.options().smt.iandMode == options::IandMode::SUM) + if (options().smt.iandMode == options::IandMode::SUM) { Node lem = sumBasedLemma(i); // add lemmas based on sum mode Trace("iand-lemma") @@ -162,7 +166,7 @@ void IAndSolver::checkFullRefine() d_im.addPendingLemma( lem, InferenceId::ARITH_NL_IAND_SUM_REFINE, nullptr, true); } - else if (d_astate.options().smt.iandMode == options::IandMode::BITWISE) + else if (options().smt.iandMode == options::IandMode::BITWISE) { Node lem = bitwiseLemma(i); // check for violated bitwise axioms Trace("iand-lemma") @@ -245,7 +249,7 @@ Node IAndSolver::sumBasedLemma(Node i) Node x = i[0]; Node y = i[1]; size_t bvsize = i.getOperator().getConst<IntAnd>().d_size; - uint64_t granularity = d_astate.options().smt.BVAndIntegerGranularity; + uint64_t granularity = options().smt.BVAndIntegerGranularity; NodeManager* nm = NodeManager::currentNM(); Node lem = nm->mkNode( EQUAL, i, d_iandUtils.createSumNode(x, y, bvsize, granularity)); @@ -259,7 +263,7 @@ Node IAndSolver::bitwiseLemma(Node i) Node y = i[1]; unsigned bvsize = i.getOperator().getConst<IntAnd>().d_size; - uint64_t granularity = d_astate.options().smt.BVAndIntegerGranularity; + uint64_t granularity = options().smt.BVAndIntegerGranularity; Rational absI = d_model.computeAbstractModelValue(i).getConst<Rational>(); Rational concI = d_model.computeConcreteModelValue(i).getConst<Rational>(); diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index 1be469259..0b6a1fac6 100644 --- a/src/theory/arith/nl/iand_solver.h +++ b/src/theory/arith/nl/iand_solver.h @@ -21,6 +21,7 @@ #include "context/cdhashset.h" #include "expr/node.h" +#include "smt/env_obj.h" #include "theory/arith/nl/iand_utils.h" namespace cvc5 { @@ -37,12 +38,12 @@ class NlModel; /** Integer and solver class * */ -class IAndSolver +class IAndSolver : protected EnvObj { typedef context::CDHashSet<Node> NodeSet; public: - IAndSolver(InferenceManager& im, ArithState& state, NlModel& model); + IAndSolver(Env& env, InferenceManager& im, ArithState& state, NlModel& model); ~IAndSolver(); /** init last call diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index db92009f4..b8170df45 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -49,17 +49,17 @@ NonlinearExtension::NonlinearExtension(Env& env, d_extTheoryCb(state.getEqualityEngine()), d_extTheory(d_extTheoryCb, context(), userContext(), d_im), d_model(), - d_trSlv(d_im, d_model, d_astate.getEnv()), - d_extState(d_im, d_model, d_astate.getEnv()), + d_trSlv(d_im, d_model, d_env), + d_extState(d_im, d_model, d_env), d_factoringSlv(&d_extState), d_monomialBoundsSlv(&d_extState), d_monomialSlv(&d_extState), d_splitZeroSlv(&d_extState), d_tangentPlaneSlv(&d_extState), - d_cadSlv(d_astate.getEnv(), d_im, d_model), + d_cadSlv(d_env, d_im, d_model), d_icpSlv(d_im), - d_iandSlv(d_im, state, d_model), - d_pow2Slv(d_im, state, d_model) + d_iandSlv(env, d_im, state, d_model), + d_pow2Slv(env, d_im, state, d_model) { d_extTheory.addFunctionKind(kind::NONLINEAR_MULT); d_extTheory.addFunctionKind(kind::EXPONENTIAL); @@ -72,9 +72,9 @@ NonlinearExtension::NonlinearExtension(Env& env, d_one = NodeManager::currentNM()->mkConst(Rational(1)); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); - if (d_astate.getEnv().isTheoryProofProducing()) + if (d_env.isTheoryProofProducing()) { - ProofChecker* pc = d_astate.getEnv().getProofNodeManager()->getChecker(); + ProofChecker* pc = d_env.getProofNodeManager()->getChecker(); d_proofChecker.registerTo(pc); } } diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp index d708e86e1..597a0df96 100644 --- a/src/theory/arith/nl/pow2_solver.cpp +++ b/src/theory/arith/nl/pow2_solver.cpp @@ -33,8 +33,11 @@ namespace theory { namespace arith { namespace nl { -Pow2Solver::Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model) - : d_im(im), d_model(model), d_initRefine(state.getUserContext()) +Pow2Solver::Pow2Solver(Env& env, + InferenceManager& im, + ArithState& state, + NlModel& model) + : EnvObj(env), d_im(im), d_model(model), d_initRefine(userContext()) { NodeManager* nm = NodeManager::currentNM(); d_false = nm->mkConst(false); diff --git a/src/theory/arith/nl/pow2_solver.h b/src/theory/arith/nl/pow2_solver.h index 4c6fb8014..b4e12616c 100644 --- a/src/theory/arith/nl/pow2_solver.h +++ b/src/theory/arith/nl/pow2_solver.h @@ -20,6 +20,7 @@ #include "context/cdhashset.h" #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5 { namespace theory { @@ -35,12 +36,12 @@ class NlModel; /** pow2 solver class * */ -class Pow2Solver +class Pow2Solver : protected EnvObj { using NodeSet = context::CDHashSet<Node>; public: - Pow2Solver(InferenceManager& im, ArithState& state, NlModel& model); + Pow2Solver(Env& env, InferenceManager& im, ArithState& state, NlModel& model); ~Pow2Solver(); /** init last call diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index d94f81e9c..9642bf394 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -42,12 +42,12 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) d_astate(env, valuation), d_im(env, *this, d_astate, d_pnm), d_ppre(context(), d_pnm), - d_bab(d_astate, d_im, d_ppre, d_pnm), + d_bab(env, d_astate, d_im, d_ppre, d_pnm), d_eqSolver(nullptr), d_internal(new TheoryArithPrivate(*this, env, d_bab)), d_nonlinearExtension(nullptr), d_opElim(d_pnm, logicInfo()), - d_arithPreproc(d_astate, d_im, d_pnm, d_opElim), + d_arithPreproc(env, d_astate, d_im, d_pnm, d_opElim), d_rewriter(d_opElim) { // currently a cyclic dependency to TheoryArithPrivate @@ -58,7 +58,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) if (options().arith.arithEqSolver) { - d_eqSolver.reset(new EqualitySolver(d_astate, d_im)); + d_eqSolver.reset(new EqualitySolver(env, d_astate, d_im)); } } diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index e59dfcc13..4eef9a018 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -33,7 +33,7 @@ InferenceManager::InferenceManager(Env& env, ProofNodeManager* pnm) : TheoryInferenceManager(env, t, state, pnm, "theory::arrays::", false), d_lemmaPg(pnm ? new EagerProofGenerator( - pnm, state.getUserContext(), "ArrayLemmaProofGenerator") + pnm, userContext(), "ArrayLemmaProofGenerator") : nullptr) { } diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp index 659886e83..7e995eab5 100644 --- a/src/theory/bags/term_registry.cpp +++ b/src/theory/bags/term_registry.cpp @@ -26,10 +26,11 @@ namespace cvc5 { namespace theory { namespace bags { -TermRegistry::TermRegistry(SolverState& state, InferenceManager& im) - : d_im(im), - d_proxy(state.getUserContext()), - d_proxy_to_term(state.getUserContext()) +TermRegistry::TermRegistry(Env& env, SolverState& state, InferenceManager& im) + : EnvObj(env), + d_im(im), + d_proxy(userContext()), + d_proxy_to_term(userContext()) { } diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h index 2b0218fdf..f36dda1a9 100644 --- a/src/theory/bags/term_registry.h +++ b/src/theory/bags/term_registry.h @@ -22,6 +22,7 @@ #include "context/cdhashmap.h" #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5 { namespace theory { @@ -34,12 +35,12 @@ class SolverState; * Term registry, the purpose of this class is to maintain a database of * commonly used terms, and mappings from bags to their "proxy variables". */ -class TermRegistry +class TermRegistry : protected EnvObj { typedef context::CDHashMap<Node, Node> NodeMap; public: - TermRegistry(SolverState& state, InferenceManager& im); + TermRegistry(Env& env, SolverState& state, InferenceManager& im); /** * Returns the existing empty bag for type tn diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index c421b9ec2..004766d83 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -35,7 +35,7 @@ TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation) d_notify(*this, d_im), d_statistics(), d_rewriter(&d_statistics.d_rewrites), - d_termReg(d_state, d_im), + d_termReg(env, d_state, d_im), d_solver(d_state, d_im, d_termReg) { // use the official theory state and inference manager objects diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 8b3988f27..59a84c86e 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -22,7 +22,6 @@ #include "proof/method_id.h" #include "proof/proof_checker.h" #include "proof/proof_node.h" -#include "theory/quantifiers/extended_rewrite.h" namespace cvc5 { @@ -114,9 +113,6 @@ class BuiltinProofRuleChecker : public ProofRuleChecker const std::vector<Node>& children, const std::vector<Node>& args) override; - /** extended rewriter object */ - quantifiers::ExtendedRewriter d_ext_rewriter; - private: /** Reference to the environment. */ Env& d_env; diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h index c959fb648..510c8a29a 100644 --- a/src/theory/bv/bv_solver.h +++ b/src/theory/bv/bv_solver.h @@ -20,17 +20,19 @@ #ifndef CVC5__THEORY__BV__BV_SOLVER_H #define CVC5__THEORY__BV__BV_SOLVER_H +#include "smt/env.h" +#include "smt/env_obj.h" #include "theory/theory.h" namespace cvc5 { namespace theory { namespace bv { -class BVSolver +class BVSolver : protected EnvObj { public: - BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr) - : d_state(state), d_im(inferMgr){}; + BVSolver(Env& env, TheoryState& state, TheoryInferenceManager& inferMgr) + : EnvObj(env), d_state(state), d_im(inferMgr){}; virtual ~BVSolver() {} diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index ecd42e4a0..9d316e91e 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -108,10 +108,11 @@ class BBRegistrar : public prop::Registrar std::unordered_set<TNode> d_registeredAtoms; }; -BVSolverBitblast::BVSolverBitblast(TheoryState* s, +BVSolverBitblast::BVSolverBitblast(Env& env, + TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm) - : BVSolver(*s, inferMgr), + : BVSolver(env, *s, inferMgr), d_bitblaster(new NodeBitblaster(s)), d_bbRegistrar(new BBRegistrar(d_bitblaster.get())), d_nullContext(new context::Context()), @@ -123,7 +124,7 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s, : nullptr), d_factLiteralCache(s->getSatContext()), d_literalFactCache(s->getSatContext()), - d_propagate(options::bitvectorPropagate()), + d_propagate(options().bv.bitvectorPropagate), d_resetNotify(new NotifyResetAssertions(s->getUserContext())) { if (pnm != nullptr) @@ -147,7 +148,7 @@ void BVSolverBitblast::postCheck(Theory::Effort level) // If we permanently added assertions to the SAT solver and the assertions // were reset, we have to reset the SAT solver and the CNF stream. - if (options::bvAssertInput() && d_resetNotify->doneResetAssertions()) + if (options().bv.bvAssertInput && d_resetNotify->doneResetAssertions()) { d_satSolver.reset(nullptr); d_cnfStream.reset(nullptr); @@ -248,7 +249,7 @@ bool BVSolverBitblast::preNotifyFact( * If this is the case we can assert `fact` to the SAT solver instead of * using assumptions. */ - if (options::bvAssertInput() && val.isSatLiteral(fact) + if (options().bv.bvAssertInput && val.isSatLiteral(fact) && val.getDecisionLevel(fact) == 0 && val.getIntroLevel(fact) == 0) { Assert(!val.isDecision(fact)); @@ -277,7 +278,7 @@ void BVSolverBitblast::computeRelevantTerms(std::set<Node>& termSet) * in BitblastMode::EAGER and therefore add all variables from the * bit-blaster to `termSet`. */ - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) { d_bitblaster->computeRelevantTerms(termSet); } @@ -303,7 +304,7 @@ bool BVSolverBitblast::collectModelValues(TheoryModel* m, // In eager bitblast mode we also have to collect the model values for // Boolean variables in the CNF stream. - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) { NodeManager* nm = NodeManager::currentNM(); std::vector<TNode> vars; @@ -327,7 +328,7 @@ bool BVSolverBitblast::collectModelValues(TheoryModel* m, void BVSolverBitblast::initSatSolver() { - switch (options::bvSatSolver()) + switch (options().bv.bvSatSolver) { case options::SatSolverMode::CRYPTOMINISAT: d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat( diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 3f4ab5025..e8931acff 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -42,7 +42,8 @@ class BBRegistrar; class BVSolverBitblast : public BVSolver { public: - BVSolverBitblast(TheoryState* state, + BVSolverBitblast(Env& env, + TheoryState* state, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm); ~BVSolverBitblast() = default; diff --git a/src/theory/bv/bv_solver_bitblast_internal.cpp b/src/theory/bv/bv_solver_bitblast_internal.cpp index 1b606a0e9..71a29f472 100644 --- a/src/theory/bv/bv_solver_bitblast_internal.cpp +++ b/src/theory/bv/bv_solver_bitblast_internal.cpp @@ -68,8 +68,11 @@ void collectBVAtoms(TNode n, std::unordered_set<Node>& atoms) } // namespace BVSolverBitblastInternal::BVSolverBitblastInternal( - TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm) - : BVSolver(*s, inferMgr), + Env& env, + TheoryState* s, + TheoryInferenceManager& inferMgr, + ProofNodeManager* pnm) + : BVSolver(env, *s, inferMgr), d_pnm(pnm), d_bitblaster(new BBProof(s, pnm, false)) { diff --git a/src/theory/bv/bv_solver_bitblast_internal.h b/src/theory/bv/bv_solver_bitblast_internal.h index 2fc7173d1..cc365e109 100644 --- a/src/theory/bv/bv_solver_bitblast_internal.h +++ b/src/theory/bv/bv_solver_bitblast_internal.h @@ -37,7 +37,8 @@ namespace bv { class BVSolverBitblastInternal : public BVSolver { public: - BVSolverBitblastInternal(TheoryState* state, + BVSolverBitblastInternal(Env& env, + TheoryState* state, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm); ~BVSolverBitblastInternal() = default; diff --git a/src/theory/bv/bv_solver_layered.cpp b/src/theory/bv/bv_solver_layered.cpp index 40daf1cb4..bf76ed2f9 100644 --- a/src/theory/bv/bv_solver_layered.cpp +++ b/src/theory/bv/bv_solver_layered.cpp @@ -38,11 +38,12 @@ namespace theory { namespace bv { BVSolverLayered::BVSolverLayered(TheoryBV& bv, + Env& env, context::Context* c, context::UserContext* u, ProofNodeManager* pnm, std::string name) - : BVSolver(bv.d_state, bv.d_im), + : BVSolver(env, bv.d_state, bv.d_im), d_bv(bv), d_context(c), d_alreadyPropagatedSet(c), @@ -61,32 +62,32 @@ BVSolverLayered::BVSolverLayered(TheoryBV& bv, d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))), d_calledPreregister(false) { - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) { d_eagerSolver.reset(new EagerBitblastSolver(c, this)); return; } - if (options::bitvectorEqualitySolver()) + if (options().bv.bitvectorEqualitySolver) { d_subtheories.emplace_back(new CoreSolver(c, this)); d_subtheoryMap[SUB_CORE] = d_subtheories.back().get(); } - if (options::bitvectorInequalitySolver()) + if (options().bv.bitvectorInequalitySolver) { d_subtheories.emplace_back(new InequalitySolver(c, u, this)); d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get(); } - if (options::bitvectorAlgebraicSolver()) + if (options().bv.bitvectorAlgebraicSolver) { d_subtheories.emplace_back(new AlgebraicSolver(c, this)); d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get(); } BitblastSolver* bb_solver = new BitblastSolver(c, this); - if (options::bvAbstraction()) + if (options().bv.bvAbstraction) { bb_solver->setAbstraction(d_abstractionModule.get()); } @@ -141,7 +142,7 @@ void BVSolverLayered::preRegisterTerm(TNode node) Debug("bitvector-preregister") << "BVSolverLayered::preRegister(" << node << ")" << std::endl; - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) { // the aig bit-blaster option is set heuristically // if bv abstraction is used @@ -235,7 +236,7 @@ void BVSolverLayered::check(Theory::Effort e) // we may be getting new assertions so the model cache may not be sound d_invalidateModelCache.set(true); // if we are using the eager solver - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) { // this can only happen on an empty benchmark if (!d_eagerSolver->isInitialized()) @@ -322,7 +323,7 @@ bool BVSolverLayered::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) { Assert(!inConflict()); - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) { if (!d_eagerSolver->collectModelInfo(m, true)) { @@ -355,7 +356,7 @@ Node BVSolverLayered::getModelValue(TNode var) void BVSolverLayered::propagate(Theory::Effort e) { Debug("bitvector") << indent() << "BVSolverLayered::propagate()" << std::endl; - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) { return; } @@ -394,15 +395,15 @@ TrustNode BVSolverLayered::ppRewrite(TNode t) { Debug("bv-pp-rewrite") << "BVSolverLayered::ppRewrite " << t << "\n"; Node res = t; - if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t)) + if (options().bv.bitwiseEq && RewriteRule<BitwiseEq>::applies(t)) { Node result = RewriteRule<BitwiseEq>::run<false>(t); - res = Rewriter::rewrite(result); + res = rewrite(result); } else if (RewriteRule<UltAddOne>::applies(t)) { Node result = RewriteRule<UltAddOne>::run<false>(t); - res = Rewriter::rewrite(result); + res = rewrite(result); } else if (res.getKind() == kind::EQUAL && ((res[0].getKind() == kind::BITVECTOR_ADD @@ -419,7 +420,7 @@ TrustNode BVSolverLayered::ppRewrite(TNode t) Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq); if (rewr_eq[0].isVar() || rewr_eq[1].isVar()) { - res = Rewriter::rewrite(rewr_eq); + res = rewrite(rewr_eq); } else { @@ -451,7 +452,7 @@ TrustNode BVSolverLayered::ppRewrite(TNode t) // if (RewriteRule<MultSlice>::applies(mult)) { // Node new_mult = RewriteRule<MultSlice>::run<false>(mult); // Node new_eq = - // Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, + // rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, // new_mult, add)); // // the simplification can cause the formula to blow up @@ -475,7 +476,7 @@ TrustNode BVSolverLayered::ppRewrite(TNode t) // } // } - if (options::bvAbstraction() && t.getType().isBoolean()) + if (options().bv.bvAbstraction && t.getType().isBoolean()) { d_abstractionModule->addInputAtom(res); } @@ -595,9 +596,9 @@ void BVSolverLayered::notifySharedTerm(TNode t) EqualityStatus BVSolverLayered::getEqualityStatus(TNode a, TNode b) { - if (options::bitblastMode() == options::BitblastMode::EAGER) + if (options().bv.bitblastMode == options::BitblastMode::EAGER) return EQUALITY_UNKNOWN; - Assert(options::bitblastMode() == options::BitblastMode::LAZY); + Assert(options().bv.bitblastMode == options::BitblastMode::LAZY); for (unsigned i = 0; i < d_subtheories.size(); ++i) { EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); @@ -665,8 +666,8 @@ bool BVSolverLayered::applyAbstraction(const std::vector<Node>& assertions, { bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions); - if (changed && options::bitblastMode() == options::BitblastMode::EAGER - && options::bitvectorAig()) + if (changed && options().bv.bitblastMode == options::BitblastMode::EAGER + && options().bv.bitvectorAig) { // disable AIG mode AlwaysAssert(!d_eagerSolver->isInitialized()); @@ -678,7 +679,7 @@ bool BVSolverLayered::applyAbstraction(const std::vector<Node>& assertions, void BVSolverLayered::setConflict(Node conflict) { - if (options::bvAbstraction()) + if (options().bv.bvAbstraction) { NodeManager* const nm = NodeManager::currentNM(); Node new_conflict = d_abstractionModule->simplifyConflict(conflict); diff --git a/src/theory/bv/bv_solver_layered.h b/src/theory/bv/bv_solver_layered.h index 023ff5a46..325f2fc72 100644 --- a/src/theory/bv/bv_solver_layered.h +++ b/src/theory/bv/bv_solver_layered.h @@ -58,6 +58,7 @@ class BVSolverLayered : public BVSolver public: BVSolverLayered(TheoryBV& bv, + Env& env, context::Context* c, context::UserContext* u, ProofNodeManager* pnm = nullptr, diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 7493a54c7..96eccea57 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -43,20 +43,22 @@ TheoryBV::TheoryBV(Env& env, d_invalidateModelCache(context(), true), d_stats("theory::bv::") { - switch (options::bvSolver()) + switch (options().bv.bvSolver) { case options::BVSolver::BITBLAST: - d_internal.reset(new BVSolverBitblast(&d_state, d_im, d_pnm)); + d_internal.reset(new BVSolverBitblast(d_env, &d_state, d_im, d_pnm)); break; case options::BVSolver::LAYERED: - d_internal.reset( - new BVSolverLayered(*this, context(), userContext(), d_pnm, name)); + d_internal.reset(new BVSolverLayered( + *this, d_env, context(), userContext(), d_pnm, name)); break; default: - AlwaysAssert(options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL); - d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, d_pnm)); + AlwaysAssert(options().bv.bvSolver + == options::BVSolver::BITBLAST_INTERNAL); + d_internal.reset( + new BVSolverBitblastInternal(d_env, &d_state, d_im, d_pnm)); } d_theoryState = &d_state; d_inferManager = &d_im; @@ -68,7 +70,7 @@ TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; } ProofRuleChecker* TheoryBV::getProofChecker() { - if (options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL) + if (options().bv.bvSolver == options::BVSolver::BITBLAST_INTERNAL) { return static_cast<BVSolverBitblastInternal*>(d_internal.get()) ->getProofChecker(); @@ -222,7 +224,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert( * x = c::sk2 if h == bw(x)-1, where bw(sk2) = l * x = sk1::c::sk2 otherwise, where bw(sk1) = bw(x)-1-h and bw(sk2) = l */ - Node node = Rewriter::rewrite(in); + Node node = rewrite(in); if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst()) || (node[1].getKind() == kind::BITVECTOR_EXTRACT && node[0].isConst())) @@ -391,7 +393,7 @@ Node TheoryBV::getValue(TNode node) Assert(iit->second.isConst()); nb << iit->second; } - it->second = Rewriter::rewrite(nb.constructNode()); + it->second = rewrite(nb.constructNode()); } } while (!visit.empty()); diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index e41bef015..33d143a36 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -199,8 +199,8 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) for (size_t i = 0, vsize = c[0].getNumChildren(); i < vsize; i++) { vars.push_back(c[0][i]); - Node sc = nm->mkNode( - APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(t, i), h); + Node sc = + nm->mkNode(APPLY_SELECTOR, dt[cindex][i].getSelector(), h); subs.push_back(sc); } } diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 7ba3c9758..eb8102856 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -24,6 +24,16 @@ namespace cvc5 { namespace theory { namespace datatypes { +/** + * The rewriter for datatypes. An invariant of the rewriter is that + * postRewrite/preRewrite should not depend on the options, in particular, + * they should not depend on whether shared selectors are enabled. Thus, + * they should not use DTypeConstructor::getSelectorInternal. Instead, + * the conversion from external to internal selectors is done in + * expandDefinition. This invariant ensures that the rewritten form of a node + * does not mix multiple option settings, which would lead to e.g. shared + * selectors being used in an SmtEngine instance where they are disabled. + */ class DatatypesRewriter : public TheoryRewriter { public: diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index c9750a505..d158cff08 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -36,12 +36,10 @@ InferenceManager::InferenceManager(Env& env, ProofNodeManager* pnm) : InferenceManagerBuffered(env, t, state, pnm, "theory::datatypes::"), d_pnm(pnm), - d_ipc(pnm == nullptr ? nullptr - : new InferProofCons(state.getSatContext(), pnm)), - d_lemPg(pnm == nullptr - ? nullptr - : new EagerProofGenerator( - pnm, state.getUserContext(), "datatypes::lemPg")) + d_ipc(pnm == nullptr ? nullptr : new InferProofCons(context(), pnm)), + d_lemPg(pnm == nullptr ? nullptr + : new EagerProofGenerator( + pnm, userContext(), "datatypes::lemPg")) { d_false = NodeManager::currentNM()->mkConst(false); } diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index e66b70934..ed112e4ea 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -42,10 +42,12 @@ using namespace cvc5::context; using namespace cvc5::theory; using namespace cvc5::theory::datatypes; -SygusExtension::SygusExtension(TheoryState& s, +SygusExtension::SygusExtension(Env& env, + TheoryState& s, InferenceManager& im, quantifiers::TermDbSygus* tds) - : d_state(s), + : EnvObj(env), + d_state(s), d_im(im), d_tds(tds), d_ssb(tds), @@ -1037,7 +1039,7 @@ Node SygusExtension::registerSearchValue(Node a, << ", type=" << tn << std::endl; Node bv = d_tds->sygusToBuiltin(cnv, tn); Trace("sygus-sb-debug") << " ......builtin is " << bv << std::endl; - Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv); + Node bvr = extendedRewrite(bv); Trace("sygus-sb-debug") << " ......search value rewrites to " << bvr << std::endl; Trace("dt-sygus") << " * DT builtin : " << n << " -> " << bvr << std::endl; unsigned sz = utils::getSygusTermSize(nv); @@ -1108,7 +1110,7 @@ Node SygusExtension::registerSearchValue(Node a, its = d_sampler[a].find(tn); } // check equivalent - its->second.checkEquivalent(bv, bvr, *d_state.options().base.out); + its->second.checkEquivalent(bv, bvr, *options().base.out); } } diff --git a/src/theory/datatypes/sygus_extension.h b/src/theory/datatypes/sygus_extension.h index 3c7607eaf..5860dca99 100644 --- a/src/theory/datatypes/sygus_extension.h +++ b/src/theory/datatypes/sygus_extension.h @@ -25,6 +25,7 @@ #include "context/cdhashset.h" #include "context/context.h" #include "expr/node.h" +#include "smt/env_obj.h" #include "theory/datatypes/sygus_simple_sym.h" #include "theory/decision_manager.h" #include "theory/quantifiers/sygus_sampler.h" @@ -62,7 +63,7 @@ class InferenceManager; * We prioritize decisions of form (1) before (2). Both kinds of decision are * critical for solution completeness, which is enforced by DecisionManager. */ -class SygusExtension +class SygusExtension : protected EnvObj { typedef context::CDHashMap<Node, int> IntMap; typedef context::CDHashMap<Node, Node> NodeMap; @@ -70,7 +71,8 @@ class SygusExtension typedef context::CDHashSet<Node> NodeSet; public: - SygusExtension(TheoryState& s, + SygusExtension(Env& env, + TheoryState& s, InferenceManager& im, quantifiers::TermDbSygus* tds); ~SygusExtension(); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 58d0dbaab..4a8976876 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -110,7 +110,7 @@ void TheoryDatatypes::finishInit() { quantifiers::TermDbSygus* tds = getQuantifiersEngine()->getTermDatabaseSygus(); - d_sygusExtension.reset(new SygusExtension(d_state, d_im, tds)); + d_sygusExtension.reset(new SygusExtension(d_env, d_state, d_im, tds)); // do congruence on evaluation functions d_equalityEngine->addFunctionKind(kind::DT_SYGUS_EVAL); } diff --git a/src/theory/difficulty_manager.cpp b/src/theory/difficulty_manager.cpp new file mode 100644 index 000000000..3df86383f --- /dev/null +++ b/src/theory/difficulty_manager.cpp @@ -0,0 +1,109 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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. + * **************************************************************************** + * + * Difficulty manager. + */ + +#include "theory/difficulty_manager.h" + +#include "options/smt_options.h" +#include "smt/env.h" +#include "theory/theory_model.h" +#include "util/rational.h" + +namespace cvc5 { +namespace theory { + +DifficultyManager::DifficultyManager(context::Context* c, Valuation val) + : d_val(val), d_dfmap(c) +{ +} + +void DifficultyManager::getDifficultyMap(std::map<Node, Node>& dmap) +{ + NodeManager* nm = NodeManager::currentNM(); + for (const std::pair<const Node, uint64_t> p : d_dfmap) + { + dmap[p.first] = nm->mkConst(Rational(p.second)); + } +} + +void DifficultyManager::notifyLemma(const std::map<TNode, TNode>& rse, Node n) +{ + if (options::difficultyMode() != options::DifficultyMode::LEMMA_LITERAL) + { + return; + } + Trace("diff-man") << "notifyLemma: " << n << std::endl; + Kind nk = n.getKind(); + // for lemma (or a_1 ... a_n), if a_i is a literal that is not true in the + // valuation, then we increment the difficulty of that assertion + std::vector<TNode> litsToCheck; + if (nk == kind::OR) + { + litsToCheck.insert(litsToCheck.end(), n.begin(), n.end()); + } + else if (nk == kind::IMPLIES) + { + litsToCheck.push_back(n[0].negate()); + litsToCheck.push_back(n[1]); + } + else + { + litsToCheck.push_back(n); + } + std::map<TNode, TNode>::const_iterator it; + for (TNode nc : litsToCheck) + { + bool pol = nc.getKind() != kind::NOT; + TNode atom = pol ? nc : nc[0]; + it = rse.find(atom); + if (it != rse.end()) + { + incrementDifficulty(it->second); + } + } +} + +void DifficultyManager::notifyCandidateModel(const NodeList& input, + TheoryModel* m) +{ + if (options::difficultyMode() != options::DifficultyMode::MODEL_CHECK) + { + return; + } + Trace("diff-man") << "DifficultyManager::notifyCandidateModel, #input=" + << input.size() << std::endl; + for (const Node& a : input) + { + // should have miniscoped the assertions upstream + Assert(a.getKind() != kind::AND); + // check if each input is satisfied + Node av = m->getValue(a); + if (av.isConst() && av.getConst<bool>()) + { + continue; + } + Trace("diff-man") << " not true: " << a << std::endl; + // not satisfied, increment counter + incrementDifficulty(a); + } + Trace("diff-man") << std::endl; +} +void DifficultyManager::incrementDifficulty(TNode a, uint64_t amount) +{ + Assert(a.getType().isBoolean()); + d_dfmap[a] = d_dfmap[a] + amount; +} + +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/difficulty_manager.h b/src/theory/difficulty_manager.h new file mode 100644 index 000000000..3030bcc9b --- /dev/null +++ b/src/theory/difficulty_manager.h @@ -0,0 +1,83 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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. + * **************************************************************************** + * + * Relevance manager. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__DIFFICULTY_MANAGER__H +#define CVC5__THEORY__DIFFICULTY_MANAGER__H + +#include "context/cdhashmap.h" +#include "context/cdlist.h" +#include "expr/node.h" +#include "theory/valuation.h" + +namespace cvc5 { +namespace theory { + +class TheoryModel; + +/** + * Difficulty manager, which tracks an estimate of the difficulty of each + * preprocessed assertion during solving. + */ +class DifficultyManager +{ + typedef context::CDList<Node> NodeList; + typedef context::CDHashMap<Node, uint64_t> NodeUIntMap; + + public: + DifficultyManager(context::Context* c, Valuation val); + /** + * Get difficulty map, which populates dmap mapping preprocessed assertions + * to a difficulty measure (a constant integer). + */ + void getDifficultyMap(std::map<Node, Node>& dmap); + /** + * Notify lemma, for difficulty measurements. This increments the difficulty + * of assertions that share literals with that lemma if the difficulty mode + * is LEMMA_LITERAL. In particular, for each literal lit in the lemma lem, we + * increment the difficulty of the assertion res[lit], which corresponds to + * the assertion that was the reason why the literal is relevant in the + * current context. + * + * @param rse Mapping from literals to the preprocessed assertion that was + * the reason why that literal was relevant in the current context + * @param lem The lemma + */ + void notifyLemma(const std::map<TNode, TNode>& rse, Node lem); + /** + * Notify that `m` is a (candidate) model. This increments the difficulty + * of assertions that are not satisfied by that model. + * + * @param input The list of preprocessed assertions + * @param m The candidate model. + */ + void notifyCandidateModel(const NodeList& input, TheoryModel* m); + + private: + /** Increment difficulty on assertion a */ + void incrementDifficulty(TNode a, uint64_t amount = 1); + /** The valuation object, used to query current value of theory literals */ + Valuation d_val; + /** + * User-context dependent mapping from input assertions to difficulty measure + */ + NodeUIntMap d_dfmap; +}; + +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__DIFFICULTY_MANAGER__H */ diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 0fd0eebd6..475df0b43 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -37,7 +37,7 @@ CandidateRewriteDatabase::CandidateRewriteDatabase( Env& env, bool doCheck, bool rewAccel, bool silent, bool filterPairs) : ExprMiner(env), d_tds(nullptr), - d_ext_rewrite(nullptr), + d_useExtRewriter(false), d_doCheck(doCheck), d_rewAccel(rewAccel), d_silent(silent), @@ -52,7 +52,7 @@ void CandidateRewriteDatabase::initialize(const std::vector<Node>& vars, d_candidate = Node::null(); d_using_sygus = false; d_tds = nullptr; - d_ext_rewrite = nullptr; + d_useExtRewriter = false; if (d_filterPairs) { d_crewrite_filter.initialize(ss, nullptr, false); @@ -69,7 +69,7 @@ void CandidateRewriteDatabase::initializeSygus(const std::vector<Node>& vars, d_candidate = f; d_using_sygus = true; d_tds = tds; - d_ext_rewrite = nullptr; + d_useExtRewriter = false; if (d_filterPairs) { d_crewrite_filter.initialize(ss, d_tds, d_using_sygus); @@ -121,10 +121,10 @@ Node CandidateRewriteDatabase::addTerm(Node sol, // get the rewritten form Node solbr; Node eq_solr; - if (d_ext_rewrite != nullptr) + if (d_useExtRewriter) { - solbr = d_ext_rewrite->extendedRewrite(solb); - eq_solr = d_ext_rewrite->extendedRewrite(eq_solb); + solbr = extendedRewrite(solb); + eq_solr = extendedRewrite(eq_solb); } else { @@ -289,9 +289,9 @@ bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) void CandidateRewriteDatabase::setSilent(bool flag) { d_silent = flag; } -void CandidateRewriteDatabase::setExtendedRewriter(ExtendedRewriter* er) +void CandidateRewriteDatabase::enableExtendedRewriter() { - d_ext_rewrite = er; + d_useExtRewriter = true; } } // namespace quantifiers diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 71ae5649f..c0e783fc1 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -100,14 +100,14 @@ class CandidateRewriteDatabase : public ExprMiner bool addTerm(Node sol, std::ostream& out) override; /** sets whether this class should output candidate rewrites it finds */ void setSilent(bool flag); - /** set the (extended) rewriter used by this class */ - void setExtendedRewriter(ExtendedRewriter* er); + /** Enable the (extended) rewriter for this class */ + void enableExtendedRewriter(); private: /** (required) pointer to the sygus term database of d_qe */ TermDbSygus* d_tds; - /** an extended rewriter object */ - ExtendedRewriter* d_ext_rewrite; + /** Whether we use the extended rewriter */ + bool d_useExtRewriter; /** the function-to-synthesize we are testing (if sygus) */ Node d_candidate; /** whether we are checking equivalence using subsolver */ diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 81366fabd..8334cc248 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -47,11 +47,12 @@ TrustNode InstRewriterCegqi::rewriteInstantiation(Node q, return d_parent->rewriteInstantiation(q, terms, inst, doVts); } -InstStrategyCegqi::InstStrategyCegqi(QuantifiersState& qs, +InstStrategyCegqi::InstStrategyCegqi(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), + : QuantifiersModule(env, qs, qim, qr, tr), d_irew(new InstRewriterCegqi(this)), d_cbqi_set_quant_inactive(false), d_incomplete_check(false), @@ -70,7 +71,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersState& qs, } if (options::cegqiNestedQE()) { - d_nestedQe.reset(new NestedQe(qs.getEnv())); + d_nestedQe.reset(new NestedQe(d_env)); } } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 882f69b85..a568b0b4d 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -18,6 +18,7 @@ #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H +#include "smt/env_obj.h" #include "theory/decision_manager.h" #include "theory/quantifiers/bv_inverter.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" @@ -69,7 +70,8 @@ class InstStrategyCegqi : public QuantifiersModule typedef context::CDHashMap<Node, int> NodeIntMap; public: - InstStrategyCegqi(QuantifiersState& qs, + InstStrategyCegqi(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 17eaad5c6..f9625d7ac 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -86,15 +86,15 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& } } -ConjectureGenerator::ConjectureGenerator(QuantifiersState& qs, +ConjectureGenerator::ConjectureGenerator(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), + : QuantifiersModule(env, qs, qim, qr, tr), d_notify(*this), - d_uequalityEngine( - d_notify, qs.getSatContext(), "ConjectureGenerator::ee", false), - d_ee_conjectures(qs.getSatContext()), + d_uequalityEngine(d_notify, context(), "ConjectureGenerator::ee", false), + d_ee_conjectures(context()), d_conj_count(0), d_subs_confirmCount(0), d_subs_unkCount(0), diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index ef60792a6..bc5f3fb13 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -21,6 +21,7 @@ #include "context/cdhashmap.h" #include "expr/node_trie.h" #include "expr/term_canonize.h" +#include "smt/env_obj.h" #include "theory/quantifiers/quant_module.h" #include "theory/type_enumerator.h" @@ -437,7 +438,8 @@ private: //information about ground equivalence classes unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ); public: - ConjectureGenerator(QuantifiersState& qs, + ConjectureGenerator(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index ead42a3cd..62c5c2440 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -32,11 +32,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -InstantiationEngine::InstantiationEngine(QuantifiersState& qs, +InstantiationEngine::InstantiationEngine(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), + : QuantifiersModule(env, qs, qim, qr, tr), d_instStrategies(), d_isup(), d_i_ag(), @@ -46,7 +47,7 @@ InstantiationEngine::InstantiationEngine(QuantifiersState& qs, { if (options::relevantTriggers()) { - d_quant_rel.reset(new quantifiers::QuantRelevance); + d_quant_rel.reset(new quantifiers::QuantRelevance(env)); } if (options::eMatching()) { // these are the instantiation strategies for E-matching diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index 45e137dd5..50685642d 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -34,7 +34,8 @@ class InstStrategyAutoGenTriggers; class InstantiationEngine : public QuantifiersModule { public: - InstantiationEngine(QuantifiersState& qs, + InstantiationEngine(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index f87ec6435..92ec1e452 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -29,8 +29,9 @@ namespace cvc5 { namespace theory { namespace quantifiers { -EqualityQuery::EqualityQuery(QuantifiersState& qs, FirstOrderModel* m) - : d_qstate(qs), +EqualityQuery::EqualityQuery(Env& env, QuantifiersState& qs, FirstOrderModel* m) + : QuantifiersUtil(env), + d_qstate(qs), d_model(m), d_eqi_counter(qs.getSatContext()), d_reset_count(0) diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index f39ff86e3..200863cd6 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -43,7 +43,7 @@ class QuantifiersState; class EqualityQuery : public QuantifiersUtil { public: - EqualityQuery(QuantifiersState& qs, FirstOrderModel* m); + EqualityQuery(Env& env, QuantifiersState& qs, FirstOrderModel* m); virtual ~EqualityQuery(); /** reset */ diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp index ae20d4909..8af456ea8 100644 --- a/src/theory/quantifiers/expr_miner_manager.cpp +++ b/src/theory/quantifiers/expr_miner_manager.cpp @@ -87,7 +87,7 @@ void ExpressionMinerManager::enableRewriteRuleSynth() { d_crd.initialize(vars, &d_sampler); } - d_crd.setExtendedRewriter(&d_ext_rew); + d_crd.enableExtendedRewriter(); d_crd.setSilent(false); } diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index 92450b3ba..43a615c97 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -21,15 +21,11 @@ #include "expr/node.h" #include "smt/env_obj.h" #include "theory/quantifiers/candidate_rewrite_database.h" -#include "theory/quantifiers/extended_rewrite.h" #include "theory/quantifiers/query_generator.h" #include "theory/quantifiers/solution_filter.h" #include "theory/quantifiers/sygus_sampler.h" namespace cvc5 { - -class Env; - namespace theory { namespace quantifiers { @@ -114,8 +110,6 @@ class ExpressionMinerManager : protected EnvObj SolutionFilterStrength d_sols; /** sygus sampler object */ SygusSampler d_sampler; - /** extended rewriter object */ - ExtendedRewriter d_ext_rew; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 58a78b4aa..40e28eb78 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -42,7 +42,8 @@ struct ExtRewriteAggAttributeId }; typedef expr::Attribute<ExtRewriteAggAttributeId, Node> ExtRewriteAggAttribute; -ExtendedRewriter::ExtendedRewriter(bool aggr) : d_aggr(aggr) +ExtendedRewriter::ExtendedRewriter(Rewriter& rew, bool aggr) + : d_rew(rew), d_aggr(aggr) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -97,7 +98,7 @@ bool ExtendedRewriter::addToChildren(Node nc, Node ExtendedRewriter::extendedRewrite(Node n) const { - n = Rewriter::rewrite(n); + n = d_rew.rewrite(n); // has it already been computed? Node ncache = getCache(n); @@ -204,7 +205,7 @@ Node ExtendedRewriter::extendedRewrite(Node n) const } } } - ret = Rewriter::rewrite(ret); + ret = d_rew.rewrite(ret); //--------------------end rewrite children // now, do extended rewrite @@ -496,7 +497,7 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full) const t2.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); if (nn != t2) { - nn = Rewriter::rewrite(nn); + nn = d_rew.rewrite(nn); if (nn == t1) { new_ret = t2; @@ -508,7 +509,7 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full) const // must use partial substitute here, to avoid substitution into witness std::map<Kind, bool> rkinds; nn = partialSubstitute(t1, vars, subs, rkinds); - nn = Rewriter::rewrite(nn); + nn = d_rew.rewrite(nn); if (nn != t1) { // If full=false, then we've duplicated a term u in the children of n. @@ -537,7 +538,7 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full) const Node nn = partialSubstitute(t2, assign, rkinds); if (nn != t2) { - nn = Rewriter::rewrite(nn); + nn = d_rew.rewrite(nn); if (nn == t1) { new_ret = nn; @@ -625,7 +626,7 @@ Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n) const { children[ii] = n[i][j + 1]; Node pull = nm->mkNode(n.getKind(), children); - Node pullr = Rewriter::rewrite(pull); + Node pullr = d_rew.rewrite(pull); children[ii] = n[i]; ite_c[i][j] = pullr; } @@ -688,7 +689,7 @@ Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n) const Assert(nite.getKind() == itek); // now, simply pull the ITE and try ITE rewrites Node pull_ite = nm->mkNode(itek, nite[0], ip.second[0], ip.second[1]); - pull_ite = Rewriter::rewrite(pull_ite); + pull_ite = d_rew.rewrite(pull_ite); if (pull_ite.getKind() == ITE) { Node new_pull_ite = extendedRewriteIte(itek, pull_ite, false); @@ -887,7 +888,7 @@ Node ExtendedRewriter::extendedRewriteBcp(Kind andk, ccs = cpol ? ccs : TermUtil::mkNegate(notk, ccs); Trace("ext-rew-bcp") << "BCP: propagated " << c << " -> " << ccs << std::endl; - ccs = Rewriter::rewrite(ccs); + ccs = d_rew.rewrite(ccs); Trace("ext-rew-bcp") << "BCP: rewritten to " << ccs << std::endl; to_process.push_back(ccs); // store this as a node that propagation touched. This marks c so that @@ -1522,7 +1523,7 @@ Node ExtendedRewriter::extendedRewriteEqChain( index--; new_ret = nm->mkNode(eqk, children[index], new_ret); } - new_ret = Rewriter::rewrite(new_ret); + new_ret = d_rew.rewrite(new_ret); if (new_ret != ret) { return new_ret; diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index b1b08657d..b4dcab041 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -24,6 +24,9 @@ namespace cvc5 { namespace theory { + +class Rewriter; + namespace quantifiers { /** Extended rewriter @@ -48,12 +51,14 @@ namespace quantifiers { class ExtendedRewriter { public: - ExtendedRewriter(bool aggr = true); + ExtendedRewriter(Rewriter& rew, bool aggr = true); ~ExtendedRewriter() {} /** return the extended rewritten form of n */ Node extendedRewrite(Node n) const; private: + /** The underlying rewriter that we are extending */ + Rewriter& d_rew; /** cache that the extended rewritten form of n is ret */ void setCache(Node n, Node ret) const; /** get the cache for n */ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index d4bc7dfcb..841177a7f 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -42,13 +42,14 @@ struct ModelBasisArgAttributeId }; using ModelBasisArgAttribute = expr::Attribute<ModelBasisArgAttributeId, uint64_t>; -FirstOrderModel::FirstOrderModel(QuantifiersState& qs, +FirstOrderModel::FirstOrderModel(Env& env, + QuantifiersState& qs, QuantifiersRegistry& qr, TermRegistry& tr) : d_model(nullptr), d_qreg(qr), d_treg(tr), - d_eq_query(qs, this), + d_eq_query(env, qs, this), d_forall_asserts(qs.getSatContext()), d_forallRlvComputed(false) { diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 1969fdde7..05bdcbee6 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -39,7 +39,8 @@ class QuantifiersRegistry; class FirstOrderModel { public: - FirstOrderModel(QuantifiersState& qs, + FirstOrderModel(Env& env, + QuantifiersState& qs, QuantifiersRegistry& qr, TermRegistry& tr); virtual ~FirstOrderModel() {} diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 3fd478c31..b04391db3 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -88,11 +88,12 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma() return lem; } -BoundedIntegers::BoundedIntegers(QuantifiersState& qs, +BoundedIntegers::BoundedIntegers(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr) + : QuantifiersModule(env, qs, qim, qr, tr) { } diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index d37e71b72..8c468c1de 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -18,13 +18,13 @@ #ifndef CVC5__BOUNDED_INTEGERS_H #define CVC5__BOUNDED_INTEGERS_H -#include "theory/quantifiers/quant_module.h" - #include "context/cdhashmap.h" #include "context/context.h" #include "expr/attribute.h" +#include "smt/env_obj.h" #include "theory/decision_strategy.h" #include "theory/quantifiers/quant_bound_inference.h" +#include "theory/quantifiers/quant_module.h" namespace cvc5 { namespace theory { @@ -164,7 +164,8 @@ private: std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it; public: - BoundedIntegers(QuantifiersState& qs, + BoundedIntegers(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp index e17271613..4be13ba5f 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp @@ -36,10 +36,11 @@ struct IsStarAttributeId }; using IsStarAttribute = expr::Attribute<IsStarAttributeId, bool>; -FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersState& qs, +FirstOrderModelFmc::FirstOrderModelFmc(Env& env, + QuantifiersState& qs, QuantifiersRegistry& qr, TermRegistry& tr) - : FirstOrderModel(qs, qr, tr) + : FirstOrderModel(env, qs, qr, tr) { } diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h index f148a9e19..5a528ede1 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.h +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h @@ -39,7 +39,8 @@ class FirstOrderModelFmc : public FirstOrderModel void processInitializeModelForTerm(Node n) override; public: - FirstOrderModelFmc(QuantifiersState& qs, + FirstOrderModelFmc(Env& env, + QuantifiersState& qs, QuantifiersRegistry& qr, TermRegistry& tr); ~FirstOrderModelFmc() override; diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index c4f83191b..f8b90f624 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -286,11 +286,13 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) { } } -FullModelChecker::FullModelChecker(QuantifiersState& qs, +FullModelChecker::FullModelChecker(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QModelBuilder(qs, qim, qr, tr), d_fm(new FirstOrderModelFmc(qs, qr, tr)) + : QModelBuilder(env, qs, qim, qr, tr), + d_fm(new FirstOrderModelFmc(env, qs, qr, tr)) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index e33d1db6d..f3f8699af 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -155,7 +155,8 @@ protected: Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ); public: - FullModelChecker(QuantifiersState& qs, + FullModelChecker(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index a331409f1..f43b7a6c9 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -30,11 +30,12 @@ using namespace cvc5::context; using namespace cvc5::theory; using namespace cvc5::theory::quantifiers; -QModelBuilder::QModelBuilder(QuantifiersState& qs, +QModelBuilder::QModelBuilder(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : TheoryEngineModelBuilder(qs.getEnv()), + : TheoryEngineModelBuilder(env), d_addedLemmas(0), d_triedLemmas(0), d_qstate(qs), @@ -48,7 +49,7 @@ QModelBuilder::QModelBuilder(QuantifiersState& qs, void QModelBuilder::finishInit() { // allocate the default model - d_modelAloc.reset(new FirstOrderModel(d_qstate, d_qreg, d_treg)); + d_modelAloc.reset(new FirstOrderModel(d_env, d_qstate, d_qreg, d_treg)); d_model = d_modelAloc.get(); } diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index a767af47a..f5dc7155b 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -43,7 +43,8 @@ class QModelBuilder : public TheoryEngineModelBuilder unsigned d_triedLemmas; public: - QModelBuilder(QuantifiersState& qs, + QModelBuilder(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index e58f66d0b..256899580 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -31,12 +31,13 @@ namespace theory { namespace quantifiers { //Model Engine constructor -ModelEngine::ModelEngine(QuantifiersState& qs, +ModelEngine::ModelEngine(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, QModelBuilder* builder) - : QuantifiersModule(qs, qim, qr, tr), + : QuantifiersModule(env, qs, qim, qr, tr), d_incomplete_check(true), d_addedLemmas(0), d_triedLemmas(0), diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index f818a6362..b5ab86f20 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -18,6 +18,7 @@ #ifndef CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H #define CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H +#include "smt/env_obj.h" #include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/quant_module.h" #include "theory/theory_model.h" @@ -42,7 +43,8 @@ private: int d_triedLemmas; int d_totalLemmas; public: - ModelEngine(QuantifiersState& qs, + ModelEngine(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, diff --git a/src/theory/quantifiers/ho_term_database.cpp b/src/theory/quantifiers/ho_term_database.cpp index 3b97409cc..a2a8b8145 100644 --- a/src/theory/quantifiers/ho_term_database.cpp +++ b/src/theory/quantifiers/ho_term_database.cpp @@ -28,8 +28,8 @@ namespace cvc5 { namespace theory { namespace quantifiers { -HoTermDb::HoTermDb(QuantifiersState& qs, QuantifiersRegistry& qr) - : TermDb(qs, qr) +HoTermDb::HoTermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr) + : TermDb(env, qs, qr) { } @@ -152,7 +152,7 @@ bool HoTermDb::resetInternal(Theory::Effort effort) bool HoTermDb::finishResetInternal(Theory::Effort effort) { - if (!d_qstate.options().quantifiers.hoMergeTermDb) + if (!options().quantifiers.hoMergeTermDb) { return true; } diff --git a/src/theory/quantifiers/ho_term_database.h b/src/theory/quantifiers/ho_term_database.h index 12bf0b49f..885fec8f4 100644 --- a/src/theory/quantifiers/ho_term_database.h +++ b/src/theory/quantifiers/ho_term_database.h @@ -34,7 +34,7 @@ namespace quantifiers { class HoTermDb : public TermDb { public: - HoTermDb(QuantifiersState& qs, QuantifiersRegistry& qr); + HoTermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr); ~HoTermDb(); /** identify */ std::string identify() const override { return "HoTermDb"; } diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index aeff27433..6769d8bc2 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -29,12 +29,13 @@ namespace cvc5 { namespace theory { namespace quantifiers { -InstStrategyEnum::InstStrategyEnum(QuantifiersState& qs, +InstStrategyEnum::InstStrategyEnum(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, RelevantDomain* rd) - : QuantifiersModule(qs, qim, qr, tr), d_rd(rd), d_fullSaturateLimit(-1) + : QuantifiersModule(env, qs, qim, qr, tr), d_rd(rd), d_fullSaturateLimit(-1) { } void InstStrategyEnum::presolve() diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index a298e3a8a..66315c070 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -18,6 +18,7 @@ #ifndef CVC5__INST_STRATEGY_ENUMERATIVE_H #define CVC5__INST_STRATEGY_ENUMERATIVE_H +#include "smt/env_obj.h" #include "theory/quantifiers/quant_module.h" namespace cvc5 { @@ -62,7 +63,8 @@ class RelevantDomain; class InstStrategyEnum : public QuantifiersModule { public: - InstStrategyEnum(QuantifiersState& qs, + InstStrategyEnum(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, diff --git a/src/theory/quantifiers/inst_strategy_pool.cpp b/src/theory/quantifiers/inst_strategy_pool.cpp index 0e32c246e..cadda033b 100644 --- a/src/theory/quantifiers/inst_strategy_pool.cpp +++ b/src/theory/quantifiers/inst_strategy_pool.cpp @@ -30,11 +30,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -InstStrategyPool::InstStrategyPool(QuantifiersState& qs, +InstStrategyPool::InstStrategyPool(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr) + : QuantifiersModule(env, qs, qim, qr, tr) { } diff --git a/src/theory/quantifiers/inst_strategy_pool.h b/src/theory/quantifiers/inst_strategy_pool.h index acdc0010b..1f79717af 100644 --- a/src/theory/quantifiers/inst_strategy_pool.h +++ b/src/theory/quantifiers/inst_strategy_pool.h @@ -18,6 +18,7 @@ #ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H #define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H +#include "smt/env_obj.h" #include "theory/quantifiers/quant_module.h" namespace cvc5 { @@ -38,7 +39,8 @@ namespace quantifiers { class InstStrategyPool : public QuantifiersModule { public: - InstStrategyPool(QuantifiersState& qs, + InstStrategyPool(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 0daf53d2d..f0af73832 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -28,7 +28,7 @@ #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/quantifiers_preprocess.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_registry.h" @@ -42,12 +42,14 @@ namespace cvc5 { namespace theory { namespace quantifiers { -Instantiate::Instantiate(QuantifiersState& qs, +Instantiate::Instantiate(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, ProofNodeManager* pnm) - : d_qstate(qs), + : QuantifiersUtil(env), + d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr), @@ -252,7 +254,7 @@ bool Instantiate::addInstantiation(Node q, q, d_qreg.d_vars[q], terms, id, pfArg, doVts, pfTmp.get()); Node orig_body = body; // now preprocess, storing the trust node for the rewrite - TrustNode tpBody = QuantifiersRewriter::preprocess(body, true); + TrustNode tpBody = d_qreg.getPreprocess().preprocess(body, true); if (!tpBody.isNull()) { Assert(tpBody.getKind() == TrustNodeKind::REWRITE); diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 1f380350f..753213f35 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -104,7 +104,8 @@ class Instantiate : public QuantifiersUtil context::CDHashMap<Node, std::shared_ptr<InstLemmaList>>; public: - Instantiate(QuantifiersState& qs, + Instantiate(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 8c4d68631..983eee9ae 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1853,11 +1853,12 @@ bool MatchGen::isHandled( TNode n ) { return true; } -QuantConflictFind::QuantConflictFind(QuantifiersState& qs, +QuantConflictFind::QuantConflictFind(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), + : QuantifiersModule(env, qs, qim, qr, tr), d_conflict(qs.getSatContext(), false), d_true(NodeManager::currentNM()->mkConst<bool>(true)), d_false(NodeManager::currentNM()->mkConst<bool>(false)), diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index de521cd07..927a74ff2 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -238,7 +238,8 @@ private: //for equivalence classes bool areMatchDisequal( TNode n1, TNode n2 ); public: - QuantConflictFind(QuantifiersState& qs, + QuantConflictFind(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp index d5488f0c9..8fb37c548 100644 --- a/src/theory/quantifiers/quant_module.cpp +++ b/src/theory/quantifiers/quant_module.cpp @@ -21,11 +21,12 @@ namespace cvc5 { namespace theory { QuantifiersModule::QuantifiersModule( + Env& env, quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, quantifiers::TermRegistry& tr) - : EnvObj(qs.getEnv()), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr) + : EnvObj(env), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr) { } diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h index 7358aa555..639f9c2b4 100644 --- a/src/theory/quantifiers/quant_module.h +++ b/src/theory/quantifiers/quant_module.h @@ -60,7 +60,8 @@ class QuantifiersModule : protected EnvObj }; public: - QuantifiersModule(quantifiers::QuantifiersState& qs, + QuantifiersModule(Env& env, + quantifiers::QuantifiersState& qs, quantifiers::QuantifiersInferenceManager& qim, quantifiers::QuantifiersRegistry& qr, quantifiers::TermRegistry& tr); diff --git a/src/theory/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp index 0c1db860f..abb8c9219 100644 --- a/src/theory/quantifiers/quant_relevance.cpp +++ b/src/theory/quantifiers/quant_relevance.cpp @@ -23,6 +23,8 @@ namespace cvc5 { namespace theory { namespace quantifiers { +QuantRelevance::QuantRelevance(Env& env) : QuantifiersUtil(env) {} + void QuantRelevance::registerQuantifier(Node f) { // compute symbols in f diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h index c22e560f9..418b859b9 100644 --- a/src/theory/quantifiers/quant_relevance.h +++ b/src/theory/quantifiers/quant_relevance.h @@ -40,7 +40,7 @@ class QuantRelevance : public QuantifiersUtil * if this is false, then all calls to getRelevance * return -1. */ - QuantRelevance() {} + QuantRelevance(Env& env); ~QuantRelevance() {} /** reset */ bool reset(Theory::Effort e) override { return true; } diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 941b94d23..905424107 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -28,11 +28,13 @@ namespace cvc5 { namespace theory { namespace quantifiers { -QuantDSplit::QuantDSplit(QuantifiersState& qs, +QuantDSplit::QuantDSplit(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), d_added_split(qs.getUserContext()) + : QuantifiersModule(env, qs, qim, qr, tr), + d_added_split(qs.getUserContext()) { } diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 18aeec773..84cc6fea7 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -19,6 +19,7 @@ #define CVC5__THEORY__QUANT_SPLIT_H #include "context/cdo.h" +#include "smt/env_obj.h" #include "theory/quantifiers/quant_module.h" namespace cvc5 { @@ -50,7 +51,8 @@ class QuantDSplit : public QuantifiersModule { typedef context::CDHashSet<Node> NodeSet; public: - QuantDSplit(QuantifiersState& qs, + QuantDSplit(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 34235a193..cbe09af2e 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -22,6 +22,8 @@ using namespace cvc5::kind; namespace cvc5 { namespace theory { +QuantifiersUtil::QuantifiersUtil(Env& env) : EnvObj(env) {} + QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){ initialize( n, computeEq ); } @@ -93,7 +95,9 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int } } -void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { +void QuantPhaseReq::getPolarity( + Node n, size_t child, bool hasPol, bool pol, bool& newHasPol, bool& newPol) +{ if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){ newHasPol = hasPol; newPol = pol; @@ -115,7 +119,9 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& } } -void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { +void QuantPhaseReq::getEntailPolarity( + Node n, size_t child, bool hasPol, bool pol, bool& newHasPol, bool& newPol) +{ if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){ newHasPol = hasPol && pol!=( n.getKind()==OR ); newPol = pol; diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 5f91a9488..a422101f0 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -23,6 +23,7 @@ #include <vector> #include "expr/node.h" +#include "smt/env_obj.h" #include "theory/incomplete_id.h" #include "theory/theory.h" @@ -34,9 +35,10 @@ namespace theory { * This is a lightweight version of a quantifiers module that does not implement * methods for checking satisfiability. */ -class QuantifiersUtil { -public: - QuantifiersUtil(){} +class QuantifiersUtil : protected EnvObj +{ + public: + QuantifiersUtil(Env& env); virtual ~QuantifiersUtil(){} /** Called at the beginning of check-sat call. */ virtual void presolve() {} @@ -78,8 +80,35 @@ public: std::map< Node, bool > d_phase_reqs_equality; std::map< Node, Node > d_phase_reqs_equality_term; - static void getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ); - static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ); + /** + * Get the polarity of the child^th child of n, assuming its polarity + * is given by (hasPol, pol). A term has polarity if it is only relevant + * if asserted with one polarity. Its polarity is (typically) the number + * of negations it is beneath. + */ + static void getPolarity(Node n, + size_t child, + bool hasPol, + bool pol, + bool& newHasPol, + bool& newPol); + + /** + * Get the entailed polarity of the child^th child of n, assuming its + * entailed polarity is given by (hasPol, pol). A term has entailed polarity + * if it must be asserted with a polarity. Its polarity is (typically) the + * number of negations it is beneath. + * + * Entailed polarity and polarity above differ, e.g.: + * (and A B): A and B have true polarity and true entailed polarity + * (or A B): A and B have true polarity and no entailed polarity + */ + static void getEntailPolarity(Node n, + size_t child, + bool hasPol, + bool pol, + bool& newHasPol, + bool& newPol); }; } diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp index 24159d397..b2a08c249 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.cpp +++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp @@ -30,7 +30,7 @@ QuantifiersInferenceManager::QuantifiersInferenceManager( TermRegistry& tr, ProofNodeManager* pnm) : InferenceManagerBuffered(env, t, state, pnm, "theory::quantifiers::"), - d_instantiate(new Instantiate(state, *this, qr, tr, pnm)), + d_instantiate(new Instantiate(env, state, *this, qr, tr, pnm)), d_skolemize(new Skolemize(state, tr, pnm)) { } diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index 27ec187a9..563951189 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -41,7 +41,8 @@ QuantifiersModules::QuantifiersModules() { } QuantifiersModules::~QuantifiersModules() {} -void QuantifiersModules::initialize(QuantifiersState& qs, +void QuantifiersModules::initialize(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, @@ -51,46 +52,46 @@ void QuantifiersModules::initialize(QuantifiersState& qs, // add quantifiers modules if (options::quantConflictFind()) { - d_qcf.reset(new QuantConflictFind(qs, qim, qr, tr)); + d_qcf.reset(new QuantConflictFind(env, qs, qim, qr, tr)); modules.push_back(d_qcf.get()); } if (options::conjectureGen()) { - d_sg_gen.reset(new ConjectureGenerator(qs, qim, qr, tr)); + d_sg_gen.reset(new ConjectureGenerator(env, qs, qim, qr, tr)); modules.push_back(d_sg_gen.get()); } if (!options::finiteModelFind() || options::fmfInstEngine()) { - d_inst_engine.reset(new InstantiationEngine(qs, qim, qr, tr)); + d_inst_engine.reset(new InstantiationEngine(env, qs, qim, qr, tr)); modules.push_back(d_inst_engine.get()); } if (options::cegqi()) { - d_i_cbqi.reset(new InstStrategyCegqi(qs, qim, qr, tr)); + d_i_cbqi.reset(new InstStrategyCegqi(env, qs, qim, qr, tr)); modules.push_back(d_i_cbqi.get()); qim.getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); } if (options::sygus()) { - d_synth_e.reset(new SynthEngine(qs, qim, qr, tr)); + d_synth_e.reset(new SynthEngine(env, qs, qim, qr, tr)); modules.push_back(d_synth_e.get()); } // bounded integer instantiation is used when the user requests it via // fmfBound, or if strings are enabled. if (options::fmfBound() || options::stringExp()) { - d_bint.reset(new BoundedIntegers(qs, qim, qr, tr)); + d_bint.reset(new BoundedIntegers(env, qs, qim, qr, tr)); modules.push_back(d_bint.get()); } if (options::finiteModelFind() || options::fmfBound() || options::stringExp()) { - d_model_engine.reset(new ModelEngine(qs, qim, qr, tr, builder)); + d_model_engine.reset(new ModelEngine(env, qs, qim, qr, tr, builder)); modules.push_back(d_model_engine.get()); } if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE) { - d_qsplit.reset(new QuantDSplit(qs, qim, qr, tr)); + d_qsplit.reset(new QuantDSplit(env, qs, qim, qr, tr)); modules.push_back(d_qsplit.get()); } if (options::quantAlphaEquiv()) @@ -100,18 +101,18 @@ void QuantifiersModules::initialize(QuantifiersState& qs, // full saturation : instantiate from relevant domain, then arbitrary terms if (options::fullSaturateQuant() || options::fullSaturateInterleave()) { - d_rel_dom.reset(new RelevantDomain(qs, qr, tr)); - d_fs.reset(new InstStrategyEnum(qs, qim, qr, tr, d_rel_dom.get())); + d_rel_dom.reset(new RelevantDomain(env, qs, qr, tr)); + d_fs.reset(new InstStrategyEnum(env, qs, qim, qr, tr, d_rel_dom.get())); modules.push_back(d_fs.get()); } if (options::poolInst()) { - d_ipool.reset(new InstStrategyPool(qs, qim, qr, tr)); + d_ipool.reset(new InstStrategyPool(env, qs, qim, qr, tr)); modules.push_back(d_ipool.get()); } if (options::sygusInst()) { - d_sygus_inst.reset(new SygusInst(qs, qim, qr, tr)); + d_sygus_inst.reset(new SygusInst(env, qs, qim, qr, tr)); modules.push_back(d_sygus_inst.get()); } } diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index f41e81f34..9878e79ae 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -57,7 +57,8 @@ class QuantifiersModules * This constructs the above modules based on the current options. It adds * a pointer to each module it constructs to modules. */ - void initialize(QuantifiersState& qs, + void initialize(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, diff --git a/src/theory/quantifiers/quantifiers_preprocess.cpp b/src/theory/quantifiers/quantifiers_preprocess.cpp new file mode 100644 index 000000000..19487bc8d --- /dev/null +++ b/src/theory/quantifiers/quantifiers_preprocess.cpp @@ -0,0 +1,267 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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. + * **************************************************************************** + * + * Preprocessor for the theory of quantifiers. + */ + +#include "theory/quantifiers/quantifiers_preprocess.h" + +#include "expr/node_algorithm.h" +#include "options/quantifiers_options.h" +#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/skolemize.h" + +using namespace cvc5::kind; + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +QuantifiersPreprocess::QuantifiersPreprocess(Env& env) : EnvObj(env) {} + +Node QuantifiersPreprocess::computePrenexAgg( + Node n, std::map<Node, Node>& visited) const +{ + std::map<Node, Node>::iterator itv = visited.find(n); + if (itv != visited.end()) + { + return itv->second; + } + if (!expr::hasClosure(n)) + { + // trivial + return n; + } + NodeManager* nm = NodeManager::currentNM(); + Node ret = n; + if (n.getKind() == NOT) + { + ret = computePrenexAgg(n[0], visited).negate(); + } + else if (n.getKind() == FORALL) + { + std::vector<Node> children; + children.push_back(computePrenexAgg(n[1], visited)); + std::vector<Node> args; + args.insert(args.end(), n[0].begin(), n[0].end()); + // for each child, strip top level quant + for (unsigned i = 0; i < children.size(); i++) + { + if (children[i].getKind() == FORALL) + { + args.insert(args.end(), children[i][0].begin(), children[i][0].end()); + children[i] = children[i][1]; + } + } + // keep the pattern + std::vector<Node> iplc; + if (n.getNumChildren() == 3) + { + iplc.insert(iplc.end(), n[2].begin(), n[2].end()); + } + Node nb = nm->mkOr(children); + ret = QuantifiersRewriter::mkForall(args, nb, iplc, true); + } + else + { + std::unordered_set<Node> argsSet; + std::unordered_set<Node> nargsSet; + Node q; + Node nn = + QuantifiersRewriter::computePrenex(q, n, argsSet, nargsSet, true, true); + Assert(n != nn || argsSet.empty()); + Assert(n != nn || nargsSet.empty()); + if (n != nn) + { + Node nnn = computePrenexAgg(nn, visited); + // merge prenex + if (nnn.getKind() == FORALL) + { + argsSet.insert(nnn[0].begin(), nnn[0].end()); + nnn = nnn[1]; + // pos polarity variables are inner + if (!argsSet.empty()) + { + nnn = QuantifiersRewriter::mkForall( + {argsSet.begin(), argsSet.end()}, nnn, true); + } + argsSet.clear(); + } + else if (nnn.getKind() == NOT && nnn[0].getKind() == FORALL) + { + nargsSet.insert(nnn[0][0].begin(), nnn[0][0].end()); + nnn = nnn[0][1].negate(); + } + if (!nargsSet.empty()) + { + nnn = QuantifiersRewriter::mkForall( + {nargsSet.begin(), nargsSet.end()}, nnn.negate(), true) + .negate(); + } + if (!argsSet.empty()) + { + nnn = QuantifiersRewriter::mkForall( + {argsSet.begin(), argsSet.end()}, nnn, true); + } + ret = nnn; + } + } + visited[n] = ret; + return ret; +} + +Node QuantifiersPreprocess::preSkolemizeQuantifiers( + Node n, + bool polarity, + std::vector<TNode>& fvs, + std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>& + visited) const +{ + std::pair<Node, bool> key(n, polarity); + std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>:: + iterator it = visited.find(key); + if (it != visited.end()) + { + return it->second; + } + NodeManager* nm = NodeManager::currentNM(); + Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() + << std::endl; + if (n.getKind() == FORALL) + { + Node ret = n; + if (n.getNumChildren() == 3) + { + // Do not pre-skolemize quantified formulas with three children. + // This includes non-standard quantified formulas + // like recursive function definitions, or sygus conjectures, and + // quantified formulas with triggers. + } + else if (polarity) + { + if (options().quantifiers.preSkolemQuant + && options().quantifiers.preSkolemQuantNested) + { + std::vector<Node> children; + children.push_back(n[0]); + // add children to current scope + std::vector<TNode> fvss; + fvss.insert(fvss.end(), fvs.begin(), fvs.end()); + fvss.insert(fvss.end(), n[0].begin(), n[0].end()); + // process body in a new context + std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction> + visitedSub; + Node pbody = preSkolemizeQuantifiers(n[1], polarity, fvss, visitedSub); + children.push_back(pbody); + // return processed quantifier + ret = nm->mkNode(FORALL, children); + } + } + else + { + // will skolemize current, process body + Node nn = preSkolemizeQuantifiers(n[1], polarity, fvs, visited); + std::vector<Node> sk; + Node sub; + std::vector<unsigned> sub_vars; + // return skolemized body + ret = Skolemize::mkSkolemizedBody(n, nn, fvs, sk, sub, sub_vars); + } + visited[key] = ret; + return ret; + } + // check if it contains a quantifier as a subterm + // if so, we may preprocess this node + if (!expr::hasClosure(n)) + { + visited[key] = n; + return n; + } + Kind k = n.getKind(); + Node ret = n; + Assert(n.getType().isBoolean()); + if (k == ITE || (k == EQUAL && n[0].getType().isBoolean())) + { + if (options().quantifiers.preSkolemQuantAgg) + { + Node nn; + // must remove structure + if (k == ITE) + { + nn = nm->mkNode(AND, + nm->mkNode(OR, n[0].notNode(), n[1]), + nm->mkNode(OR, n[0], n[2])); + } + else if (k == EQUAL) + { + nn = nm->mkNode(AND, + nm->mkNode(OR, n[0].notNode(), n[1]), + nm->mkNode(OR, n[0], n[1].notNode())); + } + ret = preSkolemizeQuantifiers(nn, polarity, fvs, visited); + } + } + else if (k == AND || k == OR || k == NOT || k == IMPLIES) + { + std::vector<Node> children; + for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity(n, i, true, polarity, newHasPol, newPol); + Assert(newHasPol); + children.push_back(preSkolemizeQuantifiers(n[i], newPol, fvs, visited)); + } + ret = nm->mkNode(k, children); + } + visited[key] = ret; + return ret; +} + +TrustNode QuantifiersPreprocess::preprocess(Node n, bool isInst) const +{ + Node prev = n; + if (options().quantifiers.preSkolemQuant) + { + if (!isInst || !options().quantifiers.preSkolemQuantNested) + { + Trace("quantifiers-preprocess-debug") + << "Pre-skolemize " << n << "..." << std::endl; + // apply pre-skolemization to existential quantifiers + std::vector<TNode> fvs; + std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction> + visited; + n = preSkolemizeQuantifiers(prev, true, fvs, visited); + } + } + // pull all quantifiers globally + if (options().quantifiers.prenexQuant == options::PrenexQuantMode::NORMAL) + { + Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; + std::map<Node, Node> visited; + n = computePrenexAgg(n, visited); + n = rewrite(n); + Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl; + } + if (n != prev) + { + Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl; + Trace("quantifiers-preprocess") << "..returned " << n << std::endl; + return TrustNode::mkTrustRewrite(prev, n, nullptr); + } + return TrustNode::null(); +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/quantifiers_preprocess.h b/src/theory/quantifiers/quantifiers_preprocess.h new file mode 100644 index 000000000..45b7ad07a --- /dev/null +++ b/src/theory/quantifiers/quantifiers_preprocess.h @@ -0,0 +1,78 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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. + * **************************************************************************** + * + * Preprocessor for the theory of quantifiers. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_PREPROCESS_H +#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_PREPROCESS_H + +#include "proof/trust_node.h" +#include "smt/env_obj.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +/** + * Module for doing preprocessing that is pertinent to quantifiers. These + * operations cannot be done in the rewriter since e.g. preskolemization + * depends on knowing the polarity of the position in which quantifiers occur. + */ +class QuantifiersPreprocess : protected EnvObj +{ + public: + QuantifiersPreprocess(Env& env); + /** preprocess + * + * This returns the result of applying simple quantifiers-specific + * pre-processing to n, including but not limited to: + * - pre-skolemization, + * - aggressive prenexing. + * The argument isInst is set to true if n is an instance of a previously + * registered quantified formula. If this flag is true, we do not apply + * certain steps like pre-skolemization since we know they will have no + * effect. + * + * The result is wrapped in a trust node of kind TrustNodeKind::REWRITE. + */ + TrustNode preprocess(Node n, bool isInst = false) const; + + private: + using NodePolPairHashFunction = PairHashFunction<Node, bool, std::hash<Node>>; + /** + * Pre-skolemize quantifiers. Return the pre-skolemized form of n. + * + * @param n The formula to preskolemize. + * @param polarity The polarity of n in the input. + * @param fvs The free variables + * @param visited Cache of visited (node, polarity) pairs. + */ + Node preSkolemizeQuantifiers( + Node n, + bool polarity, + std::vector<TNode>& fvs, + std::unordered_map<std::pair<Node, bool>, Node, NodePolPairHashFunction>& + visited) const; + /** + * Apply prenexing aggressively. Returns the prenex normal form of n. + */ + Node computePrenexAgg(Node n, std::map<Node, Node>& visited) const; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp index 7e3aebbb8..6d5e00363 100644 --- a/src/theory/quantifiers/quantifiers_registry.cpp +++ b/src/theory/quantifiers/quantifiers_registry.cpp @@ -23,10 +23,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -QuantifiersRegistry::QuantifiersRegistry() - : d_quantAttr(), +QuantifiersRegistry::QuantifiersRegistry(Env& env) + : QuantifiersUtil(env), + d_quantAttr(), d_quantBoundInf(options::fmfTypeCompletionThresh(), - options::finiteModelFind()) + options::finiteModelFind()), + d_quantPreproc(env) { } @@ -189,6 +191,10 @@ QuantifiersBoundInference& QuantifiersRegistry::getQuantifiersBoundInference() { return d_quantBoundInf; } +QuantifiersPreprocess& QuantifiersRegistry::getPreprocess() +{ + return d_quantPreproc; +} Node QuantifiersRegistry::getNameForQuant(Node q) const { diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h index ee99a284a..559939bbe 100644 --- a/src/theory/quantifiers/quantifiers_registry.h +++ b/src/theory/quantifiers/quantifiers_registry.h @@ -22,6 +22,7 @@ #include "theory/quantifiers/quant_bound_inference.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_preprocess.h" namespace cvc5 { namespace theory { @@ -42,7 +43,7 @@ class QuantifiersRegistry : public QuantifiersUtil friend class Instantiate; public: - QuantifiersRegistry(); + QuantifiersRegistry(Env& env); ~QuantifiersRegistry() {} /** * Register quantifier, which allocates the instantiation constants for q. @@ -91,6 +92,8 @@ class QuantifiersRegistry : public QuantifiersUtil QuantAttributes& getQuantAttributes(); /** Get quantifiers bound inference utility */ QuantifiersBoundInference& getQuantifiersBoundInference(); + /** Get the preprocess utility */ + QuantifiersPreprocess& getPreprocess(); /** * Get quantifiers name, which returns a variable corresponding to the name of * quantified formula q if q has a name, or otherwise returns q itself. @@ -126,6 +129,8 @@ class QuantifiersRegistry : public QuantifiersUtil QuantAttributes d_quantAttr; /** The quantifiers bound inference class */ QuantifiersBoundInference d_quantBoundInf; + /** The quantifiers preprocessor utility */ + QuantifiersPreprocess d_quantPreproc; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 6d8570287..c66324445 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -548,8 +548,7 @@ Node QuantifiersRewriter::computeExtendedRewrite(Node q) { Node body = q[1]; // apply extended rewriter - ExtendedRewriter er; - Node bodyr = er.extendedRewrite(body); + Node bodyr = Rewriter::callExtendedRewrite(body); if (body != bodyr) { std::vector<Node> children; @@ -1407,92 +1406,6 @@ Node QuantifiersRewriter::computePrenex(Node q, return body; } -Node QuantifiersRewriter::computePrenexAgg(Node n, - std::map<Node, Node>& visited) -{ - std::map< Node, Node >::iterator itv = visited.find( n ); - if( itv!=visited.end() ){ - return itv->second; - } - if (!expr::hasClosure(n)) - { - // trivial - return n; - } - NodeManager* nm = NodeManager::currentNM(); - Node ret = n; - if (n.getKind() == NOT) - { - ret = computePrenexAgg(n[0], visited).negate(); - } - else if (n.getKind() == FORALL) - { - std::vector<Node> children; - children.push_back(computePrenexAgg(n[1], visited)); - std::vector<Node> args; - args.insert(args.end(), n[0].begin(), n[0].end()); - // for each child, strip top level quant - for (unsigned i = 0; i < children.size(); i++) - { - if (children[i].getKind() == FORALL) - { - args.insert(args.end(), children[i][0].begin(), children[i][0].end()); - children[i] = children[i][1]; - } - } - // keep the pattern - std::vector<Node> iplc; - if (n.getNumChildren() == 3) - { - iplc.insert(iplc.end(), n[2].begin(), n[2].end()); - } - Node nb = children.size() == 1 ? children[0] : nm->mkNode(OR, children); - ret = mkForall(args, nb, iplc, true); - } - else - { - std::unordered_set<Node> argsSet; - std::unordered_set<Node> nargsSet; - Node q; - Node nn = computePrenex(q, n, argsSet, nargsSet, true, true); - Assert(n != nn || argsSet.empty()); - Assert(n != nn || nargsSet.empty()); - if (n != nn) - { - Node nnn = computePrenexAgg(nn, visited); - // merge prenex - if (nnn.getKind() == FORALL) - { - argsSet.insert(nnn[0].begin(), nnn[0].end()); - nnn = nnn[1]; - // pos polarity variables are inner - if (!argsSet.empty()) - { - nnn = mkForall({argsSet.begin(), argsSet.end()}, nnn, true); - } - argsSet.clear(); - } - else if (nnn.getKind() == NOT && nnn[0].getKind() == FORALL) - { - nargsSet.insert(nnn[0][0].begin(), nnn[0][0].end()); - nnn = nnn[0][1].negate(); - } - if (!nargsSet.empty()) - { - nnn = mkForall({nargsSet.begin(), nargsSet.end()}, nnn.negate(), true) - .negate(); - } - if (!argsSet.empty()) - { - nnn = mkForall({argsSet.begin(), argsSet.end()}, nnn, true); - } - ret = nnn; - } - } - visited[n] = ret; - return ret; -} - Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) { Assert(body.getKind() == OR); size_t var_found_count = 0; @@ -2000,112 +1913,6 @@ bool QuantifiersRewriter::isPrenexNormalForm( Node n ) { } } -Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs ){ - Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl; - if( n.getKind()==kind::NOT ){ - Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvTypes, fvs ); - return nn.negate(); - }else if( n.getKind()==kind::FORALL ){ - if (n.getNumChildren() == 3) - { - // Do not pre-skolemize quantified formulas with three children. - // This includes non-standard quantified formulas - // like recursive function definitions, or sygus conjectures, and - // quantified formulas with triggers. - return n; - } - else if (polarity) - { - if( options::preSkolemQuant() && options::preSkolemQuantNested() ){ - vector< Node > children; - children.push_back( n[0] ); - //add children to current scope - std::vector< TypeNode > fvt; - std::vector< TNode > fvss; - fvt.insert( fvt.begin(), fvTypes.begin(), fvTypes.end() ); - fvss.insert( fvss.begin(), fvs.begin(), fvs.end() ); - for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ - fvt.push_back( n[0][i].getType() ); - fvss.push_back( n[0][i] ); - } - //process body - children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvt, fvss ) ); - //return processed quantifier - return NodeManager::currentNM()->mkNode( kind::FORALL, children ); - } - }else{ - //process body - Node nn = preSkolemizeQuantifiers( n[1], polarity, fvTypes, fvs ); - std::vector< Node > sk; - Node sub; - std::vector< unsigned > sub_vars; - //return skolemized body - return Skolemize::mkSkolemizedBody( - n, nn, fvTypes, fvs, sk, sub, sub_vars); - } - }else{ - //check if it contains a quantifier as a subterm - //if so, we will write this node - if (expr::hasClosure(n)) - { - if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || ( n.getKind()==kind::EQUAL && n[0].getType().isBoolean() ) ){ - if( options::preSkolemQuantAgg() ){ - Node nn; - //must remove structure - if( n.getKind()==kind::ITE ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); - }else if( n.getKind()==kind::EQUAL ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); - } - return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs ); - } - }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){ - vector< Node > children; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) ); - } - return NodeManager::currentNM()->mkNode( n.getKind(), children ); - } - } - } - return n; -} - -TrustNode QuantifiersRewriter::preprocess(Node n, bool isInst) -{ - Node prev = n; - - if( options::preSkolemQuant() ){ - if( !isInst || !options::preSkolemQuantNested() ){ - Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; - //apply pre-skolemization to existential quantifiers - std::vector< TypeNode > fvTypes; - std::vector< TNode > fvs; - n = preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); - } - } - //pull all quantifiers globally - if (options::prenexQuant() == options::PrenexQuantMode::NORMAL) - { - Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; - std::map<Node, Node> visited; - n = computePrenexAgg(n, visited); - n = Rewriter::rewrite( n ); - Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl; - //Assert( isPrenexNormalForm( n ) ); - } - if( n!=prev ){ - Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl; - Trace("quantifiers-preprocess") << "..returned " << n << std::endl; - return TrustNode::mkTrustRewrite(prev, n, nullptr); - } - return TrustNode::null(); -} - } // namespace quantifiers } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index a7f107573..de5c0b0a4 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -273,10 +273,6 @@ class QuantifiersRewriter : public TheoryRewriter std::unordered_set<Node>& nargs, bool pol, bool prenexAgg); - /** - * Apply prenexing aggressively. Returns the prenex normal form of n. - */ - static Node computePrenexAgg(Node n, std::map<Node, Node>& visited); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); private: static Node computeOperation(Node f, @@ -291,25 +287,8 @@ private: /** options */ static bool doOperation(Node f, RewriteStep computeOption, QAttributes& qa); -private: - static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs); public: static bool isPrenexNormalForm( Node n ); - /** preprocess - * - * This returns the result of applying simple quantifiers-specific - * preprocessing to n, including but not limited to: - * - rewrite rule elimination, - * - pre-skolemization, - * - aggressive prenexing. - * The argument isInst is set to true if n is an instance of a previously - * registered quantified formula. If this flag is true, we do not apply - * certain steps like pre-skolemization since we know they will have no - * effect. - * - * The result is wrapped in a trust node of kind TrustNodeKind::REWRITE. - */ - static TrustNode preprocess(Node n, bool isInst = false); static Node mkForAll(const std::vector<Node>& args, Node body, QAttributes& qa); diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 7e2c0c909..f4eb95469 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -75,10 +75,11 @@ void RelevantDomain::RDomain::removeRedundantTerms(QuantifiersState& qs) } } -RelevantDomain::RelevantDomain(QuantifiersState& qs, +RelevantDomain::RelevantDomain(Env& env, + QuantifiersState& qs, QuantifiersRegistry& qr, TermRegistry& tr) - : d_qs(qs), d_qreg(qr), d_treg(tr) + : QuantifiersUtil(env), d_qs(qs), d_qreg(qr), d_treg(tr) { d_is_computed = false; } diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 5643a4665..3b44b2263 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -45,7 +45,8 @@ class TermRegistry; class RelevantDomain : public QuantifiersUtil { public: - RelevantDomain(QuantifiersState& qs, + RelevantDomain(Env& env, + QuantifiersState& qs, QuantifiersRegistry& qr, TermRegistry& tr); virtual ~RelevantDomain(); diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index fa91b1782..23b66b1de 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -178,13 +178,18 @@ void Skolemize::getSelfSel(const DType& dt, Node Skolemize::mkSkolemizedBody(Node f, Node n, - std::vector<TypeNode>& argTypes, std::vector<TNode>& fvs, std::vector<Node>& sk, Node& sub, std::vector<unsigned>& sub_vars) { NodeManager* nm = NodeManager::currentNM(); + // compute the argument types from the free variables + std::vector<TypeNode> argTypes; + for (TNode v : fvs) + { + argTypes.push_back(v.getType()); + } SkolemManager* sm = nm->getSkolemManager(); Assert(sk.empty() || sk.size() == f[0].getNumChildren()); // calculate the variables and substitution @@ -329,12 +334,11 @@ Node Skolemize::getSkolemizedBody(Node f) std::unordered_map<Node, Node>::iterator it = d_skolem_body.find(f); if (it == d_skolem_body.end()) { - std::vector<TypeNode> fvTypes; std::vector<TNode> fvs; Node sub; std::vector<unsigned> sub_vars; - Node ret = mkSkolemizedBody( - f, f[1], fvTypes, fvs, d_skolem_constants[f], sub, sub_vars); + Node ret = + mkSkolemizedBody(f, f[1], fvs, d_skolem_constants[f], sub, sub_vars); d_skolem_body[f] = ret; // store sub quantifier information if (!sub.isNull()) diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index c8e6ec7dd..fbb79f5d2 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -89,10 +89,10 @@ class Skolemize * The skolem constants/functions we generate by this * skolemization are added to sk. * - * The arguments fvTypes and fvs are used if we are + * The argument fvs are used if we are * performing skolemization within a nested quantified * formula. In this case, skolem constants we introduce - * must be parameterized based on fvTypes and must be + * must be parameterized based on the types of fvs and must be * applied to fvs. * * The last two arguments sub and sub_vars are used for @@ -103,7 +103,6 @@ class Skolemize */ static Node mkSkolemizedBody(Node q, Node n, - std::vector<TypeNode>& fvTypes, std::vector<TNode>& fvs, std::vector<Node>& sk, Node& sub, diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index d2c616238..9c43e8b51 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -228,6 +228,9 @@ bool CegSingleInv::solve() // solve the single invocation conjecture using a fresh copy of SMT engine std::unique_ptr<SmtEngine> siSmt; initializeSubsolver(siSmt, d_env); + // do not use shared selectors in subsolver, since this leads to solutions + // with non-user symbols + siSmt->setOption("dt-share-sel", "false"); siSmt->assertFormula(siq); Result r = siSmt->checkSat(); Trace("sygus-si") << "Result: " << r << std::endl; @@ -400,7 +403,7 @@ Node CegSingleInv::getSolutionFromInst(size_t index) } //simplify the solution using the extended rewriter Trace("csi-sol") << "Solution (pre-simplification): " << s << std::endl; - s = d_treg.getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(s); + s = extendedRewrite(s); Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl; // wrap into lambda, as needed return SygusUtils::wrapSolutionForSynthFun(prog, s); @@ -467,7 +470,7 @@ Node CegSingleInv::reconstructToSyntax(Node s, { Trace("csi-sol") << "Post-process solution..." << std::endl; Node prev = sol; - sol = d_treg.getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(sol); + sol = extendedRewrite(sol); if (prev != sol) { Trace("csi-sol") << "Solution (after post process) : " << sol diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 57b763044..f5774c761 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -32,11 +32,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -Cegis::Cegis(QuantifiersState& qs, +Cegis::Cegis(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : SygusModule(qs, qim, tds, p), + : SygusModule(env, qs, qim, tds, p), d_eval_unfold(tds->getEvalUnfold()), d_usingSymCons(false) { @@ -345,7 +346,7 @@ void Cegis::addRefinementLemma(Node lem) d_rl_vals.end()); } // rewrite with extended rewriter - slem = d_tds->getExtRewriter()->extendedRewrite(slem); + slem = d_tds->rewriteNode(slem); // collect all variables in slem expr::getSymbols(slem, d_refinement_lemma_vars); std::vector<Node> waiting; @@ -509,7 +510,7 @@ bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, Node lemcs = lem.substitute(vs.begin(), vs.end(), ms.begin(), ms.end()); Trace("sygus-cref-eval2") << "...under substitution it is : " << lemcs << std::endl; - Node lemcsu = vsit.doEvaluateWithUnfolding(d_tds, lemcs); + Node lemcsu = d_tds->rewriteNode(lemcs); Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu << std::endl; if (lemcsu.isConst() && !lemcsu.getConst<bool>()) diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index d6678a305..d72805950 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -19,6 +19,8 @@ #define CVC5__THEORY__QUANTIFIERS__CEGIS_H #include <map> + +#include "smt/env_obj.h" #include "theory/quantifiers/sygus/sygus_module.h" #include "theory/quantifiers/sygus_sampler.h" @@ -42,7 +44,8 @@ namespace quantifiers { class Cegis : public SygusModule { public: - Cegis(QuantifiersState& qs, + Cegis(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 9a9d8f02d..a42323227 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -68,11 +68,12 @@ bool VariadicTrie::hasSubset(const std::vector<Node>& is) const return false; } -CegisCoreConnective::CegisCoreConnective(QuantifiersState& qs, +CegisCoreConnective::CegisCoreConnective(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : Cegis(qs, qim, tds, p) + : Cegis(env, qs, qim, tds, p) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -629,9 +630,7 @@ bool CegisCoreConnective::getUnsatCore( Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const { Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl; - Env& env = d_qstate.getEnv(); - Result r = - checkWithSubsolver(n, d_vars, mvs, env.getOptions(), env.getLogicInfo()); + Result r = checkWithSubsolver(n, d_vars, mvs, options(), logicInfo()); Trace("sygus-ccore-debug") << "...got " << r << std::endl; return r; } @@ -739,7 +738,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, addSuccess = false; // try a new core std::unique_ptr<SmtEngine> checkSol; - initializeSubsolver(checkSol, d_qstate.getEnv()); + initializeSubsolver(checkSol, d_env); Trace("sygus-ccore") << "----- Check candidate " << an << std::endl; std::vector<Node> rasserts = asserts; rasserts.push_back(d_sc); @@ -779,7 +778,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, // In terms of Variant #2, this is the check "if S ^ U is unsat" Trace("sygus-ccore") << "----- Check side condition" << std::endl; std::unique_ptr<SmtEngine> checkSc; - initializeSubsolver(checkSc, d_qstate.getEnv()); + initializeSubsolver(checkSc, d_env); std::vector<Node> scasserts; scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end()); scasserts.push_back(d_sc); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index e9a73e9bb..80ba6f26e 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "expr/node_trie.h" +#include "smt/env_obj.h" #include "theory/evaluator.h" #include "theory/quantifiers/sygus/cegis.h" #include "util/result.h" @@ -160,7 +161,8 @@ class VariadicTrie class CegisCoreConnective : public Cegis { public: - CegisCoreConnective(QuantifiersState& qs, + CegisCoreConnective(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 797aecdab..871a85fbd 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -30,13 +30,14 @@ namespace cvc5 { namespace theory { namespace quantifiers { -CegisUnif::CegisUnif(QuantifiersState& qs, +CegisUnif::CegisUnif(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : Cegis(qs, qim, tds, p), - d_sygus_unif(qs.getEnv(), p), - d_u_enum_manager(qs, qim, tds, p) + : Cegis(env, qs, qim, tds, p), + d_sygus_unif(env, p), + d_u_enum_manager(env, qs, qim, tds, p) { } @@ -403,6 +404,7 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars, Node lem) } CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy( + Env& env, QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 0cddff9c1..da47aabbe 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -20,6 +20,7 @@ #include <map> #include <vector> +#include "smt/env_obj.h" #include "theory/decision_strategy.h" #include "theory/quantifiers/sygus/cegis.h" #include "theory/quantifiers/sygus/sygus_unif_rl.h" @@ -49,7 +50,8 @@ namespace quantifiers { class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf { public: - CegisUnifEnumDecisionStrategy(QuantifiersState& qs, + CegisUnifEnumDecisionStrategy(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* parent); @@ -207,7 +209,8 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf class CegisUnif : public Cegis { public: - CegisUnif(QuantifiersState& qs, + CegisUnif(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index f853ac8e8..a5be4ebd6 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -16,15 +16,16 @@ #include "theory/quantifiers/sygus/enum_stream_substitution.h" +#include <numeric> // for std::iota +#include <sstream> + #include "expr/dtype_cons.h" #include "options/base_options.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" #include "theory/quantifiers/sygus/term_database_sygus.h" - -#include <numeric> // for std::iota -#include <sstream> +#include "theory/rewriter.h" using namespace cvc5::kind; @@ -32,7 +33,7 @@ namespace cvc5 { namespace theory { namespace quantifiers { -EnumStreamPermutation::EnumStreamPermutation(quantifiers::TermDbSygus* tds) +EnumStreamPermutation::EnumStreamPermutation(TermDbSygus* tds) : d_tds(tds), d_first(true), d_curr_ind(0) { } @@ -124,8 +125,7 @@ Node EnumStreamPermutation::getNext() { d_first = false; Node bultin_value = d_tds->sygusToBuiltin(d_value, d_value.getType()); - d_perm_values.insert( - d_tds->getExtRewriter()->extendedRewrite(bultin_value)); + d_perm_values.insert(Rewriter::callExtendedRewrite(bultin_value)); return d_value; } unsigned n_classes = d_perm_state_class.size(); @@ -194,8 +194,7 @@ Node EnumStreamPermutation::getNext() << " ......perm builtin is " << bultin_perm_value; if (options::sygusSymBreakDynamic()) { - bultin_perm_value = - d_tds->getExtRewriter()->extendedRewrite(bultin_perm_value); + bultin_perm_value = Rewriter::callExtendedRewrite(bultin_perm_value); Trace("synth-stream-concrete-debug") << " and rewrites to " << bultin_perm_value; } @@ -515,8 +514,7 @@ Node EnumStreamSubstitution::getNext() d_tds->sygusToBuiltin(comb_value, comb_value.getType()); if (options::sygusSymBreakDynamic()) { - builtin_comb_value = - d_tds->getExtRewriter()->extendedRewrite(builtin_comb_value); + builtin_comb_value = Rewriter::callExtendedRewrite(builtin_comb_value); } if (Trace.isOn("synth-stream-concrete")) { diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp index 8a2d70bfa..e7b3bbaa9 100644 --- a/src/theory/quantifiers/sygus/enum_value_manager.cpp +++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp @@ -33,13 +33,15 @@ namespace cvc5 { namespace theory { namespace quantifiers { -EnumValueManager::EnumValueManager(Node e, +EnumValueManager::EnumValueManager(Env& env, QuantifiersState& qs, QuantifiersInferenceManager& qim, TermRegistry& tr, SygusStatistics& s, + Node e, bool hasExamples) - : d_enum(e), + : EnvObj(env), + d_enum(e), d_qstate(qs), d_qim(qim), d_treg(tr), @@ -108,7 +110,7 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete) d_samplerRrV->initializeSygus( d_tds, e, options::sygusSamples(), false); // use the default output for the output of sygusRewVerify - out = d_qstate.options().base.out; + out = options().base.out; } d_secd.reset(new SygusEnumeratorCallbackDefault( e, &d_stats, d_eec.get(), d_samplerRrV.get(), out)); diff --git a/src/theory/quantifiers/sygus/enum_value_manager.h b/src/theory/quantifiers/sygus/enum_value_manager.h index c786bb6f1..23fdc7391 100644 --- a/src/theory/quantifiers/sygus/enum_value_manager.h +++ b/src/theory/quantifiers/sygus/enum_value_manager.h @@ -19,6 +19,7 @@ #define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_VALUE_MANAGER_H #include "expr/node.h" +#include "smt/env_obj.h" #include "theory/quantifiers/sygus/enum_val_generator.h" #include "theory/quantifiers/sygus/example_eval_cache.h" #include "theory/quantifiers/sygus/sygus_enumerator_callback.h" @@ -38,14 +39,15 @@ class SygusStatistics; * not actively generated, or may be determined by the (fast) enumerator * when it is actively generated. */ -class EnumValueManager +class EnumValueManager : protected EnvObj { public: - EnumValueManager(Node e, + EnumValueManager(Env& env, QuantifiersState& qs, QuantifiersInferenceManager& qim, TermRegistry& tr, SygusStatistics& s, + Node e, bool hasExamples); ~EnumValueManager(); /** diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp index f45b976ec..743f67cec 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_enumerator_basic.h" #include "options/datatypes_options.h" +#include "theory/rewriter.h" using namespace cvc5::kind; using namespace std; @@ -40,7 +41,7 @@ bool EnumValGeneratorBasic::increment() if (options::sygusSymBreakDynamic()) { Node nextb = d_tds->sygusToBuiltin(d_currTerm); - nextb = d_tds->getExtRewriter()->extendedRewrite(nextb); + nextb = Rewriter::callExtendedRewrite(nextb); if (d_cache.find(nextb) == d_cache.end()) { d_cache.insert(nextb); diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp index 3b536695f..1b5b3f5af 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/sygus/example_eval_cache.h" #include "theory/quantifiers/sygus/sygus_stats.h" #include "theory/quantifiers/sygus_sampler.h" +#include "theory/rewriter.h" namespace cvc5 { namespace theory { @@ -33,7 +34,7 @@ SygusEnumeratorCallback::SygusEnumeratorCallback(Node e, SygusStatistics* s) bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms) { Node bn = datatypes::utils::sygusToBuiltin(n); - Node bnr = d_extr.extendedRewrite(bn); + Node bnr = Rewriter::callExtendedRewrite(bn); if (d_stats != nullptr) { ++(d_stats->d_enumTermsRewrite); diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h index 5ed28b309..8689d876f 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h @@ -74,8 +74,6 @@ class SygusEnumeratorCallback Node d_enum; /** The type of enum */ TypeNode d_tn; - /** extended rewriter */ - ExtendedRewriter d_extr; /** pointer to the statistics */ SygusStatistics* d_stats; }; diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 0ef1e7f17..7af1ef45b 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -180,7 +180,7 @@ void SygusEvalUnfold::registerModelValue(Node a, Node conj = nm->mkNode(DT_SYGUS_EVAL, eval_children); eval_children[0] = vn; Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children); - res = d_tds->evaluateWithUnfolding(eval_fun); + res = d_tds->rewriteNode(eval_fun); Trace("sygus-eval-unfold") << "Evaluate with unfolding returns " << res << std::endl; esit.init(conj, n, res); @@ -324,13 +324,6 @@ Node SygusEvalUnfold::unfold(Node en, return ret; } -Node SygusEvalUnfold::unfold(Node en) -{ - std::map<Node, Node> vtm; - std::vector<Node> exp; - return unfold(en, vtm, exp, false, false); -} - } // namespace quantifiers } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index bb181996a..c30d4dae7 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -122,11 +122,6 @@ class SygusEvalUnfold std::vector<Node>& exp, bool track_exp = true, bool doRec = false); - /** - * Same as above, but without explanation tracking. This is used for concrete - * evaluation heads - */ - Node unfold(Node en); private: /** sygus term database associated with this utility */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index a51fcce25..fd84f0c0a 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -21,6 +21,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" using namespace std; using namespace cvc5::kind; @@ -147,7 +148,7 @@ void SygusRedundantCons::getGenericList(TermDbSygus* tds, if (index == dt[c].getNumArgs()) { Node gt = tds->mkGeneric(dt, c, pre); - gt = tds->getExtRewriter()->extendedRewrite(gt); + gt = Rewriter::callExtendedRewrite(gt); terms.push_back(gt); return; } diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index cb7e2b84e..8048330e4 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -49,11 +49,6 @@ void EvalSygusInvarianceTest::init(Node conj, Node var, Node res) d_result = res; } -Node EvalSygusInvarianceTest::doEvaluateWithUnfolding(TermDbSygus* tds, Node n) -{ - return tds->evaluateWithUnfolding(n, d_visited); -} - bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) { TNode tnvn = nvn; @@ -61,7 +56,7 @@ bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) for (const Node& c : d_terms) { Node conj_subs = c.substitute(d_var, tnvn, cache); - Node conj_subs_unfold = doEvaluateWithUnfolding(tds, conj_subs); + Node conj_subs_unfold = tds->rewriteNode(conj_subs); Trace("sygus-cref-eval2-debug") << " ...check unfolding : " << conj_subs_unfold << std::endl; Trace("sygus-cref-eval2-debug") @@ -111,7 +106,7 @@ bool EquivSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) { TypeNode tn = nvn.getType(); Node nbv = tds->sygusToBuiltin(nvn, tn); - Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv); + Node nbvr = Rewriter::callExtendedRewrite(nbv); Trace("sygus-sb-mexp-debug") << " min-exp check : " << nbv << " -> " << nbvr << std::endl; bool exc_arg = false; @@ -181,7 +176,7 @@ bool DivByZeroSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) { TypeNode tn = nvn.getType(); Node nbv = tds->sygusToBuiltin(nvn, tn); - Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv); + Node nbvr = Rewriter::callExtendedRewrite(nbv); if (tds->involvesDivByZero(nbvr)) { Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn) @@ -212,7 +207,7 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, { TypeNode tn = nvn.getType(); Node nbv = tds->sygusToBuiltin(nvn, tn); - Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv); + Node nbvr = Rewriter::callExtendedRewrite(nbv); // if for any of the examples, it is not contained, then we can exclude for (unsigned i = 0; i < d_neg_con_indices.size(); i++) { diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index ca5f057b1..afb59bf73 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -111,9 +111,6 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest */ void init(Node conj, Node var, Node res); - /** do evaluate with unfolding, using the cache of this class */ - Node doEvaluateWithUnfolding(TermDbSygus* tds, Node n); - protected: /** does d_terms{ d_var -> nvn } still rewrite to d_result? */ bool invariant(TermDbSygus* tds, Node nvn, Node x) override; @@ -137,8 +134,6 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest * disjunctively, i.e. if one child test succeeds, the overall test succeeds. */ bool d_is_conjunctive; - /** cache of n -> the simplified form of eval( n ) */ - std::unordered_map<Node, Node> d_visited; }; /** EquivSygusInvarianceTest diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index 8272c6418..1840f0eb1 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -21,11 +21,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusModule::SygusModule(QuantifiersState& qs, +SygusModule::SygusModule(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : EnvObj(qs.getEnv()), d_qstate(qs), d_qim(qim), d_tds(tds), d_parent(p) + : EnvObj(env), d_qstate(qs), d_qim(qim), d_tds(tds), d_parent(p) { } diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 8070fe009..8ee1fc9b4 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -53,7 +53,8 @@ class QuantifiersInferenceManager; class SygusModule : protected EnvObj { public: - SygusModule(QuantifiersState& qs, + SygusModule(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 7601e2117..453ac5c18 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -30,11 +30,12 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SygusPbe::SygusPbe(QuantifiersState& qs, +SygusPbe::SygusPbe(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p) - : SygusModule(qs, qim, tds, p) + : SygusModule(env, qs, qim, tds, p) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -131,7 +132,7 @@ bool SygusPbe::initialize(Node conj, // Apply extended rewriting on the lemma. This helps utilities like // SygusEnumerator more easily recognize the shape of this lemma, e.g. // ( ~is-ite(x) or ( ~is-ite(x) ^ P ) ) --> ~is-ite(x). - lem = d_tds->getExtRewriter()->extendedRewrite(lem); + lem = extendedRewrite(lem); Trace("sygus-pbe") << " static redundant op lemma : " << lem << std::endl; // Register as a symmetry breaking lemma with the term database. diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 867764617..e55479e18 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -18,6 +18,7 @@ #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H +#include "smt/env_obj.h" #include "theory/quantifiers/sygus/sygus_module.h" namespace cvc5 { @@ -86,7 +87,8 @@ class SynthConjecture; class SygusPbe : public SygusModule { public: - SygusPbe(QuantifiersState& qs, + SygusPbe(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p); diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index bcd826799..b7611784d 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -444,7 +444,7 @@ Node SygusRepairConst::getFoQuery(Node body, Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl; Trace("sygus-repair-const") << " Unfold the specification..." << std::endl; - body = d_tds->evaluateWithUnfolding(body); + body = d_tds->rewriteNode(body); Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl; Trace("sygus-repair-const") << " Introduce first-order vars..." << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 9626f7af4..3fb80f917 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -569,7 +569,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) std::vector<Node> base_results; TypeNode xtn = e.getType(); Node bv = d_tds->sygusToBuiltin(v, xtn); - bv = d_tds->getExtRewriter()->extendedRewrite(bv); + bv = extendedRewrite(bv); Trace("sygus-sui-enum") << "PBE Compute Examples for " << bv << std::endl; // compte the results (should be cached) ExampleEvalCache* eec = d_parent->getExampleEvalCache(e); diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 10db1ef9e..6b023075b 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -264,7 +264,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren); Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..." << std::endl; - eut = d_tds->getEvalUnfold()->unfold(eut); + eut = d_tds->rewriteNode(eut); Trace("sygus-unif-debug2") << " ...got " << eut; Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 3e7095c12..da021227a 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -45,29 +45,31 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SynthConjecture::SynthConjecture(QuantifiersState& qs, +SynthConjecture::SynthConjecture(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, SygusStatistics& s) - : d_qstate(qs), + : EnvObj(env), + d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr), d_stats(s), d_tds(tr.getTermDatabaseSygus()), - d_verify(qs.options(), qs.getLogicInfo(), d_tds), + d_verify(options(), qs.getLogicInfo(), d_tds), d_hasSolution(false), - d_ceg_si(new CegSingleInv(qs.getEnv(), tr, s)), + d_ceg_si(new CegSingleInv(env, tr, s)), d_templInfer(new SygusTemplateInfer), d_ceg_proc(new SynthConjectureProcess), d_ceg_gc(new CegGrammarConstructor(d_tds, this)), - d_sygus_rconst(new SygusRepairConst(qs.getEnv(), d_tds)), + d_sygus_rconst(new SygusRepairConst(env, d_tds)), d_exampleInfer(new ExampleInfer(d_tds)), - d_ceg_pbe(new SygusPbe(qs, qim, d_tds, this)), - d_ceg_cegis(new Cegis(qs, qim, d_tds, this)), - d_ceg_cegisUnif(new CegisUnif(qs, qim, d_tds, this)), - d_sygus_ccore(new CegisCoreConnective(qs, qim, d_tds, this)), + d_ceg_pbe(new SygusPbe(env, qs, qim, d_tds, this)), + d_ceg_cegis(new Cegis(env, qs, qim, d_tds, this)), + d_ceg_cegisUnif(new CegisUnif(env, qs, qim, d_tds, this)), + d_sygus_ccore(new CegisCoreConnective(env, qs, qim, d_tds, this)), d_master(nullptr), d_set_ce_sk_vars(false), d_repair_index(0), @@ -513,7 +515,7 @@ bool SynthConjecture::doCheck() { if (printDebug) { - const Options& sopts = d_qstate.options(); + const Options& sopts = options(); std::ostream& out = *sopts.base.out; out << "(sygus-candidate "; Assert(d_quant[0].getNumChildren() == candidate_values.size()); @@ -609,8 +611,7 @@ bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const } Trace("sygus-engine") << "Check side condition..." << std::endl; Trace("cegqi-debug") << "Check side condition : " << sc << std::endl; - Env& env = d_qstate.getEnv(); - Result r = checkWithSubsolver(sc, env.getOptions(), env.getLogicInfo()); + Result r = checkWithSubsolver(sc, options(), logicInfo()); Trace("cegqi-debug") << "...got side condition : " << r << std::endl; if (r == Result::UNSAT) { @@ -763,8 +764,8 @@ EnumValueManager* SynthConjecture::getEnumValueManagerFor(Node e) Node f = d_tds->getSynthFunForEnumerator(e); bool hasExamples = (d_exampleInfer->hasExamples(f) && d_exampleInfer->getNumExamples(f) != 0); - d_enumManager[e].reset( - new EnumValueManager(e, d_qstate, d_qim, d_treg, d_stats, hasExamples)); + d_enumManager[e].reset(new EnumValueManager( + d_env, d_qstate, d_qim, d_treg, d_stats, e, hasExamples)); EnumValueManager* eman = d_enumManager[e].get(); // set up the examples if (hasExamples) @@ -800,8 +801,7 @@ void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums, Assert(d_master != nullptr); // we have generated a solution, print it // get the current output stream - const Options& sopts = d_qstate.options(); - printSynthSolutionInternal(*sopts.base.out); + printSynthSolutionInternal(*options().base.out); excludeCurrentSolution(enums, values); } @@ -885,7 +885,7 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out) d_exprm.find(prog); if (its == d_exprm.end()) { - d_exprm[prog].reset(new ExpressionMinerManager(d_qstate.getEnv())); + d_exprm[prog].reset(new ExpressionMinerManager(d_env)); ExpressionMinerManager* emm = d_exprm[prog].get(); emm->initializeSygus( d_tds, d_candidates[i], options::sygusSamples(), true); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 9cc488fd2..d7635c816 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -21,6 +21,7 @@ #include <memory> +#include "smt/env_obj.h" #include "theory/quantifiers/expr_miner_manager.h" #include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "theory/quantifiers/sygus/cegis.h" @@ -51,10 +52,11 @@ class EnumValueManager; * determines which approach and optimizations are applicable to the * conjecture, and has interfaces for implementing them. */ -class SynthConjecture +class SynthConjecture : protected EnvObj { public: - SynthConjecture(QuantifiersState& qs, + SynthConjecture(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr, diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index cdcbeb85d..454442351 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -26,14 +26,15 @@ namespace cvc5 { namespace theory { namespace quantifiers { -SynthEngine::SynthEngine(QuantifiersState& qs, +SynthEngine::SynthEngine(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp(qs.getEnv()) + : QuantifiersModule(env, qs, qim, qr, tr), d_conj(nullptr), d_sqp(env) { d_conjs.push_back(std::unique_ptr<SynthConjecture>( - new SynthConjecture(qs, qim, qr, tr, d_statistics))); + new SynthConjecture(env, qs, qim, qr, tr, d_statistics))); d_conj = d_conjs.back().get(); } @@ -153,8 +154,8 @@ void SynthEngine::assignConjecture(Node q) // allocate a new synthesis conjecture if not assigned if (d_conjs.back()->isAssigned()) { - d_conjs.push_back(std::unique_ptr<SynthConjecture>( - new SynthConjecture(d_qstate, d_qim, d_qreg, d_treg, d_statistics))); + d_conjs.push_back(std::unique_ptr<SynthConjecture>(new SynthConjecture( + d_env, d_qstate, d_qim, d_qreg, d_treg, d_statistics))); } d_conjs.back()->assign(q); } diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index d37df4e28..c623d9c0f 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -34,7 +34,8 @@ class SynthEngine : public QuantifiersModule typedef context::CDHashMap<Node, bool> NodeBoolMap; public: - SynthEngine(QuantifiersState& qs, + SynthEngine(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 3b0ea3312..035db433e 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -51,10 +51,10 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r) return os; } -TermDbSygus::TermDbSygus(QuantifiersState& qs) - : d_qstate(qs), +TermDbSygus::TermDbSygus(Env& env, QuantifiersState& qs) + : EnvObj(env), + d_qstate(qs), d_syexp(new SygusExplain(this)), - d_ext_rw(new ExtendedRewriter(true)), d_eval(new Evaluator), d_funDefEval(new FunDefEvaluator), d_eval_unfold(new SygusEvalUnfold(this)) @@ -739,7 +739,15 @@ SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn) Node TermDbSygus::rewriteNode(Node n) const { - Node res = Rewriter::rewrite(n); + Node res; + if (options().quantifiers.sygusExtRew) + { + res = extendedRewrite(n); + } + else + { + res = rewrite(n); + } if (res.isConst()) { // constant, we are done @@ -1001,59 +1009,6 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn, return rewriteNode(res); } -Node TermDbSygus::evaluateWithUnfolding(Node n, - std::unordered_map<Node, Node>& visited) -{ - std::unordered_map<Node, Node>::iterator it = visited.find(n); - if( it==visited.end() ){ - Node ret = n; - while (ret.getKind() == DT_SYGUS_EVAL - && ret[0].getKind() == APPLY_CONSTRUCTOR) - { - if (ret == n && ret[0].isConst()) - { - // use rewriting, possibly involving recursive functions - ret = rewriteNode(ret); - } - else - { - ret = d_eval_unfold->unfold(ret); - } - } - if( ret.getNumChildren()>0 ){ - std::vector< Node > children; - if( ret.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( ret.getOperator() ); - } - bool childChanged = false; - for( unsigned i=0; i<ret.getNumChildren(); i++ ){ - Node nc = evaluateWithUnfolding(ret[i], visited); - childChanged = childChanged || nc!=ret[i]; - children.push_back( nc ); - } - if( childChanged ){ - ret = NodeManager::currentNM()->mkNode( ret.getKind(), children ); - } - if (options::sygusExtRew()) - { - ret = getExtRewriter()->extendedRewrite(ret); - } - // use rewriting, possibly involving recursive functions - ret = rewriteNode(ret); - } - visited[n] = ret; - return ret; - }else{ - return it->second; - } -} - -Node TermDbSygus::evaluateWithUnfolding(Node n) -{ - std::unordered_map<Node, Node> visited; - return evaluateWithUnfolding(n, visited); -} - bool TermDbSygus::isEvaluationPoint(Node n) const { if (n.getKind() != DT_SYGUS_EVAL) diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 80411b258..7b05c70e4 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -21,6 +21,7 @@ #include <unordered_set> #include "expr/dtype.h" +#include "smt/env_obj.h" #include "theory/evaluator.h" #include "theory/quantifiers/extended_rewrite.h" #include "theory/quantifiers/fun_def_evaluator.h" @@ -53,9 +54,10 @@ enum EnumeratorRole std::ostream& operator<<(std::ostream& os, EnumeratorRole r); // TODO :issue #1235 split and document this class -class TermDbSygus { +class TermDbSygus : protected EnvObj +{ public: - TermDbSygus(QuantifiersState& qs); + TermDbSygus(Env& env, QuantifiersState& qs); ~TermDbSygus() {} /** Finish init, which sets the inference manager */ void finishInit(QuantifiersInferenceManager* qim); @@ -78,8 +80,6 @@ class TermDbSygus { //------------------------------utilities /** get the explanation utility */ SygusExplain* getExplain() { return d_syexp.get(); } - /** get the extended rewrite utility */ - ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); } /** get the evaluator */ Evaluator* getEvaluator() { return d_eval.get(); } /** (recursive) function evaluator utility */ @@ -271,21 +271,6 @@ class TermDbSygus { Node bn, const std::vector<Node>& args, bool tryEval = true); - /** evaluate with unfolding - * - * n is any term that may involve sygus evaluation functions. This function - * returns the result of unfolding the evaluation functions within n and - * rewriting the result. For example, if eval_A is the evaluation function - * for the datatype: - * A -> C_0 | C_1 | C_x | C_+( C_A, C_A ) - * corresponding to grammar: - * A -> 0 | 1 | x | A + A - * then calling this function on eval( C_+( x, 1 ), 4 ) = y returns 5 = y. - * The node returned by this function is in (extended) rewritten form. - */ - Node evaluateWithUnfolding(Node n); - /** same as above, but with a cache of visited nodes */ - Node evaluateWithUnfolding(Node n, std::unordered_map<Node, Node>& visited); /** is evaluation point? * * Returns true if n is of the form eval( x, c1...cn ) for some variable x @@ -324,8 +309,6 @@ class TermDbSygus { //------------------------------utilities /** sygus explanation */ std::unique_ptr<SygusExplain> d_syexp; - /** extended rewriter */ - std::unique_ptr<ExtendedRewriter> d_ext_rw; /** evaluator */ std::unique_ptr<Evaluator> d_eval; /** (recursive) function evaluator utility */ @@ -461,7 +444,6 @@ class TermDbSygus { /** get anchor */ static Node getAnchor( Node n ); static unsigned getAnchorDepth( Node n ); - }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 21852f25a..4da273cd9 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -182,14 +182,15 @@ void addSpecialValues(const TypeNode& tn, } // namespace -SygusInst::SygusInst(QuantifiersState& qs, +SygusInst::SygusInst(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr) - : QuantifiersModule(qs, qim, qr, tr), - d_ce_lemma_added(qs.getUserContext()), - d_global_terms(qs.getUserContext()), - d_notified_assertions(qs.getUserContext()) + : QuantifiersModule(env, qs, qim, qr, tr), + d_ce_lemma_added(userContext()), + d_global_terms(userContext()), + d_notified_assertions(userContext()) { } diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index 80c7e809f..060ab7226 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -22,6 +22,7 @@ #include <unordered_set> #include "context/cdhashset.h" +#include "smt/env_obj.h" #include "theory/decision_strategy.h" #include "theory/quantifiers/quant_module.h" @@ -64,7 +65,8 @@ namespace quantifiers { class SygusInst : public QuantifiersModule { public: - SygusInst(QuantifiersState& qs, + SygusInst(Env& env, + QuantifiersState& qs, QuantifiersInferenceManager& qim, QuantifiersRegistry& qr, TermRegistry& tr); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d2f872afb..6aa2a816a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -37,8 +37,9 @@ namespace cvc5 { namespace theory { namespace quantifiers { -TermDb::TermDb(QuantifiersState& qs, QuantifiersRegistry& qr) - : d_qstate(qs), +TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr) + : QuantifiersUtil(env), + d_qstate(qs), d_qim(nullptr), d_qreg(qr), d_termsContext(), diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index a4e95487c..af0b87bd8 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -73,8 +73,7 @@ class TermDb : public QuantifiersUtil { using NodeDbListMap = context::CDHashMap<Node, std::shared_ptr<DbList>>; public: - TermDb(QuantifiersState& qs, - QuantifiersRegistry& qr); + TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr); virtual ~TermDb(); /** Finish init, which sets the inference manager */ void finishInit(QuantifiersInferenceManager* qim); diff --git a/src/theory/quantifiers/term_pools.cpp b/src/theory/quantifiers/term_pools.cpp index 2d95c8b20..7bac0252d 100644 --- a/src/theory/quantifiers/term_pools.cpp +++ b/src/theory/quantifiers/term_pools.cpp @@ -36,7 +36,10 @@ void TermPoolQuantInfo::initialize() d_skolemAddToPool.clear(); } -TermPools::TermPools(QuantifiersState& qs) : d_qs(qs) {} +TermPools::TermPools(Env& env, QuantifiersState& qs) + : QuantifiersUtil(env), d_qs(qs) +{ +} bool TermPools::reset(Theory::Effort e) { diff --git a/src/theory/quantifiers/term_pools.h b/src/theory/quantifiers/term_pools.h index 5a7556ad9..37b16a785 100644 --- a/src/theory/quantifiers/term_pools.h +++ b/src/theory/quantifiers/term_pools.h @@ -71,7 +71,7 @@ class TermPoolQuantInfo class TermPools : public QuantifiersUtil { public: - TermPools(QuantifiersState& qs); + TermPools(Env& env, QuantifiersState& qs); ~TermPools() {} /** reset, which resets the current values of pools */ bool reset(Theory::Effort e) override; diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index 324217798..98618f3f7 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -29,20 +29,23 @@ namespace cvc5 { namespace theory { namespace quantifiers { -TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr) - : d_presolve(qs.getUserContext(), true), +TermRegistry::TermRegistry(Env& env, + QuantifiersState& qs, + QuantifiersRegistry& qr) + : EnvObj(env), + d_presolve(qs.getUserContext(), true), d_presolveCache(qs.getUserContext()), d_termEnum(new TermEnumeration), - d_termPools(new TermPools(qs)), - d_termDb(qs.getEnv().getLogicInfo().isHigherOrder() ? new HoTermDb(qs, qr) - : new TermDb(qs, qr)), + d_termPools(new TermPools(env, qs)), + d_termDb(logicInfo().isHigherOrder() ? new HoTermDb(env, qs, qr) + : new TermDb(env, qs, qr)), d_sygusTdb(nullptr), d_qmodel(nullptr) { if (options::sygus() || options::sygusInst()) { // must be constructed here since it is required for datatypes finistInit - d_sygusTdb.reset(new TermDbSygus(qs)); + d_sygusTdb.reset(new TermDbSygus(env, qs)); } Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index c3e4fcf4c..175d450df 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -22,6 +22,7 @@ #include <unordered_set> #include "context/cdhashset.h" +#include "smt/env_obj.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" @@ -37,13 +38,12 @@ class FirstOrderModel; * Term Registry, which manages notifying modules within quantifiers about * (ground) terms that exist in the current context. */ -class TermRegistry +class TermRegistry : protected EnvObj { using NodeSet = context::CDHashSet<Node>; public: - TermRegistry(QuantifiersState& qs, - QuantifiersRegistry& qr); + TermRegistry(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr); /** Finish init, which sets the inference manager on modules of this class */ void finishInit(FirstOrderModel* fm, QuantifiersInferenceManager* qim); /** Presolve */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index dff0ac979..76696c32f 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -35,14 +35,14 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env, Valuation valuation) : Theory(THEORY_QUANTIFIERS, env, out, valuation), d_qstate(env, valuation, logicInfo()), - d_qreg(), - d_treg(d_qstate, d_qreg), + d_qreg(env), + d_treg(env, d_qstate, d_qreg), d_qim(env, *this, d_qstate, d_qreg, d_treg, d_pnm), d_qengine(nullptr) { // construct the quantifiers engine d_qengine.reset( - new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, d_pnm)); + new QuantifiersEngine(env, d_qstate, d_qreg, d_treg, d_qim, d_pnm)); // indicate we are using the quantifiers theory state object d_theoryState = &d_qstate; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 213b6c55e..5f914484a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -45,12 +45,14 @@ namespace cvc5 { namespace theory { QuantifiersEngine::QuantifiersEngine( + Env& env, quantifiers::QuantifiersState& qs, quantifiers::QuantifiersRegistry& qr, quantifiers::TermRegistry& tr, quantifiers::QuantifiersInferenceManager& qim, ProofNodeManager* pnm) - : d_qstate(qs), + : EnvObj(env), + d_qstate(qs), d_qim(qim), d_te(nullptr), d_pnm(pnm), @@ -74,12 +76,12 @@ QuantifiersEngine::QuantifiersEngine( { Trace("quant-init-debug") << "...make fmc builder." << std::endl; d_builder.reset( - new quantifiers::fmcheck::FullModelChecker(qs, qim, qr, tr)); + new quantifiers::fmcheck::FullModelChecker(env, qs, qim, qr, tr)); } else { Trace("quant-init-debug") << "...make default model builder." << std::endl; - d_builder.reset(new quantifiers::QModelBuilder(qs, qim, qr, tr)); + d_builder.reset(new quantifiers::QModelBuilder(env, qs, qim, qr, tr)); } // set the model object d_builder->finishInit(); @@ -111,9 +113,9 @@ void QuantifiersEngine::finishInit(TheoryEngine* te) d_model->finishInit(te->getModel()); d_te = te; // Initialize the modules and the utilities here. - d_qmodules.reset(new quantifiers::QuantifiersModules); + d_qmodules.reset(new quantifiers::QuantifiersModules()); d_qmodules->initialize( - d_qstate, d_qim, d_qreg, d_treg, d_builder.get(), d_modules); + d_env, d_qstate, d_qim, d_qreg, d_treg, d_builder.get(), d_modules); if (d_qmodules->d_rel_dom.get()) { d_util.push_back(d_qmodules->d_rel_dom.get()); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 23b6d9708..e8c385fcd 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -24,6 +24,7 @@ #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdlist.h" +#include "smt/env_obj.h" #include "theory/quantifiers/quant_util.h" namespace cvc5 { @@ -51,14 +52,18 @@ class TermEnumeration; class TermRegistry; } -// TODO: organize this more/review this, github issue #1163 -class QuantifiersEngine { +/** + * The main class that manages techniques for quantified formulas. + */ +class QuantifiersEngine : protected EnvObj +{ friend class ::cvc5::TheoryEngine; typedef context::CDHashMap<Node, bool> BoolMap; typedef context::CDHashSet<Node> NodeSet; public: - QuantifiersEngine(quantifiers::QuantifiersState& qstate, + QuantifiersEngine(Env& env, + quantifiers::QuantifiersState& qstate, quantifiers::QuantifiersRegistry& qr, quantifiers::TermRegistry& tr, quantifiers::QuantifiersInferenceManager& qim, @@ -208,7 +213,7 @@ public: std::map<Node, Node> d_quants_red_lem; /** Number of rounds we have instantiated */ uint32_t d_numInstRoundsLemma; -};/* class QuantifiersEngine */ +}; /* class QuantifiersEngine */ } // namespace theory } // namespace cvc5 diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 5c4cc5536..460813084 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -92,10 +92,6 @@ struct RewriteStackElement { NodeBuilder d_builder; }; -RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n) -{ - return RewriteResponse(REWRITE_DONE, n); -} Node Rewriter::rewrite(TNode node) { if (node.getNumChildren() == 0) @@ -107,6 +103,17 @@ Node Rewriter::rewrite(TNode node) { return getInstance()->rewriteTo(theoryOf(node), node); } +Node Rewriter::callExtendedRewrite(TNode node, bool aggr) +{ + return getInstance()->extendedRewrite(node, aggr); +} + +Node Rewriter::extendedRewrite(TNode node, bool aggr) +{ + quantifiers::ExtendedRewriter er(*this, aggr); + return er.extendedRewrite(node); +} + TrustNode Rewriter::rewriteWithProof(TNode node, bool isExtEq) { @@ -480,8 +487,7 @@ Node Rewriter::rewriteViaMethod(TNode n, MethodId idr) } if (idr == MethodId::RW_EXT_REWRITE) { - quantifiers::ExtendedRewriter er; - return er.extendedRewrite(n); + return extendedRewrite(n); } if (idr == MethodId::RW_REWRITE_EQ_EXT) { diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 63628b0af..d87043a67 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -29,41 +29,25 @@ class TrustNode; namespace theory { -namespace builtin { -class BuiltinProofRuleChecker; -} - -/** - * The rewrite environment holds everything that the individual rewrites have - * access to. - */ -class RewriteEnvironment -{ -}; - -/** - * The identity rewrite just returns the original node. - * - * @param re The rewrite environment - * @param n The node to rewrite - * @return The original node - */ -RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n); - /** * The main rewriter class. */ class Rewriter { - friend builtin::BuiltinProofRuleChecker; public: Rewriter(); /** + * !!! Temporary until static access to rewriter is eliminated. + * * Rewrites the node using theoryOf() to determine which rewriter to * use on the node. */ static Node rewrite(TNode node); + /** + * !!! Temporary until static access to rewriter is eliminated. + */ + static Node callExtendedRewrite(TNode node, bool aggr = true); /** * Rewrites the equality node using theoryOf() to determine which rewriter to @@ -78,6 +62,16 @@ class Rewriter { Node rewriteEqualityExt(TNode node); /** + * Extended rewrite of the given node. This method is implemented by a + * custom ExtendRewriter class that wraps this class to perform custom + * rewrites (usually those that are not useful for solving, but e.g. useful + * for SyGuS symmetry breaking). + * @param node The node to rewrite + * @param aggr Whether to perform aggressive rewrites. + */ + Node extendedRewrite(TNode node, bool aggr = true); + + /** * Rewrite with proof production, which is managed by the term conversion * proof generator managed by this class (d_tpg). This method requires a call * to setProofNodeManager prior to this call. @@ -174,8 +168,6 @@ class Rewriter { /** Theory rewriters used by this rewriter instance */ TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST]; - RewriteEnvironment d_re; - /** The proof generator */ std::unique_ptr<TConvProofGenerator> d_tpg; #ifdef CVC5_ASSERTIONS diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index 9162fdeb6..574aa9355 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -46,10 +46,6 @@ class TheoryState : protected EnvObj context::Context* getSatContext() const; /** Get the user context */ context::UserContext* getUserContext() const; - /** Get the environment */ - Env& getEnv() const { return d_env; } - /** Get the options */ - const Options& options() const { return getEnv().getOptions(); } //-------------------------------------- equality information /** Is t registered as a term in the equality engine of this class? */ virtual bool hasTerm(TNode a) const; |