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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Mon, 13 Dec 2021 19:48:49 +0000 (13:48 -0600)
committer	GitHub <noreply@github.com>
	Mon, 13 Dec 2021 19:48:49 +0000 (19:48 +0000)
commit	1e6c7645d3d98ba734ab73ed76c7785b572b86c8
tree	aa006c9a8a6264085493b0082a873046cb14536f	tree
parent	8c9fff99a2be7369e33520a120e25e6d8c3ec07c	commit \| diff

Initial cut at distinguishing uses of CONST_RATIONAL (#7682)

83 files changed:

src/expr/bound_var_manager.cpp		diff \| blob \| history
src/expr/dtype.cpp		diff \| blob \| history
src/expr/nary_term_util.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/expr/node_manager_template.cpp		diff \| blob \| history
src/expr/term_context_node.cpp		diff \| blob \| history
src/expr/term_context_node.h		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/pseudo_boolean_processor.cpp		diff \| blob \| history
src/preprocessing/passes/real_to_int.cpp		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.cpp		diff \| blob \| history
src/proof/lfsc/lfsc_node_converter.cpp		diff \| blob \| history
src/proof/lfsc/lfsc_util.cpp		diff \| blob \| history
src/proof/method_id.cpp		diff \| blob \| history
src/proof/proof_checker.cpp		diff \| blob \| history
src/prop/proof_cnf_stream.cpp		diff \| blob \| history
src/smt/difficulty_post_processor.cpp		diff \| blob \| history
src/smt/proof_post_processor.cpp		diff \| blob \| history
src/theory/arith/nl/iand_solver.cpp		diff \| blob \| history
src/theory/arith/nl/iand_utils.cpp		diff \| blob \| history
src/theory/bags/bag_solver.cpp		diff \| blob \| history
src/theory/bags/bags_rewriter.cpp		diff \| blob \| history
src/theory/bags/inference_generator.cpp		diff \| blob \| history
src/theory/bags/normal_form.cpp		diff \| blob \| history
src/theory/bags/theory_bags.cpp		diff \| blob \| history
src/theory/bags/theory_bags_type_enumerator.cpp		diff \| blob \| history
src/theory/booleans/proof_circuit_propagator.cpp		diff \| blob \| history
src/theory/builtin/proof_checker.cpp		diff \| blob \| history
src/theory/bv/int_blaster.cpp		diff \| blob \| history
src/theory/bv/theory_bv_utils.cpp		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.cpp		diff \| blob \| history
src/theory/datatypes/infer_proof_cons.cpp		diff \| blob \| history
src/theory/datatypes/kinds		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/datatypes/sygus_simple_sym.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes_type_rules.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes_type_rules.h		diff \| blob \| history
src/theory/difficulty_manager.cpp		diff \| blob \| history
src/theory/inference_id.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_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/cegqi/vts_term_cache.h		diff \| blob \| history
src/theory/quantifiers/ematching/pattern_term_selector.cpp		diff \| blob \| history
src/theory/quantifiers/extended_rewrite.cpp		diff \| blob \| history
src/theory/quantifiers/extended_rewrite.h		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/quant_bound_inference.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/sets/cardinality_extension.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rewriter.cpp		diff \| blob \| history
src/theory/strings/arith_entail.cpp		diff \| blob \| history
src/theory/strings/array_solver.cpp		diff \| blob \| history
src/theory/strings/base_solver.cpp		diff \| blob \| history
src/theory/strings/core_solver.cpp		diff \| blob \| history
src/theory/strings/eager_solver.cpp		diff \| blob \| history
src/theory/strings/infer_proof_cons.cpp		diff \| blob \| history
src/theory/strings/inference_manager.cpp		diff \| blob \| history
src/theory/strings/proof_checker.cpp		diff \| blob \| history
src/theory/strings/regexp_elim.cpp		diff \| blob \| history
src/theory/strings/regexp_entail.cpp		diff \| blob \| history
src/theory/strings/regexp_operation.cpp		diff \| blob \| history
src/theory/strings/sequences_rewriter.cpp		diff \| blob \| history
src/theory/strings/skolem_cache.cpp		diff \| blob \| history
src/theory/strings/solver_state.cpp		diff \| blob \| history
src/theory/strings/strings_entail.cpp		diff \| blob \| history
src/theory/strings/strings_fmf.cpp		diff \| blob \| history
src/theory/strings/strings_rewriter.cpp		diff \| blob \| history
src/theory/strings/term_registry.cpp		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.cpp		diff \| blob \| history
src/theory/strings/theory_strings_utils.cpp		diff \| blob \| history

RSS Atom