git.libre-soc.org Git - cvc5.git/commit

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 7 Apr 2021 18:36:15 +0000 (13:36 -0500)
committer	GitHub <noreply@github.com>
	Wed, 7 Apr 2021 18:36:15 +0000 (18:36 +0000)
commit	04a494e251a8cc2c90bb429e2858f1c4eb8f88ff
tree	03b1a5792f2f6ca5537353b86682f427090668da	tree
parent	5059658ee0d6fc65e4cb1652c605895d016cd274	commit \| diff

Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)

This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.

This PR also eliminates some unused code in TheoryArithPrivate.

Followup PRs will start formalizing/eliminating calls to mkDummySkolem.

92 files changed:

src/expr/dtype.cpp		diff \| blob \| history
src/expr/dtype_cons.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/expr/skolem_manager.cpp		diff \| blob \| history
src/expr/skolem_manager.h		diff \| blob \| history
src/expr/subs.cpp		diff \| blob \| history
src/expr/sygus_datatype.cpp		diff \| blob \| history
src/preprocessing/passes/ackermann.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_int.cpp		diff \| blob \| history
src/preprocessing/passes/fun_def_fmf.cpp		diff \| blob \| history
src/preprocessing/passes/ho_elim.cpp		diff \| blob \| history
src/preprocessing/passes/int_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/miplib_trick.cpp		diff \| blob \| history
src/preprocessing/passes/nl_ext_purify.cpp		diff \| blob \| history
src/preprocessing/passes/quantifier_macros.cpp		diff \| blob \| history
src/preprocessing/passes/real_to_int.cpp		diff \| blob \| history
src/preprocessing/passes/sep_skolem_emp.cpp		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.cpp		diff \| blob \| history
src/preprocessing/util/ite_utilities.cpp		diff \| blob \| history
src/smt/quant_elim_solver.cpp		diff \| blob \| history
src/smt/sygus_solver.cpp		diff \| blob \| history
src/theory/arith/arith_ite_utils.cpp		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/callbacks.cpp		diff \| blob \| history
src/theory/arith/dio_solver.cpp		diff \| blob \| history
src/theory/arith/nl/cad_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/sine_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_solver.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.h		diff \| blob \| history
src/theory/builtin/theory_builtin_type_rules.cpp		diff \| blob \| history
src/theory/bv/abstraction.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_core.cpp		diff \| blob \| history
src/theory/bv/theory_bv_utils.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/engine_output_channel.cpp		diff \| blob \| history
src/theory/fp/theory_fp.cpp		diff \| blob \| history
src/theory/quantifiers/bv_inverter.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/vts_term_cache.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/dynamic_rewrite.cpp		diff \| blob \| history
src/theory/quantifiers/expr_miner.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/first_order_model_fmc.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/single_inv_partition.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/rcons_type_info.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_abduct.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_qe_preproc.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_reconstruct.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_rl.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_strat.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_utils.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/template_infer.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/transition_inference.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_inst.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sets/cardinality_extension.cpp		diff \| blob \| history
src/theory/sets/skolem_cache.cpp		diff \| blob \| history
src/theory/sets/term_registry.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rels.cpp		diff \| blob \| history
src/theory/sort_inference.cpp		diff \| blob \| history
src/theory/strings/regexp_operation.cpp		diff \| blob \| history
src/theory/strings/skolem_cache.cpp		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.cpp		diff \| blob \| history
src/theory/uf/cardinality_extension.cpp		diff \| blob \| history
src/theory/uf/ho_extension.cpp		diff \| blob \| history
test/unit/node/attribute_black.cpp		diff \| blob \| history
test/unit/node/node_algorithm_black.cpp		diff \| blob \| history
test/unit/node/node_black.cpp		diff \| blob \| history
test/unit/node/node_builder_black.cpp		diff \| blob \| history
test/unit/node/node_manager_black.cpp		diff \| blob \| history
test/unit/node/node_manager_white.cpp		diff \| blob \| history
test/unit/node/node_self_iterator_black.cpp		diff \| blob \| history
test/unit/test_node.h		diff \| blob \| history
test/unit/test_smt.h		diff \| blob \| history
test/unit/theory/theory_bags_rewriter_white.cpp		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_inverter_white.cpp		diff \| blob \| history
test/unit/theory/theory_strings_skolem_cache_black.cpp		diff \| blob \| history
test/unit/util/boolean_simplification_black.cpp		diff \| blob \| history

RSS Atom