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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Fri, 1 Oct 2021 01:57:24 +0000 (18:57 -0700)
committer	GitHub <noreply@github.com>
	Fri, 1 Oct 2021 01:57:24 +0000 (18:57 -0700)
commit	19f223e580b527bc17add2ea4e61e85df2977c87
tree	087d8bb7a18300d54d4f11525b8566f5c60ce6a7	tree
parent	56cd2e8f584ed36fd76144a622355511a4b09935	commit \| diff

Rename SmtEngine to SolverEngine. (#7282)

108 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/decision/decision_engine.h		diff \| blob \| history
src/decision/decision_engine_old.h		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/main/interactive_shell.cpp		diff \| blob \| history
src/omt/bitvector_optimizer.cpp		diff \| blob \| history
src/omt/bitvector_optimizer.h		diff \| blob \| history
src/omt/integer_optimizer.cpp		diff \| blob \| history
src/omt/integer_optimizer.h		diff \| blob \| history
src/omt/omt_optimizer.h		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/preprocessing/passes/apply_substs.cpp		diff \| blob \| history
src/preprocessing/passes/sygus_inference.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass_context.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass_context.h		diff \| blob \| history
src/printer/smt2/smt2_printer.h		diff \| blob \| history
src/printer/tptp/tptp_printer.h		diff \| blob \| history
src/prop/cnf_stream.h		diff \| blob \| history
src/prop/minisat/CVC4-README		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/smt/abduction_solver.cpp		diff \| blob \| history
src/smt/abduction_solver.h		diff \| blob \| history
src/smt/assertions.cpp		diff \| blob \| history
src/smt/check_models.cpp		diff \| blob \| history
src/smt/dump_manager.h		diff \| blob \| history
src/smt/env.h		diff \| blob \| history
src/smt/interpolation_solver.cpp		diff \| blob \| history
src/smt/interpolation_solver.h		diff \| blob \| history
src/smt/listeners.cpp		diff \| blob \| history
src/smt/listeners.h		diff \| blob \| history
src/smt/optimization_solver.cpp		diff \| blob \| history
src/smt/optimization_solver.h		diff \| blob \| history
src/smt/output_manager.cpp		diff \| blob \| history
src/smt/output_manager.h		diff \| blob \| history
src/smt/preprocessor.cpp		diff \| blob \| history
src/smt/preprocessor.h		diff \| blob \| history
src/smt/process_assertions.cpp		diff \| blob \| history
src/smt/process_assertions.h		diff \| blob \| history
src/smt/proof_manager.cpp		diff \| blob \| history
src/smt/proof_manager.h		diff \| blob \| history
src/smt/proof_post_processor.h		diff \| blob \| history
src/smt/quant_elim_solver.cpp		diff \| blob \| history
src/smt/quant_elim_solver.h		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/smt/set_defaults.h		diff \| blob \| history
src/smt/smt_engine_scope.cpp		diff \| blob \| history
src/smt/smt_engine_scope.h		diff \| blob \| history
src/smt/smt_engine_state.cpp		diff \| blob \| history
src/smt/smt_engine_state.h		diff \| blob \| history
src/smt/smt_engine_stats.h		diff \| blob \| history
src/smt/smt_mode.cpp		diff \| blob \| history
src/smt/smt_mode.h		diff \| blob \| history
src/smt/smt_solver.cpp		diff \| blob \| history
src/smt/smt_solver.h		diff \| blob \| history
src/smt/smt_statistics_registry.cpp		diff \| blob \| history
src/smt/smt_statistics_registry.h		diff \| blob \| history
src/smt/solver_engine.cpp		diff \| blob \| history
src/smt/solver_engine.h		diff \| blob \| history
src/smt/sygus_solver.cpp		diff \| blob \| history
src/smt/unsat_core_manager.cpp		diff \| blob \| history
src/smt/unsat_core_manager.h		diff \| blob \| history
src/theory/builtin/theory_builtin_type_rules.h		diff \| blob \| history
src/theory/bv/int_blaster.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules.h		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.h		diff \| blob \| history
src/theory/logic_info.h		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.h		diff \| blob \| history
src/theory/quantifiers/cegqi/nested_qe.cpp		diff \| blob \| history
src/theory/quantifiers/expr_miner.cpp		diff \| blob \| history
src/theory/quantifiers/expr_miner.h		diff \| blob \| history
src/theory/quantifiers/query_generator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_qe_preproc.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.h		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/rewriter.h		diff \| blob \| history
src/theory/smt_engine_subsolver.cpp		diff \| blob \| history
src/theory/smt_engine_subsolver.h		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/util/resource_manager.h		diff \| blob \| history
test/api/reset_assertions.cpp		diff \| blob \| history
test/unit/node/node_black.cpp		diff \| blob \| history
test/unit/node/type_node_white.cpp		diff \| blob \| history
test/unit/preprocessing/pass_bv_gauss_white.cpp		diff \| blob \| history
test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp		diff \| blob \| history
test/unit/prop/cnf_stream_white.cpp		diff \| blob \| history
test/unit/test_smt.h		diff \| blob \| history
test/unit/theory/evaluator_white.cpp		diff \| blob \| history
test/unit/theory/sequences_rewriter_white.cpp		diff \| blob \| history
test/unit/theory/theory_arith_pow2_white.cpp		diff \| blob \| history
test/unit/theory/theory_arith_white.cpp		diff \| blob \| history
test/unit/theory/theory_bv_int_blaster_white.cpp		diff \| blob \| history
test/unit/theory/theory_bv_opt_white.cpp		diff \| blob \| history
test/unit/theory/theory_bv_white.cpp		diff \| blob \| history
test/unit/theory/theory_engine_white.cpp		diff \| blob \| history
test/unit/theory/theory_int_opt_white.cpp		diff \| blob \| history
test/unit/theory/theory_opt_multigoal_white.cpp		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_inverter_white.cpp		diff \| blob \| history
test/unit/theory/theory_white.cpp		diff \| blob \| history

RSS Atom