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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Thu, 30 Sep 2021 21:14:59 +0000 (14:14 -0700)
committer	GitHub <noreply@github.com>
	Thu, 30 Sep 2021 21:14:59 +0000 (21:14 +0000)
commit	56cd2e8f584ed36fd76144a622355511a4b09935
tree	94a2331dd82886133c2183445a80010fcb02538e	tree
parent	b106c95296860cf89ea7cef00c8e8187409e755e	commit \| diff

Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279)

This is in preparation for renaming SmtEngine to SolverEngine.

48 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/api/cpp/cvc5.cpp		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/main/driver_unified.cpp		diff \| blob \| history
src/omt/bitvector_optimizer.cpp		diff \| blob \| history
src/omt/integer_optimizer.cpp		diff \| blob \| history
src/preprocessing/passes/sygus_inference.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass_context.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/printer/tptp/tptp_printer.cpp		diff \| blob \| history
src/smt/abduction_solver.cpp		diff \| blob \| history
src/smt/assertions.cpp		diff \| blob \| history
src/smt/expand_definitions.cpp		diff \| blob \| history
src/smt/interpolation_solver.cpp		diff \| blob \| history
src/smt/listeners.cpp		diff \| blob \| history
src/smt/optimization_solver.cpp		diff \| blob \| history
src/smt/output_manager.cpp		diff \| blob \| history
src/smt/preprocessor.cpp		diff \| blob \| history
src/smt/process_assertions.cpp		diff \| blob \| history
src/smt/proof_post_processor.cpp		diff \| blob \| history
src/smt/smt_engine.cpp	[deleted file]	blob \| history
src/smt/smt_engine.h	[deleted file]	blob \| history
src/smt/smt_engine_scope.cpp		diff \| blob \| history
src/smt/smt_engine_state.cpp		diff \| blob \| history
src/smt/smt_solver.cpp		diff \| blob \| history
src/smt/solver_engine.cpp	[new file with mode: 0644]	blob
src/smt/solver_engine.h	[new file with mode: 0644]	blob
src/theory/bv/abstraction.cpp		diff \| blob \| history
src/theory/bv/bitblast/eager_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/lazy_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules.h		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/candidate_generator.cpp		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/smt_engine_subsolver.cpp		diff \| blob \| history
src/theory/smt_engine_subsolver.h		diff \| blob \| history
src/theory/theory_model.cpp		diff \| blob \| history
test/api/smt2_compliance.cpp		diff \| blob \| history
test/unit/node/attribute_white.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/printer/smt2_printer_black.cpp		diff \| blob \| history
test/unit/test_env.h		diff \| blob \| history
test/unit/test_node.h		diff \| blob \| history
test/unit/test_smt.h		diff \| blob \| history

RSS Atom