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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 2 Feb 2021 18:25:21 +0000 (12:25 -0600)
committer	GitHub <noreply@github.com>
	Tue, 2 Feb 2021 18:25:21 +0000 (12:25 -0600)
commit	e05ad4759f2ae01cc06a9ca715c777d188f0f5fd
tree	a292cc67c0b41c3bdf325f5160bdede10346add0	tree
parent	4c1f67446ad59f1c5efe7230b96b0d3ccac0e692	commit \| diff

Cleanup some includes (#5847)

In particular, theory_engine.h is included many places spuriously.

A few blocks of code changed indentation, updated to guidelines.

35 files changed:

src/preprocessing/passes/ackermann.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_int.cpp		diff \| blob \| history
src/preprocessing/passes/extended_rewriter_pass.cpp		diff \| blob \| history
src/preprocessing/passes/int_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/ite_removal.cpp		diff \| blob \| history
src/preprocessing/passes/ite_simp.cpp		diff \| blob \| history
src/preprocessing/passes/miplib_trick.cpp		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.cpp		diff \| blob \| history
src/preprocessing/passes/quantifier_macros.cpp		diff \| blob \| history
src/preprocessing/passes/theory_preprocess.cpp		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/smt/smt_solver.cpp		diff \| blob \| history
src/theory/combination_care_graph.cpp		diff \| blob \| history
src/theory/model_manager.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_engine.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_inst.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/uf/cardinality_extension.cpp		diff \| blob \| history
src/theory/uf/theory_uf_model.cpp		diff \| blob \| history
src/theory/uf/theory_uf_model.h		diff \| blob \| history
src/theory/valuation.cpp		diff \| blob \| history

RSS Atom