diff options
Diffstat (limited to 'src')
113 files changed, 3187 insertions, 1245 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b6bf49ed8..9eb7ec3c4 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -159,6 +159,8 @@ libcvc5_add_sources( proof/lazy_proof_chain.h proof/lazy_tree_proof_generator.cpp proof/lazy_tree_proof_generator.h + proof/lfsc/lfsc_util.cpp + proof/lfsc/lfsc_util.h proof/method_id.cpp proof/method_id.h proof/proof.cpp @@ -169,6 +171,8 @@ libcvc5_add_sources( proof/proof_ensure_closed.h proof/proof_generator.cpp proof/proof_generator.h + proof/proof_letify.cpp + proof/proof_letify.h proof/proof_node.cpp proof/proof_node.h proof/proof_node_algorithm.cpp @@ -662,6 +666,8 @@ libcvc5_add_sources( theory/decision_strategy.h theory/ee_manager.cpp theory/ee_manager.h + theory/ee_manager_central.cpp + theory/ee_manager_central.h theory/ee_manager_distributed.cpp theory/ee_manager_distributed.h theory/ee_setup_info.h @@ -855,6 +861,7 @@ libcvc5_add_sources( theory/quantifiers/sygus/cegis_core_connective.h theory/quantifiers/sygus/cegis_unif.cpp theory/quantifiers/sygus/cegis_unif.h + theory/quantifiers/sygus/enum_val_generator.h theory/quantifiers/sygus/example_eval_cache.cpp theory/quantifiers/sygus/example_eval_cache.h theory/quantifiers/sygus/example_infer.cpp @@ -877,6 +884,8 @@ libcvc5_add_sources( theory/quantifiers/sygus/sygus_enumerator.h theory/quantifiers/sygus/sygus_enumerator_basic.cpp theory/quantifiers/sygus/sygus_enumerator_basic.h + theory/quantifiers/sygus/sygus_enumerator_callback.cpp + theory/quantifiers/sygus/sygus_enumerator_callback.h theory/quantifiers/sygus/sygus_eval_unfold.cpp theory/quantifiers/sygus/sygus_eval_unfold.h theory/quantifiers/sygus/sygus_explain.cpp diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 4e14b8e34..9b920b875 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -570,6 +570,7 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction> {cvc5::Kind::APPLY_UPDATER, APPLY_UPDATER}, {cvc5::Kind::DT_SIZE, DT_SIZE}, {cvc5::Kind::TUPLE_PROJECT, TUPLE_PROJECT}, + {cvc5::Kind::TUPLE_PROJECT_OP, TUPLE_PROJECT}, /* Separation Logic ------------------------------------------------ */ {cvc5::Kind::SEP_NIL, SEP_NIL}, {cvc5::Kind::SEP_EMP, SEP_EMP}, @@ -1865,6 +1866,14 @@ size_t Op::getNumIndices() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return getNumIndicesHelper(); + //////// + CVC5_API_TRY_CATCH_END; +} + +size_t Op::getNumIndicesHelper() const +{ if (!isIndexedHelper()) { return 0; @@ -1898,9 +1907,185 @@ size_t Op::getNumIndices() const break; default: CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k); } + return size; +} + +Term Op::operator[](size_t index) const +{ + return getIndexHelper(index); +} + +Term Op::getIndexHelper(size_t index) const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_CHECK(!d_node->isNull()) + << "Expecting a non-null internal expression. This Op is not indexed."; + CVC5_API_CHECK(index < getNumIndicesHelper()) << "index out of bound"; + Kind k = intToExtKind(d_node->getKind()); + Term t; + switch (k) + { + case DIVISIBLE: + { + t = d_solver->mkValHelper<Rational>( + Rational(d_node->getConst<Divisible>().k)); + break; + } + case BITVECTOR_REPEAT: + { + t = d_solver->mkValHelper<cvc5::Rational>( + d_node->getConst<BitVectorRepeat>().d_repeatAmount); + break; + } + case BITVECTOR_ZERO_EXTEND: + { + t = d_solver->mkValHelper<cvc5::Rational>( + d_node->getConst<BitVectorZeroExtend>().d_zeroExtendAmount); + break; + } + case BITVECTOR_SIGN_EXTEND: + { + t = d_solver->mkValHelper<cvc5::Rational>( + d_node->getConst<BitVectorSignExtend>().d_signExtendAmount); + break; + } + case BITVECTOR_ROTATE_LEFT: + { + t = d_solver->mkValHelper<cvc5::Rational>( + d_node->getConst<BitVectorRotateLeft>().d_rotateLeftAmount); + break; + } + case BITVECTOR_ROTATE_RIGHT: + { + t = d_solver->mkValHelper<cvc5::Rational>( + d_node->getConst<BitVectorRotateRight>().d_rotateRightAmount); + break; + } + case INT_TO_BITVECTOR: + { + t = d_solver->mkValHelper<cvc5::Rational>( + d_node->getConst<IntToBitVector>().d_size); + break; + } + case IAND: + { + t = d_solver->mkValHelper<cvc5::Rational>( + d_node->getConst<IntAnd>().d_size); + break; + } + case FLOATINGPOINT_TO_UBV: + { + t = d_solver->mkValHelper<cvc5::Rational>( + d_node->getConst<FloatingPointToUBV>().d_bv_size.d_size); + break; + } + case FLOATINGPOINT_TO_SBV: + { + t = d_solver->mkValHelper<cvc5::Rational>( + d_node->getConst<FloatingPointToSBV>().d_bv_size.d_size); + break; + } + case REGEXP_REPEAT: + { + t = d_solver->mkValHelper<cvc5::Rational>( + d_node->getConst<RegExpRepeat>().d_repeatAmount); + break; + } + case BITVECTOR_EXTRACT: + { + cvc5::BitVectorExtract ext = d_node->getConst<BitVectorExtract>(); + t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(ext.d_high) + : d_solver->mkValHelper<cvc5::Rational>(ext.d_low); + break; + } + case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: + { + cvc5::FloatingPointToFPIEEEBitVector ext = + d_node->getConst<FloatingPointToFPIEEEBitVector>(); + + t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>( + ext.getSize().exponentWidth()) + : d_solver->mkValHelper<cvc5::Rational>( + ext.getSize().significandWidth()); + break; + } + case FLOATINGPOINT_TO_FP_FLOATINGPOINT: + { + cvc5::FloatingPointToFPFloatingPoint ext = + d_node->getConst<FloatingPointToFPFloatingPoint>(); + t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>( + ext.getSize().exponentWidth()) + : d_solver->mkValHelper<cvc5::Rational>( + ext.getSize().significandWidth()); + break; + } + case FLOATINGPOINT_TO_FP_REAL: + { + cvc5::FloatingPointToFPReal ext = + d_node->getConst<FloatingPointToFPReal>(); + + t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>( + ext.getSize().exponentWidth()) + : d_solver->mkValHelper<cvc5::Rational>( + ext.getSize().significandWidth()); + break; + } + case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + { + cvc5::FloatingPointToFPSignedBitVector ext = + d_node->getConst<FloatingPointToFPSignedBitVector>(); + t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>( + ext.getSize().exponentWidth()) + : d_solver->mkValHelper<cvc5::Rational>( + ext.getSize().significandWidth()); + break; + } + case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: + { + cvc5::FloatingPointToFPUnsignedBitVector ext = + d_node->getConst<FloatingPointToFPUnsignedBitVector>(); + t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>( + ext.getSize().exponentWidth()) + : d_solver->mkValHelper<cvc5::Rational>( + ext.getSize().significandWidth()); + break; + } + case FLOATINGPOINT_TO_FP_GENERIC: + { + cvc5::FloatingPointToFPGeneric ext = + d_node->getConst<FloatingPointToFPGeneric>(); + t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>( + ext.getSize().exponentWidth()) + : d_solver->mkValHelper<cvc5::Rational>( + ext.getSize().significandWidth()); + break; + } + case REGEXP_LOOP: + { + cvc5::RegExpLoop ext = d_node->getConst<RegExpLoop>(); + t = index == 0 ? d_solver->mkValHelper<cvc5::Rational>(ext.d_loopMinOcc) + : d_solver->mkValHelper<cvc5::Rational>(ext.d_loopMaxOcc); + + break; + } + + case TUPLE_PROJECT: + { + const std::vector<uint32_t>& projectionIndices = + d_node->getConst<TupleProjectOp>().getIndices(); + t = d_solver->mkValHelper<cvc5::Rational>(projectionIndices[index]); + break; + } + default: + { + CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k); + break; + } + } //////// all checks before this line - return size; + return t; //////// CVC5_API_TRY_CATCH_END; } @@ -2043,6 +2228,25 @@ std::pair<uint32_t, uint32_t> Op::getIndices() const CVC5_API_TRY_CATCH_END; } +template <> +std::vector<api::Term> Op::getIndices() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_CHECK(!d_node->isNull()) + << "Expecting a non-null internal expression. This Op is not indexed."; + size_t size = getNumIndicesHelper(); + std::vector<Term> terms(getNumIndices()); + for (size_t i = 0; i < size; i++) + { + terms[i] = getIndexHelper(i); + } + //////// all checks before this line + return terms; + //////// + CVC5_API_TRY_CATCH_END; +} + std::string Op::toString() const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 0ee5990da..672ccf8f8 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -782,6 +782,8 @@ namespace cvc5::api { /* Op */ /* -------------------------------------------------------------------------- */ +class Term; + /** * A cvc5 operator. * An operator is a term that represents certain operators, instantiated @@ -843,6 +845,14 @@ class CVC5_EXPORT Op size_t getNumIndices() const; /** + * Get the index at position i. + * @param i the position of the index to return + * @return the index at position i + */ + + Term operator[](size_t i) const; + + /** * Get the indices used to create this Op. * Supports the following template arguments: * - string @@ -892,6 +902,19 @@ class CVC5_EXPORT Op bool isIndexedHelper() const; /** + * Helper for getNumIndices + * @return the number of indices of this op + */ + size_t getNumIndicesHelper() const; + + /** + * Helper for operator[](size_t i). + * @param i position of the index. Should be less than getNumIndicesHelper(). + * @return the index at position i + */ + Term getIndexHelper(size_t index) const; + + /** * The associated solver object. */ const Solver* d_solver; diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h index b619a36e2..507cebab3 100644 --- a/src/expr/bound_var_manager.h +++ b/src/expr/bound_var_manager.h @@ -77,7 +77,7 @@ class BoundVarManager Node mkBoundVar(Node n, const std::string& name, TypeNode tn) { Node v = mkBoundVar<T>(n, tn); - setNameAttr(n, name); + setNameAttr(v, name); return v; } //---------------------------------- utilities for computing Node hash diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 9d221450b..8c86f03cb 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -35,6 +35,7 @@ #include "main/time_limit.h" #include "options/base_options.h" #include "options/options.h" +#include "options/options_public.h" #include "options/parser_options.h" #include "options/main_options.h" #include "options/set_language.h" @@ -87,9 +88,9 @@ void printUsage(const Options& opts, bool full) { << endl << "cvc5 options:" << endl; if(full) { - Options::printUsage(ss.str(), *opts.base.out); + options::printUsage(ss.str(), *opts.base.out); } else { - Options::printShortUsage(ss.str(), *opts.base.out); + options::printShortUsage(ss.str(), *opts.base.out); } } @@ -103,8 +104,7 @@ int runCvc5(int argc, char* argv[], Options& opts) progPath = argv[0]; // Parse the options - std::vector<string> filenames = - Options::parseOptions(&opts, argc, argv, progName); + std::vector<string> filenames = options::parse(opts, argc, argv, progName); auto limit = install_time_limit(opts); @@ -115,7 +115,7 @@ int runCvc5(int argc, char* argv[], Options& opts) } else if (opts.base.languageHelp) { - Options::printLanguageHelp(*opts.base.out); + options::printLanguageHelp(*opts.base.out); exit(1); } else if (opts.driver.version) diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 926693185..a548717f3 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -29,7 +29,6 @@ libcvc5_add_sources( options_handler.cpp options_handler.h options_listener.h - options_public.cpp options_public.h outputc.cpp outputc.h @@ -67,7 +66,7 @@ set(options_toml_files string(REPLACE "toml" "cpp;" options_gen_cpp_files ${options_toml_files}) string(REPLACE "toml" "h;" options_gen_h_files ${options_toml_files}) -libcvc5_add_sources(GENERATED options.h options.cpp ${options_gen_cpp_files}) +libcvc5_add_sources(GENERATED options.h options.cpp options_public.cpp ${options_gen_cpp_files}) list_prepend(options_toml_files "${CMAKE_CURRENT_LIST_DIR}/" abs_toml_files) @@ -82,7 +81,7 @@ endif() add_custom_command( OUTPUT - options.h options.cpp + options.h options.cpp options_public.cpp ${options_gen_cpp_files} ${options_gen_h_files} ${options_gen_doc_files} COMMAND @@ -97,6 +96,7 @@ add_custom_command( ${options_toml_files} module_template.h module_template.cpp + options_public_template.cpp options_template.h options_template.cpp ) @@ -105,6 +105,7 @@ add_custom_target(gen-options DEPENDS options.h options.cpp + options_public.cpp ${options_gen_cpp_files} ${options_gen_h_files} ) diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 8766672a5..26b1cfecb 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -595,3 +595,11 @@ name = "Arithmetic Theory" type = "bool" default = "false" help = "whether to use the equality solver in the theory of arithmetic" + +[[option]] + name = "arithCongMan" + category = "regular" + long = "arith-cong-man" + type = "bool" + default = "true" + help = "(experimental) whether to use the congruence manager when the equality solver is enabled" diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 2223664d1..a766dce67 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -7,21 +7,21 @@ public = true category = "undocumented" type = "std::istream*" default = "&std::cin" - includes = ["<iosfwd>"] + includes = ["<iostream>"] [[option]] name = "out" category = "undocumented" type = "std::ostream*" default = "&std::cout" - includes = ["<iosfwd>"] + includes = ["<iostream>"] [[option]] name = "err" category = "undocumented" type = "std::ostream*" default = "&std::cerr" - includes = ["<iosfwd>"] + includes = ["<iostream>"] [[option]] name = "inputLanguage" diff --git a/src/options/fp_options.toml b/src/options/fp_options.toml index 6fd632a7c..be40b49e2 100644 --- a/src/options/fp_options.toml +++ b/src/options/fp_options.toml @@ -8,3 +8,11 @@ name = "Floating-Point" type = "bool" default = "false" help = "Allow floating-point sorts of all sizes, rather than only Float32 (8/24) or Float64 (11/53) (experimental)" + +[[option]] + name = "fpLazyWb" + category = "experimental" + long = "fp-lazy-wb" + type = "bool" + default = "false" + help = "Enable lazier word-blasting (on preNotifyFact instead of registerTerm)" diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 45b1db4d6..aeff832b5 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -27,6 +27,7 @@ Directory <tpl-src> must contain: - options_template.cpp + - options_public_template.cpp - module_template.cpp - module_template.h @@ -183,6 +184,11 @@ def concat_format(s, objs): return '\n'.join([s.format(**o.__dict__) for o in objs]) +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) @@ -237,6 +243,19 @@ def get_predicates(option): return ['opts.handler().{}("{}", option, value);'.format(x, optname) for x in option.predicates] + +def get_getall(module, option): + """Render snippet to add option to result of getAll()""" + if option.type == 'bool': + return 'res.push_back({{"{}", opts.{}.{} ? "true" : "false"}});'.format( + option.long_name, module.id, option.name) + elif is_numeric_cpp_type(option.type): + return 'res.push_back({{"{}", std::to_string(opts.{}.{})}});'.format( + option.long_name, module.id, option.name) + else: + return '{{ std::stringstream ss; ss << opts.{}.{}; res.push_back({{"{}", ss.str()}}); }}'.format( + module.id, option.name, option.long_name) + class Module(object): """Options module. @@ -705,25 +724,26 @@ def add_getopt_long(long_name, argument_req, getopt_long): 'required' if argument_req else 'no', value)) -def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_cpp): +def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, + tpl_options_cpp, tpl_options_public): """ - Generate code for all option modules (options.cpp, options_holder.h). + Generate code for all option modules (options.cpp). """ 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_smt = [] # all options names accessible via {set,get}-option + options_getall = [] # options for options::getAll() options_getoptions = [] # options for Options::getOptions() options_handler = [] # option handler calls - defaults = [] # default values - custom_handlers = [] # custom handler implementations assign/assignBool help_common = [] # help text for all common options help_others = [] # help text for all non-common options setoption_handlers = [] # handlers for set-option command getoption_handlers = [] # handlers for get-option command + assign_impls = [] + sphinxgen = SphinxGenerator() for module in modules: @@ -809,7 +829,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ cond = ' || '.join( ['key == "{}"'.format(x) for x in sorted(keys)]) - setoption_handlers.append('if({}) {{'.format(cond)) + setoption_handlers.append(' if ({}) {{'.format(cond)) if option.type == 'bool': setoption_handlers.append( TPL_CALL_ASSIGN_BOOL.format( @@ -824,15 +844,15 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ name=option.name, option='key')) elif option.handler: - h = 'handler->{handler}("{smtname}", key' + h = ' opts.handler().{handler}("{smtname}", key' if argument_req: h += ', optionarg' h += ');' setoption_handlers.append( h.format(handler=option.handler, smtname=option.long_name)) - setoption_handlers.append('return;') - setoption_handlers.append('}') + setoption_handlers.append(' return;') + setoption_handlers.append(' }') if option.name: getoption_handlers.append( @@ -880,80 +900,51 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ cases.append(' break;') options_handler.extend(cases) - optname = option.long - # collect options available to the SMT-frontend - if optname: - options_smt.append('"{}",'.format(optname)) - if option.name: # Build options for options::getOptions() - if optname: - # collect SMT option names - options_smt.append('"{}",'.format(optname)) - - if option.type == 'bool': - s = 'opts.push_back({{"{}", {}.{} ? "true" : "false"}});'.format( - optname, module.id, option.name) - elif is_numeric_cpp_type(option.type): - s = 'opts.push_back({{"{}", std::to_string({}.{})}});'.format( - optname, module.id, option.name) - else: - s = '{{ std::stringstream ss; ss << {}.{}; opts.push_back({{"{}", ss.str()}}); }}'.format( - module.id, option.name, optname) - options_getoptions.append(s) + if option.long_name: + options_getall.append(get_getall(module, option)) # Define handler assign/assignBool if not mode_handler: if option.type == 'bool': - custom_handlers.append(TPL_ASSIGN_BOOL.format( + assign_impls.append(TPL_ASSIGN_BOOL.format( module=module.id, name=option.name, handler=handler, predicates='\n'.join(predicates) )) elif option.short or option.long: - custom_handlers.append(TPL_ASSIGN.format( + assign_impls.append(TPL_ASSIGN.format( module=module.id, name=option.name, handler=handler, predicates='\n'.join(predicates) )) - # Default option values - default = option.default if option.default else '' - # Prepend enum name - if option.mode and option.type not in default: - default = '{}::{}'.format(option.type, default) - defaults.append('{}({})'.format(option.name, default)) - defaults.append('{}WasSetByUser(false)'.format(option.name)) - - write_file(dst_dir, 'options.h', tpl_options_h.format( - holder_fwd_decls=get_holder_fwd_decls(modules), - holder_mem_decls=get_holder_mem_decls(modules), - holder_ref_decls=get_holder_ref_decls(modules), - )) - - write_file(dst_dir, 'options.cpp', tpl_options_cpp.format( - headers_module='\n'.join(headers_module), - headers_handler='\n'.join(sorted(list(headers_handler))), - holder_mem_copy=get_holder_mem_copy(modules), - holder_mem_inits=get_holder_mem_inits(modules), - holder_ref_inits=get_holder_ref_inits(modules), - custom_handlers='\n'.join(custom_handlers), - module_defaults=',\n '.join(defaults), - help_common='\n'.join(help_common), - help_others='\n'.join(help_others), - cmdline_options='\n '.join(getopt_long), - options_short=''.join(getopt_short), - options_handler='\n '.join(options_handler), - option_value_begin=g_getopt_long_start, - option_value_end=g_getopt_long_start + len(getopt_long), - options_smt='\n '.join(options_smt), - options_getoptions='\n '.join(options_getoptions), - setoption_handlers='\n'.join(setoption_handlers), - getoption_handlers='\n'.join(getoption_handlers) - )) + 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), + 'cmdline_options': '\n '.join(getopt_long), + 'help_common': '\n'.join(help_common), + 'help_others': '\n'.join(help_others), + 'options_handler': '\n '.join(options_handler), + 'options_short': ''.join(getopt_short), + 'assigns': '\n'.join(assign_impls), + 'options_getall': '\n '.join(options_getall), + 'getoption_handlers': '\n'.join(getoption_handlers), + 'setoption_handlers': '\n'.join(setoption_handlers), + } + write_file(dst_dir, 'options.h', tpl_options_h.format(**data)) + write_file(dst_dir, 'options.cpp', tpl_options_cpp.format(**data)) + write_file(dst_dir, 'options_public.cpp', tpl_options_public.format(**data)) if os.path.isdir('{}/docs/'.format(build_dir)): sphinxgen.render('{}/docs/'.format(build_dir), 'options_generated.rst') @@ -1093,6 +1084,7 @@ def mkoptions_main(): # Read source code template files from source directory. tpl_module_h = read_tpl(src_dir, 'module_template.h') tpl_module_cpp = read_tpl(src_dir, 'module_template.cpp') + tpl_options_public = read_tpl(src_dir, 'options_public_template.cpp') tpl_options_h = read_tpl(src_dir, 'options_template.h') tpl_options_cpp = read_tpl(src_dir, 'options_template.cpp') @@ -1113,8 +1105,7 @@ def mkoptions_main(): codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp) # Create options.cpp in destination directory - codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_cpp) - + codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_cpp, tpl_options_public) if __name__ == "__main__": diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index e423dc149..7a80c4d7a 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -155,11 +155,11 @@ void OptionsHandler::checkBvSatSolver(const std::string& option, throw OptionException(ss.str()); } - if (options::bvSolver() != options::BVSolver::BITBLAST + if (d_options->bv.bvSolver != options::BVSolver::BITBLAST && (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL || m == SatSolverMode::KISSAT)) { - if (options::bitblastMode() == options::BitblastMode::LAZY + if (d_options->bv.bitblastMode == options::BitblastMode::LAZY && d_options->bv.bitblastModeWasSetByUser) { throwLazyBBUnsupported(m); @@ -178,9 +178,9 @@ void OptionsHandler::checkBitblastMode(const std::string& option, options::bv::setDefaultBitvectorEqualitySolver(*d_options, true); options::bv::setDefaultBitvectorInequalitySolver(*d_options, true); options::bv::setDefaultBitvectorAlgebraicSolver(*d_options, true); - if (options::bvSatSolver() != options::SatSolverMode::MINISAT) + if (d_options->bv.bvSatSolver != options::SatSolverMode::MINISAT) { - throwLazyBBUnsupported(options::bvSatSolver()); + throwLazyBBUnsupported(d_options->bv.bvSatSolver); } } else if (m == BitblastMode::EAGER) @@ -195,7 +195,7 @@ void OptionsHandler::setBitblastAig(const std::string& option, { if(arg) { if (d_options->bv.bitblastModeWasSetByUser) { - if (options::bitblastMode() != options::BitblastMode::EAGER) + if (d_options->bv.bitblastMode != options::BitblastMode::EAGER) { throw OptionException("bitblast-aig must be used with eager bitblaster"); } diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp deleted file mode 100644 index 552058312..000000000 --- a/src/options/options_public.cpp +++ /dev/null @@ -1,26 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Tim King, Gereon Kremer, 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. - * **************************************************************************** - * - * Definitions of public facing interface functions for Options. - * - * These are all one line wrappers for accessing the internal option data. - */ - -#include "options_public.h" - -#include "options/uf_options.h" - -namespace cvc5::options { - -bool getUfHo(const Options& opts) { return opts.uf.ufHo; } - -} // namespace cvc5::options diff --git a/src/options/options_public.h b/src/options/options_public.h index 60929c96c..03d7ec41a 100644 --- a/src/options/options_public.h +++ b/src/options/options_public.h @@ -10,12 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Public facing functions for options that need to be accessed from the - * outside. - * - * These are all one line wrappers for accessing the internal option data so - * that external code (including parser/ and main/) does not need to include - * the option modules (*_options.h). + * Global (command-line, set-option, ...) parameters for SMT. */ #include "cvc5_public.h" @@ -23,12 +18,77 @@ #ifndef CVC5__OPTIONS__OPTIONS_PUBLIC_H #define CVC5__OPTIONS__OPTIONS_PUBLIC_H +#include <iosfwd> +#include <string> +#include <vector> + +#include "cvc5_export.h" #include "options/options.h" namespace cvc5::options { bool getUfHo(const Options& opts) CVC5_EXPORT; +/** + * Get a description of the command-line flags accepted by + * parse. The returned string will be escaped so that it is + * suitable as an argument to printf. */ +const std::string& getDescription() CVC5_EXPORT; + +/** + * Print overall command-line option usage message, prefixed by + * "msg"---which could be an error message causing the usage + * output in the first place, e.g. "no such option --foo" + */ +void printUsage(const std::string& msg, std::ostream& os) CVC5_EXPORT; + +/** + * Print command-line option usage message for only the most-commonly + * used options. The message is prefixed by "msg"---which could be + * an error message causing the usage output in the first place, e.g. + * "no such option --foo" + */ +void printShortUsage(const std::string& msg, std::ostream& os) CVC5_EXPORT; + +/** Print help for the --lang command line option */ +void printLanguageHelp(std::ostream& os) CVC5_EXPORT; + +/** + * Initialize the Options object options based on the given + * command-line arguments given in argc and argv. The return value + * is what's left of the command line (that is, the non-option + * arguments). + * + * This function uses getopt_long() and is not thread safe. + * + * Throws OptionException on failures. + * + * Preconditions: options and argv must be non-null. + */ +std::vector<std::string> parse(Options& opts, + int argc, + char* argv[], + std::string& binaryName) CVC5_EXPORT; + +/** + * Retrieve an option value by name (as given in key) from the Options object + * opts as a string. + */ +std::string get(const Options& opts, const std::string& key) CVC5_EXPORT; + +/** + * Update the Options object opts, set the value of the option specified by key + * to the value parsed from optionarg. + */ +void set(Options& opts, + const std::string& key, + const std::string& optionarg) CVC5_EXPORT; + +/** + * Get the setting for all options. + */ +std::vector<std::vector<std::string> > getAll(const Options& opts) CVC5_EXPORT; + } // namespace cvc5::options #endif diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp new file mode 100644 index 000000000..70c6f420a --- /dev/null +++ b/src/options/options_public_template.cpp @@ -0,0 +1,496 @@ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Gereon Kremer, 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. + * **************************************************************************** + * + * Global (command-line, set-option, ...) parameters for SMT. + */ + +#include "options/options_public.h" + +#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__) +// force use of optreset; mingw32 croaks on argv-switching otherwise +#include "base/cvc5config.h" +#define _BSD_SOURCE +#undef HAVE_DECL_OPTRESET +#define HAVE_DECL_OPTRESET 1 +#define CVC5_IS_NOT_REALLY_BSD +#endif /* !_BSD_SOURCE && __MINGW32__ && !__MINGW64__ */ + +#ifdef __MINGW64__ +extern int optreset; +#endif /* __MINGW64__ */ + +#include <getopt.h> + +// clean up +#ifdef CVC5_IS_NOT_REALLY_BSD +# undef _BSD_SOURCE +#endif /* CVC5_IS_NOT_REALLY_BSD */ + +#include "base/check.h" +#include "base/output.h" +#include "options/didyoumean.h" +#include "options/options_handler.h" +#include "options/options_listener.h" +#include "options/options.h" +#include "options/uf_options.h" +${headers_module}$ +${headers_handler}$ + +#include <cstring> +#include <iostream> +#include <limits> + +namespace cvc5::options { + +bool getUfHo(const Options& opts) { return opts.uf.ufHo; } + +// clang-format off +static const std::string mostCommonOptionsDescription = + "\ +Most commonly-used cvc5 options:\n" +${help_common}$ + ; + +static const std::string optionsDescription = + mostCommonOptionsDescription + "\n\nAdditional cvc5 options:\n" +${help_others}$; + +static const std::string optionsFootnote = "\n\ +[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\ + sense of the option.\n\ +"; + +static const std::string languageDescription = + "\ +Languages currently supported as arguments to the -L / --lang option:\n\ + auto attempt to automatically determine language\n\ + cvc | presentation | pl CVC presentation language\n\ + smt | smtlib | smt2 |\n\ + smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ + tptp TPTP format (cnf, fof and tff)\n\ + sygus | sygus2 SyGuS version 2.0\n\ +\n\ +Languages currently supported as arguments to the --output-lang option:\n\ + auto match output language to input language\n\ + cvc | presentation | pl CVC presentation language\n\ + smt | smtlib | smt2 |\n\ + smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ + tptp TPTP format\n\ + ast internal format (simple syntax trees)\n\ +"; +// clang-format on + +const std::string& getDescription() +{ + return optionsDescription; +} + +void printUsage(const std::string& msg, std::ostream& os) { + os << msg << optionsDescription << std::endl + << optionsFootnote << std::endl << std::flush; +} + +void printShortUsage(const std::string& msg, std::ostream& os) { + os << msg << mostCommonOptionsDescription << std::endl + << optionsFootnote << std::endl + << "For full usage, please use --help." + << std::endl << std::endl << std::flush; +} + +void printLanguageHelp(std::ostream& os) { + os << languageDescription << std::flush; +} + +/** Set a given Options* as "current" just for a particular scope. */ +class OptionsGuard { + Options** d_field; + Options* d_old; +public: + OptionsGuard(Options** field, Options* opts) : + d_field(field), + d_old(*field) { + *field = opts; + } + ~OptionsGuard() { + *d_field = d_old; + } +};/* class OptionsGuard */ + +/** + * This is a table of long options. By policy, each short option + * should have an equivalent long option (but the reverse isn't the + * case), so this table should thus contain all command-line options. + * + * Each option in this array has four elements: + * + * 1. the long option string + * 2. argument behavior for the option: + * no_argument - no argument permitted + * required_argument - an argument is expected + * optional_argument - an argument is permitted but not required + * 3. this is a pointer to an int which is set to the 4th entry of the + * array if the option is present; or NULL, in which case + * getopt_long() returns the 4th entry + * 4. the return value for getopt_long() when this long option (or the + * value to set the 3rd entry to; see #3) + * + * If you add something here, you should add it in src/main/usage.h + * also, to document it. + * + * If you add something that has a short option equivalent, you should + * add it to the getopt_long() call in parse(). + */ +// clang-format off +static struct option cmdlineOptions[] = { + ${cmdline_options}$ + {nullptr, no_argument, nullptr, '\0'}}; +// clang-format on + +std::string suggestCommandLineOptions(const std::string& optionName) +{ + DidYouMean didYouMean; + + const char* opt; + for(size_t i = 0; (opt = cmdlineOptions[i].name) != nullptr; ++i) { + didYouMean.addWord(std::string("--") + cmdlineOptions[i].name); + } + + return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('='))); +} + +/** + * This is a default handler for options of built-in C++ type. This + * template is really just a helper for the handleOption() template, + * below. Variants of this template handle numeric and non-numeric, + * integral and non-integral, signed and unsigned C++ types. + * handleOption() makes sure to instantiate the right one. + * + * This implements default behavior when e.g. an option is + * unsigned but the user specifies a negative argument; etc. + */ +template <class T, bool is_numeric, bool is_integer> +struct OptionHandler { + static T handle(const std::string& option, const std::string& flag, const std::string& optionarg); +};/* struct OptionHandler<> */ + +/** Variant for integral C++ types */ +template <class T> +struct OptionHandler<T, true, true> { + static bool stringToInt(T& t, const std::string& str) { + std::istringstream ss(str); + ss >> t; + char tmp; + return !(ss.fail() || ss.get(tmp)); + } + + static bool containsMinus(const std::string& str) { + return str.find('-') != std::string::npos; + } + + static T handle(const std::string& option, const std::string& flag, const std::string& optionarg) { + try { + T i; + bool success = stringToInt(i, optionarg); + + if(!success){ + throw OptionException(flag + ": failed to parse "+ optionarg + + " as an integer of the appropriate type."); + } + + // Depending in the platform unsigned numbers with '-' signs may parse. + // Reject these by looking for any minus if it is not signed. + if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) { + // unsigned type but user gave negative argument + throw OptionException(flag + " requires a nonnegative argument"); + } else if(i < std::numeric_limits<T>::min()) { + // negative overflow for type + std::stringstream ss; + ss << flag << " requires an argument >= " + << std::numeric_limits<T>::min(); + throw OptionException(ss.str()); + } else if(i > std::numeric_limits<T>::max()) { + // positive overflow for type + std::stringstream ss; + ss << flag << " requires an argument <= " + << std::numeric_limits<T>::max(); + throw OptionException(ss.str()); + } + + return i; + + // if(std::numeric_limits<T>::is_signed) { + // return T(i.getLong()); + // } else { + // return T(i.getUnsignedLong()); + // } + } catch(std::invalid_argument&) { + // user gave something other than an integer + throw OptionException(flag + " requires an integer argument"); + } + } +};/* struct OptionHandler<T, true, true> */ + +/** Variant for numeric but non-integral C++ types */ +template <class T> +struct OptionHandler<T, true, false> { + static T handle(const std::string& option, const std::string& flag, const std::string& optionarg) { + std::stringstream inss(optionarg); + long double r; + inss >> r; + if(! inss.eof()) { + // we didn't consume the whole string (junk at end) + throw OptionException(flag + " requires a numeric argument"); + } + + if(! std::numeric_limits<T>::is_signed && r < 0.0) { + // unsigned type but user gave negative value + throw OptionException(flag + " requires a nonnegative argument"); + } else if(r < -std::numeric_limits<T>::max()) { + // negative overflow for type + std::stringstream ss; + ss << flag << " requires an argument >= " + << -std::numeric_limits<T>::max(); + throw OptionException(ss.str()); + } else if(r > std::numeric_limits<T>::max()) { + // positive overflow for type + std::stringstream ss; + ss << flag << " requires an argument <= " + << std::numeric_limits<T>::max(); + throw OptionException(ss.str()); + } + + return T(r); + } +};/* struct OptionHandler<T, true, false> */ + +/** Variant for non-numeric C++ types */ +template <class T> +struct OptionHandler<T, false, false> { + static T handle(const std::string& option, const std::string& flag, const std::string& optionarg) { + T::unsupported_handleOption_call___please_write_me; + // The above line causes a compiler error if this version of the template + // is ever instantiated (meaning that a specialization is missing). So + // don't worry about the segfault in the next line, the "return" is only + // there to keep the compiler from giving additional, distracting errors + // and warnings. + return *(T*)0; + } +};/* struct OptionHandler<T, false, false> */ + +/** Handle an option of type T in the default way. */ +template <class T> +T handleOption(const std::string& option, const std::string& flag, const std::string& optionarg) { + return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, flag, optionarg); +} + +/** Handle an option of type std::string in the default way. */ +template <> +std::string handleOption<std::string>(const std::string& option, const std::string& flag, const std::string& optionarg) { + return optionarg; +} + +// clang-format off +${assigns}$ +// clang-format off + +void parseInternal(Options& opts, int argc, + char* argv[], + std::vector<std::string>& nonoptions) +{ + Assert(argv != nullptr); + if(Debug.isOn("options")) { + Debug("options") << "starting a new parseInternal with " + << argc << " arguments" << std::endl; + for( int i = 0; i < argc ; i++ ){ + Assert(argv[i] != NULL); + Debug("options") << " argv[" << i << "] = " << argv[i] << std::endl; + } + } + + // Reset getopt(), in the case of multiple calls to parse(). + // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. + optind = 0; +#if HAVE_DECL_OPTRESET + optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this +#endif /* HAVE_DECL_OPTRESET */ + + // We must parse the binary name, which is manually ignored below. Setting + // this to 1 leads to incorrect behavior on some platforms. + int main_optind = 0; + int old_optind; + + + while(true) { // Repeat Forever + + optopt = 0; + std::string option, optionarg; + + optind = main_optind; + old_optind = main_optind; + + // If we encounter an element that is not at zero and does not start + // with a "-", this is a non-option. We consume this element as a + // non-option. + if (main_optind > 0 && main_optind < argc && + argv[main_optind][0] != '-') { + Debug("options") << "enqueueing " << argv[main_optind] + << " as a non-option." << std::endl; + nonoptions.push_back(argv[main_optind]); + ++main_optind; + continue; + } + + + Debug("options") << "[ before, main_optind == " << main_optind << " ]" + << std::endl; + Debug("options") << "[ before, optind == " << optind << " ]" << std::endl; + Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]" + << std::endl; + // clang-format off + int c = getopt_long(argc, argv, + "+:${options_short}$", + cmdlineOptions, NULL); + // clang-format on + + main_optind = optind; + + Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]" + << "[ next option will be at pos: " << optind << " ]" + << std::endl; + + // The initial getopt_long call should always determine that argv[0] + // is not an option and returns -1. We always manually advance beyond + // this element. + if ( old_optind == 0 && c == -1 ) { + Assert(main_optind > 0); + continue; + } + + if ( c == -1 ) { + if(Debug.isOn("options")) { + Debug("options") << "done with option parsing" << std::endl; + for(int index = optind; index < argc; ++index) { + Debug("options") << "remaining " << argv[index] << std::endl; + } + } + break; + } + + option = argv[old_optind == 0 ? 1 : old_optind]; + optionarg = (optarg == NULL) ? "" : optarg; + + Debug("preemptGetopt") << "processing option " << c + << " (`" << char(c) << "'), " << option << std::endl; + + // clang-format off + switch(c) + { +${options_handler}$ + + case ':' : + // This can be a long or short option, and the way to get at the + // name of it is different. + throw OptionException(std::string("option `") + option + + "' missing its required argument"); + + case '?': + default: + throw OptionException(std::string("can't understand option `") + option + + "'" + suggestCommandLineOptions(option)); + } + } + // clang-format on + + Debug("options") << "got " << nonoptions.size() + << " non-option arguments." << std::endl; +} + +/** + * Parse argc/argv and put the result into a cvc5::Options. + * The return value is what's left of the command line (that is, the + * non-option arguments). + * + * Throws OptionException on failures. + */ +std::vector<std::string> parse( + Options & opts, int argc, char* argv[], std::string& binaryName) +{ + Assert(argv != nullptr); + + Options* cur = &Options::current(); + OptionsGuard guard(&cur, &opts); + + const char *progName = argv[0]; + + // To debug options parsing, you may prefer to simply uncomment this + // and recompile. Debug flags have not been parsed yet so these have + // not been set. + //DebugChannel.on("options"); + + Debug("options") << "options::parse == " << &opts << std::endl; + Debug("options") << "argv == " << argv << std::endl; + + // Find the base name of the program. + const char *x = strrchr(progName, '/'); + if(x != nullptr) { + progName = x + 1; + } + binaryName = std::string(progName); + + std::vector<std::string> nonoptions; + parseInternal(opts, argc, argv, nonoptions); + if (Debug.isOn("options")){ + for(std::vector<std::string>::const_iterator i = nonoptions.begin(), + iend = nonoptions.end(); i != iend; ++i){ + Debug("options") << "nonoptions " << *i << std::endl; + } + } + + return nonoptions; +} + +std::string get(const Options& options, const std::string& key) +{ + Trace("options") << "Options::getOption(" << key << ")" << std::endl; + ${getoption_handlers}$ + + throw UnrecognizedOptionException(key); +} + +void setInternal(Options& opts, const std::string& key, + const std::string& optionarg) + { + ${setoption_handlers}$ + throw UnrecognizedOptionException(key); +} + +void set(Options& opts, const std::string& key, const std::string& optionarg) +{ + + Trace("options") << "setOption(" << key << ", " << optionarg << ")" + << std::endl; + // first update this object + setInternal(opts, key, optionarg); + // then, notify the provided listener + opts.notifyListener(key); +} + +std::vector<std::vector<std::string> > getAll(const Options& opts) +{ + std::vector<std::vector<std::string>> res; + +${options_getall}$ + + return res; +} + +} // namespace cvc5::options diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 2c22065c2..db58c3a4a 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -13,43 +13,11 @@ * Contains code for handling command-line options. */ -#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__) -// force use of optreset; mingw32 croaks on argv-switching otherwise -#include "base/cvc5config.h" -#define _BSD_SOURCE -#undef HAVE_DECL_OPTRESET -#define HAVE_DECL_OPTRESET 1 -#define CVC5_IS_NOT_REALLY_BSD -#endif /* !_BSD_SOURCE && __MINGW32__ && !__MINGW64__ */ - -#ifdef __MINGW64__ -extern int optreset; -#endif /* __MINGW64__ */ - -#include <getopt.h> - -// clean up -#ifdef CVC5_IS_NOT_REALLY_BSD -# undef _BSD_SOURCE -#endif /* CVC5_IS_NOT_REALLY_BSD */ - -#include <unistd.h> -#include <string.h> -#include <time.h> - -#include <cstdio> -#include <cstdlib> -#include <cstring> -#include <iomanip> -#include <new> -#include <string> -#include <sstream> -#include <limits> +#include "options/options.h" #include "base/check.h" #include "base/exception.h" #include "base/output.h" -#include "options/didyoumean.h" #include "options/language.h" #include "options/options_handler.h" #include "options/options_listener.h" @@ -65,175 +33,22 @@ using namespace cvc5; using namespace cvc5::options; // clang-format on -namespace cvc5 { - -thread_local Options* Options::s_current = NULL; - -/** - * This is a default handler for options of built-in C++ type. This - * template is really just a helper for the handleOption() template, - * below. Variants of this template handle numeric and non-numeric, - * integral and non-integral, signed and unsigned C++ types. - * handleOption() makes sure to instantiate the right one. - * - * This implements default behavior when e.g. an option is - * unsigned but the user specifies a negative argument; etc. - */ -template <class T, bool is_numeric, bool is_integer> -struct OptionHandler { - static T handle(const std::string& option, - const std::string& flag, - const std::string& optionarg); -};/* struct OptionHandler<> */ - -/** Variant for integral C++ types */ -template <class T> -struct OptionHandler<T, true, true> { - static bool stringToInt(T& t, const std::string& str) { - std::istringstream ss(str); - ss >> t; - char tmp; - return !(ss.fail() || ss.get(tmp)); - } - - static bool containsMinus(const std::string& str) { - return str.find('-') != std::string::npos; - } - - static T handle(const std::string& option, - const std::string& flag, - const std::string& optionarg) - { - try { - T i; - bool success = stringToInt(i, optionarg); - - if(!success){ - throw OptionException(flag + ": failed to parse " + optionarg - + " as an integer of the appropriate type."); - } - - // Depending in the platform unsigned numbers with '-' signs may parse. - // Reject these by looking for any minus if it is not signed. - if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) { - // unsigned type but user gave negative argument - throw OptionException(flag + " requires a nonnegative argument"); - } else if(i < std::numeric_limits<T>::min()) { - // negative overflow for type - std::stringstream ss; - ss << flag - << " requires an argument >= " << std::numeric_limits<T>::min(); - throw OptionException(ss.str()); - } else if(i > std::numeric_limits<T>::max()) { - // positive overflow for type - std::stringstream ss; - ss << flag - << " requires an argument <= " << std::numeric_limits<T>::max(); - throw OptionException(ss.str()); - } - - return i; - - // if(std::numeric_limits<T>::is_signed) { - // return T(i.getLong()); - // } else { - // return T(i.getUnsignedLong()); - // } - } catch(std::invalid_argument&) { - // user gave something other than an integer - throw OptionException(flag + " requires an integer argument"); - } - } -};/* struct OptionHandler<T, true, true> */ - -/** Variant for numeric but non-integral C++ types */ -template <class T> -struct OptionHandler<T, true, false> { - static T handle(const std::string& option, - const std::string& flag, - const std::string& optionarg) - { - std::stringstream inss(optionarg); - long double r; - inss >> r; - if (!inss.eof()) - { - // we didn't consume the whole string (junk at end) - throw OptionException(flag + " requires a numeric argument"); - } - - if(! std::numeric_limits<T>::is_signed && r < 0.0) { - // unsigned type but user gave negative value - throw OptionException(flag + " requires a nonnegative argument"); - } else if(r < -std::numeric_limits<T>::max()) { - // negative overflow for type - std::stringstream ss; - ss << flag - << " requires an argument >= " << -std::numeric_limits<T>::max(); - throw OptionException(ss.str()); - } else if(r > std::numeric_limits<T>::max()) { - // positive overflow for type - std::stringstream ss; - ss << flag - << " requires an argument <= " << std::numeric_limits<T>::max(); - throw OptionException(ss.str()); - } - - return T(r); - } -};/* struct OptionHandler<T, true, false> */ - -/** Variant for non-numeric C++ types */ -template <class T> -struct OptionHandler<T, false, false> { - static T handle(const std::string& option, - const std::string& flag, - const std::string& optionarg) - { - T::unsupported_handleOption_call___please_write_me; - // The above line causes a compiler error if this version of the template - // is ever instantiated (meaning that a specialization is missing). So - // don't worry about the segfault in the next line, the "return" is only - // there to keep the compiler from giving additional, distracting errors - // and warnings. - return *(T*)0; - } -};/* struct OptionHandler<T, false, false> */ - -/** Handle an option of type T in the default way. */ -template <class T> -T handleOption(const std::string& option, - const std::string& flag, - const std::string& optionarg) -{ - return OptionHandler<T, - std::numeric_limits<T>::is_specialized, - std::numeric_limits<T>::is_integer>::handle(option, - flag, - optionarg); -} - -/** Handle an option of type std::string in the default way. */ -template <> -std::string handleOption<std::string>(const std::string& option, - const std::string& flag, - const std::string& optionarg) +namespace cvc5 { - return optionarg; -} + thread_local Options* Options::s_current = nullptr; -Options::Options(OptionsListener* ol) - : d_handler(new options::OptionsHandler(this)), + Options::Options(OptionsListener * ol) + : + d_olisten(ol), // clang-format off ${holder_mem_inits}$ ${holder_ref_inits}$ // clang-format on - d_olisten(ol) -{} + d_handler(std::make_unique<options::OptionsHandler>(this)) + { + } -Options::~Options() { - delete d_handler; -} + Options::~Options() {} void Options::copyValues(const Options& options){ if(this != &options) { @@ -244,333 +59,14 @@ ${holder_mem_copy}$ } void Options::setListener(OptionsListener* ol) { d_olisten = ol; } - -// clang-format off -${custom_handlers}$ -// clang-format on - -static const std::string mostCommonOptionsDescription = - "\ -Most commonly-used cvc5 options:\n" - // clang-format off -${help_common}$ - // clang-format on - ; - -// clang-format off -static const std::string optionsDescription = - mostCommonOptionsDescription + "\n\nAdditional cvc5 options:\n" -${help_others}$; -// clang-format on - -static const std::string optionsFootnote = "\n\ -[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\ - sense of the option.\n\ -"; - -static const std::string languageDescription = - "\ -Languages currently supported as arguments to the -L / --lang option:\n\ - auto attempt to automatically determine language\n\ - cvc | presentation | pl CVC presentation language\n\ - smt | smtlib | smt2 |\n\ - smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ - tptp TPTP format (cnf, fof and tff)\n\ - sygus | sygus2 SyGuS version 2.0\n\ -\n\ -Languages currently supported as arguments to the --output-lang option:\n\ - auto match output language to input language\n\ - cvc | presentation | pl CVC presentation language\n\ - smt | smtlib | smt2 |\n\ - smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ - tptp TPTP format\n\ - ast internal format (simple syntax trees)\n\ -"; - -std::string Options::getDescription() const { - return optionsDescription; -} - -void Options::printUsage(const std::string msg, std::ostream& out) { - out << msg << optionsDescription << std::endl - << optionsFootnote << std::endl << std::flush; -} - -void Options::printShortUsage(const std::string msg, std::ostream& out) { - out << msg << mostCommonOptionsDescription << std::endl - << optionsFootnote << std::endl - << "For full usage, please use --help." - << std::endl << std::endl << std::flush; -} - -void Options::printLanguageHelp(std::ostream& out) { - out << languageDescription << std::flush; -} - -/** - * This is a table of long options. By policy, each short option - * should have an equivalent long option (but the reverse isn't the - * case), so this table should thus contain all command-line options. - * - * Each option in this array has four elements: - * - * 1. the long option string - * 2. argument behavior for the option: - * no_argument - no argument permitted - * required_argument - an argument is expected - * optional_argument - an argument is permitted but not required - * 3. this is a pointer to an int which is set to the 4th entry of the - * array if the option is present; or NULL, in which case - * getopt_long() returns the 4th entry - * 4. the return value for getopt_long() when this long option (or the - * value to set the 3rd entry to; see #3) - * - * If you add something here, you should add it in src/main/usage.h - * also, to document it. - * - * If you add something that has a short option equivalent, you should - * add it to the getopt_long() call in parseOptions(). - */ -// clang-format off -static struct option cmdlineOptions[] = { - ${cmdline_options}$ - {nullptr, no_argument, nullptr, '\0'}}; -// clang-format on - -namespace options { - -/** Set a given Options* as "current" just for a particular scope. */ -class OptionsGuard { - Options** d_field; - Options* d_old; -public: - OptionsGuard(Options** field, Options* opts) : - d_field(field), - d_old(*field) { - *field = opts; - } - ~OptionsGuard() { - *d_field = d_old; - } -};/* class OptionsGuard */ - -} // namespace options - -/** - * Parse argc/argv and put the result into a cvc5::Options. - * The return value is what's left of the command line (that is, the - * non-option arguments). - * - * Throws OptionException on failures. - */ -std::vector<std::string> Options::parseOptions(Options* options, - int argc, - char* argv[], - std::string& binaryName) -{ - Assert(options != NULL); - Assert(argv != NULL); - - options::OptionsGuard guard(&s_current, options); - - const char *progName = argv[0]; - - // To debug options parsing, you may prefer to simply uncomment this - // and recompile. Debug flags have not been parsed yet so these have - // not been set. - //DebugChannel.on("options"); - - Debug("options") << "Options::parseOptions == " << options << std::endl; - Debug("options") << "argv == " << argv << std::endl; - - // Find the base name of the program. - const char *x = strrchr(progName, '/'); - if(x != NULL) { - progName = x + 1; - } - binaryName = std::string(progName); - - std::vector<std::string> nonoptions; - options->parseOptionsRecursive(argc, argv, &nonoptions); - if(Debug.isOn("options")){ - for(std::vector<std::string>::const_iterator i = nonoptions.begin(), - iend = nonoptions.end(); i != iend; ++i){ - Debug("options") << "nonoptions " << *i << std::endl; - } - } - - return nonoptions; -} - -std::string suggestCommandLineOptions(const std::string& optionName) -{ - DidYouMean didYouMean; - - const char* opt; - for(size_t i = 0; (opt = cmdlineOptions[i].name) != nullptr; ++i) { - didYouMean.addWord(std::string("--") + cmdlineOptions[i].name); - } - - return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('='))); -} - -void Options::parseOptionsRecursive(int argc, - char* argv[], - std::vector<std::string>* nonoptions) -{ - Options& opts = *this; - if(Debug.isOn("options")) { - Debug("options") << "starting a new parseOptionsRecursive with " - << argc << " arguments" << std::endl; - for( int i = 0; i < argc ; i++ ){ - Assert(argv[i] != NULL); - Debug("options") << " argv[" << i << "] = " << argv[i] << std::endl; - } - } - - // Reset getopt(), in the case of multiple calls to parseOptions(). - // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. - optind = 0; -#if HAVE_DECL_OPTRESET - optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this -#endif /* HAVE_DECL_OPTRESET */ - - // We must parse the binary name, which is manually ignored below. Setting - // this to 1 leads to incorrect behavior on some platforms. - int main_optind = 0; - int old_optind; - - - while(true) { // Repeat Forever - - optopt = 0; - std::string option, optionarg; - - optind = main_optind; - old_optind = main_optind; - - // If we encounter an element that is not at zero and does not start - // with a "-", this is a non-option. We consume this element as a - // non-option. - if (main_optind > 0 && main_optind < argc && - argv[main_optind][0] != '-') { - Debug("options") << "enqueueing " << argv[main_optind] - << " as a non-option." << std::endl; - nonoptions->push_back(argv[main_optind]); - ++main_optind; - continue; - } - - - Debug("options") << "[ before, main_optind == " << main_optind << " ]" - << std::endl; - Debug("options") << "[ before, optind == " << optind << " ]" << std::endl; - Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]" - << std::endl; - // clang-format off - int c = getopt_long(argc, argv, - "+:${options_short}$", - cmdlineOptions, NULL); - // clang-format on - - main_optind = optind; - - Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]" - << "[ next option will be at pos: " << optind << " ]" - << std::endl; - - // The initial getopt_long call should always determine that argv[0] - // is not an option and returns -1. We always manually advance beyond - // this element. - if ( old_optind == 0 && c == -1 ) { - Assert(main_optind > 0); - continue; - } - - if ( c == -1 ) { - if(Debug.isOn("options")) { - Debug("options") << "done with option parsing" << std::endl; - for(int index = optind; index < argc; ++index) { - Debug("options") << "remaining " << argv[index] << std::endl; - } - } - break; - } - - option = argv[old_optind == 0 ? 1 : old_optind]; - optionarg = (optarg == NULL) ? "" : optarg; - - Debug("preemptGetopt") << "processing option " << c - << " (`" << char(c) << "'), " << option << std::endl; - - // clang-format off - switch(c) + +void Options::notifyListener(const std::string& key) + { + if (d_olisten != nullptr) { -${options_handler}$ - - case ':' : - // This can be a long or short option, and the way to get at the - // name of it is different. - throw OptionException(std::string("option `") + option - + "' missing its required argument"); - - case '?': - default: - throw OptionException(std::string("can't understand option `") + option - + "'" + suggestCommandLineOptions(option)); + d_olisten->notifySetOption(key); } } - // clang-format on - - Debug("options") << "got " << nonoptions->size() - << " non-option arguments." << std::endl; -} - -// clang-format off -std::vector<std::vector<std::string> > Options::getOptions() const -{ - std::vector< std::vector<std::string> > opts; - - ${options_getoptions}$ - - return opts; -} -// clang-format on - -void Options::setOption(const std::string& key, const std::string& optionarg) -{ - Trace("options") << "setOption(" << key << ", " << optionarg << ")" - << std::endl; - // first update this object - setOptionInternal(key, optionarg); - // then, notify the provided listener - if (d_olisten != nullptr) - { - d_olisten->notifySetOption(key); - } -} - -// clang-format off -void Options::setOptionInternal(const std::string& key, - const std::string& optionarg) -{ - options::OptionsHandler* handler = d_handler; - Options& opts = *this; - ${setoption_handlers}$ - throw UnrecognizedOptionException(key); -} -// clang-format on - -// clang-format off -std::string Options::getOption(const std::string& key) const -{ - Trace("options") << "Options::getOption(" << key << ")" << std::endl; - const Options& options = *this; - ${getoption_handlers}$ - - throw UnrecognizedOptionException(key); -} -// clang-format on } // namespace cvc5 diff --git a/src/options/options_template.h b/src/options/options_template.h index e9a4a6999..a4e595f0d 100644 --- a/src/options/options_template.h +++ b/src/options/options_template.h @@ -25,46 +25,20 @@ #include "base/listener.h" #include "cvc5_export.h" -#include "options/language.h" -#include "options/printer_modes.h" namespace cvc5 { - -namespace api { -class Solver; -} namespace options { - struct OptionsHolder; class OptionsHandler; // clang-format off ${holder_fwd_decls}$ // clang-format on - } // namespace options +} // namespace options class OptionsListener; class CVC5_EXPORT Options { - friend api::Solver; - - /** The handler for the options of the theory. */ - options::OptionsHandler* d_handler; - -// clang-format off -${holder_mem_decls}$ -// clang-format on - public: -// clang-format off -${holder_ref_decls}$ -// clang-format on - - private: - - /** The current Options in effect */ - static thread_local Options* s_current; - - friend class options::OptionsHandler; - + public: /** * Options cannot be copied as they are given an explicit list of * Listeners to respond to. @@ -77,25 +51,25 @@ ${holder_ref_decls}$ */ Options& operator=(const Options& options) = delete; -public: - class OptionsScope - { - private: - Options* d_oldOptions; - public: - OptionsScope(Options* newOptions) : - d_oldOptions(Options::s_current) - { - Options::s_current = newOptions; - } - ~OptionsScope(){ - Options::s_current = d_oldOptions; - } - }; + class OptionsScope + { + private: + Options* d_oldOptions; + public: + OptionsScope(Options* newOptions) : + d_oldOptions(Options::s_current) + { + Options::s_current = newOptions; + } + ~OptionsScope(){ + Options::s_current = d_oldOptions; + } + }; + friend class OptionsScope; /** Return true if current Options are null */ static inline bool isCurrentNull() { - return s_current == NULL; + return s_current == nullptr; } /** Get the current Options in effect */ @@ -117,103 +91,31 @@ public: */ void copyValues(const Options& options); - /** - * Set the value of the given option by key. - * - * Throws OptionException or ModalException on failures. - */ - void setOption(const std::string& key, const std::string& optionarg); - - /** - * Gets the value of the given option by key and returns value as a string. - * - * Throws OptionException on failures, such as key not being the name of an - * option. - */ - std::string getOption(const std::string& key) const; - - // Static accessor functions. - // TODO: Document these. - static std::ostream* currentGetOut(); - - /** - * Get a description of the command-line flags accepted by - * parseOptions. The returned string will be escaped so that it is - * suitable as an argument to printf. */ - std::string getDescription() const; - - /** - * Print overall command-line option usage message, prefixed by - * "msg"---which could be an error message causing the usage - * output in the first place, e.g. "no such option --foo" - */ - static void printUsage(const std::string msg, std::ostream& out); - - /** - * Print command-line option usage message for only the most-commonly - * used options. The message is prefixed by "msg"---which could be - * an error message causing the usage output in the first place, e.g. - * "no such option --foo" - */ - static void printShortUsage(const std::string msg, std::ostream& out); - - /** Print help for the --lang command line option */ - static void printLanguageHelp(std::ostream& out); - - /** - * Initialize the Options object options based on the given - * command-line arguments given in argc and argv. The return value - * is what's left of the command line (that is, the non-option - * arguments). - * - * This function uses getopt_long() and is not thread safe. - * - * Throws OptionException on failures. - * - * Preconditions: options and argv must be non-null. - */ - static std::vector<std::string> parseOptions(Options* options, - int argc, - char* argv[], - std::string& binaryName); - - /** - * Get the setting for all options. - */ - std::vector<std::vector<std::string> > getOptions() const; - /** Set the generic listener associated with this class to ol */ void setListener(OptionsListener* ol); - /** Sends a std::flush to getErr(). */ - void flushErr(); - - /** Sends a std::flush to getOut(). */ - void flushOut(); + void notifyListener(const std::string& key); private: /** Pointer to the options listener, if one exists */ - OptionsListener* d_olisten; - /** - * Helper method for setOption, updates this object for setting the given - * option. - */ - void setOptionInternal(const std::string& key, const std::string& optionarg); - /** - * Internal procedure for implementing the parseOptions function. - * Initializes the options object based on the given command-line - * arguments. The command line arguments are stored in argc/argv. - * Nonoptions are stored into nonoptions. - * - * This is not thread safe. - * - * Throws OptionException on failures. - * - * Preconditions: options, extender and nonoptions are non-null. - */ - void parseOptionsRecursive(int argc, - char* argv[], - std::vector<std::string>* nonoptions); + OptionsListener* d_olisten = nullptr; + +// clang-format off +${holder_mem_decls}$ +// clang-format on + public: +// clang-format off +${holder_ref_decls}$ +// clang-format on + + private: + /** The handler for the options of the theory. */ + std::unique_ptr<options::OptionsHandler> d_handler; + + /** The current Options in effect */ + static thread_local Options* s_current; + + }; /* class Options */ } // namespace cvc5 diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 9b5a93486..a97fe572f 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -195,6 +195,14 @@ name = "SMT Layer" help = "Produce unsat cores using solving under assumptions and preprocessing proofs." [[option]] + name = "minimalUnsatCores" + category = "regular" + long = "minimal-unsat-cores" + type = "bool" + default = "false" + help = "if an unsat core is produced, it is reduced to a minimal unsat core" + +[[option]] name = "checkUnsatCores" category = "regular" long = "check-unsat-cores" diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b5a8472e6..bf26b80ee 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -824,8 +824,8 @@ void Smt2Printer::toStream(std::ostream& out, case kind::PRODUCT: case kind::TRANSPOSE: case kind::TCLOSURE: - out << smtKindString(k, d_variant) << " "; - break; + case kind::IDEN: + case kind::JOIN_IMAGE: out << smtKindString(k, d_variant) << " "; break; case kind::COMPREHENSION: out << smtKindString(k, d_variant) << " "; break; case kind::SINGLETON: { @@ -1237,6 +1237,11 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right"; case kind::INT_TO_BITVECTOR: return "int2bv"; + // datatypes theory + case kind::APPLY_TESTER: return "is"; + case kind::APPLY_UPDATER: return "update"; + + // set theory case kind::UNION: return "union"; case kind::INTERSECTION: return "intersection"; case kind::SETMINUS: return "setminus"; @@ -1254,6 +1259,8 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::PRODUCT: return "product"; case kind::TRANSPOSE: return "transpose"; case kind::TCLOSURE: return "tclosure"; + case kind::IDEN: return "iden"; + case kind::JOIN_IMAGE: return "join_image"; // bag theory case kind::BAG_TYPE: return "Bag"; diff --git a/src/proof/lfsc/lfsc_util.cpp b/src/proof/lfsc/lfsc_util.cpp new file mode 100644 index 000000000..d8bd8f548 --- /dev/null +++ b/src/proof/lfsc/lfsc_util.cpp @@ -0,0 +1,88 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Yoni Zohar + * + * 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. + * **************************************************************************** + * + * Utilities for LFSC proofs. + */ + +#include "proof/lfsc/lfsc_util.h" + +#include "proof/proof_checker.h" +#include "util/rational.h" + +namespace cvc5 { +namespace proof { + +const char* toString(LfscRule id) +{ + switch (id) + { + case LfscRule::SCOPE: return "scope"; + case LfscRule::NEG_SYMM: return "neg_symm"; + case LfscRule::CONG: return "cong"; + case LfscRule::AND_INTRO1: return "and_intro1"; + case LfscRule::AND_INTRO2: return "and_intro2"; + case LfscRule::NOT_AND_REV: return "not_and_rev"; + case LfscRule::PROCESS_SCOPE: return "process_scope"; + case LfscRule::ARITH_SUM_UB: return "arith_sum_ub"; + case LfscRule::INSTANTIATE: return "instantiate"; + case LfscRule::SKOLEMIZE: return "skolemize"; + case LfscRule::LAMBDA: return "\\"; + case LfscRule::PLET: return "plet"; + default: return "?"; + } +} +std::ostream& operator<<(std::ostream& out, LfscRule id) +{ + out << toString(id); + return out; +} + +bool getLfscRule(Node n, LfscRule& lr) +{ + uint32_t id; + if (ProofRuleChecker::getUInt32(n, id)) + { + lr = static_cast<LfscRule>(id); + return true; + } + return false; +} + +LfscRule getLfscRule(Node n) +{ + LfscRule lr = LfscRule::UNKNOWN; + getLfscRule(n, lr); + return lr; +} + +Node mkLfscRuleNode(LfscRule r) +{ + return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(r))); +} + +bool LfscProofLetifyTraverseCallback::shouldTraverse(const ProofNode* pn) +{ + if (pn->getRule() == PfRule::SCOPE) + { + return false; + } + if (pn->getRule() != PfRule::LFSC_RULE) + { + return true; + } + // do not traverse under LFSC (lambda) scope + LfscRule lr = getLfscRule(pn->getArguments()[0]); + return lr != LfscRule::LAMBDA; +} + +} // namespace proof +} // namespace cvc5 diff --git a/src/proof/lfsc/lfsc_util.h b/src/proof/lfsc/lfsc_util.h new file mode 100644 index 000000000..c97c07489 --- /dev/null +++ b/src/proof/lfsc/lfsc_util.h @@ -0,0 +1,105 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Yoni Zohar + * + * 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. + * **************************************************************************** + * + * Utilities for LFSC proofs. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__LFSC__LFSC_UTIL_H +#define CVC5__PROOF__LFSC__LFSC_UTIL_H + +#include <iostream> +#include <map> + +#include "expr/node.h" +#include "proof/proof_letify.h" + +namespace cvc5 { +namespace proof { + +/** + * LFSC rules. The enum below contains all rules that don't correspond to a + * PfRule, e.g. congruence in LFSC does not have the same form as congruence + * in the internal calculus. + */ +enum class LfscRule : uint32_t +{ + //----------- translated rules + + // We defined LFSC versions for rules that either don't exist in the internal + // calculus, or have a different set of arugments/children. + + // scope has a different structure, e.g. uses lambdas + SCOPE, + // must distinguish equalities and disequalities + NEG_SYMM, + // congruence is done via a higher-order variant of congruence + CONG, + // we use unrolled binary versions of and intro + AND_INTRO1, + AND_INTRO2, + // needed as a helper for SCOPE + NOT_AND_REV, + PROCESS_SCOPE, + // arithmetic + ARITH_SUM_UB, + + // form of quantifier rules varies from internal calculus + INSTANTIATE, + SKOLEMIZE, + + // a lambda with argument + LAMBDA, + // a proof-let "plet" + PLET, + //----------- unknown + UNKNOWN, +}; + +/** + * Converts a lfsc rule to a string. Note: This function is also used in + * `safe_print()`. Changing this function name or signature will result in + * `safe_print()` printing "<unsupported>" instead of the proper strings for + * the enum values. + * + * @param id The lfsc rule + * @return The name of the lfsc rule + */ +const char* toString(LfscRule id); + +/** + * Writes a lfsc rule name to a stream. + * + * @param out The stream to write to + * @param id The lfsc rule to write to the stream + * @return The stream + */ +std::ostream& operator<<(std::ostream& out, LfscRule id); +/** Get LFSC rule from a node */ +LfscRule getLfscRule(Node n); +/** Get LFSC rule from a node, return true if success and store in lr */ +bool getLfscRule(Node n, LfscRule& lr); +/** Make node for LFSC rule */ +Node mkLfscRuleNode(LfscRule r); + +/** Helper class used for letifying LFSC proofs. */ +class LfscProofLetifyTraverseCallback : public ProofLetifyTraverseCallback +{ + public: + bool shouldTraverse(const ProofNode* pn) override; +}; + +} // namespace proof +} // namespace cvc5 + +#endif diff --git a/src/proof/print_expr.cpp b/src/proof/print_expr.cpp new file mode 100644 index 000000000..becd9195a --- /dev/null +++ b/src/proof/print_expr.cpp @@ -0,0 +1,58 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Utilities for printing expressions in proofs + */ + +#include "proof/print_expr.h" + +namespace cvc5 { +namespace proof { + +PExprStream::PExprStream(std::vector<PExpr>& stream, Node tt, Node ff) + : d_stream(stream), d_tt(tt), d_ff(ff) +{ +} + +PExprStream& PExprStream::operator<<(const ProofNode* pn) +{ + d_stream.push_back(PExpr(pn)); + return *this; +} + +PExprStream& PExprStream::operator<<(Node n) +{ + d_stream.push_back(PExpr(n)); + return *this; +} + +PExprStream& PExprStream::operator<<(TypeNode tn) +{ + d_stream.push_back(PExpr(tn)); + return *this; +} + +PExprStream& PExprStream::operator<<(bool b) +{ + Assert(!d_tt.isNull() && !d_ff.isNull()); + d_stream.push_back(b ? d_tt : d_ff); + return *this; +} + +PExprStream& PExprStream::operator<<(PExpr p) +{ + d_stream.push_back(p); + return *this; +} + +} // namespace proof +} // namespace cvc5 diff --git a/src/proof/print_expr.h b/src/proof/print_expr.h new file mode 100644 index 000000000..15a8bb6c2 --- /dev/null +++ b/src/proof/print_expr.h @@ -0,0 +1,86 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Utilities for printing expressions in proofs + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PRINT_EXPR_H +#define CVC5__PROOF__PRINT_EXPR_H + +#include <iostream> +#include <map> + +#include "expr/node.h" +#include "proof/proof_node.h" + +namespace cvc5 { +namespace proof { + +/** + * A term, type or a proof. This class is used for printing combinations of + * proofs terms and types. + */ +class PExpr +{ + public: + PExpr() : d_node(), d_pnode(nullptr), d_typeNode() {} + PExpr(Node n) : d_node(n), d_pnode(nullptr), d_typeNode() {} + PExpr(const ProofNode* pn) : d_node(), d_pnode(pn), d_typeNode() {} + PExpr(TypeNode tn) : d_node(), d_pnode(nullptr), d_typeNode(tn) {} + ~PExpr() {} + /** The node, if this p-exression is a node */ + Node d_node; + /** The proof node, if this p-expression is a proof */ + const ProofNode* d_pnode; + /** The type node, if this p-expression is a type */ + TypeNode d_typeNode; +}; + +/** + * A stream of p-expressions, which appends p-expressions to a reference vector. + * That vector can then be used when printing a proof. + */ +class PExprStream +{ + public: + /** + * Takes a reference to a stream (vector of p-expressions), and the + * representation true/false (tt/ff). + */ + PExprStream(std::vector<PExpr>& stream, + Node tt = Node::null(), + Node ff = Node::null()); + /** Append a proof node */ + PExprStream& operator<<(const ProofNode* pn); + /** Append a node */ + PExprStream& operator<<(Node n); + /** Append a type node */ + PExprStream& operator<<(TypeNode tn); + /** Append a Boolean */ + PExprStream& operator<<(bool b); + /** Append a pexpr */ + PExprStream& operator<<(PExpr p); + + private: + /** Reference to the stream */ + std::vector<PExpr>& d_stream; + /** Builtin nodes for true and false */ + Node d_tt; + Node d_ff; +}; + +} // namespace proof +} // namespace cvc5 + +#endif diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp index 96f5197e3..6a9979f75 100644 --- a/src/proof/proof_checker.cpp +++ b/src/proof/proof_checker.cpp @@ -85,6 +85,11 @@ ProofCheckerStatistics::ProofCheckerStatistics() { } +ProofChecker::ProofChecker(uint32_t pclevel, theory::RewriteDb* rdb) + : d_pclevel(pclevel), d_rdb(rdb) +{ +} + Node ProofChecker::check(ProofNode* pn, Node expected) { return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected); @@ -303,6 +308,8 @@ ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id) return it->second; } +theory::RewriteDb* ProofChecker::getRewriteDatabase() { return d_rdb; } + uint32_t ProofChecker::getPedanticLevel(PfRule id) const { std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id); diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h index ac5531bf4..f1f10eedb 100644 --- a/src/proof/proof_checker.h +++ b/src/proof/proof_checker.h @@ -29,6 +29,10 @@ namespace cvc5 { class ProofChecker; class ProofNode; +namespace theory { +class RewriteDb; +} + /** A virtual base class for checking a proof rule */ class ProofRuleChecker { @@ -101,7 +105,7 @@ class ProofCheckerStatistics class ProofChecker { public: - ProofChecker(uint32_t pclevel = 0) : d_pclevel(pclevel) {} + ProofChecker(uint32_t pclevel = 0, theory::RewriteDb* rdb = nullptr); ~ProofChecker() {} /** * Return the formula that is proven by proof node pn, or null if pn is not @@ -162,7 +166,8 @@ class ProofChecker uint32_t plevel = 10); /** get checker for */ ProofRuleChecker* getCheckerFor(PfRule id); - + /** get the rewrite database */ + theory::RewriteDb* getRewriteDatabase(); /** * Get the pedantic level for id if it has been assigned a pedantic * level via registerTrustedChecker above, or zero otherwise. @@ -186,6 +191,8 @@ class ProofChecker std::map<PfRule, uint32_t> d_plevel; /** The pedantic level of this checker */ uint32_t d_pclevel; + /** Pointer to the rewrite database */ + theory::RewriteDb* d_rdb; /** * Check internal. This is used by check and checkDebug above. It writes * checking errors on out when enableOutput is true. We treat trusted checkers diff --git a/src/proof/proof_letify.cpp b/src/proof/proof_letify.cpp new file mode 100644 index 000000000..c6269631c --- /dev/null +++ b/src/proof/proof_letify.cpp @@ -0,0 +1,124 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Utilities for computing letification of proofs. + */ + +#include "proof/proof_letify.h" + +namespace cvc5 { +namespace proof { + +bool ProofLetifyTraverseCallback::shouldTraverse(const ProofNode* pn) +{ + return pn->getRule() != PfRule::SCOPE; +} + +void ProofLetify::computeProofLet(const ProofNode* pn, + std::vector<const ProofNode*>& pletList, + std::map<const ProofNode*, size_t>& pletMap, + size_t thresh, + ProofLetifyTraverseCallback* pltc) +{ + Assert(pletList.empty() && pletMap.empty()); + if (thresh == 0) + { + // value of 0 means do not introduce let + return; + } + std::vector<const ProofNode*> visitList; + std::map<const ProofNode*, size_t> pcount; + if (pltc == nullptr) + { + // use default callback + ProofLetifyTraverseCallback defaultPltc; + computeProofCounts(pn, visitList, pcount, &defaultPltc); + } + else + { + computeProofCounts(pn, visitList, pcount, pltc); + } + // Now populate the pletList and pletMap + convertProofCountToLet(visitList, pcount, pletList, pletMap, thresh); +} + +void ProofLetify::computeProofCounts(const ProofNode* pn, + std::vector<const ProofNode*>& visitList, + std::map<const ProofNode*, size_t>& pcount, + ProofLetifyTraverseCallback* pltc) +{ + std::map<const ProofNode*, size_t>::iterator it; + std::vector<const ProofNode*> visit; + const ProofNode* cur; + visit.push_back(pn); + do + { + cur = visit.back(); + it = pcount.find(cur); + if (it == pcount.end()) + { + pcount[cur] = 0; + if (!pltc->shouldTraverse(cur)) + { + // callback indicated we should not traverse + continue; + } + const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren(); + for (const std::shared_ptr<ProofNode>& cp : pc) + { + visit.push_back(cp.get()); + } + } + else + { + if (it->second == 0) + { + visitList.push_back(cur); + } + pcount[cur]++; + visit.pop_back(); + } + } while (!visit.empty()); +} + +void ProofLetify::convertProofCountToLet( + const std::vector<const ProofNode*>& visitList, + const std::map<const ProofNode*, size_t>& pcount, + std::vector<const ProofNode*>& pletList, + std::map<const ProofNode*, size_t>& pletMap, + size_t thresh) +{ + Assert(pletList.empty() && pletMap.empty()); + if (thresh == 0) + { + // value of 0 means do not introduce let + return; + } + // Assign ids for those whose count is > 1, traverse in reverse order + // so that deeper proofs are assigned lower identifiers + std::map<const ProofNode*, size_t>::const_iterator itc; + for (const ProofNode* pn : visitList) + { + itc = pcount.find(pn); + Assert(itc != pcount.end()); + if (itc->second >= thresh && pn->getRule() != PfRule::ASSUME) + { + pletList.push_back(pn); + // start with id 1 + size_t id = pletMap.size() + 1; + pletMap[pn] = id; + } + } +} + +} // namespace proof +} // namespace cvc5 diff --git a/src/proof/proof_letify.h b/src/proof/proof_letify.h new file mode 100644 index 000000000..cfe1259e5 --- /dev/null +++ b/src/proof/proof_letify.h @@ -0,0 +1,98 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Utilities for computing letification of proofs. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_LETIFY_H +#define CVC5__PROOF__PROOF_LETIFY_H + +#include <iostream> +#include <map> + +#include "expr/node.h" +#include "proof/proof_node.h" + +namespace cvc5 { +namespace proof { + +/** + * A callback which asks whether a proof node should be traversed for + * proof letification. For example, this may make it so that SCOPE is not + * traversed. + */ +class ProofLetifyTraverseCallback +{ + public: + virtual ~ProofLetifyTraverseCallback() {} + /** + * Should we traverse proof node pn for letification? If this returns false, + * then pn is being treated as a black box for letification. + */ + virtual bool shouldTraverse(const ProofNode* pn); +}; + +/** + * Utilities for letification. + */ +class ProofLetify +{ + public: + /** + * Stores proofs in map that require letification, mapping them to a unique + * identifier. For each proof node in the domain of pletMap in the list + * pletList such that pletList[i] does not contain subproof pletList[j] for + * j>i. + * + * @param pn The proof node to letify + * @param pletList The list of proofs occurring in pn that should be letified + * @param pletMap Mapping from proofs in pletList to an identifier + * @param thresh The number of times a proof node has to occur to be added + * to pletList + * @param pltc A callback indicating whether to traverse a proof node during + * this call. + */ + static void computeProofLet(const ProofNode* pn, + std::vector<const ProofNode*>& pletList, + std::map<const ProofNode*, size_t>& pletMap, + size_t thresh = 2, + ProofLetifyTraverseCallback* pltc = nullptr); + + private: + /** + * Convert a map from proof nodes to # occurrences (pcount) to a list + * pletList / pletMap as described in the method above, where thresh + * is the minimum number of occurrences to be added to the list. + */ + static void convertProofCountToLet( + const std::vector<const ProofNode*>& visitList, + const std::map<const ProofNode*, size_t>& pcount, + std::vector<const ProofNode*>& pletList, + std::map<const ProofNode*, size_t>& pletMap, + size_t thresh = 2); + /** + * Compute the count of sub proof nodes in pn, store in pcount. Additionally, + * store each proof node in the domain of pcount in an order in visitList + * such that visitList[i] does not contain sub proof visitList[j] for j>i. + */ + static void computeProofCounts(const ProofNode* pn, + std::vector<const ProofNode*>& visitList, + std::map<const ProofNode*, size_t>& pcount, + ProofLetifyTraverseCallback* pltc); +}; + +} // namespace proof +} // namespace cvc5 + +#endif diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp index 7be07f7f5..7e1cdf8d3 100644 --- a/src/proof/proof_rule.cpp +++ b/src/proof/proof_rule.cpp @@ -47,6 +47,7 @@ const char* toString(PfRule id) case PfRule::TRUST_SUBS: return "TRUST_SUBS"; case PfRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP"; case PfRule::TRUST_SUBS_EQ: return "TRUST_SUBS_EQ"; + case PfRule::THEORY_INFERENCE: return "THEORY_INFERENCE"; //================================================= Boolean rules case PfRule::RESOLUTION: return "RESOLUTION"; case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION"; @@ -119,6 +120,7 @@ const char* toString(PfRule id) case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; case PfRule::ARRAYS_EXT: return "ARRAYS_EXT"; case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST"; + case PfRule::ARRAYS_EQ_RANGE_EXPAND: return "ARRAYS_EQ_RANGE_EXPAND"; //================================================= Bit-Vector rules case PfRule::BV_BITBLAST: return "BV_BITBLAST"; case PfRule::BV_BITBLAST_STEP: return "BV_BITBLAST_STEP"; @@ -200,6 +202,8 @@ const char* toString(PfRule id) return "ARITH_TRANS_SINE_APPROX_BELOW_POS"; case PfRule::ARITH_NL_CAD_DIRECT: return "ARITH_NL_CAD_DIRECT"; case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE"; + //================================================= External rules + case PfRule::LFSC_RULE: return "LFSC_RULE"; //================================================= Unknown rule case PfRule::UNKNOWN: return "UNKNOWN"; default: return "?"; diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 9625e1d28..78e773bdc 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -257,6 +257,8 @@ enum class PfRule : uint32_t // where F is a solved equality of the form (= x t) derived as the solved // form of F', where F' is given as a child. TRUST_SUBS_EQ, + // where F is a fact derived by a theory-specific inference + THEORY_INFERENCE, // ========= SAT Refutation for assumption-based unsat cores // Children: (P1, ..., Pn) // Arguments: none @@ -711,6 +713,15 @@ enum class PfRule : uint32_t // Conclusion: (not (= (select a k) (select b k))) // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))). ARRAYS_EXT, + // ======== EQ_RANGE expansion + // Children: none + // Arguments: ((eqrange a b i j)) + // ---------------------------------------- + // Conclusion: (= + // (eqrange a b i j) + // (forall ((x T)) + // (=> (and (<= i x) (<= x j)) (= (select a x) (select b x))))) + ARRAYS_EQ_RANGE_EXPAND, // ======== Array Trust // Children: (P1 ... Pn) // Arguments: (F) @@ -825,10 +836,16 @@ enum class PfRule : uint32_t SKOLEMIZE, // ======== Instantiate // Children: (P:(forall ((x1 T1) ... (xn Tn)) F)) - // Arguments: (t1 ... tn) + // Arguments: (t1 ... tn, (id (t)?)? ) // ---------------------------------------- // Conclusion: F*sigma - // sigma maps x1 ... xn to t1 ... tn. + // where sigma maps x1 ... xn to t1 ... tn. + // + // The optional argument id indicates the inference id that caused the + // instantiation. The term t indicates an additional term (e.g. the trigger) + // associated with the instantiation, which depends on the id. If the id + // has prefix "QUANTIFIERS_INST_E_MATCHING", then t is the trigger that + // generated the instantiation. INSTANTIATE, // ======== (Trusted) quantifiers preprocess // Children: ? @@ -1387,6 +1404,14 @@ enum class PfRule : uint32_t // that extends the Cell and satisfies all assumptions. ARITH_NL_CAD_RECURSIVE, + //================================================ Place holder for Lfsc rules + // ======== Lfsc rule + // Children: (P1 ... Pn) + // Arguments: (id, Q, A1, ..., Am) + // --------------------- + // Conclusion: (Q) + LFSC_RULE, + //================================================= Unknown rule UNKNOWN, }; diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index bb104e98d..e12d3eb1d 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -69,7 +69,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.driver.dumpUnsatCores = true; } if (options::checkUnsatCores() || options::dumpUnsatCores() - || options::unsatAssumptions() + || options::unsatAssumptions() || options::minimalUnsatCores() || options::unsatCoresMode() != options::UnsatCoresMode::OFF) { opts.smt.unsatCores = true; @@ -968,6 +968,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Trace("smt") << "setting decision mode to " << opts.decision.decisionMode << std::endl; } + + // set up of central equality engine + if (opts.arith.arithEqSolver) + { + if (!opts.arith.arithCongManWasSetByUser) + { + // if we are using the arithmetic equality solver, do not use the + // arithmetic congruence manager by default + opts.arith.arithCongMan = false; + } + } + if (options::incrementalSolving()) { // disable modes not supported by incremental diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9056e7c94..bbd65c24f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -27,6 +27,8 @@ #include "options/language.h" #include "options/main_options.h" #include "options/option_exception.h" +#include "options/options_public.h" +#include "options/parser_options.h" #include "options/printer_options.h" #include "options/proof_options.h" #include "options/smt_options.h" @@ -549,7 +551,7 @@ std::string SmtEngine::getInfo(const std::string& key) const } Assert(key == "all-options"); // get the options, like all-statistics - return toSExpr(Options::current().getOptions()); + return toSExpr(options::getAll(getOptions())); } void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func) @@ -1400,9 +1402,80 @@ UnsatCore SmtEngine::getUnsatCoreInternal() std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(pepf, *d_asserts); std::vector<Node> core; d_ucManager->getUnsatCore(pfn, *d_asserts, core); + if (options::minimalUnsatCores()) + { + core = reduceUnsatCore(core); + } return UnsatCore(core); } +std::vector<Node> SmtEngine::reduceUnsatCore(const std::vector<Node>& core) +{ + Assert(options::unsatCores()) + << "cannot reduce unsat core if unsat cores are turned off"; + + Notice() << "SmtEngine::reduceUnsatCore(): reducing unsat core" << endl; + std::unordered_set<Node> removed; + for (const Node& skip : core) + { + std::unique_ptr<SmtEngine> coreChecker; + initializeSubsolver(coreChecker); + coreChecker->setLogic(getLogicInfo()); + coreChecker->getOptions().smt.checkUnsatCores = false; + // disable all proof options + coreChecker->getOptions().smt.produceProofs = false; + coreChecker->getOptions().smt.checkProofs = false; + coreChecker->getOptions().proof.proofEagerChecking = false; + + for (const Node& ucAssertion : core) + { + if (ucAssertion != skip && removed.find(ucAssertion) == removed.end()) + { + Node assertionAfterExpansion = expandDefinitions(ucAssertion); + coreChecker->assertFormula(assertionAfterExpansion); + } + } + Result r; + try + { + r = coreChecker->checkSat(); + } + catch (...) + { + throw; + } + + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + removed.insert(skip); + } + else if (r.asSatisfiabilityResult().isUnknown()) + { + Warning() << "SmtEngine::reduceUnsatCore(): could not reduce unsat core " + "due to " + "unknown result."; + } + } + + if (removed.empty()) + { + return core; + } + else + { + std::vector<Node> newUcAssertions; + for (const Node& n : core) + { + if (removed.find(n) == removed.end()) + { + newUcAssertions.push_back(n); + } + } + + return newUcAssertions; + } +} + void SmtEngine::checkUnsatCore() { Assert(d_env->getOptions().smt.unsatCores) << "cannot check unsat core if unsat cores are turned off"; @@ -1907,7 +1980,7 @@ void SmtEngine::setOption(const std::string& key, const std::string& value) } std::string optionarg = value; - getOptions().setOption(key, optionarg); + options::set(getOptions(), key, optionarg); } void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; } @@ -1972,7 +2045,7 @@ std::string SmtEngine::getOption(const std::string& key) const return nm->mkNode(Kind::SEXPR, result).toString(); } - std::string atom = getOptions().getOption(key); + std::string atom = options::get(getOptions(), key); if (atom != "true" && atom != "false") { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 3128257e6..02e5c6b06 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Andrew Reynolds, Morgan Deters, Aina Niemetz + * * This file is part of the cvc5 project. * @@ -368,6 +368,11 @@ class CVC5_EXPORT SmtEngine Result assertFormula(const Node& formula, bool inUnsatCore = true); /** + * Reduce an unsatisfiable core to make it minimal. + */ + std::vector<Node> reduceUnsatCore(const std::vector<Node>& core); + + /** * Check if a given (set of) expression(s) is entailed with respect to the * current set of assertions. We check this by asserting the negation of * the (big AND over the) given (set of) expression(s). diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp index ba2c07326..22304f9e8 100644 --- a/src/smt/unsat_core_manager.cpp +++ b/src/smt/unsat_core_manager.cpp @@ -80,7 +80,10 @@ void UnsatCoreManager::getRelevantInstantiations( const std::vector<Node>& instTerms = cur->getArguments(); Assert(cs.size() == 1); Node q = cs[0]->getResult(); - insts[q].push_back({instTerms.begin(), instTerms.end()}); + // the instantiation is a prefix of the arguments up to the number of + // variables + insts[q].push_back( + {instTerms.begin(), instTerms.begin() + q[0].getNumChildren()}); } for (const std::shared_ptr<ProofNode>& cp : cs) { diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 9e7202f1d..3a35319ed 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -71,24 +71,44 @@ ArithCongruenceManager::~ArithCongruenceManager() {} bool ArithCongruenceManager::needsEqualityEngine(EeSetupInfo& esi) { + Assert(!options::arithEqSolver()); esi.d_notify = &d_notify; - esi.d_name = "theory::arith::ArithCongruenceManager"; + esi.d_name = "arithCong::ee"; return true; } -void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee, - eq::ProofEqEngine* pfee) +void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee) { - Assert(ee != nullptr); - d_ee = ee; + if (options::arithEqSolver()) + { + // use our own copy + d_allocEe.reset( + new eq::EqualityEngine(d_notify, d_satContext, "arithCong::ee", true)); + d_ee = d_allocEe.get(); + if (d_pnm != nullptr) + { + // allocate an internal proof equality engine + d_allocPfee.reset( + new eq::ProofEqEngine(d_satContext, d_userContext, *d_ee, d_pnm)); + d_ee->setProofEqualityEngine(d_allocPfee.get()); + } + } + else + { + Assert(ee != nullptr); + // otherwise, we use the official one + d_ee = ee; + } + // set the congruence kinds on the separate equality engine d_ee->addFunctionKind(kind::NONLINEAR_MULT); d_ee->addFunctionKind(kind::EXPONENTIAL); d_ee->addFunctionKind(kind::SINE); d_ee->addFunctionKind(kind::IAND); d_ee->addFunctionKind(kind::POW2); + // the proof equality engine is the one from the equality engine + d_pfee = d_ee->getProofEqualityEngine(); // have proof equality engine only if proofs are enabled - Assert(isProofEnabled() == (pfee != nullptr)); - d_pfee = pfee; + Assert(isProofEnabled() == (d_pfee != nullptr)); } ArithCongruenceManager::Statistics::Statistics() diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 4ab0b313b..2c59a405f 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -110,6 +110,8 @@ private: /** The equality engine being used by this class */ eq::EqualityEngine* d_ee; + /** The equality engine we allocated */ + std::unique_ptr<eq::EqualityEngine> d_allocEe; /** The sat context */ context::Context* d_satContext; /** The user context */ @@ -143,6 +145,8 @@ private: /** Pointer to the proof equality engine of TheoryArith */ theory::eq::ProofEqEngine* d_pfee; + /** The proof equality engine we allocated */ + std::unique_ptr<eq::ProofEqEngine> d_allocPfee; /** Raise a conflict node `conflict` to the theory of arithmetic. * @@ -240,9 +244,9 @@ private: bool needsEqualityEngine(EeSetupInfo& esi); /** * Finish initialize. This class is instructed by TheoryArithPrivate to use - * the equality engine ee and proof equality engine pfee. + * the equality engine ee. */ - void finishInit(eq::EqualityEngine* ee, eq::ProofEqEngine* pfee); + void finishInit(eq::EqualityEngine* ee); //--------------------------------- end initialization /** diff --git a/src/theory/arith/equality_solver.cpp b/src/theory/arith/equality_solver.cpp index 58793c654..8b4e1b8dd 100644 --- a/src/theory/arith/equality_solver.cpp +++ b/src/theory/arith/equality_solver.cpp @@ -80,6 +80,11 @@ TrustNode EqualitySolver::explain(TNode lit) } bool EqualitySolver::propagateLit(Node lit) { + // if we've already propagated, ignore + if (d_aim.hasPropagated(lit)) + { + return true; + } // notice this is only used when ee-mode=distributed // remember that this was a literal we propagated Trace("arith-eq-solver-debug") << "propagate lit " << lit << std::endl; diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index 90c17be4a..9cb232908 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -27,7 +27,10 @@ namespace arith { InferenceManager::InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm) - : InferenceManagerBuffered(ta, astate, pnm, "theory::arith::") + : InferenceManagerBuffered(ta, astate, pnm, "theory::arith::"), + // currently must track propagated literals if using the equality solver + d_trackPropLits(options::arithEqSolver()), + d_propLits(astate.getSatContext()) { } @@ -146,6 +149,21 @@ bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem) return false; } +bool InferenceManager::propagateLit(TNode lit) +{ + if (d_trackPropLits) + { + d_propLits.insert(lit); + } + return TheoryInferenceManager::propagateLit(lit); +} + +bool InferenceManager::hasPropagated(TNode lit) const +{ + Assert(d_trackPropLits); + return d_propLits.find(lit) != d_propLits.end(); +} + } // namespace arith } // namespace theory } // namespace cvc5 diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index 7e103797e..eeb9d096f 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -97,6 +97,13 @@ class InferenceManager : public InferenceManagerBuffered /** Checks whether the given lemma is already present in the cache. */ virtual bool hasCachedLemma(TNode lem, LemmaProperty p) override; + /** overrides propagateLit to track which literals have been propagated */ + bool propagateLit(TNode lit) override; + /** + * Return true if we have propagated lit already. This call is only valid if + * d_trackPropLits is true. + */ + bool hasPropagated(TNode lit) const; protected: /** @@ -111,9 +118,12 @@ class InferenceManager : public InferenceManagerBuffered * conflict. */ bool isEntailedFalse(const SimpleTheoryLemma& lem); - /** The waiting lemmas. */ std::vector<std::unique_ptr<SimpleTheoryLemma>> d_waitingLem; + /** Whether we are tracking the set of propagated literals */ + bool d_trackPropLits; + /** The literals we have propagated */ + NodeSet d_propLits; }; } // namespace arith diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index fb9de9641..053b91d90 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -137,7 +137,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_partialModel, RaiseEqualityEngineConflict(*this), d_pnm), - d_cmEnabled(c, true), + d_cmEnabled(c, options::arithCongMan()), d_dualSimplex( d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), @@ -181,14 +181,20 @@ TheoryArithPrivate::~TheoryArithPrivate(){ bool TheoryArithPrivate::needsEqualityEngine(EeSetupInfo& esi) { + if (!d_cmEnabled) + { + return false; + } return d_congruenceManager.needsEqualityEngine(esi); } void TheoryArithPrivate::finishInit() { - eq::EqualityEngine* ee = d_containing.getEqualityEngine(); - eq::ProofEqEngine* pfee = d_containing.getProofEqEngine(); - Assert(ee != nullptr); - d_congruenceManager.finishInit(ee, pfee); + if (d_cmEnabled) + { + eq::EqualityEngine* ee = d_containing.getEqualityEngine(); + Assert(ee != nullptr); + d_congruenceManager.finishInit(ee); + } } static bool contains(const ConstraintCPVec& v, ConstraintP con){ diff --git a/src/theory/arrays/proof_checker.cpp b/src/theory/arrays/proof_checker.cpp index f8c5b2669..6d546d746 100644 --- a/src/theory/arrays/proof_checker.cpp +++ b/src/theory/arrays/proof_checker.cpp @@ -14,8 +14,10 @@ */ #include "theory/arrays/proof_checker.h" + #include "expr/skolem_manager.h" #include "theory/arrays/skolem_cache.h" +#include "theory/arrays/theory_arrays_rewriter.h" #include "theory/rewriter.h" namespace cvc5 { @@ -28,6 +30,7 @@ void ArraysProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_CONTRA, this); pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_1, this); pc->registerChecker(PfRule::ARRAYS_EXT, this); + pc->registerChecker(PfRule::ARRAYS_EQ_RANGE_EXPAND, this); // trusted rules pc->registerTrustedChecker(PfRule::ARRAYS_TRUST, this, 2); } @@ -103,6 +106,11 @@ Node ArraysProofRuleChecker::checkInternal(PfRule id, Node bs = nm->mkNode(kind::SELECT, b, k); return as.eqNode(bs).notNode(); } + if (id == PfRule::ARRAYS_EQ_RANGE_EXPAND) + { + Node expandedEqRange = TheoryArraysRewriter::expandEqRange(args[0]); + return args[0].eqNode(expandedEqRange); + } if (id == PfRule::ARRAYS_TRUST) { // "trusted" rules diff --git a/src/theory/arrays/skolem_cache.cpp b/src/theory/arrays/skolem_cache.cpp index 19ab1aaae..7cf192b7f 100644 --- a/src/theory/arrays/skolem_cache.cpp +++ b/src/theory/arrays/skolem_cache.cpp @@ -35,6 +35,14 @@ struct ExtIndexVarAttributeId }; typedef expr::Attribute<ExtIndexVarAttributeId, Node> ExtIndexVarAttribute; +/** + * A bound variable corresponding to the index used in the eqrange expansion. + */ +struct EqRangeVarAttributeId +{ +}; +typedef expr::Attribute<EqRangeVarAttributeId, Node> EqRangeVarAttribute; + SkolemCache::SkolemCache() {} Node SkolemCache::getExtIndexSkolem(Node deq) @@ -66,6 +74,13 @@ Node SkolemCache::getExtIndexSkolem(Node deq) "an extensional lemma index variable from the theory of arrays"); } +Node SkolemCache::getEqRangeVar(TNode eqr) +{ + Assert(eqr.getKind() == kind::EQ_RANGE); + BoundVarManager* bvm = NodeManager::currentNM()->getBoundVarManager(); + return bvm->mkBoundVar<EqRangeVarAttribute>(eqr, eqr[2].getType()); +} + Node SkolemCache::getExtIndexVar(Node deq) { Node a = deq[0][0]; diff --git a/src/theory/arrays/skolem_cache.h b/src/theory/arrays/skolem_cache.h index 12578c01f..17a5c6975 100644 --- a/src/theory/arrays/skolem_cache.h +++ b/src/theory/arrays/skolem_cache.h @@ -43,6 +43,13 @@ class SkolemCache */ static Node getExtIndexSkolem(Node deq); + /** + * Get the bound variable for given EQ_RANGE operator. This bound variable + * is unique for `eqr`. Calling this method will always return the same bound + * variable over the lifetime of `eqr`. + */ + static Node getEqRangeVar(TNode eqr); + private: /** * Get the bound variable x of the witness term above for disequality deq diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index be8e1a08e..8fa7e0fd3 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -85,6 +85,7 @@ TheoryArrays::TheoryArrays(context::Context* c, name + "number of setModelVal conflicts")), d_ppEqualityEngine(u, name + "pp", true), d_ppFacts(u), + d_rewriter(pnm), d_state(c, u, valuation), d_im(*this, d_state, pnm), d_literalsToPropagate(c), diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index 1072ffaf4..dd7a56d33 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -20,6 +20,9 @@ #include "expr/array_store_all.h" #include "expr/attribute.h" +#include "proof/conv_proof_generator.h" +#include "proof/eager_proof_generator.h" +#include "theory/arrays/skolem_cache.h" #include "util/cardinality.h" namespace cvc5 { @@ -48,6 +51,11 @@ void setMostFrequentValueCount(TNode store, uint64_t count) { return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count); } +TheoryArraysRewriter::TheoryArraysRewriter(ProofNodeManager* pnm) + : d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr) +{ +} + Node TheoryArraysRewriter::normalizeConstant(TNode node) { return normalizeConstant(node, node[1].getType().getCardinality()); @@ -271,6 +279,48 @@ Node TheoryArraysRewriter::normalizeConstant(TNode node, Cardinality indexCard) return n; } +Node TheoryArraysRewriter::expandEqRange(TNode node) +{ + Assert(node.getKind() == kind::EQ_RANGE); + + NodeManager* nm = NodeManager::currentNM(); + TNode a = node[0]; + TNode b = node[1]; + TNode i = node[2]; + TNode j = node[3]; + Node k = SkolemCache::getEqRangeVar(node); + Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, k); + TypeNode type = k.getType(); + + Kind kle; + Node range; + if (type.isBitVector()) + { + kle = kind::BITVECTOR_ULE; + } + else if (type.isFloatingPoint()) + { + kle = kind::FLOATINGPOINT_LEQ; + } + else if (type.isInteger() || type.isReal()) + { + kle = kind::LEQ; + } + else + { + Unimplemented() << "Type " << type << " is not supported for predicate " + << node.getKind(); + } + + range = nm->mkNode(kind::AND, nm->mkNode(kle, i, k), nm->mkNode(kle, k, j)); + + Node eq = nm->mkNode(kind::EQUAL, + nm->mkNode(kind::SELECT, a, k), + nm->mkNode(kind::SELECT, b, k)); + Node implies = nm->mkNode(kind::IMPLIES, range, eq); + return nm->mkNode(kind::FORALL, bvl, implies); +} + RewriteResponse TheoryArraysRewriter::postRewrite(TNode node) { Trace("arrays-postrewrite") @@ -610,57 +660,22 @@ RewriteResponse TheoryArraysRewriter::preRewrite(TNode node) TrustNode TheoryArraysRewriter::expandDefinition(Node node) { - NodeManager* nm = NodeManager::currentNM(); Kind kind = node.getKind(); - /* Expand - * - * (eqrange a b i j) - * - * to - * - * forall k . i <= k <= j => a[k] = b[k] - * - */ if (kind == kind::EQ_RANGE) { - TNode a = node[0]; - TNode b = node[1]; - TNode i = node[2]; - TNode j = node[3]; - Node k = nm->mkBoundVar(i.getType()); - Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, k); - TypeNode type = k.getType(); - - Kind kle; - Node range; - if (type.isBitVector()) - { - kle = kind::BITVECTOR_ULE; - } - else if (type.isFloatingPoint()) + Node expandedEqRange = expandEqRange(node); + if (d_epg) { - kle = kind::FLOATINGPOINT_LEQ; + TrustNode tn = d_epg->mkTrustNode(node.eqNode(expandedEqRange), + PfRule::ARRAYS_EQ_RANGE_EXPAND, + {}, + {node}); + return TrustNode::mkTrustRewrite(node, expandedEqRange, d_epg.get()); } - else if (type.isInteger() || type.isReal()) - { - kle = kind::LEQ; - } - else - { - Unimplemented() << "Type " << type << " is not supported for predicate " - << kind; - } - - range = nm->mkNode(kind::AND, nm->mkNode(kle, i, k), nm->mkNode(kle, k, j)); - - Node eq = nm->mkNode(kind::EQUAL, - nm->mkNode(kind::SELECT, a, k), - nm->mkNode(kind::SELECT, b, k)); - Node implies = nm->mkNode(kind::IMPLIES, range, eq); - Node ret = nm->mkNode(kind::FORALL, bvl, implies); - return TrustNode::mkTrustRewrite(node, ret, nullptr); + return TrustNode::mkTrustRewrite(node, expandedEqRange, nullptr); } + return TrustNode::null(); } diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 498266ce3..95a19004e 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -29,6 +29,9 @@ #include "theory/type_enumerator.h" namespace cvc5 { + +class EagerProofGenerator; + namespace theory { namespace arrays { @@ -43,16 +46,18 @@ static inline Node mkEqNode(Node a, Node b) { class TheoryArraysRewriter : public TheoryRewriter { - /** - * Puts array constant node into normal form. This is so that array constants - * that are distinct nodes are semantically disequal. - */ - static Node normalizeConstant(TNode node); - public: + TheoryArraysRewriter(ProofNodeManager* pnm); + /** Normalize a constant whose index type has cardinality indexCard */ static Node normalizeConstant(TNode node, Cardinality indexCard); + /* Expands the eqrange predicate (eqrange a b i j) to the quantified formula + * (forall ((x T)) + * (=> (and (<= i x) (<= x j)) (= (select a x) (select b x)))). + */ + static Node expandEqRange(TNode node); + RewriteResponse postRewrite(TNode node) override; RewriteResponse preRewrite(TNode node) override; @@ -62,6 +67,14 @@ class TheoryArraysRewriter : public TheoryRewriter static inline void init() {} static inline void shutdown() {} + private: + /** + * Puts array constant node into normal form. This is so that array constants + * that are distinct nodes are semantically disequal. + */ + static Node normalizeConstant(TNode node); + + std::unique_ptr<EagerProofGenerator> d_epg; }; /* class TheoryArraysRewriter */ } // namespace arrays diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index c2aa9eb1e..580d26c08 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -35,7 +35,7 @@ TheoryBags::TheoryBags(context::Context* c, ProofNodeManager* pnm) : Theory(THEORY_BAGS, c, u, out, valuation, logicInfo, pnm), d_state(c, u, valuation), - d_im(*this, d_state, nullptr), + d_im(*this, d_state, pnm), d_ig(&d_state, &d_im), d_notify(*this, d_im), d_statistics(), diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index dae3922e6..54d1779ec 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -53,6 +53,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1); pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1); pc->registerTrustedChecker(PfRule::TRUST_SUBS_EQ, this, 3); + pc->registerTrustedChecker(PfRule::THEORY_INFERENCE, this, 3); } Node BuiltinProofRuleChecker::applySubstitutionRewrite( @@ -400,7 +401,8 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, || id == PfRule::THEORY_EXPAND_DEF || id == PfRule::WITNESS_AXIOM || id == PfRule::THEORY_LEMMA || id == PfRule::THEORY_REWRITE || id == PfRule::TRUST_REWRITE || id == PfRule::TRUST_SUBS - || id == PfRule::TRUST_SUBS_MAP || id == PfRule::TRUST_SUBS_EQ) + || id == PfRule::TRUST_SUBS_MAP || id == PfRule::TRUST_SUBS_EQ + || id == PfRule::THEORY_INFERENCE) { // "trusted" rules Assert(!args.empty()); diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp index f714ffda9..43618974b 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.cpp +++ b/src/theory/bv/bitblast/proof_bitblaster.cpp @@ -172,6 +172,11 @@ Node BBProof::getStoredBBAtom(TNode node) return d_bb->getStoredBBAtom(node); } +void BBProof::getBBTerm(TNode node, Bits& bits) const +{ + d_bb->getBBTerm(node, bits); +} + bool BBProof::collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms) { diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h index f6aa71f21..bc99d27bf 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.h +++ b/src/theory/bv/bitblast/proof_bitblaster.h @@ -43,6 +43,8 @@ class BBProof bool hasBBTerm(TNode node) const; /** Get bit-blasted node stored for atom. */ Node getStoredBBAtom(TNode node); + /** Get bit-blasted bits stored for node. */ + void getBBTerm(TNode node, Bits& bits) const; /** Collect model values for all relevant terms given in 'relevantTerms'. */ bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms); diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h index 6ccc6c7c1..c959fb648 100644 --- a/src/theory/bv/bv_solver.h +++ b/src/theory/bv/bv_solver.h @@ -102,6 +102,14 @@ class BVSolver return EqualityStatus::EQUALITY_UNKNOWN; } + /** + * Get the current value of `node`. + * + * The `initialize` flag indicates whether bits should be zero-initialized + * if they don't have a value yet. + */ + virtual Node getValue(TNode node, bool initialize) { return Node::null(); } + /** Called by abstraction preprocessing pass. */ virtual bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index 5b70fb3a2..ecd42e4a0 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -119,8 +119,6 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s, d_bbInputFacts(s->getSatContext()), d_assumptions(s->getSatContext()), d_assertions(s->getSatContext()), - d_invalidateModelCache(s->getSatContext(), true), - d_inSatMode(s->getSatContext(), false), d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "") : nullptr), d_factLiteralCache(s->getSatContext()), @@ -208,12 +206,9 @@ void BVSolverBitblast::postCheck(Theory::Effort level) d_assumptions.push_back(d_factLiteralCache[fact]); } - d_invalidateModelCache.set(true); std::vector<prop::SatLiteral> assumptions(d_assumptions.begin(), d_assumptions.end()); prop::SatValue val = d_satSolver->solve(assumptions); - d_inSatMode = val == prop::SatValue::SAT_VALUE_TRUE; - Debug("bv-bitblast") << "d_inSatMode: " << d_inSatMode << std::endl; if (val == prop::SatValue::SAT_VALUE_FALSE) { @@ -298,7 +293,7 @@ bool BVSolverBitblast::collectModelValues(TheoryModel* m, continue; } - Node value = getValueFromSatSolver(term, true); + Node value = getValue(term, true); Assert(value.isConst()); if (!m->assertEquality(term, value, true)) { @@ -330,27 +325,6 @@ bool BVSolverBitblast::collectModelValues(TheoryModel* m, return true; } -EqualityStatus BVSolverBitblast::getEqualityStatus(TNode a, TNode b) -{ - Debug("bv-bitblast") << "getEqualityStatus on " << a << " and " << b - << std::endl; - if (!d_inSatMode) - { - Debug("bv-bitblast") << EQUALITY_UNKNOWN << std::endl; - return EQUALITY_UNKNOWN; - } - Node value_a = getValue(a); - Node value_b = getValue(b); - - if (value_a == value_b) - { - Debug("bv-bitblast") << EQUALITY_TRUE_IN_MODEL << std::endl; - return EQUALITY_TRUE_IN_MODEL; - } - Debug("bv-bitblast") << EQUALITY_FALSE_IN_MODEL << std::endl; - return EQUALITY_FALSE_IN_MODEL; -} - void BVSolverBitblast::initSatSolver() { switch (options::bvSatSolver()) @@ -372,7 +346,7 @@ void BVSolverBitblast::initSatSolver() "theory::bv::BVSolverBitblast")); } -Node BVSolverBitblast::getValueFromSatSolver(TNode node, bool initialize) +Node BVSolverBitblast::getValue(TNode node, bool initialize) { if (node.isConst()) { @@ -405,76 +379,6 @@ Node BVSolverBitblast::getValueFromSatSolver(TNode node, bool initialize) return utils::mkConst(bits.size(), value); } -Node BVSolverBitblast::getValue(TNode node) -{ - if (d_invalidateModelCache.get()) - { - d_modelCache.clear(); - } - d_invalidateModelCache.set(false); - - std::vector<TNode> visit; - - TNode cur; - visit.push_back(node); - do - { - cur = visit.back(); - visit.pop_back(); - - auto it = d_modelCache.find(cur); - if (it != d_modelCache.end() && !it->second.isNull()) - { - continue; - } - - if (d_bitblaster->hasBBTerm(cur)) - { - Node value = getValueFromSatSolver(cur, false); - if (value.isConst()) - { - d_modelCache[cur] = value; - continue; - } - } - if (Theory::isLeafOf(cur, theory::THEORY_BV)) - { - Node value = getValueFromSatSolver(cur, true); - d_modelCache[cur] = value; - continue; - } - - if (it == d_modelCache.end()) - { - visit.push_back(cur); - d_modelCache.emplace(cur, Node()); - visit.insert(visit.end(), cur.begin(), cur.end()); - } - else if (it->second.isNull()) - { - NodeBuilder nb(cur.getKind()); - if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) - { - nb << cur.getOperator(); - } - - std::unordered_map<Node, Node>::iterator iit; - for (const TNode& child : cur) - { - iit = d_modelCache.find(child); - Assert(iit != d_modelCache.end()); - Assert(iit->second.isConst()); - nb << iit->second; - } - it->second = Rewriter::rewrite(nb.constructNode()); - } - } while (!visit.empty()); - - auto it = d_modelCache.find(node); - Assert(it != d_modelCache.end()); - return it->second; -} - void BVSolverBitblast::handleEagerAtom(TNode fact, bool assertFact) { Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM); diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 87f3f25cd..3f4ab5025 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -63,31 +63,22 @@ class BVSolverBitblast : public BVSolver std::string identify() const override { return "BVSolverBitblast"; }; - EqualityStatus getEqualityStatus(TNode a, TNode b) override; - void computeRelevantTerms(std::set<Node>& termSet) override; bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet) override; - private: - /** Initialize SAT solver and CNF stream. */ - void initSatSolver(); - /** - * Get value of `node` from SAT solver. + * Get the current value of `node`. * * The `initialize` flag indicates whether bits should be zero-initialized * if they were not bit-blasted yet. */ - Node getValueFromSatSolver(TNode node, bool initialize); + Node getValue(TNode node, bool initialize) override; - /** - * Get the current value of `node`. - * - * Computes the value if `node` was not yet bit-blasted. - */ - Node getValue(TNode node); + private: + /** Initialize SAT solver and CNF stream. */ + void initSatSolver(); /** * Handle BITVECTOR_EAGER_ATOM atoms and assert/assume to CnfStream. @@ -97,14 +88,6 @@ class BVSolverBitblast : public BVSolver */ void handleEagerAtom(TNode fact, bool assertFact); - /** - * Cache for getValue() calls. - * - * Is cleared at the beginning of a getValue() call if the - * `d_invalidateModelCache` flag is set to true. - */ - std::unordered_map<Node, Node> d_modelCache; - /** Bit-blaster used to bit-blast atoms/terms. */ std::unique_ptr<NodeBitblaster> d_bitblaster; @@ -120,7 +103,7 @@ class BVSolverBitblast : public BVSolver /** * Bit-blast queue for facts sent to this solver. * - * Get populated on preNotifyFact(). + * Gets populated on preNotifyFact(). */ context::CDQueue<Node> d_bbFacts; @@ -137,12 +120,6 @@ class BVSolverBitblast : public BVSolver /** Stores the current input assertions. */ context::CDList<Node> d_assertions; - /** Flag indicating whether `d_modelCache` should be invalidated. */ - context::CDO<bool> d_invalidateModelCache; - - /** Indicates whether the last check() call was satisfiable. */ - context::CDO<bool> d_inSatMode; - /** Proof generator that manages proofs for lemmas generated by this class. */ std::unique_ptr<EagerProofGenerator> d_epg; diff --git a/src/theory/bv/bv_solver_bitblast_internal.cpp b/src/theory/bv/bv_solver_bitblast_internal.cpp index bd47cc45e..ef4f3559b 100644 --- a/src/theory/bv/bv_solver_bitblast_internal.cpp +++ b/src/theory/bv/bv_solver_bitblast_internal.cpp @@ -147,6 +147,40 @@ bool BVSolverBitblastInternal::collectModelValues(TheoryModel* m, return d_bitblaster->collectModelValues(m, termSet); } +Node BVSolverBitblastInternal::getValue(TNode node, bool initialize) +{ + if (node.isConst()) + { + return node; + } + + if (!d_bitblaster->hasBBTerm(node)) + { + return initialize ? utils::mkConst(utils::getSize(node), 0u) : Node(); + } + + Valuation& val = d_state.getValuation(); + + std::vector<Node> bits; + d_bitblaster->getBBTerm(node, bits); + Integer value(0), one(1), zero(0), bit; + for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j) + { + bool satValue; + if (val.hasSatValue(bits[j], satValue)) + { + bit = satValue ? one : zero; + } + else + { + if (!initialize) return Node(); + bit = zero; + } + value = value * 2 + bit; + } + return utils::mkConst(bits.size(), value); +} + BVProofRuleChecker* BVSolverBitblastInternal::getProofChecker() { return &d_checker; diff --git a/src/theory/bv/bv_solver_bitblast_internal.h b/src/theory/bv/bv_solver_bitblast_internal.h index 8a1886084..1ec3ec1fe 100644 --- a/src/theory/bv/bv_solver_bitblast_internal.h +++ b/src/theory/bv/bv_solver_bitblast_internal.h @@ -42,6 +42,8 @@ class BVSolverBitblastInternal : public BVSolver ProofNodeManager* pnm); ~BVSolverBitblastInternal() = default; + bool needsEqualityEngine(EeSetupInfo& esi) override { return true; } + void preRegisterTerm(TNode n) override {} bool preNotifyFact(TNode atom, @@ -55,6 +57,8 @@ class BVSolverBitblastInternal : public BVSolver bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet) override; + Node getValue(TNode node, bool initialize) override; + /** get the proof checker of this theory */ BVProofRuleChecker* getProofChecker(); diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 37881f9b2..547d24b23 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -43,6 +43,7 @@ TheoryBV::TheoryBV(context::Context* c, d_state(c, u, valuation), d_im(*this, d_state, nullptr, "theory::bv::"), d_notify(d_im), + d_invalidateModelCache(c, true), d_stats("theory::bv::") { switch (options::bvSolver()) @@ -158,7 +159,11 @@ void TheoryBV::preRegisterTerm(TNode node) bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); } -void TheoryBV::postCheck(Effort e) { d_internal->postCheck(e); } +void TheoryBV::postCheck(Effort e) +{ + d_invalidateModelCache = true; + d_internal->postCheck(e); +} bool TheoryBV::preNotifyFact( TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) @@ -282,7 +287,27 @@ void TheoryBV::presolve() { d_internal->presolve(); } EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) { - return d_internal->getEqualityStatus(a, b); + EqualityStatus status = d_internal->getEqualityStatus(a, b); + + if (status == EqualityStatus::EQUALITY_UNKNOWN) + { + Node value_a = getValue(a); + Node value_b = getValue(b); + + if (value_a.isNull() || value_b.isNull()) + { + return status; + } + + if (value_a == value_b) + { + Debug("theory-bv") << EQUALITY_TRUE_IN_MODEL << std::endl; + return EQUALITY_TRUE_IN_MODEL; + } + Debug("theory-bv") << EQUALITY_FALSE_IN_MODEL << std::endl; + return EQUALITY_FALSE_IN_MODEL; + } + return status; } TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); } @@ -303,6 +328,80 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, return d_internal->applyAbstraction(assertions, new_assertions); } +Node TheoryBV::getValue(TNode node) +{ + if (d_invalidateModelCache.get()) + { + d_modelCache.clear(); + } + d_invalidateModelCache.set(false); + + std::vector<TNode> visit; + + TNode cur; + visit.push_back(node); + do + { + cur = visit.back(); + visit.pop_back(); + + auto it = d_modelCache.find(cur); + if (it != d_modelCache.end() && !it->second.isNull()) + { + continue; + } + + if (cur.isConst()) + { + d_modelCache[cur] = cur; + continue; + } + + Node value = d_internal->getValue(cur, false); + if (value.isConst()) + { + d_modelCache[cur] = value; + continue; + } + + if (Theory::isLeafOf(cur, theory::THEORY_BV)) + { + value = d_internal->getValue(cur, true); + d_modelCache[cur] = value; + continue; + } + + if (it == d_modelCache.end()) + { + visit.push_back(cur); + d_modelCache.emplace(cur, Node()); + visit.insert(visit.end(), cur.begin(), cur.end()); + } + else if (it->second.isNull()) + { + NodeBuilder nb(cur.getKind()); + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) + { + nb << cur.getOperator(); + } + + std::unordered_map<Node, Node>::iterator iit; + for (const TNode& child : cur) + { + iit = d_modelCache.find(child); + Assert(iit != d_modelCache.end()); + Assert(iit->second.isConst()); + nb << iit->second; + } + it->second = Rewriter::rewrite(nb.constructNode()); + } + } while (!visit.empty()); + + auto it = d_modelCache.find(node); + Assert(it != d_modelCache.end()); + return it->second; +} + TheoryBV::Statistics::Statistics(const std::string& name) : d_solveSubstitutions( smtStatisticsRegistry().registerInt(name + "NumSolveSubstitutions")) diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index f2d6bb47e..da44d7022 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -109,6 +109,8 @@ class TheoryBV : public Theory private: void notifySharedTerm(TNode t) override; + Node getValue(TNode node); + /** Internal BV solver. */ std::unique_ptr<BVSolver> d_internal; @@ -124,6 +126,17 @@ class TheoryBV : public Theory /** The notify class for equality engine. */ TheoryEqNotifyClass d_notify; + /** Flag indicating whether `d_modelCache` should be invalidated. */ + context::CDO<bool> d_invalidateModelCache; + + /** + * Cache for getValue() calls. + * + * Is cleared at the beginning of a getValue() call if the + * `d_invalidateModelCache` flag is set to true. + */ + std::unordered_map<Node, Node> d_modelCache; + /** TheoryBV statistics. */ struct Statistics { diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 014255a7c..ccd0e6853 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -69,6 +69,13 @@ void InferenceManager::addPendingInference(Node conc, void InferenceManager::process() { + // if we are in conflict, immediately reset and clear pending + if (d_theoryState.isInConflict()) + { + reset(); + clearPending(); + return; + } // process pending lemmas, used infrequently, only for definitional lemmas doPendingLemmas(); // now process the pending facts diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index 7e5099d55..72ddd7b0e 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -718,6 +718,24 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, return sdtS; } +unsigned getSygusTermSize(Node n) +{ + if (n.getKind() != APPLY_CONSTRUCTOR) + { + return 0; + } + unsigned sum = 0; + for (const Node& nc : n) + { + sum += getSygusTermSize(nc); + } + const DType& dt = datatypeOf(n.getOperator()); + int cindex = indexOf(n.getOperator()); + Assert(cindex >= 0 && static_cast<size_t>(cindex) < dt.getNumConstructors()); + unsigned weight = dt[cindex].getWeight(); + return weight + sum; +} + } // namespace utils } // namespace datatypes } // namespace theory diff --git a/src/theory/datatypes/sygus_datatype_utils.h b/src/theory/datatypes/sygus_datatype_utils.h index 6f3791a4d..35672434c 100644 --- a/src/theory/datatypes/sygus_datatype_utils.h +++ b/src/theory/datatypes/sygus_datatype_utils.h @@ -227,6 +227,11 @@ TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, const std::vector<Node>& syms, const std::vector<Node>& vars); +/** + * Get SyGuS term size, which is based on the weight of constructor applications + * in n. + */ +unsigned getSygusTermSize(Node n); // ------------------------ end sygus utils } // namespace utils diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index ee96b95d8..63af57592 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -1040,7 +1040,7 @@ Node SygusExtension::registerSearchValue(Node a, Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv); Trace("sygus-sb-debug") << " ......search value rewrites to " << bvr << std::endl; Trace("dt-sygus") << " * DT builtin : " << n << " -> " << bvr << std::endl; - unsigned sz = d_tds->getSygusTermSize( nv ); + unsigned sz = utils::getSygusTermSize(nv); if( d_tds->involvesDivByZero( bvr ) ){ quantifiers::DivByZeroSygusInvarianceTest dbzet; Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in " @@ -1143,7 +1143,7 @@ Node SygusExtension::registerSearchValue(Node a, } Trace("sygus-sb-exc") << std::endl; } - Assert(d_tds->getSygusTermSize(bad_val) == sz); + Assert(utils::getSygusTermSize(bad_val) == sz); // generalize the explanation for why the analog of bad_val // is equivalent to bvr @@ -1177,7 +1177,7 @@ void SygusExtension::registerSymBreakLemmaForValue( { TypeNode tn = val.getType(); Node x = getFreeVar(tn); - unsigned sz = d_tds->getSygusTermSize(val); + unsigned sz = utils::getSygusTermSize(val); std::vector<Node> exp; d_tds->getExplain()->getExplanationFor(x, val, exp, et, valr, var_count, sz); Node lem = diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 53f128286..50c955d48 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -168,13 +168,17 @@ TNode TheoryDatatypes::getEqcConstructor( TNode r ) { bool TheoryDatatypes::preCheck(Effort level) { + Trace("datatypes-check") << "TheoryDatatypes::preCheck: " << level + << std::endl; + d_im.process(); d_im.reset(); - d_im.clearPending(); return false; } void TheoryDatatypes::postCheck(Effort level) { + Trace("datatypes-check") << "TheoryDatatypes::postCheck: " << level + << std::endl; // Apply any last pending inferences, which may occur if the last processed // fact was an internal one and triggered further internal inferences. d_im.process(); @@ -182,7 +186,6 @@ void TheoryDatatypes::postCheck(Effort level) { Assert(d_sygusExtension != nullptr); d_sygusExtension->check(); - return; } else if (level == EFFORT_FULL && !d_state.isInConflict() && !d_im.hasSentLemma() && !d_valuation.needCheck()) @@ -532,18 +535,19 @@ void TheoryDatatypes::eqNotifyNewClass(TNode t){ void TheoryDatatypes::eqNotifyMerge(TNode t1, TNode t2) { if( t1.getType().isDatatype() ){ - Trace("datatypes-debug") + Trace("datatypes-merge") << "NotifyMerge : " << t1 << " " << t2 << std::endl; - merge(t1,t2); + merge(t1, t2); } } void TheoryDatatypes::merge( Node t1, Node t2 ){ if (!d_state.isInConflict()) { + Trace("datatypes-merge") << "Merge " << t1 << " " << t2 << std::endl; + Assert(areEqual(t1, t2)); TNode trep1 = t1; TNode trep2 = t2; - Trace("datatypes-debug") << "Merge " << t1 << " " << t2 << std::endl; EqcInfo* eqc2 = getOrMakeEqcInfo( t2 ); if( eqc2 ){ bool checkInst = false; @@ -575,6 +579,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ } else { + Assert(areEqual(cons1, cons2)); //do unification for( int i=0; i<(int)cons1.getNumChildren(); i++ ) { if( !areEqual( cons1[i], cons2[i] ) ){ @@ -1852,38 +1857,16 @@ void TheoryDatatypes::computeRelevantTerms(std::set<Node>& termSet) Trace("dt-cmi") << "Have " << termSet.size() << " relevant terms..." << std::endl; - //also include non-singleton equivalence classes TODO : revisit this + //also include non-singleton dt equivalence classes TODO : revisit this eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine); while( !eqcs_i.isFinished() ){ TNode r = (*eqcs_i); - bool addedFirst = false; - Node first; - TypeNode rtn = r.getType(); - if (!rtn.isBoolean()) + if (r.getType().isDatatype()) { eq::EqClassIterator eqc_i = eq::EqClassIterator(r, d_equalityEngine); while (!eqc_i.isFinished()) { - TNode n = (*eqc_i); - if (first.isNull()) - { - first = n; - // always include all datatypes - if (rtn.isDatatype()) - { - addedFirst = true; - termSet.insert(n); - } - } - else - { - if (!addedFirst) - { - addedFirst = true; - termSet.insert(first); - } - termSet.insert(n); - } + termSet.insert(*eqc_i); ++eqc_i; } } diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h index 898ee3491..705e867b9 100644 --- a/src/theory/datatypes/theory_datatypes_utils.h +++ b/src/theory/datatypes/theory_datatypes_utils.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H -#define CVC5__THEORY__STRINGS__THEORY_DATATYPES_UTILS_H +#ifndef CVC5__THEORY__DATATYPES__THEORY_DATATYPES_UTILS_H +#define CVC5__THEORY__DATATYPES__THEORY_DATATYPES_UTILS_H #include <vector> diff --git a/src/theory/ee_manager_central.cpp b/src/theory/ee_manager_central.cpp new file mode 100644 index 000000000..f98bce970 --- /dev/null +++ b/src/theory/ee_manager_central.cpp @@ -0,0 +1,306 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Equality engine manager for central equality engine architecture + */ + +#include "theory/ee_manager_central.h" + +#include "theory/quantifiers_engine.h" +#include "theory/shared_solver.h" +#include "theory/theory_engine.h" +#include "theory/theory_state.h" + +namespace cvc5 { +namespace theory { + +EqEngineManagerCentral::EqEngineManagerCentral(TheoryEngine& te, + SharedSolver& shs, + ProofNodeManager* pnm) + : EqEngineManager(te, shs), + d_masterEENotify(nullptr), + d_masterEqualityEngine(nullptr), + d_centralEENotify(*this), + d_centralEqualityEngine( + d_centralEENotify, te.getSatContext(), "central::ee", true) +{ + for (TheoryId theoryId = theory::THEORY_FIRST; + theoryId != theory::THEORY_LAST; + ++theoryId) + { + d_theoryNotify[theoryId] = nullptr; + } + if (pnm != nullptr) + { + d_centralPfee.reset(new eq::ProofEqEngine(d_te.getSatContext(), + d_te.getUserContext(), + d_centralEqualityEngine, + pnm)); + d_centralEqualityEngine.setProofEqualityEngine(d_centralPfee.get()); + } +} + +EqEngineManagerCentral::~EqEngineManagerCentral() {} + +void EqEngineManagerCentral::initializeTheories() +{ + context::Context* c = d_te.getSatContext(); + // initialize the shared solver + EeSetupInfo esis; + if (d_sharedSolver.needsEqualityEngine(esis)) + { + // the shared solver uses central equality engine + d_sharedSolver.setEqualityEngine(&d_centralEqualityEngine); + } + else + { + Unreachable() << "Expected shared solver to use equality engine"; + } + // whether to use master equality engine as central + bool masterEqToCentral = true; + // setup info for each theory + std::map<TheoryId, EeSetupInfo> esiMap; + // set of theories that need equality engines + std::unordered_set<TheoryId> eeTheories; + const LogicInfo& logicInfo = d_te.getLogicInfo(); + for (TheoryId theoryId = theory::THEORY_FIRST; + theoryId != theory::THEORY_LAST; + ++theoryId) + { + Theory* t = d_te.theoryOf(theoryId); + if (t == nullptr) + { + // theory not active, skip + continue; + } + if (!t->needsEqualityEngine(esiMap[theoryId])) + { + // theory said it doesn't need an equality engine, skip + continue; + } + // otherwise add it to the set of equality engine theories + eeTheories.insert(theoryId); + // if the logic has a theory that does not use central equality engine, + // we can't use the central equality engine for the master equality + // engine + if (theoryId != THEORY_QUANTIFIERS && logicInfo.isTheoryEnabled(theoryId) + && !Theory::usesCentralEqualityEngine(theoryId)) + { + Trace("ee-central") << "Must use separate master equality engine due to " + << theoryId << std::endl; + masterEqToCentral = false; + } + } + + // initialize the master equality engine, which may be the central equality + // engine + if (logicInfo.isQuantified()) + { + // construct the master equality engine + Assert(d_masterEqualityEngine == nullptr); + QuantifiersEngine* qe = d_te.getQuantifiersEngine(); + Assert(qe != nullptr); + d_masterEENotify.reset(new quantifiers::MasterNotifyClass(qe)); + if (!masterEqToCentral) + { + d_masterEqualityEngineAlloc.reset(new eq::EqualityEngine( + *d_masterEENotify.get(), d_te.getSatContext(), "master::ee", false)); + d_masterEqualityEngine = d_masterEqualityEngineAlloc.get(); + } + else + { + Trace("ee-central") + << "Master equality engine is the central equality engine" + << std::endl; + d_masterEqualityEngine = &d_centralEqualityEngine; + d_centralEENotify.d_newClassNotify.push_back(d_masterEENotify.get()); + } + } + + // allocate equality engines per theory + for (TheoryId theoryId = theory::THEORY_FIRST; + theoryId != theory::THEORY_LAST; + ++theoryId) + { + Trace("ee-central") << "Setup equality engine for " << theoryId + << std::endl; + // always allocate an object in d_einfo here + EeTheoryInfo& eet = d_einfo[theoryId]; + if (eeTheories.find(theoryId) == eeTheories.end()) + { + Trace("ee-central") << "..." << theoryId << " does not need ee" + << std::endl; + continue; + } + Theory* t = d_te.theoryOf(theoryId); + Assert(t != nullptr); + Assert(esiMap.find(theoryId) != esiMap.end()); + EeSetupInfo& esi = esiMap[theoryId]; + if (esi.d_useMaster) + { + Trace("ee-central") << "...uses master" << std::endl; + // the theory said it wants to use the master equality engine + eet.d_usedEe = d_masterEqualityEngine; + continue; + } + // set the notify + eq::EqualityEngineNotify* notify = esi.d_notify; + d_theoryNotify[theoryId] = notify; + // split on whether integrated, or whether asked for master + if (t->usesCentralEqualityEngine()) + { + Trace("ee-central") << "...uses central" << std::endl; + // the theory uses the central equality engine + eet.d_usedEe = &d_centralEqualityEngine; + if (logicInfo.isTheoryEnabled(theoryId)) + { + // add to vectors for the kinds of notifications + if (esi.needsNotifyNewClass()) + { + d_centralEENotify.d_newClassNotify.push_back(notify); + } + if (esi.needsNotifyMerge()) + { + d_centralEENotify.d_mergeNotify.push_back(notify); + } + if (esi.needsNotifyDisequal()) + { + d_centralEENotify.d_disequalNotify.push_back(notify); + } + } + continue; + } + Trace("ee-central") << "...uses new" << std::endl; + eet.d_allocEe.reset(allocateEqualityEngine(esi, c)); + // the theory uses the equality engine + eet.d_usedEe = eet.d_allocEe.get(); + if (!masterEqToCentral) + { + // set the master equality engine of the theory's equality engine + eet.d_allocEe->setMasterEqualityEngine(d_masterEqualityEngine); + } + } + + // set the master equality engine of the theory's equality engine + if (!masterEqToCentral) + { + d_centralEqualityEngine.setMasterEqualityEngine(d_masterEqualityEngine); + } +} + +void EqEngineManagerCentral::notifyBuildingModel() {} + +EqEngineManagerCentral::CentralNotifyClass::CentralNotifyClass( + EqEngineManagerCentral& eemc) + : d_eemc(eemc), d_mNotify(nullptr), d_quantEngine(nullptr) +{ +} + +bool EqEngineManagerCentral::CentralNotifyClass::eqNotifyTriggerPredicate( + TNode predicate, bool value) +{ + Trace("eem-central") << "eqNotifyTriggerPredicate: " << predicate + << std::endl; + return d_eemc.eqNotifyTriggerPredicate(predicate, value); +} + +bool EqEngineManagerCentral::CentralNotifyClass::eqNotifyTriggerTermEquality( + TheoryId tag, TNode t1, TNode t2, bool value) +{ + Trace("eem-central") << "eqNotifyTriggerTermEquality: " << t1 << " " << t2 + << value << ", tag = " << tag << std::endl; + return d_eemc.eqNotifyTriggerTermEquality(tag, t1, t2, value); +} + +void EqEngineManagerCentral::CentralNotifyClass::eqNotifyConstantTermMerge( + TNode t1, TNode t2) +{ + Trace("eem-central") << "eqNotifyConstantTermMerge: " << t1 << " " << t2 + << std::endl; + d_eemc.eqNotifyConstantTermMerge(t1, t2); +} + +void EqEngineManagerCentral::CentralNotifyClass::eqNotifyNewClass(TNode t) +{ + Trace("eem-central") << "...eqNotifyNewClass " << t << std::endl; + // notify all theories that have new equivalence class notifications + for (eq::EqualityEngineNotify* notify : d_newClassNotify) + { + notify->eqNotifyNewClass(t); + } +} + +void EqEngineManagerCentral::CentralNotifyClass::eqNotifyMerge(TNode t1, + TNode t2) +{ + Trace("eem-central") << "...eqNotifyMerge " << t1 << ", " << t2 << std::endl; + // notify all theories that have merge notifications + for (eq::EqualityEngineNotify* notify : d_mergeNotify) + { + notify->eqNotifyMerge(t1, t2); + } +} + +void EqEngineManagerCentral::CentralNotifyClass::eqNotifyDisequal(TNode t1, + TNode t2, + TNode reason) +{ + Trace("eem-central") << "...eqNotifyDisequal " << t1 << ", " << t2 + << std::endl; + // notify all theories that have disequal notifications + for (eq::EqualityEngineNotify* notify : d_disequalNotify) + { + notify->eqNotifyDisequal(t1, t2, reason); + } +} + +bool EqEngineManagerCentral::eqNotifyTriggerPredicate(TNode predicate, + bool value) +{ + // always propagate with the shared solver + Trace("eem-central") << "...propagate " << predicate << ", " << value + << " with shared solver" << std::endl; + return d_sharedSolver.propagateLit(predicate, value); +} + +bool EqEngineManagerCentral::eqNotifyTriggerTermEquality(TheoryId tag, + TNode a, + TNode b, + bool value) +{ + // propagate to theory engine + bool ok = d_sharedSolver.propagateLit(a.eqNode(b), value); + if (!ok) + { + return false; + } + // no need to propagate shared term equalities to the UF theory + if (tag == THEORY_UF) + { + return true; + } + // propagate shared equality + return d_sharedSolver.propagateSharedEquality(tag, a, b, value); +} + +void EqEngineManagerCentral::eqNotifyConstantTermMerge(TNode t1, TNode t2) +{ + Node lit = t1.eqNode(t2); + Node conflict = d_centralEqualityEngine.mkExplainLit(lit); + Trace("eem-central") << "...explained conflict of " << lit << " ... " + << conflict << std::endl; + d_sharedSolver.sendConflict(TrustNode::mkTrustConflict(conflict)); + return; +} + +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/ee_manager_central.h b/src/theory/ee_manager_central.h new file mode 100644 index 000000000..eb13b7820 --- /dev/null +++ b/src/theory/ee_manager_central.h @@ -0,0 +1,130 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Equality engine manager for central equality engine architecture + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__EE_MANAGER_CENTRAL__H +#define CVC5__THEORY__EE_MANAGER_CENTRAL__H + +#include <map> +#include <memory> + +#include "theory/ee_manager.h" +#include "theory/quantifiers/master_eq_notify.h" +#include "theory/uf/equality_engine.h" + +namespace cvc5 { +namespace theory { + +/** + * The (central) equality engine manager. This encapsulates an architecture + * in which all applicable theories use a single central equality engine. + * + * This class is not responsible for actually initializing equality engines in + * theories (since this class does not have access to the internals of Theory). + * Instead, it is only responsible for the construction of the equality + * engine objects themselves. TheoryEngine is responsible for querying this + * class during finishInit() to determine the equality engines to pass to each + * theories based on getEeTheoryInfo. + * + * It also may allocate a "master" equality engine, which is intuitively the + * equality engine of the theory of quantifiers. If all theories use the + * central equality engine, then the master equality engine is the same as the + * central equality engine. + * + * The theories that use central equality engine are determined by + * Theory::usesCentralEqualityEngine. + * + * The main idea behind this class is to use a notification class on the + * central equality engine which dispatches *multiple* notifications to the + * theories that use the central equality engine. + */ +class EqEngineManagerCentral : public EqEngineManager +{ + public: + EqEngineManagerCentral(TheoryEngine& te, + SharedSolver& shs, + ProofNodeManager* pnm); + ~EqEngineManagerCentral(); + /** + * Initialize theories. This method allocates unique equality engines + * per theories and connects them to a master equality engine. + */ + void initializeTheories() override; + /** Notify this class that we are building the model. */ + void notifyBuildingModel(); + + private: + /** + * Notify class for central equality engine. This class dispatches + * notifications from the central equality engine to the appropriate + * theory(s). + */ + class CentralNotifyClass : public theory::eq::EqualityEngineNotify + { + public: + CentralNotifyClass(EqEngineManagerCentral& eemc); + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override; + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value) override; + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override; + void eqNotifyNewClass(TNode t) override; + void eqNotifyMerge(TNode t1, TNode t2) override; + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override; + /** Parent */ + EqEngineManagerCentral& d_eemc; + /** List of notify classes that need new class notification */ + std::vector<eq::EqualityEngineNotify*> d_newClassNotify; + /** List of notify classes that need merge notification */ + std::vector<eq::EqualityEngineNotify*> d_mergeNotify; + /** List of notify classes that need disequality notification */ + std::vector<eq::EqualityEngineNotify*> d_disequalNotify; + /** The model notify class */ + eq::EqualityEngineNotify* d_mNotify; + /** The quantifiers engine */ + QuantifiersEngine* d_quantEngine; + }; + /** Notification when predicate gets value in central equality engine */ + bool eqNotifyTriggerPredicate(TNode predicate, bool value); + bool eqNotifyTriggerTermEquality(TheoryId tag, + TNode t1, + TNode t2, + bool value); + /** Notification when constants are merged in central equality engine */ + void eqNotifyConstantTermMerge(TNode t1, TNode t2); + /** The master equality engine notify class */ + std::unique_ptr<quantifiers::MasterNotifyClass> d_masterEENotify; + /** The master equality engine. */ + eq::EqualityEngine* d_masterEqualityEngine; + /** The master equality engine, if we allocated it */ + std::unique_ptr<eq::EqualityEngine> d_masterEqualityEngineAlloc; + /** The central equality engine notify class */ + CentralNotifyClass d_centralEENotify; + /** The central equality engine. */ + eq::EqualityEngine d_centralEqualityEngine; + /** The proof equality engine for the central equality engine */ + std::unique_ptr<eq::ProofEqEngine> d_centralPfee; + /** + * A table of from theory IDs to notify classes. + */ + eq::EqualityEngineNotify* d_theoryNotify[theory::THEORY_LAST]; +}; + +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__EE_MANAGER_CENTRAL__H */ diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index e309ab2e4..f6f1f3bb3 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -1296,15 +1296,18 @@ Node FpConverter::getValue(Valuation &val, TNode var) if (t.isRoundingMode()) { rmMap::const_iterator i(d_rmMap.find(var)); - - Assert(i != d_rmMap.end()) - << "Asking for the value of an unregistered expression"; + if (i == d_rmMap.end()) + { + return Node::null(); + } return rmToNode((*i).second); } - fpMap::const_iterator i(d_fpMap.find(var)); - Assert(i != d_fpMap.end()) - << "Asking for the value of an unregistered expression"; + fpMap::const_iterator i(d_fpMap.find(var)); + if (i == d_fpMap.end()) + { + return Node::null(); + } return ufToNode(fpt(t), (*i).second); } diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 9900c2987..d589eff60 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -300,7 +300,10 @@ class FpConverter /** Adds a node to the conversion, returns the converted node */ Node convert(TNode); - /** Gives the node representing the value of a given variable */ + /** + * Gives the node representing the value of a word-blasted variable. + * Returns a null node if it has not been word-blasted. + */ Node getValue(Valuation&, TNode); context::CDList<Node> d_additionalAssertions; diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 1c8f10f77..9b5ac66d3 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -76,12 +76,13 @@ TheoryFp::TheoryFp(context::Context* c, d_abstractionMap(u), d_rewriter(u), d_state(c, u, valuation), - d_im(*this, d_state, pnm, "theory::fp::", false) + d_im(*this, d_state, pnm, "theory::fp::", false), + d_wbFactsCache(u) { // indicate we are using the default theory state and inference manager d_theoryState = &d_state; d_inferManager = &d_im; -} /* TheoryFp::TheoryFp() */ +} TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; } @@ -304,6 +305,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) Node floatValue = m->getValue(concrete[0]); Node undefValue = m->getValue(concrete[1]); + Assert(!abstractValue.isNull()); + Assert(!floatValue.isNull()); + Assert(!undefValue.isNull()); Assert(abstractValue.isConst()); Assert(floatValue.isConst()); Assert(undefValue.isConst()); @@ -413,6 +417,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) Node rmValue = m->getValue(concrete[0]); Node realValue = m->getValue(concrete[1]); + Assert(!abstractValue.isNull()); + Assert(!rmValue.isNull()); + Assert(!realValue.isNull()); Assert(abstractValue.isConst()); Assert(rmValue.isConst()); Assert(realValue.isConst()); @@ -509,12 +516,16 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) return false; } -void TheoryFp::convertAndEquateTerm(TNode node) { +void TheoryFp::convertAndEquateTerm(TNode node) +{ Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl; - size_t oldAdditionalAssertions = d_conv->d_additionalAssertions.size(); + + size_t oldSize = d_conv->d_additionalAssertions.size(); Node converted(d_conv->convert(node)); + size_t newSize = d_conv->d_additionalAssertions.size(); + if (converted != node) { Debug("fp-convertTerm") << "TheoryFp::convertTerm(): before " << node << std::endl; @@ -522,12 +533,11 @@ void TheoryFp::convertAndEquateTerm(TNode node) { << "TheoryFp::convertTerm(): after " << converted << std::endl; } - size_t newAdditionalAssertions = d_conv->d_additionalAssertions.size(); - Assert(oldAdditionalAssertions <= newAdditionalAssertions); + Assert(oldSize <= newSize); - while (oldAdditionalAssertions < newAdditionalAssertions) + while (oldSize < newSize) { - Node addA = d_conv->d_additionalAssertions[oldAdditionalAssertions]; + Node addA = d_conv->d_additionalAssertions[oldSize]; Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion " << addA << std::endl; @@ -538,7 +548,7 @@ void TheoryFp::convertAndEquateTerm(TNode node) { nm->mkNode(kind::EQUAL, addA, nm->mkConst(::cvc5::BitVector(1U, 1U))), InferenceId::FP_EQUATE_TERM); - ++oldAdditionalAssertions; + ++oldSize; } // Equate the floating-point atom and the converted one. @@ -578,10 +588,12 @@ void TheoryFp::convertAndEquateTerm(TNode node) { return; } -void TheoryFp::registerTerm(TNode node) { +void TheoryFp::registerTerm(TNode node) +{ Trace("fp-registerTerm") << "TheoryFp::registerTerm(): " << node << std::endl; - if (!isRegistered(node)) { + if (!isRegistered(node)) + { Kind k = node.getKind(); Assert(k != kind::FLOATINGPOINT_TO_FP_GENERIC && k != kind::FLOATINGPOINT_SUB && k != kind::FLOATINGPOINT_EQ @@ -646,14 +658,19 @@ void TheoryFp::registerTerm(TNode node) { InferenceId::FP_REGISTER_TERM); } - // Use symfpu to produce an equivalent bit-vector statement - convertAndEquateTerm(node); + /* When not word-blasting lazier, we word-blast every term on + * registration. */ + if (!options::fpLazyWb()) + { + convertAndEquateTerm(node); + } } return; } -bool TheoryFp::isRegistered(TNode node) { - return !(d_registeredTerms.find(node) == d_registeredTerms.end()); +bool TheoryFp::isRegistered(TNode node) +{ + return d_registeredTerms.find(node) != d_registeredTerms.end(); } void TheoryFp::preRegisterTerm(TNode node) @@ -714,7 +731,7 @@ bool TheoryFp::needsCheckLastEffort() void TheoryFp::postCheck(Effort level) { - // Resolve the abstractions for the conversion lemmas + /* Resolve the abstractions for the conversion lemmas */ if (level == EFFORT_LAST_CALL) { Trace("fp") << "TheoryFp::check(): checking abstractions" << std::endl; @@ -739,6 +756,13 @@ void TheoryFp::postCheck(Effort level) bool TheoryFp::preNotifyFact( TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) { + /* Word-blast lazier if configured. */ + if (options::fpLazyWb() && d_wbFactsCache.find(atom) == d_wbFactsCache.end()) + { + d_wbFactsCache.insert(atom); + convertAndEquateTerm(atom); + } + if (atom.getKind() == kind::EQUAL) { Assert(!(atom[0].getType().isFloatingPoint() @@ -763,6 +787,16 @@ bool TheoryFp::preNotifyFact( return false; } +void TheoryFp::notifySharedTerm(TNode n) +{ + /* Word-blast lazier if configured. */ + if (options::fpLazyWb() && d_wbFactsCache.find(n) == d_wbFactsCache.end()) + { + d_wbFactsCache.insert(n); + convertAndEquateTerm(n); + } +} + TrustNode TheoryFp::explain(TNode n) { Trace("fp") << "TheoryFp::explain(): explain " << n << std::endl; @@ -846,7 +880,10 @@ bool TheoryFp::collectModelValues(TheoryModel* m, << "TheoryFp::collectModelInfo(): relevantVariable " << node << std::endl; - if (!m->assertEquality(node, d_conv->getValue(d_valuation, node), true)) + Node converted = d_conv->getValue(d_valuation, node); + // We only assign the value if the FpConverter actually has one, that is, + // if FpConverter::getValue() does not return a null node. + if (!converted.isNull() && !m->assertEquality(node, converted, true)) { return false; } diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index ada9b39d0..14779cc3d 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -114,6 +114,8 @@ class TheoryFp : public Theory }; friend NotifyClass; + void notifySharedTerm(TNode n) override; + NotifyClass d_notification; /** General utility. */ @@ -148,18 +150,19 @@ class TheoryFp : public Theory Node abstractFloatToReal(Node); private: - ConversionAbstractionMap d_realToFloatMap; ConversionAbstractionMap d_floatToRealMap; AbstractionMap d_abstractionMap; // abstract -> original /** The theory rewriter for this theory. */ TheoryFpRewriter d_rewriter; - /** A (default) theory state object */ + /** A (default) theory state object. */ TheoryState d_state; - /** A (default) inference manager */ + /** A (default) inference manager. */ TheoryInferenceManager d_im; -}; /* class TheoryFp */ + /** Cache of word-blasted facts. */ + context::CDHashSet<Node> d_wbFactsCache; +}; } // namespace fp } // namespace theory diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index a26147f09..c0700c06e 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -16,6 +16,7 @@ #include "theory/inference_id.h" #include <iostream> +#include "util/rational.h" namespace cvc5 { namespace theory { @@ -243,9 +244,11 @@ const char* toString(InferenceId i) case InferenceId::SEP_DISTINCT_REF: return "SEP_DISTINCT_REF"; case InferenceId::SEP_REF_BOUND: return "SEP_REF_BOUND"; + case InferenceId::SETS_CG_SPLIT: return "SETS_CG_SPLIT"; case InferenceId::SETS_COMPREHENSION: return "SETS_COMPREHENSION"; case InferenceId::SETS_DEQ: return "SETS_DEQ"; case InferenceId::SETS_DOWN_CLOSURE: return "SETS_DOWN_CLOSURE"; + case InferenceId::SETS_EQ_CONFLICT: return "SETS_EQ_CONFLICT"; case InferenceId::SETS_EQ_MEM: return "SETS_EQ_MEM"; case InferenceId::SETS_EQ_MEM_CONFLICT: return "SETS_EQ_MEM_CONFLICT"; case InferenceId::SETS_MEM_EQ: return "SETS_MEM_EQ"; @@ -393,5 +396,10 @@ std::ostream& operator<<(std::ostream& out, InferenceId i) return out; } +Node mkInferenceIdNode(InferenceId i) +{ + return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(i))); +} + } // namespace theory } // namespace cvc5 diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index f32c80b68..b3be59c5c 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -20,6 +20,8 @@ #include <iosfwd> +#include "expr/node.h" + namespace cvc5 { namespace theory { @@ -378,9 +380,13 @@ enum class InferenceId // ---------------------------------- sets theory //-------------------- sets core solver + // split when computing care graph + SETS_CG_SPLIT, SETS_COMPREHENSION, SETS_DEQ, SETS_DOWN_CLOSURE, + // conflict when two singleton/emptyset terms merge + SETS_EQ_CONFLICT, SETS_EQ_MEM, SETS_EQ_MEM_CONFLICT, SETS_MEM_EQ, @@ -782,6 +788,9 @@ const char* toString(InferenceId i); */ std::ostream& operator<<(std::ostream& out, InferenceId i); +/** Make node from inference id */ +Node mkInferenceIdNode(InferenceId i); + } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 789a723b9..c2ee563e3 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -20,6 +20,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" @@ -244,8 +245,8 @@ Node CandidateRewriteDatabase::addTerm(Node sol, // wish to enumerate any term that contains sol (resp. eq_sol) // as a subterm. Node exc_sol = sol; - unsigned sz = d_tds->getSygusTermSize(sol); - unsigned eqsz = d_tds->getSygusTermSize(eq_sol); + unsigned sz = datatypes::utils::getSygusTermSize(sol); + unsigned eqsz = datatypes::utils::getSygusTermSize(eq_sol); if (eqsz > sz) { sz = eqsz; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index f059767a6..f65828d2f 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -491,7 +491,7 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { else if (inst->addInstantiation(d_curr_quant, subs, InferenceId::QUANTIFIERS_INST_CEGQI, - false, + Node::null(), false, usedVts)) { diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 62558e2c6..529125978 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -59,6 +59,7 @@ Trigger::Trigger(QuantifiersState& qs, Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms); d_nodes.push_back(np); } + d_trNode = NodeManager::currentNM()->mkNode(SEXPR, d_nodes); if (Trace.isOn("trigger")) { QuantAttributes& qa = d_qreg.getQuantAttributes(); @@ -163,7 +164,7 @@ uint64_t Trigger::addInstantiations() bool Trigger::sendInstantiation(std::vector<Node>& m, InferenceId id) { - return d_qim.getInstantiate()->addInstantiation(d_quant, m, id); + return d_qim.getInstantiate()->addInstantiation(d_quant, m, id, d_trNode); } bool Trigger::sendInstantiation(InstMatch& m, InferenceId id) diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 172e93c12..944a082c0 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -181,6 +181,8 @@ class Trigger { std::vector<Node>& gts); /** The nodes comprising this trigger. */ std::vector<Node> d_nodes; + /** The nodes as a single s-expression */ + Node d_trNode; /** * The preprocessed ground terms in the nodes of the trigger, which as an * optimization omits variables and constant subterms. These terms are diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index aa7e183bb..58a78b4aa 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -48,7 +48,7 @@ ExtendedRewriter::ExtendedRewriter(bool aggr) : d_aggr(aggr) d_false = NodeManager::currentNM()->mkConst(false); } -void ExtendedRewriter::setCache(Node n, Node ret) +void ExtendedRewriter::setCache(Node n, Node ret) const { if (d_aggr) { @@ -62,7 +62,7 @@ void ExtendedRewriter::setCache(Node n, Node ret) } } -Node ExtendedRewriter::getCache(Node n) +Node ExtendedRewriter::getCache(Node n) const { if (d_aggr) { @@ -83,7 +83,7 @@ Node ExtendedRewriter::getCache(Node n) bool ExtendedRewriter::addToChildren(Node nc, std::vector<Node>& children, - bool dropDup) + bool dropDup) const { // If the operator is non-additive, do not consider duplicates if (dropDup @@ -95,7 +95,7 @@ bool ExtendedRewriter::addToChildren(Node nc, return true; } -Node ExtendedRewriter::extendedRewrite(Node n) +Node ExtendedRewriter::extendedRewrite(Node n) const { n = Rewriter::rewrite(n); @@ -280,7 +280,7 @@ Node ExtendedRewriter::extendedRewrite(Node n) return ret; } -Node ExtendedRewriter::extendedRewriteAggr(Node n) +Node ExtendedRewriter::extendedRewriteAggr(Node n) const { Node new_ret; Trace("q-ext-rewrite-debug2") @@ -341,7 +341,7 @@ Node ExtendedRewriter::extendedRewriteAggr(Node n) return new_ret; } -Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full) +Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full) const { Assert(n.getKind() == itek); Assert(n[1] != n[2]); @@ -561,7 +561,7 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full) return new_ret; } -Node ExtendedRewriter::extendedRewriteAndOr(Node n) +Node ExtendedRewriter::extendedRewriteAndOr(Node n) const { // all the below rewrites are aggressive if (!d_aggr) @@ -592,7 +592,7 @@ Node ExtendedRewriter::extendedRewriteAndOr(Node n) return new_ret; } -Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n) +Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n) const { Assert(n.getKind() != ITE); if (n.isClosure()) @@ -715,7 +715,7 @@ Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n) return Node::null(); } -Node ExtendedRewriter::extendedRewriteNnf(Node ret) +Node ExtendedRewriter::extendedRewriteNnf(Node ret) const { Assert(ret.getKind() == NOT); @@ -761,8 +761,11 @@ Node ExtendedRewriter::extendedRewriteNnf(Node ret) return NodeManager::currentNM()->mkNode(nk, new_children); } -Node ExtendedRewriter::extendedRewriteBcp( - Kind andk, Kind ork, Kind notk, std::map<Kind, bool>& bcp_kinds, Node ret) +Node ExtendedRewriter::extendedRewriteBcp(Kind andk, + Kind ork, + Kind notk, + std::map<Kind, bool>& bcp_kinds, + Node ret) const { Kind k = ret.getKind(); Assert(k == andk || k == ork); @@ -926,7 +929,7 @@ Node ExtendedRewriter::extendedRewriteBcp( Node ExtendedRewriter::extendedRewriteFactoring(Kind andk, Kind ork, Kind notk, - Node n) + Node n) const { Trace("ext-rew-factoring") << "Factoring: *** INPUT: " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); @@ -1019,7 +1022,7 @@ Node ExtendedRewriter::extendedRewriteEqRes(Kind andk, Kind notk, std::map<Kind, bool>& bcp_kinds, Node n, - bool isXor) + bool isXor) const { Assert(n.getKind() == andk || n.getKind() == ork); Trace("ext-rew-eqres") << "Eq res: **** INPUT: " << n << std::endl; @@ -1166,7 +1169,7 @@ class SimpSubsumeTrie }; Node ExtendedRewriter::extendedRewriteEqChain( - Kind eqk, Kind andk, Kind ork, Kind notk, Node ret, bool isXor) + Kind eqk, Kind andk, Kind ork, Kind notk, Node ret, bool isXor) const { Assert(ret.getKind() == eqk); @@ -1527,9 +1530,10 @@ Node ExtendedRewriter::extendedRewriteEqChain( return Node::null(); } -Node ExtendedRewriter::partialSubstitute(Node n, - const std::map<Node, Node>& assign, - const std::map<Kind, bool>& rkinds) +Node ExtendedRewriter::partialSubstitute( + Node n, + const std::map<Node, Node>& assign, + const std::map<Kind, bool>& rkinds) const { std::unordered_map<TNode, Node> visited; std::unordered_map<TNode, Node>::iterator it; @@ -1601,10 +1605,11 @@ Node ExtendedRewriter::partialSubstitute(Node n, return visited[n]; } -Node ExtendedRewriter::partialSubstitute(Node n, - const std::vector<Node>& vars, - const std::vector<Node>& subs, - const std::map<Kind, bool>& rkinds) +Node ExtendedRewriter::partialSubstitute( + Node n, + const std::vector<Node>& vars, + const std::vector<Node>& subs, + const std::map<Kind, bool>& rkinds) const { Assert(vars.size() == subs.size()); std::map<Node, Node> assign; @@ -1615,7 +1620,7 @@ Node ExtendedRewriter::partialSubstitute(Node n, return partialSubstitute(n, assign, rkinds); } -Node ExtendedRewriter::solveEquality(Node n) +Node ExtendedRewriter::solveEquality(Node n) const { // TODO (#1706) : implement Assert(n.getKind() == EQUAL); @@ -1626,7 +1631,7 @@ Node ExtendedRewriter::solveEquality(Node n) bool ExtendedRewriter::inferSubstitution(Node n, std::vector<Node>& vars, std::vector<Node>& subs, - bool usePred) + bool usePred) const { if (n.getKind() == AND) { @@ -1696,7 +1701,7 @@ bool ExtendedRewriter::inferSubstitution(Node n, return false; } -Node ExtendedRewriter::extendedRewriteStrings(Node ret) +Node ExtendedRewriter::extendedRewriteStrings(Node ret) const { Node new_ret; Trace("q-ext-rewrite-debug") diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index 047318e86..8996fc441 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -51,7 +51,7 @@ class ExtendedRewriter ExtendedRewriter(bool aggr = true); ~ExtendedRewriter() {} /** return the extended rewritten form of n */ - Node extendedRewrite(Node n); + Node extendedRewrite(Node n) const; private: /** @@ -69,16 +69,16 @@ class ExtendedRewriter Node d_true; Node d_false; /** cache that the extended rewritten form of n is ret */ - void setCache(Node n, Node ret); + void setCache(Node n, Node ret) const; /** get the cache for n */ - Node getCache(Node n); + Node getCache(Node n) const; /** add to children * * Adds nc to the vector of children, if dropDup is true, we do not add * nc if it already occurs in children. This method returns false in this * case, otherwise it returns true. */ - bool addToChildren(Node nc, std::vector<Node>& children, bool dropDup); + bool addToChildren(Node nc, std::vector<Node>& children, bool dropDup) const; //--------------------------------------generic utilities /** Rewrite ITE, for example: @@ -92,13 +92,13 @@ class ExtendedRewriter * take. If full is false, then we do only perform rewrites that * strictly decrease the term size of n. */ - Node extendedRewriteIte(Kind itek, Node n, bool full = true); + Node extendedRewriteIte(Kind itek, Node n, bool full = true) const; /** Rewrite AND/OR * * This implements BCP, factoring, and equality resolution for the Boolean * term n whose top symbolic is AND/OR. */ - Node extendedRewriteAndOr(Node n); + Node extendedRewriteAndOr(Node n) const; /** Pull ITE, for example: * * D=C2 ---> false @@ -111,7 +111,7 @@ class ExtendedRewriter * * If this function returns a non-null node ret, then n ---> ret. */ - Node extendedRewritePullIte(Kind itek, Node n); + Node extendedRewritePullIte(Kind itek, Node n) const; /** Negation Normal Form (NNF), for example: * * ~( A & B ) ---> ( ~ A | ~B ) @@ -119,7 +119,7 @@ class ExtendedRewriter * * If this function returns a non-null node ret, then n ---> ret. */ - Node extendedRewriteNnf(Node n); + Node extendedRewriteNnf(Node n) const; /** (type-independent) Boolean constraint propagation, for example: * * ~A & ( B V A ) ---> ~A & B @@ -137,8 +137,11 @@ class ExtendedRewriter * * If this function returns a non-null node ret, then n ---> ret. */ - Node extendedRewriteBcp( - Kind andk, Kind ork, Kind notk, std::map<Kind, bool>& bcp_kinds, Node n); + Node extendedRewriteBcp(Kind andk, + Kind ork, + Kind notk, + std::map<Kind, bool>& bcp_kinds, + Node n) const; /** (type-independent) factoring, for example: * * ( A V B ) ^ ( A V C ) ----> A V ( B ^ C ) @@ -147,7 +150,7 @@ class ExtendedRewriter * This function takes as arguments the kinds that specify AND, OR, NOT. * We assume that the children of n do not contain duplicates. */ - Node extendedRewriteFactoring(Kind andk, Kind ork, Kind notk, Node n); + Node extendedRewriteFactoring(Kind andk, Kind ork, Kind notk, Node n) const; /** (type-independent) equality resolution, for example: * * ( A V C ) & ( A = B ) ---> ( B V C ) & ( A = B ) @@ -167,7 +170,7 @@ class ExtendedRewriter Kind notk, std::map<Kind, bool>& bcp_kinds, Node n, - bool isXor = false); + bool isXor = false) const; /** (type-independent) Equality chain rewriting, for example: * * A = ( A = B ) ---> B @@ -178,26 +181,32 @@ class ExtendedRewriter * This function takes as arguments the kinds that specify EQUAL, AND, OR, * and NOT. If the flag isXor is true, the eqk is treated as XOR. */ - Node extendedRewriteEqChain( - Kind eqk, Kind andk, Kind ork, Kind notk, Node n, bool isXor = false); + Node extendedRewriteEqChain(Kind eqk, + Kind andk, + Kind ork, + Kind notk, + Node n, + bool isXor = false) const; /** extended rewrite aggressive * * All aggressive rewriting techniques (those that should be prioritized * at a lower level) go in this function. */ - Node extendedRewriteAggr(Node n); + Node extendedRewriteAggr(Node n) const; /** Decompose right associative chain * * For term f( ... f( f( base, tn ), t{n-1} ) ... t1 ), returns term base, and * appends t1...tn to children. */ - Node decomposeRightAssocChain(Kind k, Node n, std::vector<Node>& children); + Node decomposeRightAssocChain(Kind k, + Node n, + std::vector<Node>& children) const; /** Make right associative chain * * Sorts children to obtain list { tn...t1 }, and returns the term * f( ... f( f( base, tn ), t{n-1} ) ... t1 ). */ - Node mkRightAssocChain(Kind k, Node base, std::vector<Node>& children); + Node mkRightAssocChain(Kind k, Node base, std::vector<Node>& children) const; /** Partial substitute * * Applies the substitution specified by assign to n, recursing only beneath @@ -206,18 +215,18 @@ class ExtendedRewriter */ Node partialSubstitute(Node n, const std::map<Node, Node>& assign, - const std::map<Kind, bool>& rkinds); + const std::map<Kind, bool>& rkinds) const; /** same as above, with vectors */ Node partialSubstitute(Node n, const std::vector<Node>& vars, const std::vector<Node>& subs, - const std::map<Kind, bool>& rkinds); + const std::map<Kind, bool>& rkinds) const; /** solve equality * * If this function returns a non-null node n', then n' is equivalent to n * and is of the form that can be used by inferSubstitution below. */ - Node solveEquality(Node n); + Node solveEquality(Node n) const; /** infer substitution * * If n is an equality of the form x = t, where t is either: @@ -231,12 +240,12 @@ class ExtendedRewriter bool inferSubstitution(Node n, std::vector<Node>& vars, std::vector<Node>& subs, - bool usePred = false); + bool usePred = false) const; /** extended rewrite * * Prints debug information, indicating the rewrite n ---> ret was found. */ - inline void debugExtendedRewrite(Node n, Node ret, const char* c) const; + void debugExtendedRewrite(Node n, Node ret, const char* c) const; //--------------------------------------end generic utilities //--------------------------------------theory-specific top-level calls @@ -245,7 +254,7 @@ class ExtendedRewriter * If this method returns a non-null node ret', then ret is equivalent to * ret'. */ - Node extendedRewriteStrings(Node ret); + Node extendedRewriteStrings(Node ret) const; //--------------------------------------end theory-specific top-level calls }; diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index c3fa664d9..c4f83191b 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -725,8 +725,11 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i } // just add the instance d_triedLemmas++; - if (instq->addInstantiation( - f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC, true)) + if (instq->addInstantiation(f, + inst, + InferenceId::QUANTIFIERS_INST_FMF_FMC, + Node::null(), + true)) { Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; @@ -875,8 +878,11 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm, if (ev!=d_true) { Trace("fmc-exh-debug") << ", add!"; //add as instantiation - if (ie->addInstantiation( - f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, true)) + if (ie->addInstantiation(f, + inst, + InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, + Node::null(), + true)) { Trace("fmc-exh-debug") << " ...success."; addedLemmas++; diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index cfccd4d93..a767af47a 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -56,8 +56,6 @@ class QModelBuilder : public TheoryEngineModelBuilder virtual int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; } //whether to construct model virtual bool optUseModel(); - /** exist instantiation ? */ - virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; } //debug model void debugModel(TheoryModel* m) override; //statistics diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 747b0621f..e58f66d0b 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -301,8 +301,11 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; triedLemmas++; //add as instantiation - if (inst->addInstantiation( - f, m.d_vals, InferenceId::QUANTIFIERS_INST_FMF_EXH, true)) + if (inst->addInstantiation(f, + m.d_vals, + InferenceId::QUANTIFIERS_INST_FMF_EXH, + Node::null(), + true)) { addedLemmas++; if (d_qstate.isInConflict()) diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 268d1371f..05361eaa1 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -101,8 +101,8 @@ void Instantiate::addRewriter(InstantiationRewriter* ir) bool Instantiate::addInstantiation(Node q, std::vector<Node>& terms, InferenceId id, + Node pfArg, bool mkRep, - bool modEq, bool doVts) { // For resource-limiting (also does a time check). @@ -229,7 +229,7 @@ bool Instantiate::addInstantiation(Node q, } // record the instantiation - bool recorded = recordInstantiationInternal(q, terms, modEq); + bool recorded = recordInstantiationInternal(q, terms); if (!recorded) { Trace("inst-add-debug") << " --> Already exists (no record)." << std::endl; @@ -250,7 +250,8 @@ bool Instantiate::addInstantiation(Node q, Trace("inst-add-debug") << "Constructing instantiation..." << std::endl; Assert(d_qreg.d_vars[q].size() == terms.size()); // get the instantiation - Node body = getInstantiation(q, d_qreg.d_vars[q], terms, doVts, pfTmp.get()); + Node body = getInstantiation( + 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); @@ -394,12 +395,12 @@ bool Instantiate::addInstantiationExpFail(Node q, std::vector<Node>& terms, std::vector<bool>& failMask, InferenceId id, + Node pfArg, bool mkRep, - bool modEq, bool doVts, bool expFull) { - if (addInstantiation(q, terms, id, mkRep, modEq, doVts)) + if (addInstantiation(q, terms, id, pfArg, mkRep, doVts)) { return true; } @@ -421,7 +422,9 @@ bool Instantiate::addInstantiationExpFail(Node q, subs[vars[i]] = terms[i]; } // get the instantiation body - Node ibody = getInstantiation(q, vars, terms, doVts); + InferenceId idNone = InferenceId::UNKNOWN; + Node nulln; + Node ibody = getInstantiation(q, vars, terms, idNone, nulln, doVts); ibody = Rewriter::rewrite(ibody); for (size_t i = 0; i < tsize; i++) { @@ -450,7 +453,7 @@ bool Instantiate::addInstantiationExpFail(Node q, // check whether the instantiation rewrites to the same thing if (!success) { - Node ibodyc = getInstantiation(q, vars, terms, doVts); + Node ibodyc = getInstantiation(q, vars, terms, idNone, nulln, doVts); ibodyc = Rewriter::rewrite(ibodyc); success = (ibodyc == ibody); Trace("inst-exp-fail") << " rewrite invariant: " << success << std::endl; @@ -521,6 +524,8 @@ bool Instantiate::existsInstantiation(Node q, Node Instantiate::getInstantiation(Node q, std::vector<Node>& vars, std::vector<Node>& terms, + InferenceId id, + Node pfArg, bool doVts, LazyCDProof* pf) { @@ -534,7 +539,19 @@ Node Instantiate::getInstantiation(Node q, // store the proof of the instantiated body, with (open) assumption q if (pf != nullptr) { - pf->addStep(body, PfRule::INSTANTIATE, {q}, terms); + // additional arguments: if the inference id is not unknown, include it, + // followed by the proof argument if non-null. The latter is used e.g. + // to track which trigger caused an instantiation. + std::vector<Node> pfTerms = terms; + if (id != InferenceId::UNKNOWN) + { + pfTerms.push_back(mkInferenceIdNode(id)); + if (!pfArg.isNull()) + { + pfTerms.push_back(pfArg); + } + } + pf->addStep(body, PfRule::INSTANTIATE, {q}, pfTerms); } // run rewriters to rewrite the instantiation in sequence. @@ -564,18 +581,16 @@ Node Instantiate::getInstantiation(Node q, Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts) { Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end()); - return getInstantiation(q, d_qreg.d_vars[q], terms, doVts); + return getInstantiation( + q, d_qreg.d_vars[q], terms, InferenceId::UNKNOWN, Node::null(), doVts); } -bool Instantiate::recordInstantiationInternal(Node q, - std::vector<Node>& terms, - bool modEq) +bool Instantiate::recordInstantiationInternal(Node q, std::vector<Node>& terms) { if (options::incrementalSolving()) { Trace("inst-add-debug") - << "Adding into context-dependent inst trie, modEq = " << modEq - << std::endl; + << "Adding into context-dependent inst trie" << std::endl; CDInstMatchTrie* imt; std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q); if (it != d_c_inst_match_trie.end()) @@ -588,10 +603,10 @@ bool Instantiate::recordInstantiationInternal(Node q, d_c_inst_match_trie[q] = imt; } d_c_inst_match_trie_dom.insert(q); - return imt->addInstMatch(d_qstate, q, terms, modEq); + return imt->addInstMatch(d_qstate, q, terms); } Trace("inst-add-debug") << "Adding into inst trie" << std::endl; - return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms, modEq); + return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms); } bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms) diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index eddc7470b..1f380350f 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -139,10 +139,10 @@ class Instantiate : public QuantifiersUtil * @param terms the terms to instantiate with * @param id the identifier of the instantiation lemma sent via the inference * manager + * @param pfArg an additional node to add to the arguments of the INSTANTIATE + * step * @param mkRep whether to take the representatives of the terms in the * range of the substitution m, - * @param modEq whether to check for duplication modulo equality in - * instantiation tries (for performance), * @param doVts whether we must apply virtual term substitution to the * instantiation lemma. * @@ -161,8 +161,8 @@ class Instantiate : public QuantifiersUtil bool addInstantiation(Node q, std::vector<Node>& terms, InferenceId id, + Node pfArg = Node::null(), bool mkRep = false, - bool modEq = false, bool doVts = false); /** * Same as above, but we also compute a vector failMask indicating which @@ -191,8 +191,8 @@ class Instantiate : public QuantifiersUtil std::vector<Node>& terms, std::vector<bool>& failMask, InferenceId id, + Node pfArg = Node::null(), bool mkRep = false, - bool modEq = false, bool doVts = false, bool expFull = true); /** record instantiation @@ -226,6 +226,8 @@ class Instantiate : public QuantifiersUtil Node getInstantiation(Node q, std::vector<Node>& vars, std::vector<Node>& terms, + InferenceId id = InferenceId::UNKNOWN, + Node pfArg = Node::null(), bool doVts = false, LazyCDProof* pf = nullptr); /** get instantiation @@ -293,14 +295,8 @@ class Instantiate : public QuantifiersUtil Statistics d_statistics; private: - /** record instantiation, return true if it was not a duplicate - * - * modEq : whether to check for duplication modulo equality in instantiation - * tries (for performance), - */ - bool recordInstantiationInternal(Node q, - std::vector<Node>& terms, - bool modEq = false); + /** record instantiation, return true if it was not a duplicate */ + bool recordInstantiationInternal(Node q, std::vector<Node>& terms); /** remove instantiation from the cache */ bool removeInstantiationInternal(Node q, std::vector<Node>& terms); /** diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index f44f2f291..5e02e16a5 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -102,15 +102,16 @@ Node QuantifiersProofRuleChecker::checkInternal( else if (id == PfRule::INSTANTIATE) { Assert(children.size() == 1); + // note we may have more arguments than just the term vector if (children[0].getKind() != FORALL - || args.size() != children[0][0].getNumChildren()) + || args.size() < children[0][0].getNumChildren()) { return Node::null(); } Node body = children[0][1]; std::vector<Node> vars; std::vector<Node> subs; - for (unsigned i = 0, nargs = args.size(); i < nargs; i++) + for (size_t i = 0, nc = children[0][0].getNumChildren(); i < nc; i++) { vars.push_back(children[0][0][i]); subs.push_back(args[i]); diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 28788a5ea..544bdcc5c 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -19,6 +19,7 @@ #include "expr/sygus_datatype.h" #include "options/quantifiers_options.h" #include "printer/printer.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/sygus_unif_rl.h" #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -205,8 +206,8 @@ bool CegisUnif::getEnumValues(const std::vector<Node>& enums, if (curr_val < prev_val) { // must have the same size - unsigned prev_size = d_tds->getSygusTermSize(prev_val); - unsigned curr_size = d_tds->getSygusTermSize(curr_val); + unsigned prev_size = datatypes::utils::getSygusTermSize(prev_val); + unsigned curr_size = datatypes::utils::getSygusTermSize(curr_val); Assert(prev_size <= curr_size); if (curr_size == prev_size) { diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index 3ae34d82c..f853ac8e8 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -24,6 +24,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include <numeric> // for std::iota +#include <sstream> using namespace cvc5::kind; diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index ea028991b..05c693ace 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -19,12 +19,14 @@ #define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H #include "expr/node.h" -#include "theory/quantifiers/sygus/synth_conjecture.h" +#include "theory/quantifiers/sygus/enum_val_generator.h" namespace cvc5 { namespace theory { namespace quantifiers { +class TermDbSygus; + /** Streamer of different values according to variable permutations * * Generates a new value (modulo rewriting) when queried in which its variables @@ -33,7 +35,7 @@ namespace quantifiers { class EnumStreamPermutation { public: - EnumStreamPermutation(quantifiers::TermDbSygus* tds); + EnumStreamPermutation(TermDbSygus* tds); ~EnumStreamPermutation() {} /** resets utility * @@ -70,7 +72,7 @@ class EnumStreamPermutation private: /** sygus term database of current quantifiers engine */ - quantifiers::TermDbSygus* d_tds; + TermDbSygus* d_tds; /** maps subclass ids to subset of d_vars with that subclass id */ std::map<unsigned, std::vector<Node>> d_var_classes; /** maps variables to subfield types with constructors for @@ -165,7 +167,7 @@ class EnumStreamPermutation class EnumStreamSubstitution { public: - EnumStreamSubstitution(quantifiers::TermDbSygus* tds); + EnumStreamSubstitution(TermDbSygus* tds); ~EnumStreamSubstitution() {} /** initializes utility * @@ -211,7 +213,7 @@ class EnumStreamSubstitution private: /** sygus term database of current quantifiers engine */ - quantifiers::TermDbSygus* d_tds; + TermDbSygus* d_tds; /** type this utility has been initialized for */ TypeNode d_tn; /** current value */ @@ -281,7 +283,7 @@ class EnumStreamSubstitution class EnumStreamConcrete : public EnumValGenerator { public: - EnumStreamConcrete(quantifiers::TermDbSygus* tds) : d_ess(tds) {} + EnumStreamConcrete(TermDbSygus* tds) : d_ess(tds) {} /** initialize this class with enumerator e */ void initialize(Node e) override; /** get that value v was enumerated */ diff --git a/src/theory/quantifiers/sygus/enum_val_generator.h b/src/theory/quantifiers/sygus/enum_val_generator.h new file mode 100644 index 000000000..64c069087 --- /dev/null +++ b/src/theory/quantifiers/sygus/enum_val_generator.h @@ -0,0 +1,62 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Base class for sygus enumerators + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_VAL_GENERATOR_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_VAL_GENERATOR_H + +#include "expr/node.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +/** + * A base class for generating values for actively-generated enumerators. + * At a high level, the job of this class is to accept a stream of "abstract + * values" a1, ..., an, ..., and generate a (possibly larger) stream of + * "concrete values" c11, ..., c1{m_1}, ..., cn1, ... cn{m_n}, .... + */ +class EnumValGenerator +{ + public: + virtual ~EnumValGenerator() {} + /** initialize this class with enumerator e */ + virtual void initialize(Node e) = 0; + /** Inform this generator that abstract value v was enumerated. */ + virtual void addValue(Node v) = 0; + /** + * Increment this value generator. If this returns false, then we are out of + * values. If this returns true, getCurrent(), if non-null, returns the + * current term. + * + * Notice that increment() may return true and afterwards it may be the case + * getCurrent() is null. We do this so that increment() does not take too + * much time per call, which can be the case for grammars where it is + * difficult to find the next (non-redundant) term. Returning true with + * a null current term gives the caller the chance to interleave other + * reasoning. + */ + virtual bool increment() = 0; + /** Get the current concrete value generated by this class. */ + virtual Node getCurrent() = 0; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif diff --git a/src/theory/quantifiers/sygus/rcons_type_info.cpp b/src/theory/quantifiers/sygus/rcons_type_info.cpp index 1c62f030d..a1ae53ad1 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.cpp +++ b/src/theory/quantifiers/sygus/rcons_type_info.cpp @@ -31,7 +31,7 @@ void RConsTypeInfo::initialize(TermDbSygus* tds, NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - d_enumerator.reset(new SygusEnumerator(tds, nullptr, s, true)); + d_enumerator.reset(new SygusEnumerator(tds, nullptr, &s, true)); d_enumerator->initialize(sm->mkDummySkolem("sygus_rcons", stn)); d_crd.reset(new CandidateRewriteDatabase(true, false, true, false)); // since initial samples are not always useful for equivalence checks, set diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 0cf92b373..2dfd41fb4 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -20,6 +20,7 @@ #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "smt/logic_exception.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/sygus/type_node_id_trie.h" @@ -33,12 +34,14 @@ namespace quantifiers { SygusEnumerator::SygusEnumerator(TermDbSygus* tds, SynthConjecture* p, - SygusStatistics& s, - bool enumShapes) + SygusStatistics* s, + bool enumShapes, + bool enumAnyConstHoles) : d_tds(tds), d_parent(p), d_stats(s), d_enumShapes(enumShapes), + d_enumAnyConstHoles(enumAnyConstHoles), d_tlEnum(nullptr), d_abortSize(-1) { @@ -54,6 +57,12 @@ void SygusEnumerator::initialize(Node e) d_tlEnum = getMasterEnumForType(d_etype); d_abortSize = options::sygusAbortSize(); + // if we don't have a term database, we don't register symmetry breaking + // lemmas + if (!d_tds) + { + return; + } // Get the statically registered symmetry breaking clauses for e, see if they // can be used for speeding up the enumeration. NodeManager* nm = NodeManager::currentNM(); @@ -141,7 +150,8 @@ Node SygusEnumerator::getCurrent() if (d_sbExcTlCons.find(ret.getOperator()) != d_sbExcTlCons.end()) { Trace("sygus-enum-exc") - << "Exclude (external) : " << d_tds->sygusToBuiltin(ret) << std::endl; + << "Exclude (external) : " << datatypes::utils::sygusToBuiltin(ret) + << std::endl; ret = Node::null(); } } @@ -330,9 +340,12 @@ bool SygusEnumerator::TermCache::addTerm(Node n) Assert(!n.isNull()); if (options::sygusSymBreakDynamic()) { - Node bn = d_tds->sygusToBuiltin(n); - Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn); - ++(d_stats->d_enumTermsRewrite); + Node bn = datatypes::utils::sygusToBuiltin(n); + Node bnr = d_extr.extendedRewrite(bn); + if (d_stats != nullptr) + { + ++(d_stats->d_enumTermsRewrite); + } if (options::sygusRewVerify()) { if (bn != bnr) @@ -358,7 +371,10 @@ bool SygusEnumerator::TermCache::addTerm(Node n) // if we are doing PBE symmetry breaking if (d_eec != nullptr) { - ++(d_stats->d_enumTermsExampleEval); + if (d_stats != nullptr) + { + ++(d_stats->d_enumTermsExampleEval); + } // Is it equivalent under examples? Node bne = d_eec->addSearchVal(d_tn, bnr); if (!bne.isNull()) @@ -374,7 +390,10 @@ bool SygusEnumerator::TermCache::addTerm(Node n) } Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl; } - ++(d_stats->d_enumTerms); + if (d_stats != nullptr) + { + ++(d_stats->d_enumTerms); + } d_terms.push_back(n); return true; } @@ -474,8 +493,8 @@ Node SygusEnumerator::TermEnumSlave::getCurrent() Node curr = tc.getTerm(d_index); Trace("sygus-enum-debug2") << "slave(" << d_tn - << "): current : " << d_se->d_tds->sygusToBuiltin(curr) - << ", sizes = " << d_se->d_tds->getSygusTermSize(curr) << " " + << "): current : " << datatypes::utils::sygusToBuiltin(curr) + << ", sizes = " << datatypes::utils::getSygusTermSize(curr) << " " << getCurrentSize() << std::endl; Trace("sygus-enum-debug2") << "slave(" << d_tn << "): indices : " << d_hasIndexNextEnd << " " @@ -560,7 +579,7 @@ void SygusEnumerator::initializeTermCache(TypeNode tn) { eec = d_parent->getExampleEvalCache(d_enum); } - d_tcache[tn].initialize(&d_stats, d_enum, tn, d_tds, eec); + d_tcache[tn].initialize(d_stats, d_enum, tn, d_tds, eec); } SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn) @@ -578,7 +597,7 @@ SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn) AlwaysAssert(ret); return &d_masterEnum[tn]; } - if (options::sygusRepairConst()) + if (d_enumAnyConstHoles) { std::map<TypeNode, TermEnumMasterFv>::iterator it = d_masterEnumFv.find(tn); if (it != d_masterEnumFv.end()) @@ -720,6 +739,7 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal() // If we are enumerating shapes, the first enumerated term is a free variable. if (d_enumShapes && !d_enumShapesInit) { + Assert(d_tds != nullptr); Node fv = d_tds->getFreeVar(d_tn, 0); d_enumShapesInit = true; d_currTermSet = true; @@ -1083,6 +1103,7 @@ void SygusEnumerator::TermEnumMaster::childrenToShape( Node SygusEnumerator::TermEnumMaster::convertShape( Node n, std::map<TypeNode, int>& vcounter) { + Assert(d_tds != nullptr); NodeManager* nm = NodeManager::currentNM(); std::unordered_map<TNode, Node> visited; std::unordered_map<TNode, Node>::iterator it; @@ -1195,6 +1216,7 @@ bool SygusEnumerator::TermEnumMasterFv::initialize(SygusEnumerator* se, Node SygusEnumerator::TermEnumMasterFv::getCurrent() { + Assert(d_se->d_tds != nullptr); Node ret = d_se->d_tds->getFreeVar(d_tn, d_currSize); Trace("sygus-enum-debug2") << "master_fv(" << d_tn << "): mk " << ret << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index 355108957..39e58d5f3 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -22,6 +22,7 @@ #include <unordered_set> #include "expr/node.h" #include "expr/type_node.h" +#include "theory/quantifiers/sygus/enum_val_generator.h" #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -56,10 +57,23 @@ class SygusPbe; class SygusEnumerator : public EnumValGenerator { public: - SygusEnumerator(TermDbSygus* tds, - SynthConjecture* p, - SygusStatistics& s, - bool enumShapes = false); + /** + * @param tds Pointer to the term database, required if enumShapes or + * enumAnyConstHoles is true, or if we want to include symmetry breaking from + * lemmas stored in the sygus term database, + * @param p Pointer to the conjecture, required if we wish to do + * conjecture-specific symmetry breaking + * @param s Pointer to the statistics + * @param enumShapes If true, this enumerator will generate terms having any + * number of free variables + * @param enumAnyConstHoles If true, this enumerator will generate terms where + * free variables are the arguments to any-constant constructors. + */ + SygusEnumerator(TermDbSygus* tds = nullptr, + SynthConjecture* p = nullptr, + SygusStatistics* s = nullptr, + bool enumShapes = false, + bool enumAnyConstHoles = false); ~SygusEnumerator() {} /** initialize this class with enumerator e */ void initialize(Node e) override; @@ -77,10 +91,13 @@ class SygusEnumerator : public EnumValGenerator TermDbSygus* d_tds; /** pointer to the synth conjecture that owns this enumerator */ SynthConjecture* d_parent; - /** reference to the statistics of parent */ - SygusStatistics& d_stats; + /** pointer to the statistics */ + SygusStatistics* d_stats; /** Whether we are enumerating shapes */ bool d_enumShapes; + /** Whether we are enumerating free variables as arguments to any-constant + * constructors */ + bool d_enumAnyConstHoles; /** Term cache * * This stores a list of terms for a given sygus type. The key features of @@ -171,6 +188,8 @@ class SygusEnumerator : public EnumValGenerator TypeNode d_tn; /** pointer to term database sygus */ TermDbSygus* d_tds; + /** extended rewriter */ + ExtendedRewriter d_extr; /** * Pointer to the example evaluation cache utility (used for symmetry * breaking). diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h index bae6f6327..42bce471d 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h @@ -22,7 +22,7 @@ #include <unordered_set> #include "expr/node.h" #include "expr/type_node.h" -#include "theory/quantifiers/sygus/synth_conjecture.h" +#include "theory/quantifiers/sygus/enum_val_generator.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/type_enumerator.h" diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp new file mode 100644 index 000000000..7b3236832 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp @@ -0,0 +1,107 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner + * + * 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. + * **************************************************************************** + * + * sygus_enumerator + */ + +#include "theory/quantifiers/sygus/sygus_enumerator_callback.h" + +#include "theory/datatypes/sygus_datatype_utils.h" +#include "theory/quantifiers/sygus/example_eval_cache.h" +#include "theory/quantifiers/sygus/sygus_stats.h" +#include "theory/quantifiers/sygus_sampler.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +SygusEnumeratorCallback::SygusEnumeratorCallback(Node e, SygusStatistics* s) + : d_enum(e), d_stats(s) +{ + d_tn = e.getType(); +} + +bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms) +{ + Node bn = datatypes::utils::sygusToBuiltin(n); + Node bnr = d_extr.extendedRewrite(bn); + if (d_stats != nullptr) + { + ++(d_stats->d_enumTermsRewrite); + } + // call the solver-specific notify term + notifyTermInternal(n, bn, bnr); + // check whether we should keep the term, which is based on the callback, + // and the builtin terms + // First, must be unique up to rewriting + if (bterms.find(bnr) != bterms.end()) + { + Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl; + return false; + } + // insert to builtin term cache, regardless of whether it is redundant + // based on the callback + bterms.insert(bnr); + // callback-specific add term + if (!addTermInternal(n, bn, bnr)) + { + Trace("sygus-enum-exc") + << "Exclude: " << bn << " due to callback" << std::endl; + return false; + } + Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl; + return true; +} + +SygusEnumeratorCallbackDefault::SygusEnumeratorCallbackDefault( + Node e, SygusStatistics* s, ExampleEvalCache* eec, SygusSampler* ssrv) + : SygusEnumeratorCallback(e, s), d_eec(eec), d_samplerRrV(ssrv) +{ +} +void SygusEnumeratorCallbackDefault::notifyTermInternal(Node n, + Node bn, + Node bnr) +{ + if (d_samplerRrV != nullptr) + { + d_samplerRrV->checkEquivalent(bn, bnr); + } +} + +bool SygusEnumeratorCallbackDefault::addTermInternal(Node n, Node bn, Node bnr) +{ + // if we are doing PBE symmetry breaking + if (d_eec != nullptr) + { + if (d_stats != nullptr) + { + ++(d_stats->d_enumTermsExampleEval); + } + // Is it equivalent under examples? + Node bne = d_eec->addSearchVal(d_tn, bnr); + if (!bne.isNull()) + { + if (bnr != bne) + { + Trace("sygus-enum-exc") + << "Exclude (by examples): " << bn << ", since we already have " + << bne << std::endl; + return false; + } + } + } + return true; +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h new file mode 100644 index 000000000..545440eef --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h @@ -0,0 +1,110 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Mathias Preiner + * + * 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. + * **************************************************************************** + * + * sygus_enumerator + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H +#define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H + +#include <unordered_set> + +#include "expr/node.h" +#include "theory/quantifiers/extended_rewrite.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +class ExampleEvalCache; +class SygusStatistics; +class SygusSampler; + +/** + * Base class for callbacks in the fast enumerator. This allows a user to + * provide custom criteria for whether or not enumerated values should be + * considered. + */ +class SygusEnumeratorCallback +{ + public: + SygusEnumeratorCallback(Node e, SygusStatistics* s = nullptr); + virtual ~SygusEnumeratorCallback() {} + /** + * Add term, return true if the term should be considered in the enumeration. + * Notice that returning false indicates that n should not be considered as a + * subterm of any other term in the enumeration. + * + * @param n The SyGuS term + * @param bterms The (rewritten, builtin) terms we have already enumerated + * @return true if n should be considered in the enumeration. + */ + virtual bool addTerm(Node n, std::unordered_set<Node>& bterms) = 0; + + protected: + /** + * Callback-specific notification of the above + * + * @param n The SyGuS term + * @param bn The builtin version of the enumerated term + * @param bnr The (extended) rewritten form of bn + */ + virtual void notifyTermInternal(Node n, Node bn, Node bnr) = 0; + /** + * Callback-specific add term + * + * @param n The SyGuS term + * @param bn The builtin version of the enumerated term + * @param bnr The (extended) rewritten form of bn + * @return true if the term should be considered in the enumeration. + */ + virtual bool addTermInternal(Node n, Node bn, Node bnr) = 0; + /** The enumerator */ + Node d_enum; + /** The type of enum */ + TypeNode d_tn; + /** extended rewriter */ + ExtendedRewriter d_extr; + /** pointer to the statistics */ + SygusStatistics* d_stats; +}; + +class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback +{ + public: + SygusEnumeratorCallbackDefault(Node e, + SygusStatistics* s = nullptr, + ExampleEvalCache* eec = nullptr, + SygusSampler* ssrv = nullptr); + virtual ~SygusEnumeratorCallbackDefault() {} + + protected: + /** Notify that bn / bnr is an enumerated builtin, rewritten form of a term */ + void notifyTermInternal(Node n, Node bn, Node bnr) override; + /** Add term, return true if n should be considered in the enumeration */ + bool addTermInternal(Node n, Node bn, Node bnr) override; + /** + * Pointer to the example evaluation cache utility (used for symmetry + * breaking). + */ + ExampleEvalCache* d_eec; + /** sampler (for --sygus-rr-verify) */ + SygusSampler* d_samplerRrV; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_ENUMERATOR_CALLBACK_H */ diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index 395f16beb..23c315f42 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -18,6 +18,7 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "smt/logic_exception.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/sygus_invariance.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -220,7 +221,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb, // we are tracking term size if positive if (sz >= 0) { - int s = d_tdb->getSygusTermSize(vn[i]); + int s = datatypes::utils::getSygusTermSize(vn[i]); sz = sz - s; } } diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 86d0bbc8e..892ee6dd4 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_pbe.h" #include "options/quantifiers_options.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/example_infer.h" #include "theory/quantifiers/sygus/sygus_unif_io.h" #include "theory/quantifiers/sygus/synth_conjecture.h" @@ -180,7 +181,7 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, Trace("sygus-pbe-enum") << std::endl; if (!enum_values[i].isNull()) { - unsigned sz = d_tds->getSygusTermSize(enum_values[i]); + unsigned sz = datatypes::utils::getSygusTermSize(enum_values[i]); szs.push_back(sz); if (i == 0 || sz < min_term_size) { diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 16ca1f4e6..00370ffa2 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_unif.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "util/random.h" @@ -52,7 +53,7 @@ Node SygusUnif::getMinimalTerm(const std::vector<Node>& terms) unsigned ssize = 0; if (it == d_termToSize.end()) { - ssize = d_tds->getSygusTermSize(n); + ssize = datatypes::utils::getSygusTermSize(n); d_termToSize[n] = ssize; } else diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 8c8f5ccd4..8207a07f2 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/sygus/sygus_unif_io.h" #include "options/quantifiers_options.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/evaluator.h" #include "theory/quantifiers/sygus/example_infer.h" #include "theory/quantifiers/sygus/synth_conjecture.h" @@ -835,7 +836,8 @@ Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas) if (!vcc.isNull() && (d_solution.isNull() || (!d_solution.isNull() - && d_tds->getSygusTermSize(vcc) < d_sol_term_size))) + && datatypes::utils::getSygusTermSize(vcc) + < d_sol_term_size))) { if (Trace.isOn("sygus-pbe")) { @@ -846,7 +848,7 @@ Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas) } d_solution = vcc; newSolution = vcc; - d_sol_term_size = d_tds->getSygusTermSize(vcc); + d_sol_term_size = datatypes::utils::getSygusTermSize(vcc); Trace("sygus-pbe-sol") << "PBE solution size: " << d_sol_term_size << std::endl; // We've determined its feasible, now, enable information gain and diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 1ddc2fa22..73bd6b8a4 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -827,7 +827,10 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete) == options::SygusActiveGenMode::ENUM || options::sygusActiveGenMode() == options::SygusActiveGenMode::AUTO); - d_evg[e].reset(new SygusEnumerator(d_tds, this, d_stats)); + // if sygus repair const is enabled, we enumerate terms with free + // variables as arguments to any-constant constructors + d_evg[e].reset(new SygusEnumerator( + d_tds, this, &d_stats, false, options::sygusRepairConst())); } } Trace("sygus-active-gen") diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index e6645ddf2..04999da0d 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -26,6 +26,7 @@ #include "theory/quantifiers/sygus/cegis.h" #include "theory/quantifiers/sygus/cegis_core_connective.h" #include "theory/quantifiers/sygus/cegis_unif.h" +#include "theory/quantifiers/sygus/enum_val_generator.h" #include "theory/quantifiers/sygus/example_eval_cache.h" #include "theory/quantifiers/sygus/example_infer.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" @@ -42,37 +43,6 @@ class CegGrammarConstructor; class SygusPbe; class SygusStatistics; -/** - * A base class for generating values for actively-generated enumerators. - * At a high level, the job of this class is to accept a stream of "abstract - * values" a1, ..., an, ..., and generate a (possibly larger) stream of - * "concrete values" c11, ..., c1{m_1}, ..., cn1, ... cn{m_n}, .... - */ -class EnumValGenerator -{ - public: - virtual ~EnumValGenerator() {} - /** initialize this class with enumerator e */ - virtual void initialize(Node e) = 0; - /** Inform this generator that abstract value v was enumerated. */ - virtual void addValue(Node v) = 0; - /** - * Increment this value generator. If this returns false, then we are out of - * values. If this returns true, getCurrent(), if non-null, returns the - * current term. - * - * Notice that increment() may return true and afterwards it may be the case - * getCurrent() is null. We do this so that increment() does not take too - * much time per call, which can be the case for grammars where it is - * difficult to find the next (non-redundant) term. Returning true with - * a null current term gives the caller the chance to interleave other - * reasoning. - */ - virtual bool increment() = 0; - /** Get the current concrete value generated by this class. */ - virtual Node getCurrent() = 0; -}; - /** a synthesis conjecture * This class implements approaches for a synthesis conjecture, given by data * member d_quant. diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 826563401..3b0ea3312 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -359,23 +359,6 @@ Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn) return ret; } -unsigned TermDbSygus::getSygusTermSize( Node n ){ - if (n.getKind() != APPLY_CONSTRUCTOR) - { - return 0; - } - unsigned sum = 0; - for (unsigned i = 0; i < n.getNumChildren(); i++) - { - sum += getSygusTermSize(n[i]); - } - const DType& dt = datatypes::utils::datatypeOf(n.getOperator()); - int cindex = datatypes::utils::indexOf(n.getOperator()); - Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors()); - unsigned weight = dt[cindex].getWeight(); - return weight + sum; -} - bool TermDbSygus::registerSygusType(TypeNode tn) { std::map<TypeNode, bool>::iterator it = d_registerStatus.find(tn); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index e0a812069..80411b258 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -456,7 +456,6 @@ class TermDbSygus { Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ); Node getNormalized(TypeNode t, Node prog); - unsigned getSygusTermSize( Node n ); /** involves div-by-zero */ bool involvesDivByZero( Node n ); /** get anchor */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index bedab16f1..523b84e65 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -480,9 +480,8 @@ void TermDb::addTermHo(Node n) Node psk; if (itp == d_ho_fun_op_purify.end()) { - psk = sm->mkDummySkolem("pfun", - curr.getType(), - "purify for function operator term indexing"); + psk = sm->mkPurifySkolem( + curr, "pfun", "purify for function operator term indexing"); d_ho_fun_op_purify[curr] = psk; // we do not add it to d_ops since it is an internal operator } @@ -1034,7 +1033,10 @@ bool TermDb::reset( Theory::Effort effort ){ eq = itpe->second; } Trace("quant-ho") << "- assert purify equality : " << eq << std::endl; - ee->assertEquality(eq, true, eq); + // Note that ee may be the central equality engine, in which case this + // equality is explained trivially with "true", since both sides of + // eq are HOL and FOL encodings of the same thing. + ee->assertEquality(eq, true, d_true); if (!ee->consistent()) { // In some rare cases, purification functions (in the domain of diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index efede77ba..98130beb5 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -52,7 +52,7 @@ TheorySep::TheorySep(context::Context* c, d_lemmas_produced_c(u), d_bounds_init(false), d_state(c, u, valuation), - d_im(*this, d_state, nullptr, "theory::sep::"), + d_im(*this, d_state, pnm, "theory::sep::"), d_notify(*this), d_reduce(u), d_spatial_assertions(c) @@ -1785,11 +1785,12 @@ void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, InferenceId id, if( conc==d_false ){ Trace("sep-lemma") << "Sep::Conflict: " << ant << " by " << id << std::endl; - d_im.conflictExp(id, ant, nullptr); + d_im.conflictExp(id, PfRule::THEORY_INFERENCE, ant, {conc}); }else{ Trace("sep-lemma") << "Sep::Lemma: " << conc << " from " << ant << " by " << id << std::endl; - TrustNode trn = d_im.mkLemmaExp(conc, ant, {}); + TrustNode trn = + d_im.mkLemmaExp(conc, PfRule::THEORY_INFERENCE, ant, {}, {conc}); d_im.addPendingLemma( trn.getNode(), id, LemmaProperty::NONE, trn.getGenerator()); } diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index 73c6db35f..d0dc21839 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -92,7 +92,7 @@ bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int in || (atom.getKind() == EQUAL && atom[0].getType().isSet())) { // send to equality engine - if (assertInternalFact(atom, polarity, id, exp)) + if (assertSetsFact(atom, polarity, id, exp)) { // return true if this wasn't redundant return true; @@ -111,6 +111,17 @@ bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int in } return false; } + +bool InferenceManager::assertSetsFact(Node atom, + bool polarity, + InferenceId id, + Node exp) +{ + Node conc = polarity ? atom : atom.notNode(); + return assertInternalFact( + atom, polarity, id, PfRule::THEORY_INFERENCE, {exp}, {conc}); +} + void InferenceManager::assertInference(Node fact, InferenceId id, Node exp, diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h index 7a64b10c7..0a7c42e11 100644 --- a/src/theory/sets/inference_manager.h +++ b/src/theory/sets/inference_manager.h @@ -71,6 +71,10 @@ class InferenceManager : public InferenceManagerBuffered InferenceId id, std::vector<Node>& exp, int inferType = 0); + /** + * Immediately assert an internal fact with the default handling of proofs. + */ + bool assertSetsFact(Node atom, bool polarity, InferenceId id, Node exp); /** flush the splitting lemma ( n OR (NOT n) ) * diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 439e9443d..718077888 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -36,7 +36,7 @@ TheorySets::TheorySets(context::Context* c, : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm), d_skCache(), d_state(c, u, valuation, d_skCache), - d_im(*this, d_state, nullptr), + d_im(*this, d_state, pnm), d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, pnm)), d_notify(*d_internal.get(), d_im) { diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 42e317402..3817079a3 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -85,7 +85,7 @@ void TheorySetsPrivate::eqNotifyNewClass(TNode t) void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2) { - if (!d_state.isInConflict()) + if (!d_state.isInConflict() && t1.getType().isSet()) { Trace("sets-prop-debug") << "Merge " << t1 << " and " << t2 << "..." << std::endl; @@ -108,14 +108,15 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2) // infer equality between elements of singleton Node exp = s1.eqNode(s2); Node eq = s1[0].eqNode(s2[0]); - d_im.assertInternalFact(eq, true, InferenceId::SETS_SINGLETON_EQ, exp); + d_im.assertSetsFact(eq, true, InferenceId::SETS_SINGLETON_EQ, exp); } else { // singleton equal to emptyset, conflict Trace("sets-prop") << "Propagate conflict : " << s1 << " == " << s2 << std::endl; - d_im.conflictEqConstantMerge(s1, s2); + Node eqs = s1.eqNode(s2); + d_im.conflict(eqs, InferenceId::SETS_EQ_CONFLICT); return; } } @@ -149,7 +150,7 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2) Assert(f.getKind() == kind::IMPLIES); Trace("sets-prop") << "Propagate eq-mem eq inference : " << f[0] << " => " << f[1] << std::endl; - d_im.assertInternalFact(f[1], true, InferenceId::SETS_EQ_MEM, f[0]); + d_im.assertSetsFact(f[1], true, InferenceId::SETS_EQ_MEM, f[0]); } } } @@ -829,7 +830,7 @@ void TheorySetsPrivate::notifyFact(TNode atom, bool polarity, TNode fact) Trace("sets-prop") << "Propagate mem-eq : " << pexp << std::endl; Node eq = s[0].eqNode(atom[0]); // triggers an internal inference - d_im.assertInternalFact(eq, true, InferenceId::SETS_MEM_EQ, pexp); + d_im.assertSetsFact(eq, true, InferenceId::SETS_MEM_EQ, pexp); } } else @@ -907,7 +908,7 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1, { Trace("sets-cg-lemma") << "Should split on : " << x << "==" << y << std::endl; - d_im.split(x.eqNode(y), InferenceId::UNKNOWN); + d_im.split(x.eqNode(y), InferenceId::SETS_CG_SPLIT); } } } diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp index f2266c236..b020a3938 100644 --- a/src/theory/shared_solver.cpp +++ b/src/theory/shared_solver.cpp @@ -57,13 +57,17 @@ void SharedSolver::preRegister(TNode atom) // See term_registration_visitor.h for more details. if (d_logicInfo.isSharingEnabled()) { - // register it with the shared terms database if sharing is enabled - preRegisterSharedInternal(atom); // Collect the shared terms in atom, as well as calling preregister on the // appropriate theories in atom. // This calls Theory::preRegisterTerm and Theory::addSharedTerm, possibly // multiple times. NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, atom); + // Register it with the shared terms database if sharing is enabled. + // Notice that this must come *after* the above call, since we must ensure + // that all subterms of atom have already been added to the central + // equality engine before atom is added. This avoids spurious notifications + // from the equality engine. + preRegisterSharedInternal(atom); } else { diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 10c31edb7..891a3ca08 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -598,5 +598,26 @@ eq::EqualityEngine* Theory::getEqualityEngine() return d_equalityEngine; } +bool Theory::usesCentralEqualityEngine() const +{ + return usesCentralEqualityEngine(d_id); +} + +bool Theory::usesCentralEqualityEngine(TheoryId id) +{ + if (id == THEORY_BUILTIN) + { + return true; + } + if (options::eeMode() == options::EqEngineMode::DISTRIBUTED) + { + return false; + } + // Below are all theories with an equality engine except id ==THEORY_ARITH + return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS + || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS + || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV; +} + } // namespace theory } // namespace cvc5 diff --git a/src/theory/theory.h b/src/theory/theory.h index 4dbb7a436..7149d8e3f 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -307,13 +307,13 @@ class Theory { * class (see addSharedTerm). */ virtual void notifySharedTerm(TNode n); - /** * Notify in conflict, called when a conflict clause is added to TheoryEngine * by any theory (not necessarily this one). This signals that the theory * should suspend what it is currently doing and wait for backtracking. */ virtual void notifyInConflict(); + public: //--------------------------------- initialization /** @@ -876,6 +876,11 @@ class Theory { * E |= lit in the theory. */ virtual std::pair<bool, Node> entailmentCheck(TNode lit); + + /** uses central equality engine */ + bool usesCentralEqualityEngine() const; + /** uses central equality engine (static) */ + static bool usesCentralEqualityEngine(TheoryId id); };/* class Theory */ std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index bf196273e..f98f1cb6c 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -899,7 +899,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (no sharing)" << endl; Trace("dtview::conflict") << ":THEORY-CONFLICT: " << assertion << std::endl; - d_inConflict = true; + markInConflict(); } else { return; } @@ -954,7 +954,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo << endl; Trace("dtview::conflict") << ":THEORY-CONFLICT: " << assertion << std::endl; - d_inConflict = true; + markInConflict(); } } return; diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index bfd23fb23..bad90f061 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -393,7 +393,7 @@ bool TheoryInferenceManager::processInternalFact(TNode atom, Assert(d_ee != nullptr); Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: " << (pol ? Node(atom) : atom.notNode()) << " from " - << expn << std::endl; + << expn << " / " << iid << " " << id << std::endl; if (Configuration::isAssertionBuild()) { // check that all facts hold in the equality engine, to ensure that we @@ -431,10 +431,10 @@ bool TheoryInferenceManager::processInternalFact(TNode atom, } d_numCurrentFacts++; // Now, assert the fact. How to do so depends on whether proofs are enabled. - // If no proof production, or no proof rule was given bool ret = false; - if (d_pfee == nullptr || id == PfRule::UNKNOWN) + if (d_pfee == nullptr) { + Trace("infer-manager") << "...assert without proofs..." << std::endl; if (atom.getKind() == kind::EQUAL) { ret = d_ee->assertEquality(atom, pol, expn); @@ -453,6 +453,8 @@ bool TheoryInferenceManager::processInternalFact(TNode atom, } else { + Assert(id != PfRule::UNKNOWN); + Trace("infer-manager") << "...assert with proofs..." << std::endl; // Note that we reconstruct the original literal lit here, since both the // original literal is needed for bookkeeping proofs. It is possible to // optimize this so that a few less nodes are created, but at the cost @@ -472,7 +474,8 @@ bool TheoryInferenceManager::processInternalFact(TNode atom, // call the notify fact method with isInternal = true d_theory.notifyFact(atom, pol, expn, true); Trace("infer-manager") - << "TheoryInferenceManager::finished assertInternalFact" << std::endl; + << "TheoryInferenceManager::finished assertInternalFact, ret=" << ret + << std::endl; return ret; } diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index c61f4311b..cea0e698b 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -132,7 +132,7 @@ class TheoryInferenceManager * EqualityEngineNotify::eqNotifyTriggerPredicate and * EqualityEngineNotify::eqNotifyTriggerTermEquality. */ - bool propagateLit(TNode lit); + virtual bool propagateLit(TNode lit); /** * Return an explanation for the literal represented by parameter lit * (which was previously propagated by this theory). By default, this @@ -300,6 +300,8 @@ class TheoryInferenceManager * Theory's preNotifyFact and notifyFact method have been called with * isInternal = true. * + * Note this method should never be used when proofs are enabled. + * * @param atom The atom of the fact to assert * @param pol Its polarity * @param exp Its explanation, i.e. ( exp => (~) atom ) is valid. diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 6b2fae389..27b61e87d 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -1049,6 +1049,13 @@ Node EqProof::addToProof(CDProof* p, } // build constant application (f c1 ... cn) and equality (= (f c1 ... cn) c) Kind k = d_node[0].getKind(); + std::vector<Node> cargs; + cargs.push_back(ProofRuleChecker::mkKindNode(k)); + if (d_node[0].getMetaKind() == kind::metakind::PARAMETERIZED) + { + constChildren.insert(constChildren.begin(), d_node[0].getOperator()); + cargs.push_back(d_node[0].getOperator()); + } Node constApp = NodeManager::currentNM()->mkNode(k, constChildren); Node constEquality = constApp.eqNode(d_node[1]); Trace("eqproof-conv") << "EqProof::addToProof: adding " @@ -1060,11 +1067,7 @@ Node EqProof::addToProof(CDProof* p, Trace("eqproof-conv") << "EqProof::addToProof: adding " << PfRule::CONG << " step for " << congConclusion << " from " << subChildren << "\n"; - p->addStep(congConclusion, - PfRule::CONG, - {subChildren}, - {ProofRuleChecker::mkKindNode(k)}, - true); + p->addStep(congConclusion, PfRule::CONG, {subChildren}, cargs, true); Trace("eqproof-conv") << "EqProof::addToProof: adding " << PfRule::TRANS << " step for original conclusion " << d_node << "\n"; std::vector<Node> transitivityChildren{congConclusion, constEquality}; diff --git a/src/util/iand.h b/src/util/iand.h index 117ab6f02..6c29c38b4 100644 --- a/src/util/iand.h +++ b/src/util/iand.h @@ -39,7 +39,7 @@ struct IntAnd inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia); inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia) { - return os << "[" << ia.d_size << "]"; + return os << "(_ iand " << ia.d_size << ")"; } } // namespace cvc5 |