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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Tue, 17 Dec 2019 21:43:44 +0000 (13:43 -0800)
committer	GitHub <noreply@github.com>
	Tue, 17 Dec 2019 21:43:44 +0000 (13:43 -0800)
commit	e9499c41f405df8b42fd9ae10004b1b91a869106
tree	fa1475f43a3e61b8f6ffdcb903b65919eba28661	tree
parent	9b2914ed9f7b14ecf535ffe9e1328d0fa042e072	commit \| diff

Generate code for options with modes. (#3561)

This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.

125 files changed:

.travis.yml		diff \| blob \| history
INSTALL.md		diff \| blob \| history
src/CMakeLists.txt		diff \| blob \| history
src/bindings/java/CMakeLists.txt		diff \| blob \| history
src/decision/decision_engine.cpp		diff \| blob \| history
src/decision/justification_heuristic.cpp		diff \| blob \| history
src/expr/type_properties_template.h		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/options/CMakeLists.txt		diff \| blob \| history
src/options/arith_heuristic_pivot_rule.cpp	[deleted file]	blob \| history
src/options/arith_heuristic_pivot_rule.h	[deleted file]	blob \| history
src/options/arith_options.toml		diff \| blob \| history
src/options/arith_propagation_mode.cpp	[deleted file]	blob \| history
src/options/arith_propagation_mode.h	[deleted file]	blob \| history
src/options/arith_unate_lemma_mode.cpp	[deleted file]	blob \| history
src/options/arith_unate_lemma_mode.h	[deleted file]	blob \| history
src/options/bool_to_bv_mode.cpp	[deleted file]	blob \| history
src/options/bool_to_bv_mode.h	[deleted file]	blob \| history
src/options/bv_bitblast_mode.cpp	[deleted file]	blob \| history
src/options/bv_bitblast_mode.h	[deleted file]	blob \| history
src/options/bv_options.toml		diff \| blob \| history
src/options/datatypes_modes.h	[deleted file]	blob \| history
src/options/datatypes_options.toml		diff \| blob \| history
src/options/decision_mode.cpp	[deleted file]	blob \| history
src/options/decision_mode.h	[deleted file]	blob \| history
src/options/decision_options.toml		diff \| blob \| history
src/options/mkoptions.py		diff \| blob \| history
src/options/module_template.cpp		diff \| blob \| history
src/options/module_template.h		diff \| blob \| history
src/options/options.h		diff \| blob \| history
src/options/options.i		diff \| blob \| history
src/options/options_handler.cpp		diff \| blob \| history
src/options/options_handler.h		diff \| blob \| history
src/options/options_public_functions.cpp		diff \| blob \| history
src/options/printer_modes.cpp		diff \| blob \| history
src/options/printer_modes.h		diff \| blob \| history
src/options/printer_options.toml		diff \| blob \| history
src/options/quantifiers_modes.cpp	[deleted file]	blob \| history
src/options/quantifiers_modes.h	[deleted file]	blob \| history
src/options/quantifiers_options.toml		diff \| blob \| history
src/options/smt_modes.cpp	[deleted file]	blob \| history
src/options/smt_modes.h	[deleted file]	blob \| history
src/options/smt_options.toml		diff \| blob \| history
src/options/strings_modes.cpp	[deleted file]	blob \| history
src/options/strings_modes.h	[deleted file]	blob \| history
src/options/strings_options.toml		diff \| blob \| history
src/options/sygus_out_mode.h	[deleted file]	blob \| history
src/options/theory_options.toml		diff \| blob \| history
src/options/theoryof_mode.cpp	[deleted file]	blob \| history
src/options/theoryof_mode.h	[deleted file]	blob \| history
src/options/uf_options.toml		diff \| blob \| history
src/options/ufss_mode.h	[deleted file]	blob \| history
src/preprocessing/passes/bool_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/bv_abstraction.cpp		diff \| blob \| history
src/preprocessing/passes/quantifier_macros.cpp		diff \| blob \| history
src/proof/bitvector_proof.cpp		diff \| blob \| history
src/proof/clausal_bitvector_proof.cpp		diff \| blob \| history
src/proof/proof_manager.cpp		diff \| blob \| history
src/proof/resolution_bitvector_proof.cpp		diff \| blob \| history
src/proof/theory_proof.cpp		diff \| blob \| history
src/prop/bvminisat/simp/SimpSolver.cc		diff \| blob \| history
src/prop/minisat/minisat.cpp		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/model_blocker.cpp		diff \| blob \| history
src/smt/model_blocker.h		diff \| blob \| history
src/smt/model_core_builder.cpp		diff \| blob \| history
src/smt/model_core_builder.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.cpp		diff \| blob \| history
src/theory/arith/dual_simplex.cpp		diff \| blob \| history
src/theory/arith/error_set.cpp		diff \| blob \| history
src/theory/arith/error_set.h		diff \| blob \| history
src/theory/arith/fc_simplex.cpp		diff \| blob \| history
src/theory/arith/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/simplex.h		diff \| blob \| history
src/theory/arith/soi_simplex.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.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/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.cpp		diff \| blob \| history
src/theory/bv/slicer.cpp		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv_utils.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching.h		diff \| blob \| history
src/theory/quantifiers/ematching/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.h		diff \| blob \| history
src/theory/quantifiers/equality_query.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_builder.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/quant_split.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		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.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_rl.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/sort_inference.cpp		diff \| blob \| history
src/theory/strings/regexp_solver.cpp		diff \| blob \| history
src/theory/strings/solver_state.cpp		diff \| blob \| history
src/theory/strings/solver_state.h		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/theory.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
src/theory/type_enumerator_template.cpp		diff \| blob \| history
src/theory/uf/cardinality_extension.cpp		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/valuation.cpp		diff \| blob \| history
src/theory/valuation.h		diff \| blob \| history

RSS Atom