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

author	Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
	Wed, 16 Sep 2020 17:45:01 +0000 (12:45 -0500)
committer	GitHub <noreply@github.com>
	Wed, 16 Sep 2020 17:45:01 +0000 (12:45 -0500)
commit	2c2f05c96e021006275a2bc70b9ede70b280616d
tree	db702d7b8fbd14dd8003b1f03c02b77c89d2fced	tree
parent	0534ea1bbee9a3a7049580449ab25025a4f92a9a	commit \| diff

Dump commands in internal code using command printing functions. (#5040)

This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.

53 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/main/command_executor.h		diff \| blob \| history
src/main/main.cpp		diff \| blob \| history
src/parser/antlr_input.cpp		diff \| blob \| history
src/parser/cvc/cvc.cpp		diff \| blob \| history
src/parser/cvc/cvc.h		diff \| blob \| history
src/parser/input.cpp		diff \| blob \| history
src/parser/smt2/smt2.h		diff \| blob \| history
src/parser/tptp/tptp.cpp		diff \| blob \| history
src/parser/tptp/tptp.h		diff \| blob \| history
src/preprocessing/preprocessing_pass.cpp		diff \| blob \| history
src/printer/ast/ast_printer.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/proof/unsat_core.cpp		diff \| blob \| history
src/prop/cnf_stream.cpp		diff \| blob \| history
src/prop/cnf_stream.h		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/prop/theory_proxy.h		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/dump.cpp		diff \| blob \| history
src/smt/dump.h		diff \| blob \| history
src/smt/dump_manager.cpp		diff \| blob \| history
src/smt/dump_manager.h		diff \| blob \| history
src/smt/listeners.cpp		diff \| blob \| history
src/smt/listeners.h		diff \| blob \| history
src/smt/output_manager.cpp	[new file with mode: 0644]	blob
src/smt/output_manager.h	[new file with mode: 0644]	blob
src/smt/preprocessor.cpp		diff \| blob \| history
src/smt/process_assertions.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/smt/smt_solver.cpp		diff \| blob \| history
src/smt/sygus_solver.cpp		diff \| blob \| history
src/smt/sygus_solver.h		diff \| blob \| history
src/smt/term_formula_removal.h		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
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/skolemize.h		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
test/unit/parser/parser_builder_black.h		diff \| blob \| history
test/unit/prop/cnf_stream_white.h		diff \| blob \| history

RSS Atom