From e9c29bb348bd8fab5cedc48ab96ce2a0e6f98078 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 5 Jun 2020 10:19:10 -0500 Subject: (proof-new) Rename ProofSkolemCache to SkolemManager (#4556) This PR changes the design of ProofSkolemCache so that it has facilities for tracking proofs. This is required so that the term formula removal pass can be made proof-producing. This makes it so that ProofSkolemCache is renamed to SkolemManager, which lives in NodeManager. Creating (most) skolems must be accompanied by a corresponding ProofGenerator that can provide the proof for the existential corresponding to their witness form. Further updates will include refactoring the mkSkolemExists method of SkolemManager so that its contract wrt proofs is simpler. Once all calls to mkSkolem go through the standard interface, then NodeManager::mkSkolem will be moved to SkolemManager::mkSkolemInternal. --- src/theory/strings/skolem_cache.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/theory/strings/skolem_cache.cpp') diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 4af75f1cc..85a948567 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -82,12 +82,13 @@ Node SkolemCache::mkTypedSkolemCached( } NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); Node sk; switch (id) { // exists k. k = a case SK_PURIFY: - sk = ProofSkolemCache::mkPurifySkolem(a, c, "string purify skolem"); + sk = sm->mkPurifySkolem(a, c, "string purify skolem"); break; // these are eliminated by normalizeStringSkolem case SK_ID_V_SPT: @@ -113,7 +114,7 @@ Node SkolemCache::mkTypedSkolemCached( Notice() << "Don't know how to handle Skolem ID " << id << std::endl; Node v = nm->mkBoundVar(tn); Node cond = nm->mkConst(true); - sk = ProofSkolemCache::mkSkolem(v, cond, c, "string skolem"); + sk = sm->mkSkolem(v, cond, c, "string skolem"); } break; } -- cgit v1.2.3 From e37d0c385d698d46f14fb30e5a44de63c686fadb Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 16 Jun 2020 13:48:05 -0700 Subject: Update copyright headers. --- contrib/get-authors | 4 +++- contrib/update-copyright.pl | 4 ++-- examples/SimpleVC.java | 4 ++-- examples/api/bitvectors-new.cpp | 2 +- examples/api/bitvectors.cpp | 2 +- examples/api/bitvectors_and_arrays-new.cpp | 4 ++-- examples/api/bitvectors_and_arrays.cpp | 2 +- examples/api/combination-new.cpp | 4 ++-- examples/api/combination.cpp | 4 ++-- examples/api/datatypes-new.cpp | 4 ++-- examples/api/datatypes.cpp | 4 ++-- examples/api/extract-new.cpp | 2 +- examples/api/extract.cpp | 4 ++-- examples/api/helloworld-new.cpp | 4 ++-- examples/api/helloworld.cpp | 2 +- examples/api/java/BitVectors.java | 4 ++-- examples/api/java/BitVectorsAndArrays.java | 4 ++-- examples/api/java/CVC4Streams.java | 4 ++-- examples/api/java/Combination.java | 4 ++-- examples/api/java/Datatypes.java | 4 ++-- examples/api/java/Exceptions.java | 2 +- examples/api/java/FloatingPointArith.java | 2 +- examples/api/java/HelloWorld.java | 4 ++-- examples/api/java/LinearArith.java | 4 ++-- examples/api/java/PipedInput.java | 4 ++-- examples/api/java/Relations.java | 2 +- examples/api/java/Statistics.java | 2 +- examples/api/java/Strings.java | 4 ++-- examples/api/java/UnsatCores.java | 4 ++-- examples/api/linear_arith-new.cpp | 4 ++-- examples/api/linear_arith.cpp | 4 ++-- examples/api/sets-new.cpp | 4 ++-- examples/api/sets.cpp | 4 ++-- examples/api/strings-new.cpp | 4 ++-- examples/api/strings.cpp | 2 +- examples/api/sygus-fun.cpp | 4 ++-- examples/api/sygus-grammar.cpp | 4 ++-- examples/api/sygus-inv.cpp | 4 ++-- examples/hashsmt/sha1.hpp | 2 +- examples/hashsmt/sha1_collision.cpp | 2 +- examples/hashsmt/sha1_inversion.cpp | 2 +- examples/hashsmt/word.cpp | 2 +- examples/hashsmt/word.h | 2 +- examples/nra-translate/normalize.cpp | 2 +- examples/nra-translate/smt2info.cpp | 2 +- examples/nra-translate/smt2todreal.cpp | 2 +- examples/nra-translate/smt2toisat.cpp | 2 +- examples/nra-translate/smt2tomathematica.cpp | 2 +- examples/nra-translate/smt2toqepcad.cpp | 2 +- examples/nra-translate/smt2toredlog.cpp | 2 +- examples/sets-translate/sets_translate.cpp | 2 +- examples/simple_vc_cxx.cpp | 4 ++-- examples/simple_vc_quant_cxx.cpp | 2 +- examples/translator.cpp | 4 ++-- src/api/cvc4cpp.cpp | 4 ++-- src/api/cvc4cpp.h | 4 ++-- src/api/cvc4cppkind.h | 4 ++-- src/base/check.cpp | 4 ++-- src/base/check.h | 4 ++-- src/base/configuration.cpp | 2 +- src/base/configuration.h | 2 +- src/base/configuration_private.h | 4 ++-- src/base/exception.cpp | 2 +- src/base/exception.h | 4 ++-- src/base/git_versioninfo.cpp.in | 2 +- src/base/listener.cpp | 2 +- src/base/listener.h | 4 ++-- src/base/map_util.h | 4 ++-- src/base/modal_exception.h | 4 ++-- src/base/output.cpp | 2 +- src/base/output.h | 2 +- src/bindings/java_iterator_adapter.h | 4 ++-- src/bindings/java_stream_adapters.h | 4 ++-- src/bindings/swig.h | 4 ++-- src/context/backtrackable.h | 4 ++-- src/context/cddense_set.h | 2 +- src/context/cdhashmap.h | 2 +- src/context/cdhashmap_forward.h | 4 ++-- src/context/cdhashset.h | 4 ++-- src/context/cdhashset_forward.h | 4 ++-- src/context/cdinsert_hashmap.h | 2 +- src/context/cdinsert_hashmap_forward.h | 4 ++-- src/context/cdlist.h | 2 +- src/context/cdlist_forward.h | 4 ++-- src/context/cdmaybe.h | 2 +- src/context/cdo.h | 4 ++-- src/context/cdqueue.h | 4 ++-- src/context/cdtrail_queue.h | 4 ++-- src/context/context.cpp | 2 +- src/context/context.h | 2 +- src/context/context_mm.cpp | 2 +- src/context/context_mm.h | 2 +- src/decision/decision_attributes.h | 4 ++-- src/decision/decision_engine.cpp | 4 ++-- src/decision/decision_engine.h | 4 ++-- src/decision/decision_strategy.h | 4 ++-- src/decision/justification_heuristic.cpp | 4 ++-- src/decision/justification_heuristic.h | 4 ++-- src/expr/array.h | 4 ++-- src/expr/array_store_all.cpp | 2 +- src/expr/array_store_all.h | 4 ++-- src/expr/ascription_type.h | 4 ++-- src/expr/attribute.cpp | 2 +- src/expr/attribute.h | 2 +- src/expr/attribute_internals.h | 4 ++-- src/expr/attribute_unique_id.h | 2 +- src/expr/datatype.cpp | 2 +- src/expr/datatype.h | 2 +- src/expr/dtype.cpp | 4 ++-- src/expr/dtype.h | 4 ++-- src/expr/dtype_cons.cpp | 4 ++-- src/expr/dtype_cons.h | 4 ++-- src/expr/dtype_selector.cpp | 2 +- src/expr/dtype_selector.h | 4 ++-- src/expr/emptyset.cpp | 2 +- src/expr/emptyset.h | 2 +- src/expr/expr_iomanip.cpp | 2 +- src/expr/expr_iomanip.h | 4 ++-- src/expr/expr_manager_scope.h | 4 ++-- src/expr/expr_manager_template.cpp | 2 +- src/expr/expr_manager_template.h | 4 ++-- src/expr/expr_sequence.cpp | 2 +- src/expr/expr_sequence.h | 2 +- src/expr/expr_template.cpp | 4 ++-- src/expr/expr_template.h | 2 +- src/expr/kind_map.h | 4 ++-- src/expr/kind_template.cpp | 4 ++-- src/expr/kind_template.h | 4 ++-- src/expr/lazy_proof.cpp | 2 +- src/expr/lazy_proof.h | 2 +- src/expr/match_trie.cpp | 2 +- src/expr/match_trie.h | 4 ++-- src/expr/metakind_template.cpp | 4 ++-- src/expr/metakind_template.h | 4 ++-- src/expr/node.cpp | 2 +- src/expr/node.h | 4 ++-- src/expr/node_algorithm.cpp | 4 ++-- src/expr/node_algorithm.h | 4 ++-- src/expr/node_builder.h | 4 ++-- src/expr/node_manager.cpp | 2 +- src/expr/node_manager.h | 2 +- src/expr/node_manager_attributes.h | 2 +- src/expr/node_manager_listeners.cpp | 2 +- src/expr/node_manager_listeners.h | 2 +- src/expr/node_self_iterator.h | 4 ++-- src/expr/node_traversal.cpp | 2 +- src/expr/node_traversal.h | 2 +- src/expr/node_trie.cpp | 2 +- src/expr/node_trie.h | 4 ++-- src/expr/node_value.cpp | 4 ++-- src/expr/node_value.h | 4 ++-- src/expr/node_visitor.h | 4 ++-- src/expr/proof.cpp | 2 +- src/expr/proof.h | 2 +- src/expr/proof_checker.cpp | 2 +- src/expr/proof_checker.h | 2 +- src/expr/proof_generator.cpp | 2 +- src/expr/proof_generator.h | 2 +- src/expr/proof_node.cpp | 2 +- src/expr/proof_node.h | 2 +- src/expr/proof_node_algorithm.cpp | 2 +- src/expr/proof_node_algorithm.h | 2 +- src/expr/proof_node_manager.cpp | 2 +- src/expr/proof_node_manager.h | 2 +- src/expr/proof_node_to_sexpr.cpp | 2 +- src/expr/proof_node_to_sexpr.h | 4 ++-- src/expr/proof_rule.cpp | 4 ++-- src/expr/proof_rule.h | 4 ++-- src/expr/proof_step_buffer.cpp | 2 +- src/expr/proof_step_buffer.h | 2 +- src/expr/record.cpp | 4 ++-- src/expr/record.h | 4 ++-- src/expr/sequence.cpp | 2 +- src/expr/sequence.h | 2 +- src/expr/skolem_manager.cpp | 2 +- src/expr/skolem_manager.h | 2 +- src/expr/sygus_datatype.cpp | 4 ++-- src/expr/sygus_datatype.h | 4 ++-- src/expr/symbol_table.cpp | 2 +- src/expr/symbol_table.h | 2 +- src/expr/term_canonize.cpp | 2 +- src/expr/term_canonize.h | 2 +- src/expr/term_conversion_proof_generator.cpp | 2 +- src/expr/term_conversion_proof_generator.h | 2 +- src/expr/type.cpp | 4 ++-- src/expr/type.h | 4 ++-- src/expr/type_checker.h | 4 ++-- src/expr/type_checker_template.cpp | 4 ++-- src/expr/type_checker_util.h | 2 +- src/expr/type_matcher.cpp | 4 ++-- src/expr/type_matcher.h | 4 ++-- src/expr/type_node.cpp | 2 +- src/expr/type_node.h | 2 +- src/expr/type_properties_template.h | 4 ++-- src/expr/uninterpreted_constant.cpp | 4 ++-- src/expr/uninterpreted_constant.h | 2 +- src/expr/variable_type_map.h | 4 ++-- src/include/cvc4.h | 4 ++-- src/include/cvc4_private.h | 4 ++-- src/include/cvc4_private_library.h | 4 ++-- src/include/cvc4_public.h | 4 ++-- src/include/cvc4parser_private.h | 2 +- src/include/cvc4parser_public.h | 2 +- src/lib/clock_gettime.c | 2 +- src/lib/clock_gettime.h | 4 ++-- src/lib/ffs.c | 2 +- src/lib/ffs.h | 4 ++-- src/lib/replacements.h | 4 ++-- src/lib/strtok_r.c | 2 +- src/lib/strtok_r.h | 4 ++-- src/main/command_executor.cpp | 4 ++-- src/main/command_executor.h | 4 ++-- src/main/driver_unified.cpp | 4 ++-- src/main/interactive_shell.cpp | 2 +- src/main/interactive_shell.h | 2 +- src/main/main.cpp | 2 +- src/main/main.h | 4 ++-- src/main/util.cpp | 2 +- src/options/base_handlers.h | 4 ++-- src/options/decision_weight.h | 4 ++-- src/options/didyoumean.cpp | 2 +- src/options/didyoumean.h | 2 +- src/options/didyoumean_test.cpp | 4 ++-- src/options/language.cpp | 4 ++-- src/options/language.h | 2 +- src/options/module_template.cpp | 2 +- src/options/module_template.h | 2 +- src/options/open_ostream.cpp | 2 +- src/options/open_ostream.h | 4 ++-- src/options/option_exception.cpp | 2 +- src/options/option_exception.h | 4 ++-- src/options/options.h | 2 +- src/options/options_handler.cpp | 4 ++-- src/options/options_handler.h | 4 ++-- src/options/options_holder_template.h | 4 ++-- src/options/options_public_functions.cpp | 4 ++-- src/options/options_template.cpp | 4 ++-- src/options/printer_modes.cpp | 4 ++-- src/options/printer_modes.h | 4 ++-- src/options/set_language.cpp | 2 +- src/options/set_language.h | 4 ++-- src/parser/antlr_input.cpp | 4 ++-- src/parser/antlr_input.h | 2 +- src/parser/antlr_input_imports.cpp | 2 +- src/parser/antlr_line_buffered_input.cpp | 2 +- src/parser/antlr_line_buffered_input.h | 4 ++-- src/parser/antlr_tracing.h | 4 ++-- src/parser/bounded_token_buffer.cpp | 2 +- src/parser/bounded_token_buffer.h | 4 ++-- src/parser/bounded_token_factory.cpp | 2 +- src/parser/bounded_token_factory.h | 4 ++-- src/parser/cvc/Cvc.g | 2 +- src/parser/cvc/cvc.cpp | 4 ++-- src/parser/cvc/cvc.h | 4 ++-- src/parser/cvc/cvc_input.cpp | 4 ++-- src/parser/cvc/cvc_input.h | 4 ++-- src/parser/input.cpp | 2 +- src/parser/input.h | 2 +- src/parser/line_buffer.cpp | 4 ++-- src/parser/line_buffer.h | 4 ++-- src/parser/memory_mapped_input_buffer.cpp | 2 +- src/parser/memory_mapped_input_buffer.h | 4 ++-- src/parser/parse_op.cpp | 2 +- src/parser/parse_op.h | 2 +- src/parser/parser.cpp | 4 ++-- src/parser/parser.h | 4 ++-- src/parser/parser_builder.cpp | 2 +- src/parser/parser_builder.h | 2 +- src/parser/parser_exception.h | 2 +- src/parser/smt2/Smt2.g | 4 ++-- src/parser/smt2/smt2.cpp | 4 ++-- src/parser/smt2/smt2.h | 4 ++-- src/parser/smt2/smt2_input.cpp | 4 ++-- src/parser/smt2/smt2_input.h | 4 ++-- src/parser/smt2/sygus_input.cpp | 4 ++-- src/parser/smt2/sygus_input.h | 4 ++-- src/parser/tptp/Tptp.g | 4 ++-- src/parser/tptp/tptp.cpp | 4 ++-- src/parser/tptp/tptp.h | 4 ++-- src/parser/tptp/tptp_input.cpp | 4 ++-- src/parser/tptp/tptp_input.h | 4 ++-- src/preprocessing/assertion_pipeline.cpp | 2 +- src/preprocessing/assertion_pipeline.h | 2 +- src/preprocessing/passes/ackermann.cpp | 4 ++-- src/preprocessing/passes/ackermann.h | 4 ++-- src/preprocessing/passes/apply_substs.cpp | 4 ++-- src/preprocessing/passes/apply_substs.h | 4 ++-- src/preprocessing/passes/bool_to_bv.cpp | 2 +- src/preprocessing/passes/bool_to_bv.h | 4 ++-- src/preprocessing/passes/bv_abstraction.cpp | 2 +- src/preprocessing/passes/bv_abstraction.h | 2 +- src/preprocessing/passes/bv_eager_atoms.cpp | 2 +- src/preprocessing/passes/bv_eager_atoms.h | 2 +- src/preprocessing/passes/bv_gauss.cpp | 4 ++-- src/preprocessing/passes/bv_gauss.h | 4 ++-- src/preprocessing/passes/bv_intro_pow2.cpp | 2 +- src/preprocessing/passes/bv_intro_pow2.h | 2 +- src/preprocessing/passes/bv_to_bool.cpp | 2 +- src/preprocessing/passes/bv_to_bool.h | 4 ++-- src/preprocessing/passes/bv_to_int.cpp | 4 ++-- src/preprocessing/passes/bv_to_int.h | 4 ++-- src/preprocessing/passes/extended_rewriter_pass.cpp | 2 +- src/preprocessing/passes/extended_rewriter_pass.h | 4 ++-- src/preprocessing/passes/global_negate.cpp | 2 +- src/preprocessing/passes/global_negate.h | 4 ++-- src/preprocessing/passes/ho_elim.cpp | 2 +- src/preprocessing/passes/ho_elim.h | 2 +- src/preprocessing/passes/int_to_bv.cpp | 4 ++-- src/preprocessing/passes/int_to_bv.h | 4 ++-- src/preprocessing/passes/ite_removal.cpp | 4 ++-- src/preprocessing/passes/ite_removal.h | 4 ++-- src/preprocessing/passes/ite_simp.cpp | 2 +- src/preprocessing/passes/ite_simp.h | 4 ++-- src/preprocessing/passes/miplib_trick.cpp | 4 ++-- src/preprocessing/passes/miplib_trick.h | 2 +- src/preprocessing/passes/nl_ext_purify.cpp | 4 ++-- src/preprocessing/passes/nl_ext_purify.h | 4 ++-- src/preprocessing/passes/non_clausal_simp.cpp | 4 ++-- src/preprocessing/passes/non_clausal_simp.h | 4 ++-- src/preprocessing/passes/pseudo_boolean_processor.cpp | 2 +- src/preprocessing/passes/pseudo_boolean_processor.h | 4 ++-- src/preprocessing/passes/quantifier_macros.cpp | 4 ++-- src/preprocessing/passes/quantifier_macros.h | 4 ++-- src/preprocessing/passes/quantifiers_preprocess.cpp | 2 +- src/preprocessing/passes/quantifiers_preprocess.h | 4 ++-- src/preprocessing/passes/real_to_int.cpp | 4 ++-- src/preprocessing/passes/real_to_int.h | 4 ++-- src/preprocessing/passes/rewrite.cpp | 2 +- src/preprocessing/passes/rewrite.h | 4 ++-- src/preprocessing/passes/sep_skolem_emp.cpp | 2 +- src/preprocessing/passes/sep_skolem_emp.h | 4 ++-- src/preprocessing/passes/sort_infer.cpp | 2 +- src/preprocessing/passes/sort_infer.h | 4 ++-- src/preprocessing/passes/static_learning.cpp | 4 ++-- src/preprocessing/passes/static_learning.h | 4 ++-- src/preprocessing/passes/sygus_inference.cpp | 4 ++-- src/preprocessing/passes/sygus_inference.h | 4 ++-- src/preprocessing/passes/synth_rew_rules.cpp | 4 ++-- src/preprocessing/passes/synth_rew_rules.h | 4 ++-- src/preprocessing/passes/theory_preprocess.cpp | 2 +- src/preprocessing/passes/theory_preprocess.h | 2 +- src/preprocessing/passes/unconstrained_simplifier.cpp | 4 ++-- src/preprocessing/passes/unconstrained_simplifier.h | 4 ++-- src/preprocessing/preprocessing_pass.cpp | 2 +- src/preprocessing/preprocessing_pass.h | 4 ++-- src/preprocessing/preprocessing_pass_context.cpp | 2 +- src/preprocessing/preprocessing_pass_context.h | 4 ++-- src/preprocessing/preprocessing_pass_registry.cpp | 4 ++-- src/preprocessing/preprocessing_pass_registry.h | 4 ++-- src/preprocessing/util/ite_utilities.cpp | 2 +- src/preprocessing/util/ite_utilities.h | 2 +- src/printer/ast/ast_printer.cpp | 4 ++-- src/printer/ast/ast_printer.h | 4 ++-- src/printer/cvc/cvc_printer.cpp | 2 +- src/printer/cvc/cvc_printer.h | 4 ++-- src/printer/dagification_visitor.cpp | 4 ++-- src/printer/dagification_visitor.h | 4 ++-- src/printer/printer.cpp | 2 +- src/printer/printer.h | 4 ++-- src/printer/smt2/smt2_printer.cpp | 2 +- src/printer/smt2/smt2_printer.h | 2 +- src/printer/sygus_print_callback.cpp | 2 +- src/printer/sygus_print_callback.h | 4 ++-- src/printer/tptp/tptp_printer.cpp | 4 ++-- src/printer/tptp/tptp_printer.h | 2 +- src/proof/arith_proof.cpp | 4 ++-- src/proof/arith_proof.h | 2 +- src/proof/arith_proof_recorder.cpp | 2 +- src/proof/arith_proof_recorder.h | 4 ++-- src/proof/array_proof.cpp | 2 +- src/proof/array_proof.h | 2 +- src/proof/bitvector_proof.cpp | 2 +- src/proof/bitvector_proof.h | 2 +- src/proof/clausal_bitvector_proof.cpp | 4 ++-- src/proof/clausal_bitvector_proof.h | 2 +- src/proof/clause_id.h | 4 ++-- src/proof/cnf_proof.cpp | 2 +- src/proof/cnf_proof.h | 2 +- src/proof/dimacs.cpp | 2 +- src/proof/dimacs.h | 2 +- src/proof/drat/drat_proof.cpp | 4 ++-- src/proof/drat/drat_proof.h | 4 ++-- src/proof/er/er_proof.cpp | 4 ++-- src/proof/er/er_proof.h | 4 ++-- src/proof/lemma_proof.cpp | 4 ++-- src/proof/lemma_proof.h | 4 ++-- src/proof/lfsc_proof_printer.cpp | 2 +- src/proof/lfsc_proof_printer.h | 4 ++-- src/proof/lrat/lrat_proof.cpp | 4 ++-- src/proof/lrat/lrat_proof.h | 4 ++-- src/proof/proof.h | 4 ++-- src/proof/proof_manager.cpp | 2 +- src/proof/proof_manager.h | 4 ++-- src/proof/proof_output_channel.cpp | 2 +- src/proof/proof_output_channel.h | 2 +- src/proof/proof_utils.cpp | 2 +- src/proof/proof_utils.h | 2 +- src/proof/resolution_bitvector_proof.cpp | 2 +- src/proof/resolution_bitvector_proof.h | 2 +- src/proof/sat_proof.h | 2 +- src/proof/sat_proof_implementation.h | 2 +- src/proof/simplify_boolean_node.cpp | 2 +- src/proof/simplify_boolean_node.h | 4 ++-- src/proof/skolemization_manager.cpp | 4 ++-- src/proof/skolemization_manager.h | 4 ++-- src/proof/theory_proof.cpp | 2 +- src/proof/theory_proof.h | 4 ++-- src/proof/uf_proof.cpp | 2 +- src/proof/uf_proof.h | 4 ++-- src/proof/unsat_core.cpp | 2 +- src/proof/unsat_core.h | 4 ++-- src/prop/bv_sat_solver_notify.h | 4 ++-- src/prop/bvminisat/bvminisat.cpp | 2 +- src/prop/bvminisat/bvminisat.h | 2 +- src/prop/cadical.cpp | 4 ++-- src/prop/cadical.h | 4 ++-- src/prop/cnf_stream.cpp | 2 +- src/prop/cnf_stream.h | 2 +- src/prop/cryptominisat.cpp | 2 +- src/prop/cryptominisat.h | 4 ++-- src/prop/minisat/minisat.cpp | 2 +- src/prop/minisat/minisat.h | 4 ++-- src/prop/prop_engine.cpp | 2 +- src/prop/prop_engine.h | 2 +- src/prop/registrar.h | 4 ++-- src/prop/sat_solver.h | 2 +- src/prop/sat_solver_factory.cpp | 4 ++-- src/prop/sat_solver_factory.h | 4 ++-- src/prop/sat_solver_types.cpp | 2 +- src/prop/sat_solver_types.h | 4 ++-- src/prop/theory_proxy.cpp | 4 ++-- src/prop/theory_proxy.h | 4 ++-- src/smt/command.cpp | 2 +- src/smt/command.h | 2 +- src/smt/command_list.cpp | 2 +- src/smt/command_list.h | 4 ++-- src/smt/defined_function.h | 2 +- src/smt/dump.cpp | 4 ++-- src/smt/dump.h | 2 +- src/smt/logic_exception.h | 4 ++-- src/smt/logic_request.cpp | 2 +- src/smt/logic_request.h | 4 ++-- src/smt/managed_ostreams.cpp | 2 +- src/smt/managed_ostreams.h | 2 +- src/smt/model.cpp | 4 ++-- src/smt/model.h | 4 ++-- src/smt/model_blocker.cpp | 4 ++-- src/smt/model_blocker.h | 4 ++-- src/smt/model_core_builder.cpp | 4 ++-- src/smt/model_core_builder.h | 4 ++-- src/smt/process_assertions.cpp | 4 ++-- src/smt/process_assertions.h | 4 ++-- src/smt/set_defaults.cpp | 4 ++-- src/smt/set_defaults.h | 2 +- src/smt/smt_engine.cpp | 4 ++-- src/smt/smt_engine.h | 4 ++-- src/smt/smt_engine_scope.cpp | 4 ++-- src/smt/smt_engine_scope.h | 2 +- src/smt/smt_engine_stats.cpp | 2 +- src/smt/smt_engine_stats.h | 2 +- src/smt/smt_statistics_registry.cpp | 2 +- src/smt/smt_statistics_registry.h | 4 ++-- src/smt/term_formula_removal.cpp | 4 ++-- src/smt/term_formula_removal.h | 2 +- src/smt/update_ostream.h | 2 +- src/smt_util/boolean_simplification.cpp | 2 +- src/smt_util/boolean_simplification.h | 4 ++-- src/smt_util/nary_builder.cpp | 4 ++-- src/smt_util/nary_builder.h | 2 +- src/theory/arith/approx_simplex.cpp | 4 ++-- src/theory/arith/approx_simplex.h | 2 +- src/theory/arith/arith_ite_utils.cpp | 4 ++-- src/theory/arith/arith_ite_utils.h | 4 ++-- src/theory/arith/arith_msum.cpp | 2 +- src/theory/arith/arith_msum.h | 4 ++-- src/theory/arith/arith_rewriter.cpp | 2 +- src/theory/arith/arith_rewriter.h | 4 ++-- src/theory/arith/arith_static_learner.cpp | 2 +- src/theory/arith/arith_static_learner.h | 4 ++-- src/theory/arith/arith_utilities.cpp | 4 ++-- src/theory/arith/arith_utilities.h | 4 ++-- src/theory/arith/arithvar.cpp | 2 +- src/theory/arith/arithvar.h | 2 +- src/theory/arith/arithvar_node_map.h | 4 ++-- src/theory/arith/attempt_solution_simplex.cpp | 4 ++-- src/theory/arith/attempt_solution_simplex.h | 2 +- src/theory/arith/bound_counts.h | 2 +- src/theory/arith/callbacks.cpp | 4 ++-- src/theory/arith/callbacks.h | 2 +- src/theory/arith/congruence_manager.cpp | 4 ++-- src/theory/arith/congruence_manager.h | 4 ++-- src/theory/arith/constraint.cpp | 4 ++-- src/theory/arith/constraint.h | 2 +- src/theory/arith/constraint_forward.h | 4 ++-- src/theory/arith/cut_log.cpp | 4 ++-- src/theory/arith/cut_log.h | 2 +- src/theory/arith/delta_rational.cpp | 2 +- src/theory/arith/delta_rational.h | 2 +- src/theory/arith/dio_solver.cpp | 4 ++-- src/theory/arith/dio_solver.h | 4 ++-- src/theory/arith/dual_simplex.cpp | 4 ++-- src/theory/arith/dual_simplex.h | 2 +- src/theory/arith/error_set.cpp | 4 ++-- src/theory/arith/error_set.h | 4 ++-- src/theory/arith/fc_simplex.cpp | 4 ++-- src/theory/arith/fc_simplex.h | 2 +- src/theory/arith/infer_bounds.cpp | 2 +- src/theory/arith/infer_bounds.h | 2 +- src/theory/arith/linear_equality.cpp | 4 ++-- src/theory/arith/linear_equality.h | 2 +- src/theory/arith/matrix.cpp | 2 +- src/theory/arith/matrix.h | 2 +- src/theory/arith/nl/nl_constraint.cpp | 4 ++-- src/theory/arith/nl/nl_constraint.h | 4 ++-- src/theory/arith/nl/nl_lemma_utils.cpp | 2 +- src/theory/arith/nl/nl_lemma_utils.h | 4 ++-- src/theory/arith/nl/nl_model.cpp | 4 ++-- src/theory/arith/nl/nl_model.h | 4 ++-- src/theory/arith/nl/nl_monomial.cpp | 4 ++-- src/theory/arith/nl/nl_monomial.h | 2 +- src/theory/arith/nl/nl_solver.cpp | 4 ++-- src/theory/arith/nl/nl_solver.h | 4 ++-- src/theory/arith/nl/nonlinear_extension.cpp | 2 +- src/theory/arith/nl/nonlinear_extension.h | 4 ++-- src/theory/arith/nl/transcendental_solver.cpp | 4 ++-- src/theory/arith/nl/transcendental_solver.h | 4 ++-- src/theory/arith/normal_form.cpp | 2 +- src/theory/arith/normal_form.h | 4 ++-- src/theory/arith/partial_model.cpp | 2 +- src/theory/arith/partial_model.h | 4 ++-- src/theory/arith/simplex.cpp | 2 +- src/theory/arith/simplex.h | 4 ++-- src/theory/arith/simplex_update.cpp | 2 +- src/theory/arith/simplex_update.h | 2 +- src/theory/arith/soi_simplex.cpp | 4 ++-- src/theory/arith/soi_simplex.h | 2 +- src/theory/arith/tableau.cpp | 2 +- src/theory/arith/tableau.h | 2 +- src/theory/arith/tableau_sizes.cpp | 2 +- src/theory/arith/tableau_sizes.h | 2 +- src/theory/arith/theory_arith.cpp | 4 ++-- src/theory/arith/theory_arith.h | 2 +- src/theory/arith/theory_arith_private.cpp | 4 ++-- src/theory/arith/theory_arith_private.h | 2 +- src/theory/arith/theory_arith_private_forward.h | 2 +- src/theory/arith/theory_arith_type_rules.h | 4 ++-- src/theory/arith/type_enumerator.h | 4 ++-- src/theory/arrays/array_info.cpp | 2 +- src/theory/arrays/array_info.h | 2 +- src/theory/arrays/array_proof_reconstruction.cpp | 2 +- src/theory/arrays/array_proof_reconstruction.h | 4 ++-- src/theory/arrays/static_fact_manager.cpp | 4 ++-- src/theory/arrays/static_fact_manager.h | 4 ++-- src/theory/arrays/theory_arrays.cpp | 2 +- src/theory/arrays/theory_arrays.h | 2 +- src/theory/arrays/theory_arrays_rewriter.cpp | 2 +- src/theory/arrays/theory_arrays_rewriter.h | 4 ++-- src/theory/arrays/theory_arrays_type_rules.h | 2 +- src/theory/arrays/type_enumerator.h | 2 +- src/theory/arrays/union_find.cpp | 2 +- src/theory/arrays/union_find.h | 4 ++-- src/theory/assertion.cpp | 4 ++-- src/theory/assertion.h | 4 ++-- src/theory/atom_requests.cpp | 4 ++-- src/theory/atom_requests.h | 4 ++-- src/theory/booleans/circuit_propagator.cpp | 2 +- src/theory/booleans/circuit_propagator.h | 2 +- src/theory/booleans/proof_checker.cpp | 4 ++-- src/theory/booleans/proof_checker.h | 4 ++-- src/theory/booleans/theory_bool.cpp | 2 +- src/theory/booleans/theory_bool.h | 4 ++-- src/theory/booleans/theory_bool_rewriter.cpp | 2 +- src/theory/booleans/theory_bool_rewriter.h | 4 ++-- src/theory/booleans/theory_bool_type_rules.h | 2 +- src/theory/booleans/type_enumerator.h | 4 ++-- src/theory/builtin/proof_checker.cpp | 2 +- src/theory/builtin/proof_checker.h | 2 +- src/theory/builtin/theory_builtin.cpp | 4 ++-- src/theory/builtin/theory_builtin.h | 4 ++-- src/theory/builtin/theory_builtin_rewriter.cpp | 4 ++-- src/theory/builtin/theory_builtin_rewriter.h | 4 ++-- src/theory/builtin/theory_builtin_type_rules.h | 2 +- src/theory/builtin/type_enumerator.cpp | 2 +- src/theory/builtin/type_enumerator.h | 2 +- src/theory/bv/abstraction.cpp | 2 +- src/theory/bv/abstraction.h | 4 ++-- src/theory/bv/bitblast/aig_bitblaster.cpp | 2 +- src/theory/bv/bitblast/aig_bitblaster.h | 2 +- src/theory/bv/bitblast/bitblast_strategies_template.h | 2 +- src/theory/bv/bitblast/bitblast_utils.h | 2 +- src/theory/bv/bitblast/bitblaster.h | 2 +- src/theory/bv/bitblast/eager_bitblaster.cpp | 2 +- src/theory/bv/bitblast/eager_bitblaster.h | 2 +- src/theory/bv/bitblast/lazy_bitblaster.cpp | 2 +- src/theory/bv/bitblast/lazy_bitblaster.h | 4 ++-- src/theory/bv/bv_eager_solver.cpp | 2 +- src/theory/bv/bv_eager_solver.h | 2 +- src/theory/bv/bv_inequality_graph.cpp | 4 ++-- src/theory/bv/bv_inequality_graph.h | 4 ++-- src/theory/bv/bv_quick_check.cpp | 2 +- src/theory/bv/bv_quick_check.h | 4 ++-- src/theory/bv/bv_subtheory.h | 2 +- src/theory/bv/bv_subtheory_algebraic.cpp | 2 +- src/theory/bv/bv_subtheory_algebraic.h | 2 +- src/theory/bv/bv_subtheory_bitblast.cpp | 2 +- src/theory/bv/bv_subtheory_bitblast.h | 2 +- src/theory/bv/bv_subtheory_core.cpp | 2 +- src/theory/bv/bv_subtheory_core.h | 2 +- src/theory/bv/bv_subtheory_inequality.cpp | 2 +- src/theory/bv/bv_subtheory_inequality.h | 2 +- src/theory/bv/slicer.cpp | 4 ++-- src/theory/bv/slicer.h | 4 ++-- src/theory/bv/theory_bv.cpp | 2 +- src/theory/bv/theory_bv.h | 4 ++-- src/theory/bv/theory_bv_rewrite_rules.h | 2 +- .../bv/theory_bv_rewrite_rules_constant_evaluation.h | 2 +- src/theory/bv/theory_bv_rewrite_rules_core.h | 2 +- src/theory/bv/theory_bv_rewrite_rules_normalization.h | 2 +- .../bv/theory_bv_rewrite_rules_operator_elimination.h | 4 ++-- src/theory/bv/theory_bv_rewrite_rules_simplification.h | 2 +- src/theory/bv/theory_bv_rewriter.cpp | 2 +- src/theory/bv/theory_bv_rewriter.h | 4 ++-- src/theory/bv/theory_bv_type_rules.h | 4 ++-- src/theory/bv/theory_bv_utils.cpp | 4 ++-- src/theory/bv/theory_bv_utils.h | 4 ++-- src/theory/bv/type_enumerator.h | 2 +- src/theory/care_graph.h | 4 ++-- src/theory/datatypes/datatypes_rewriter.cpp | 4 ++-- src/theory/datatypes/datatypes_rewriter.h | 4 ++-- src/theory/datatypes/sygus_datatype_utils.cpp | 4 ++-- src/theory/datatypes/sygus_datatype_utils.h | 2 +- src/theory/datatypes/sygus_extension.cpp | 4 ++-- src/theory/datatypes/sygus_extension.h | 4 ++-- src/theory/datatypes/sygus_simple_sym.cpp | 4 ++-- src/theory/datatypes/sygus_simple_sym.h | 4 ++-- src/theory/datatypes/theory_datatypes.cpp | 4 ++-- src/theory/datatypes/theory_datatypes.h | 2 +- src/theory/datatypes/theory_datatypes_type_rules.h | 2 +- src/theory/datatypes/theory_datatypes_utils.cpp | 4 ++-- src/theory/datatypes/theory_datatypes_utils.h | 4 ++-- src/theory/datatypes/type_enumerator.cpp | 2 +- src/theory/datatypes/type_enumerator.h | 4 ++-- src/theory/decision_manager.cpp | 2 +- src/theory/decision_manager.h | 4 ++-- src/theory/decision_strategy.cpp | 2 +- src/theory/decision_strategy.h | 4 ++-- src/theory/eager_proof_generator.cpp | 2 +- src/theory/eager_proof_generator.h | 2 +- src/theory/engine_output_channel.cpp | 4 ++-- src/theory/engine_output_channel.h | 4 ++-- src/theory/evaluator.cpp | 2 +- src/theory/evaluator.h | 4 ++-- src/theory/example/ecdata.cpp | 2 +- src/theory/example/ecdata.h | 4 ++-- src/theory/example/theory_uf_tim.cpp | 4 ++-- src/theory/example/theory_uf_tim.h | 4 ++-- src/theory/ext_theory.cpp | 2 +- src/theory/ext_theory.h | 4 ++-- src/theory/fp/fp_converter.cpp | 4 ++-- src/theory/fp/fp_converter.h | 4 ++-- src/theory/fp/theory_fp.cpp | 4 ++-- src/theory/fp/theory_fp.h | 4 ++-- src/theory/fp/theory_fp_rewriter.cpp | 4 ++-- src/theory/fp/theory_fp_rewriter.h | 4 ++-- src/theory/fp/theory_fp_type_rules.h | 4 ++-- src/theory/fp/type_enumerator.h | 2 +- src/theory/interrupted.h | 4 ++-- src/theory/logic_info.cpp | 2 +- src/theory/logic_info.h | 2 +- src/theory/output_channel.h | 2 +- src/theory/quantifiers/alpha_equivalence.cpp | 4 ++-- src/theory/quantifiers/alpha_equivalence.h | 4 ++-- src/theory/quantifiers/anti_skolem.cpp | 4 ++-- src/theory/quantifiers/anti_skolem.h | 4 ++-- src/theory/quantifiers/bv_inverter.cpp | 2 +- src/theory/quantifiers/bv_inverter.h | 2 +- src/theory/quantifiers/bv_inverter_utils.cpp | 2 +- src/theory/quantifiers/bv_inverter_utils.h | 4 ++-- src/theory/quantifiers/candidate_rewrite_database.cpp | 2 +- src/theory/quantifiers/candidate_rewrite_database.h | 4 ++-- src/theory/quantifiers/candidate_rewrite_filter.cpp | 4 ++-- src/theory/quantifiers/candidate_rewrite_filter.h | 4 ++-- src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp | 2 +- src/theory/quantifiers/cegqi/ceg_arith_instantiator.h | 4 ++-- src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp | 4 ++-- src/theory/quantifiers/cegqi/ceg_bv_instantiator.h | 4 ++-- .../quantifiers/cegqi/ceg_bv_instantiator_utils.cpp | 4 ++-- .../quantifiers/cegqi/ceg_bv_instantiator_utils.h | 2 +- src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp | 4 ++-- src/theory/quantifiers/cegqi/ceg_dt_instantiator.h | 2 +- src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp | 2 +- src/theory/quantifiers/cegqi/ceg_epr_instantiator.h | 2 +- src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 4 ++-- src/theory/quantifiers/cegqi/ceg_instantiator.h | 2 +- src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 4 ++-- src/theory/quantifiers/cegqi/inst_strategy_cegqi.h | 2 +- src/theory/quantifiers/cegqi/vts_term_cache.cpp | 4 ++-- src/theory/quantifiers/cegqi/vts_term_cache.h | 2 +- src/theory/quantifiers/conjecture_generator.cpp | 4 ++-- src/theory/quantifiers/conjecture_generator.h | 2 +- src/theory/quantifiers/dynamic_rewrite.cpp | 2 +- src/theory/quantifiers/dynamic_rewrite.h | 4 ++-- .../quantifiers/ematching/candidate_generator.cpp | 2 +- src/theory/quantifiers/ematching/candidate_generator.h | 2 +- src/theory/quantifiers/ematching/ho_trigger.cpp | 4 ++-- src/theory/quantifiers/ematching/ho_trigger.h | 4 ++-- .../quantifiers/ematching/inst_match_generator.cpp | 4 ++-- src/theory/quantifiers/ematching/inst_match_generator.h | 2 +- .../quantifiers/ematching/inst_strategy_e_matching.cpp | 4 ++-- .../quantifiers/ematching/inst_strategy_e_matching.h | 2 +- .../quantifiers/ematching/instantiation_engine.cpp | 2 +- src/theory/quantifiers/ematching/instantiation_engine.h | 2 +- src/theory/quantifiers/ematching/trigger.cpp | 4 ++-- src/theory/quantifiers/ematching/trigger.h | 4 ++-- src/theory/quantifiers/equality_infer.cpp | 2 +- src/theory/quantifiers/equality_infer.h | 4 ++-- src/theory/quantifiers/equality_query.cpp | 4 ++-- src/theory/quantifiers/equality_query.h | 2 +- src/theory/quantifiers/expr_miner.cpp | 2 +- src/theory/quantifiers/expr_miner.h | 4 ++-- src/theory/quantifiers/expr_miner_manager.cpp | 2 +- src/theory/quantifiers/expr_miner_manager.h | 4 ++-- src/theory/quantifiers/extended_rewrite.cpp | 4 ++-- src/theory/quantifiers/extended_rewrite.h | 4 ++-- src/theory/quantifiers/first_order_model.cpp | 2 +- src/theory/quantifiers/first_order_model.h | 2 +- src/theory/quantifiers/fmf/bounded_integers.cpp | 4 ++-- src/theory/quantifiers/fmf/bounded_integers.h | 4 ++-- src/theory/quantifiers/fmf/full_model_check.cpp | 4 ++-- src/theory/quantifiers/fmf/full_model_check.h | 4 ++-- src/theory/quantifiers/fmf/model_builder.cpp | 2 +- src/theory/quantifiers/fmf/model_builder.h | 4 ++-- src/theory/quantifiers/fmf/model_engine.cpp | 2 +- src/theory/quantifiers/fmf/model_engine.h | 4 ++-- src/theory/quantifiers/fun_def_evaluator.cpp | 4 ++-- src/theory/quantifiers/fun_def_evaluator.h | 2 +- src/theory/quantifiers/fun_def_process.cpp | 4 ++-- src/theory/quantifiers/fun_def_process.h | 4 ++-- src/theory/quantifiers/inst_match.cpp | 2 +- src/theory/quantifiers/inst_match.h | 4 ++-- src/theory/quantifiers/inst_match_trie.cpp | 2 +- src/theory/quantifiers/inst_match_trie.h | 4 ++-- src/theory/quantifiers/inst_strategy_enumerative.cpp | 2 +- src/theory/quantifiers/inst_strategy_enumerative.h | 4 ++-- src/theory/quantifiers/instantiate.cpp | 4 ++-- src/theory/quantifiers/instantiate.h | 2 +- src/theory/quantifiers/lazy_trie.cpp | 2 +- src/theory/quantifiers/lazy_trie.h | 4 ++-- src/theory/quantifiers/proof_checker.cpp | 2 +- src/theory/quantifiers/proof_checker.h | 2 +- src/theory/quantifiers/quant_conflict_find.cpp | 2 +- src/theory/quantifiers/quant_conflict_find.h | 2 +- src/theory/quantifiers/quant_epr.cpp | 2 +- src/theory/quantifiers/quant_epr.h | 4 ++-- src/theory/quantifiers/quant_relevance.cpp | 2 +- src/theory/quantifiers/quant_relevance.h | 2 +- src/theory/quantifiers/quant_rep_bound_ext.cpp | 4 ++-- src/theory/quantifiers/quant_rep_bound_ext.h | 4 ++-- src/theory/quantifiers/quant_split.cpp | 4 ++-- src/theory/quantifiers/quant_split.h | 2 +- src/theory/quantifiers/quant_util.cpp | 2 +- src/theory/quantifiers/quant_util.h | 4 ++-- src/theory/quantifiers/quantifiers_attributes.cpp | 2 +- src/theory/quantifiers/quantifiers_attributes.h | 4 ++-- src/theory/quantifiers/quantifiers_rewriter.cpp | 4 ++-- src/theory/quantifiers/quantifiers_rewriter.h | 4 ++-- src/theory/quantifiers/query_generator.cpp | 4 ++-- src/theory/quantifiers/query_generator.h | 4 ++-- src/theory/quantifiers/relevant_domain.cpp | 4 ++-- src/theory/quantifiers/relevant_domain.h | 2 +- src/theory/quantifiers/single_inv_partition.cpp | 4 ++-- src/theory/quantifiers/single_inv_partition.h | 4 ++-- src/theory/quantifiers/skolemize.cpp | 2 +- src/theory/quantifiers/skolemize.h | 4 ++-- src/theory/quantifiers/solution_filter.cpp | 4 ++-- src/theory/quantifiers/solution_filter.h | 4 ++-- src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 4 ++-- src/theory/quantifiers/sygus/ce_guided_single_inv.h | 2 +- .../quantifiers/sygus/ce_guided_single_inv_sol.cpp | 4 ++-- src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h | 4 ++-- src/theory/quantifiers/sygus/cegis.cpp | 4 ++-- src/theory/quantifiers/sygus/cegis.h | 4 ++-- src/theory/quantifiers/sygus/cegis_core_connective.cpp | 4 ++-- src/theory/quantifiers/sygus/cegis_core_connective.h | 2 +- src/theory/quantifiers/sygus/cegis_unif.cpp | 4 ++-- src/theory/quantifiers/sygus/cegis_unif.h | 2 +- .../quantifiers/sygus/enum_stream_substitution.cpp | 2 +- src/theory/quantifiers/sygus/enum_stream_substitution.h | 4 ++-- src/theory/quantifiers/sygus/example_eval_cache.cpp | 2 +- src/theory/quantifiers/sygus/example_eval_cache.h | 2 +- src/theory/quantifiers/sygus/example_infer.cpp | 2 +- src/theory/quantifiers/sygus/example_infer.h | 4 ++-- src/theory/quantifiers/sygus/example_min_eval.cpp | 2 +- src/theory/quantifiers/sygus/example_min_eval.h | 2 +- src/theory/quantifiers/sygus/sygus_abduct.cpp | 2 +- src/theory/quantifiers/sygus/sygus_abduct.h | 2 +- src/theory/quantifiers/sygus/sygus_enumerator.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_enumerator.h | 4 ++-- src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_enumerator_basic.h | 2 +- src/theory/quantifiers/sygus/sygus_eval_unfold.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_eval_unfold.h | 4 ++-- src/theory/quantifiers/sygus/sygus_explain.cpp | 2 +- src/theory/quantifiers/sygus/sygus_explain.h | 4 ++-- src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_grammar_cons.h | 4 ++-- src/theory/quantifiers/sygus/sygus_grammar_norm.cpp | 2 +- src/theory/quantifiers/sygus/sygus_grammar_norm.h | 2 +- src/theory/quantifiers/sygus/sygus_grammar_red.cpp | 2 +- src/theory/quantifiers/sygus/sygus_grammar_red.h | 4 ++-- src/theory/quantifiers/sygus/sygus_invariance.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_invariance.h | 2 +- src/theory/quantifiers/sygus/sygus_module.cpp | 2 +- src/theory/quantifiers/sygus/sygus_module.h | 4 ++-- src/theory/quantifiers/sygus/sygus_pbe.cpp | 2 +- src/theory/quantifiers/sygus/sygus_pbe.h | 4 ++-- src/theory/quantifiers/sygus/sygus_process_conj.cpp | 2 +- src/theory/quantifiers/sygus/sygus_process_conj.h | 4 ++-- src/theory/quantifiers/sygus/sygus_repair_const.cpp | 2 +- src/theory/quantifiers/sygus/sygus_repair_const.h | 4 ++-- src/theory/quantifiers/sygus/sygus_stats.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_stats.h | 2 +- src/theory/quantifiers/sygus/sygus_unif.cpp | 2 +- src/theory/quantifiers/sygus/sygus_unif.h | 4 ++-- src/theory/quantifiers/sygus/sygus_unif_io.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_unif_io.h | 4 ++-- src/theory/quantifiers/sygus/sygus_unif_rl.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_unif_rl.h | 4 ++-- src/theory/quantifiers/sygus/sygus_unif_strat.cpp | 4 ++-- src/theory/quantifiers/sygus/sygus_unif_strat.h | 4 ++-- src/theory/quantifiers/sygus/synth_conjecture.cpp | 4 ++-- src/theory/quantifiers/sygus/synth_conjecture.h | 4 ++-- src/theory/quantifiers/sygus/synth_engine.cpp | 4 ++-- src/theory/quantifiers/sygus/synth_engine.h | 2 +- src/theory/quantifiers/sygus/term_database_sygus.cpp | 4 ++-- src/theory/quantifiers/sygus/term_database_sygus.h | 2 +- src/theory/quantifiers/sygus/transition_inference.cpp | 4 ++-- src/theory/quantifiers/sygus/transition_inference.h | 2 +- src/theory/quantifiers/sygus/type_info.cpp | 4 ++-- src/theory/quantifiers/sygus/type_info.h | 2 +- src/theory/quantifiers/sygus/type_node_id_trie.cpp | 2 +- src/theory/quantifiers/sygus/type_node_id_trie.h | 2 +- src/theory/quantifiers/sygus_inst.cpp | 2 +- src/theory/quantifiers/sygus_sampler.cpp | 4 ++-- src/theory/quantifiers/sygus_sampler.h | 4 ++-- src/theory/quantifiers/term_database.cpp | 4 ++-- src/theory/quantifiers/term_database.h | 4 ++-- src/theory/quantifiers/term_enumeration.cpp | 2 +- src/theory/quantifiers/term_enumeration.h | 4 ++-- src/theory/quantifiers/term_util.cpp | 4 ++-- src/theory/quantifiers/term_util.h | 2 +- src/theory/quantifiers/theory_quantifiers.cpp | 2 +- src/theory/quantifiers/theory_quantifiers.h | 4 ++-- src/theory/quantifiers/theory_quantifiers_type_rules.h | 2 +- src/theory/quantifiers_engine.cpp | 4 ++-- src/theory/quantifiers_engine.h | 2 +- src/theory/rep_set.cpp | 2 +- src/theory/rep_set.h | 4 ++-- src/theory/rewriter.cpp | 4 ++-- src/theory/rewriter.h | 4 ++-- src/theory/rewriter_attributes.h | 2 +- src/theory/rewriter_tables_template.h | 4 ++-- src/theory/sep/theory_sep.cpp | 2 +- src/theory/sep/theory_sep.h | 2 +- src/theory/sep/theory_sep_rewriter.cpp | 2 +- src/theory/sep/theory_sep_rewriter.h | 4 ++-- src/theory/sep/theory_sep_type_rules.h | 4 ++-- src/theory/sets/cardinality_extension.cpp | 4 ++-- src/theory/sets/cardinality_extension.h | 4 ++-- src/theory/sets/inference_manager.cpp | 4 ++-- src/theory/sets/inference_manager.h | 2 +- src/theory/sets/normal_form.h | 2 +- src/theory/sets/rels_utils.h | 2 +- src/theory/sets/skolem_cache.cpp | 2 +- src/theory/sets/skolem_cache.h | 2 +- src/theory/sets/solver_state.cpp | 4 ++-- src/theory/sets/solver_state.h | 4 ++-- src/theory/sets/theory_sets.cpp | 4 ++-- src/theory/sets/theory_sets.h | 2 +- src/theory/sets/theory_sets_private.cpp | 4 ++-- src/theory/sets/theory_sets_private.h | 4 ++-- src/theory/sets/theory_sets_rels.cpp | 4 ++-- src/theory/sets/theory_sets_rels.h | 2 +- src/theory/sets/theory_sets_rewriter.cpp | 2 +- src/theory/sets/theory_sets_rewriter.h | 4 ++-- src/theory/sets/theory_sets_type_enumerator.cpp | 2 +- src/theory/sets/theory_sets_type_enumerator.h | 2 +- src/theory/sets/theory_sets_type_rules.h | 2 +- src/theory/shared_terms_database.cpp | 2 +- src/theory/shared_terms_database.h | 2 +- src/theory/smt_engine_subsolver.cpp | 4 ++-- src/theory/smt_engine_subsolver.h | 4 ++-- src/theory/sort_inference.cpp | 4 ++-- src/theory/sort_inference.h | 4 ++-- src/theory/strings/arith_entail.cpp | 2 +- src/theory/strings/arith_entail.h | 2 +- src/theory/strings/base_solver.cpp | 4 ++-- src/theory/strings/base_solver.h | 4 ++-- src/theory/strings/core_solver.cpp | 6 +++--- src/theory/strings/core_solver.h | 6 +++--- src/theory/strings/eqc_info.cpp | 4 ++-- src/theory/strings/eqc_info.h | 2 +- src/theory/strings/extf_solver.cpp | 6 +++--- src/theory/strings/extf_solver.h | 6 +++--- src/theory/strings/infer_info.cpp | 4 ++-- src/theory/strings/infer_info.h | 4 ++-- src/theory/strings/inference_manager.cpp | 4 ++-- src/theory/strings/inference_manager.h | 4 ++-- src/theory/strings/normal_form.cpp | 4 ++-- src/theory/strings/normal_form.h | 4 ++-- src/theory/strings/regexp_elim.cpp | 4 ++-- src/theory/strings/regexp_elim.h | 4 ++-- src/theory/strings/regexp_entail.cpp | 4 ++-- src/theory/strings/regexp_entail.h | 4 ++-- src/theory/strings/regexp_operation.cpp | 4 ++-- src/theory/strings/regexp_operation.h | 4 ++-- src/theory/strings/regexp_solver.cpp | 4 ++-- src/theory/strings/regexp_solver.h | 2 +- src/theory/strings/rewrites.cpp | 4 ++-- src/theory/strings/rewrites.h | 4 ++-- src/theory/strings/sequences_rewriter.cpp | 2 +- src/theory/strings/sequences_rewriter.h | 4 ++-- src/theory/strings/sequences_stats.cpp | 2 +- src/theory/strings/sequences_stats.h | 2 +- src/theory/strings/skolem_cache.cpp | 2 +- src/theory/strings/skolem_cache.h | 4 ++-- src/theory/strings/solver_state.cpp | 4 ++-- src/theory/strings/solver_state.h | 4 ++-- src/theory/strings/strings_entail.cpp | 2 +- src/theory/strings/strings_entail.h | 2 +- src/theory/strings/strings_fmf.cpp | 4 ++-- src/theory/strings/strings_fmf.h | 4 ++-- src/theory/strings/strings_rewriter.cpp | 4 ++-- src/theory/strings/strings_rewriter.h | 4 ++-- src/theory/strings/term_registry.cpp | 4 ++-- src/theory/strings/term_registry.h | 6 +++--- src/theory/strings/theory_strings.cpp | 4 ++-- src/theory/strings/theory_strings.h | 2 +- src/theory/strings/theory_strings_preprocess.cpp | 4 ++-- src/theory/strings/theory_strings_preprocess.h | 4 ++-- src/theory/strings/theory_strings_type_rules.h | 4 ++-- src/theory/strings/theory_strings_utils.cpp | 4 ++-- src/theory/strings/theory_strings_utils.h | 4 ++-- src/theory/strings/type_enumerator.cpp | 4 ++-- src/theory/strings/type_enumerator.h | 4 ++-- src/theory/strings/word.cpp | 2 +- src/theory/strings/word.h | 4 ++-- src/theory/subs_minimize.cpp | 4 ++-- src/theory/subs_minimize.h | 4 ++-- src/theory/substitutions.cpp | 2 +- src/theory/substitutions.h | 2 +- src/theory/term_registration_visitor.cpp | 2 +- src/theory/term_registration_visitor.h | 2 +- src/theory/theory.cpp | 4 ++-- src/theory/theory.h | 4 ++-- src/theory/theory_engine.cpp | 4 ++-- src/theory/theory_engine.h | 4 ++-- src/theory/theory_id.cpp | 17 +++++++++++++++++ src/theory/theory_id.h | 17 +++++++++++++++++ src/theory/theory_model.cpp | 2 +- src/theory/theory_model.h | 2 +- src/theory/theory_model_builder.cpp | 2 +- src/theory/theory_model_builder.h | 4 ++-- src/theory/theory_preprocessor.cpp | 4 ++-- src/theory/theory_preprocessor.h | 4 ++-- src/theory/theory_proof_step_buffer.cpp | 2 +- src/theory/theory_proof_step_buffer.h | 2 +- src/theory/theory_registrar.h | 4 ++-- src/theory/theory_rewriter.h | 4 ++-- src/theory/theory_test_utils.h | 4 ++-- src/theory/theory_traits_template.h | 4 ++-- src/theory/trust_node.cpp | 2 +- src/theory/trust_node.h | 2 +- src/theory/type_enumerator.h | 2 +- src/theory/type_enumerator_template.cpp | 4 ++-- src/theory/type_set.cpp | 2 +- src/theory/type_set.h | 4 ++-- src/theory/uf/cardinality_extension.cpp | 2 +- src/theory/uf/cardinality_extension.h | 2 +- src/theory/uf/equality_engine.cpp | 4 ++-- src/theory/uf/equality_engine.h | 4 ++-- src/theory/uf/equality_engine_types.h | 4 ++-- src/theory/uf/ho_extension.cpp | 4 ++-- src/theory/uf/ho_extension.h | 2 +- src/theory/uf/proof_checker.cpp | 4 ++-- src/theory/uf/proof_checker.h | 4 ++-- src/theory/uf/symmetry_breaker.cpp | 4 ++-- src/theory/uf/symmetry_breaker.h | 2 +- src/theory/uf/theory_uf.cpp | 2 +- src/theory/uf/theory_uf.h | 4 ++-- src/theory/uf/theory_uf_model.cpp | 4 ++-- src/theory/uf/theory_uf_model.h | 4 ++-- src/theory/uf/theory_uf_rewriter.h | 2 +- src/theory/uf/theory_uf_type_rules.h | 2 +- src/theory/valuation.cpp | 2 +- src/theory/valuation.h | 2 +- src/util/abstract_value.cpp | 2 +- src/util/abstract_value.h | 2 +- src/util/bin_heap.h | 4 ++-- src/util/bitvector.cpp | 2 +- src/util/bitvector.h | 4 ++-- src/util/bool.h | 4 ++-- src/util/cardinality.cpp | 4 ++-- src/util/cardinality.h | 4 ++-- src/util/dense_map.h | 2 +- src/util/divisible.cpp | 2 +- src/util/divisible.h | 4 ++-- src/util/floatingpoint.cpp | 4 ++-- src/util/floatingpoint.h.in | 4 ++-- src/util/gmp_util.h | 4 ++-- src/util/hash.h | 4 ++-- src/util/index.cpp | 2 +- src/util/index.h | 4 ++-- src/util/integer.h.in | 2 +- src/util/integer_cln_imp.cpp | 2 +- src/util/integer_cln_imp.h | 2 +- src/util/integer_gmp_imp.cpp | 2 +- src/util/integer_gmp_imp.h | 2 +- src/util/maybe.h | 4 ++-- src/util/ostream_util.cpp | 2 +- src/util/ostream_util.h | 4 ++-- src/util/proof.h | 4 ++-- src/util/random.cpp | 2 +- src/util/random.h | 4 ++-- src/util/rational.h.in | 2 +- src/util/rational_cln_imp.cpp | 2 +- src/util/rational_cln_imp.h | 2 +- src/util/rational_gmp_imp.cpp | 2 +- src/util/rational_gmp_imp.h | 2 +- src/util/regexp.cpp | 2 +- src/util/regexp.h | 2 +- src/util/resource_manager.cpp | 4 ++-- src/util/resource_manager.h | 4 ++-- src/util/result.cpp | 4 ++-- src/util/result.h | 4 ++-- src/util/safe_print.cpp | 4 ++-- src/util/safe_print.h | 4 ++-- src/util/sampler.cpp | 2 +- src/util/sampler.h | 4 ++-- src/util/sexpr.cpp | 2 +- src/util/sexpr.h | 2 +- src/util/smt2_quote_string.cpp | 4 ++-- src/util/smt2_quote_string.h | 4 ++-- src/util/statistics.cpp | 2 +- src/util/statistics.h | 4 ++-- src/util/statistics_registry.cpp | 4 ++-- src/util/statistics_registry.h | 2 +- src/util/string.cpp | 4 ++-- src/util/string.h | 2 +- src/util/tuple.h | 4 ++-- src/util/unsafe_interrupt_exception.h | 4 ++-- src/util/utility.cpp | 2 +- src/util/utility.h | 2 +- test/java/BitVectors.java | 4 ++-- test/java/BitVectorsAndArrays.java | 4 ++-- test/java/Combination.java | 4 ++-- test/java/HelloWorld.java | 4 ++-- test/java/LinearArith.java | 4 ++-- test/system/CVC4JavaTest.java | 2 +- test/system/boilerplate.cpp | 4 ++-- test/system/ouroborous.cpp | 2 +- test/system/reset_assertions.cpp | 2 +- test/system/sep_log_api.cpp | 2 +- test/system/smt2_compliance.cpp | 2 +- test/system/statistics.cpp | 4 ++-- test/system/two_smt_engines.cpp | 4 ++-- test/unit/api/datatype_api_black.h | 4 ++-- test/unit/api/grammar_black.h | 4 ++-- test/unit/api/op_black.h | 4 ++-- test/unit/api/solver_black.h | 4 ++-- test/unit/api/sort_black.h | 4 ++-- test/unit/api/term_black.h | 4 ++-- test/unit/base/map_util_black.h | 2 +- test/unit/context/cdlist_black.h | 2 +- test/unit/context/cdmap_black.h | 4 ++-- test/unit/context/cdmap_white.h | 4 ++-- test/unit/context/cdo_black.h | 2 +- test/unit/context/context_black.h | 2 +- test/unit/context/context_mm_black.h | 4 ++-- test/unit/context/context_white.h | 2 +- test/unit/expr/attribute_black.h | 2 +- test/unit/expr/attribute_white.h | 2 +- test/unit/expr/expr_manager_public.h | 2 +- test/unit/expr/expr_public.h | 2 +- test/unit/expr/kind_black.h | 2 +- test/unit/expr/kind_map_black.h | 2 +- test/unit/expr/node_algorithm_black.h | 2 +- test/unit/expr/node_black.h | 2 +- test/unit/expr/node_builder_black.h | 4 ++-- test/unit/expr/node_manager_black.h | 2 +- test/unit/expr/node_manager_white.h | 2 +- test/unit/expr/node_self_iterator_black.h | 2 +- test/unit/expr/node_traversal_black.h | 2 +- test/unit/expr/node_white.h | 2 +- test/unit/expr/symbol_table_black.h | 2 +- test/unit/expr/type_cardinality_public.h | 2 +- test/unit/expr/type_node_white.h | 2 +- test/unit/main/interactive_shell_black.h | 4 ++-- test/unit/memory.h | 2 +- test/unit/parser/parser_black.h | 2 +- test/unit/parser/parser_builder_black.h | 2 +- test/unit/preprocessing/pass_bv_gauss_white.h | 4 ++-- test/unit/proof/drat_proof_black.h | 2 +- test/unit/proof/er_proof_black.h | 2 +- test/unit/proof/lfsc_proof_printer_black.h | 2 +- test/unit/proof/lrat_proof_black.h | 4 ++-- test/unit/proof/utils.h | 2 +- test/unit/prop/cnf_stream_white.h | 2 +- test/unit/test_utils.h | 2 +- test/unit/theory/evaluator_white.h | 2 +- test/unit/theory/logic_info_white.h | 2 +- test/unit/theory/regexp_operation_black.h | 4 ++-- test/unit/theory/sequences_rewriter_white.h | 4 ++-- test/unit/theory/theory_arith_white.h | 4 ++-- test/unit/theory/theory_black.h | 2 +- test/unit/theory/theory_bv_rewriter_white.h | 2 +- test/unit/theory/theory_bv_white.h | 2 +- test/unit/theory/theory_engine_white.h | 2 +- .../theory/theory_quantifiers_bv_instantiator_white.h | 2 +- test/unit/theory/theory_quantifiers_bv_inverter_white.h | 4 ++-- test/unit/theory/theory_sets_type_enumerator_white.h | 4 ++-- test/unit/theory/theory_strings_skolem_cache_black.h | 2 +- test/unit/theory/theory_strings_word_white.h | 2 +- test/unit/theory/theory_white.h | 2 +- test/unit/theory/type_enumerator_white.h | 4 ++-- test/unit/util/array_store_all_black.h | 4 ++-- test/unit/util/assert_white.h | 4 ++-- test/unit/util/binary_heap_black.h | 4 ++-- test/unit/util/bitvector_black.h | 2 +- test/unit/util/boolean_simplification_black.h | 2 +- test/unit/util/cardinality_public.h | 2 +- test/unit/util/check_white.h | 4 ++-- test/unit/util/configuration_black.h | 2 +- test/unit/util/datatype_black.h | 2 +- test/unit/util/exception_black.h | 2 +- test/unit/util/integer_black.h | 2 +- test/unit/util/integer_white.h | 2 +- test/unit/util/listener_black.h | 2 +- test/unit/util/output_black.h | 2 +- test/unit/util/rational_black.h | 2 +- test/unit/util/rational_white.h | 2 +- test/unit/util/stats_black.h | 2 +- 1142 files changed, 1790 insertions(+), 1754 deletions(-) (limited to 'src/theory/strings/skolem_cache.cpp') diff --git a/contrib/get-authors b/contrib/get-authors index 0fb3f6ae1..80c4f57a5 100755 --- a/contrib/get-authors +++ b/contrib/get-authors @@ -1,7 +1,7 @@ #!/bin/sh # # get-authors -# Copyright (c) 2009-2019 The CVC4 Project +# Copyright (c) 2009-2020 The CVC4 Project # # usage: get-authors [ files... ] # @@ -65,6 +65,8 @@ while [ $# -gt 0 ]; do sed 's/justinxu421/Justin Xu/' | \ sed 's/yoni206/Yoni Zohar/' | \ sed 's/ayveejay/Andrew V. Jones/' | \ + sed 's/FabianWolff/Fabian Wolff/' | \ + sed 's/mudathirmahgoub/Mudathir Mohamed/' | \ # Determine top three contributors sort | uniq -c | sort -rn | head -n3 | \ diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index 148392aab..bbe0ebb12 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -1,7 +1,7 @@ #!/usr/bin/perl -w # # update-copyright.pl -# Copyright (c) 2009-2019 The CVC4 Project +# Copyright (c) 2009-2020 The CVC4 Project # # usage: update-copyright [-m] [files/directories...] # update-copyright [-h | --help] @@ -47,7 +47,7 @@ $excluded_paths .= ')$'; # Years of copyright for the template. E.g., the string # "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever. -my $years = '2009-2019'; +my $years = '2009-2020'; my $standard_template = <