Remove `ConstantMap<Rational>` (#7635)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 12 Nov 2021 14:14:49 +0000 (06:14 -0800)
committerGitHub <noreply@github.com>
Fri, 12 Nov 2021 14:14:49 +0000 (08:14 -0600)
commitad340126a7adbb9840cca1d082c57b43995987a4
treeda06599c2691f063b770b2b1ba7e2ccf87f26cc6
parent5cfbb67e228daf76835b7fd0a95d214859be030e
Remove `ConstantMap<Rational>` (#7635)

This is in preparation of having two different kinds (CONST_RATIONAL
and CONST_INT) share the same payload. To do so, we cannot rely on
ConstantMap<Rational> anymore to map the payload type to a kind. This
commit extends support in the mkmetakind script to deal with such
payloads by adding a + suffix to the type. The commit also does some
minor refactoring of NodeManager::mkConst() and
NodeManager::mkConstInternal() to support setting the kind explicitly.
Finally, the commit addresses all instances where mkConst<Rational>()
is used, including the API.
144 files changed:
src/api/cpp/cvc5.cpp
src/api/cpp/cvc5.h
src/expr/bound_var_manager.cpp
src/expr/dtype.cpp
src/expr/mkmetakind
src/expr/nary_term_util.cpp
src/expr/node_manager.h
src/expr/term_context_node.cpp
src/parser/antlr_input.cpp
src/parser/input.cpp
src/parser/parser.cpp
src/preprocessing/passes/bv_to_int.cpp
src/preprocessing/passes/miplib_trick.cpp
src/preprocessing/passes/real_to_int.cpp
src/preprocessing/passes/unconstrained_simplifier.cpp
src/proof/alethe/alethe_post_processor.cpp
src/proof/lfsc/lfsc_node_converter.cpp
src/proof/lfsc/lfsc_util.cpp
src/proof/method_id.cpp
src/proof/proof_checker.cpp
src/prop/proof_cnf_stream.cpp
src/smt/difficulty_post_processor.cpp
src/smt/proof_post_processor.cpp
src/smt_util/nary_builder.cpp
src/theory/arith/arith_msum.cpp
src/theory/arith/arith_rewriter.cpp
src/theory/arith/arith_utilities.cpp
src/theory/arith/arith_utilities.h
src/theory/arith/bound_inference.cpp
src/theory/arith/congruence_manager.cpp
src/theory/arith/constraint.cpp
src/theory/arith/infer_bounds.cpp
src/theory/arith/kinds
src/theory/arith/nl/cad/cdcac.cpp
src/theory/arith/nl/cad/proof_generator.cpp
src/theory/arith/nl/ext/ext_state.cpp
src/theory/arith/nl/ext/factoring_check.cpp
src/theory/arith/nl/ext/monomial.cpp
src/theory/arith/nl/ext/monomial_bounds_check.cpp
src/theory/arith/nl/ext/proof_checker.cpp
src/theory/arith/nl/ext/tangent_plane_check.cpp
src/theory/arith/nl/ext_theory_callback.cpp
src/theory/arith/nl/iand_solver.cpp
src/theory/arith/nl/iand_utils.cpp
src/theory/arith/nl/nl_model.cpp
src/theory/arith/nl/nonlinear_extension.cpp
src/theory/arith/nl/poly_conversion.cpp
src/theory/arith/nl/pow2_solver.cpp
src/theory/arith/nl/transcendental/exponential_solver.cpp
src/theory/arith/nl/transcendental/proof_checker.cpp
src/theory/arith/nl/transcendental/sine_solver.cpp
src/theory/arith/nl/transcendental/taylor_generator.cpp
src/theory/arith/nl/transcendental/transcendental_state.cpp
src/theory/arith/operator_elim.cpp
src/theory/arith/proof_checker.cpp
src/theory/arith/theory_arith_private.cpp
src/theory/arith/type_enumerator.h
src/theory/bags/bag_solver.cpp
src/theory/bags/bags_rewriter.cpp
src/theory/bags/inference_generator.cpp
src/theory/bags/normal_form.cpp
src/theory/bags/theory_bags.cpp
src/theory/bags/theory_bags_type_enumerator.cpp
src/theory/booleans/proof_circuit_propagator.cpp
src/theory/builtin/proof_checker.cpp
src/theory/bv/int_blaster.cpp
src/theory/bv/theory_bv_utils.cpp
src/theory/datatypes/datatypes_rewriter.cpp
src/theory/datatypes/infer_proof_cons.cpp
src/theory/datatypes/sygus_extension.cpp
src/theory/datatypes/sygus_simple_sym.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/difficulty_manager.cpp
src/theory/evaluator.cpp
src/theory/fp/theory_fp.cpp
src/theory/fp/theory_fp_rewriter.cpp
src/theory/inference_id.cpp
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
src/theory/quantifiers/cegqi/ceg_instantiator.cpp
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
src/theory/quantifiers/cegqi/vts_term_cache.cpp
src/theory/quantifiers/ematching/inst_match_generator.cpp
src/theory/quantifiers/ematching/pattern_term_selector.cpp
src/theory/quantifiers/ematching/relational_match_generator.cpp
src/theory/quantifiers/extended_rewrite.cpp
src/theory/quantifiers/fmf/bounded_integers.cpp
src/theory/quantifiers/quant_bound_inference.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/skolemize.cpp
src/theory/quantifiers/sygus/cegis_unif.cpp
src/theory/quantifiers/sygus/sygus_enumerator.cpp
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
src/theory/quantifiers/sygus_sampler.cpp
src/theory/quantifiers/term_util.cpp
src/theory/sets/cardinality_extension.cpp
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_rewriter.cpp
src/theory/strings/arith_entail.cpp
src/theory/strings/array_solver.cpp
src/theory/strings/base_solver.cpp
src/theory/strings/core_solver.cpp
src/theory/strings/infer_proof_cons.cpp
src/theory/strings/inference_manager.cpp
src/theory/strings/proof_checker.cpp
src/theory/strings/regexp_elim.cpp
src/theory/strings/regexp_entail.cpp
src/theory/strings/regexp_operation.cpp
src/theory/strings/sequences_rewriter.cpp
src/theory/strings/skolem_cache.cpp
src/theory/strings/solver_state.cpp
src/theory/strings/strings_entail.cpp
src/theory/strings/strings_fmf.cpp
src/theory/strings/strings_rewriter.cpp
src/theory/strings/term_registry.cpp
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings_preprocess.cpp
src/theory/strings/theory_strings_utils.cpp
test/unit/node/node_algorithm_black.cpp
test/unit/node/node_black.cpp
test/unit/node/node_builder_black.cpp
test/unit/node/node_manager_black.cpp
test/unit/node/node_manager_white.cpp
test/unit/node/node_white.cpp
test/unit/node/type_node_white.cpp
test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
test/unit/theory/arith_poly_white.cpp
test/unit/theory/evaluator_white.cpp
test/unit/theory/sequences_rewriter_white.cpp
test/unit/theory/theory_arith_cad_white.cpp
test/unit/theory/theory_arith_pow2_white.cpp
test/unit/theory/theory_arith_white.cpp
test/unit/theory/theory_bags_normal_form_white.cpp
test/unit/theory/theory_bags_rewriter_white.cpp
test/unit/theory/theory_bags_type_rules_white.cpp
test/unit/theory/theory_black.cpp
test/unit/theory/theory_bv_int_blaster_white.cpp
test/unit/theory/theory_engine_white.cpp
test/unit/theory/theory_int_opt_white.cpp
test/unit/theory/theory_sets_type_rules_white.cpp
test/unit/theory/theory_strings_skolem_cache_black.cpp
test/unit/theory/type_enumerator_white.cpp
test/unit/util/array_store_all_white.cpp
test/unit/util/datatype_black.cpp