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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 23 Mar 2022 23:53:14 +0000 (18:53 -0500)
committer	GitHub <noreply@github.com>
	Wed, 23 Mar 2022 23:53:14 +0000 (23:53 +0000)
commit	4a84ee32687d84ff18835c23196086f1ef1ba3aa
tree	2798b8956f504ad9b76268f16c85e281c76779f0	tree
parent	81eb37c14982676242779547349984931e99f110	commit \| diff

Clean options (#8309)

Deletes many unnecessary options, cleans some documentation, consolidates several options.

79 files changed:

contrib/competitions/smt-comp/run-script-smtcomp-current		diff \| blob \| history
src/options/arith_options.toml		diff \| blob \| history
src/options/main_options.toml		diff \| blob \| history
src/options/printer_options.toml		diff \| blob \| history
src/options/quantifiers_options.toml		diff \| blob \| history
src/options/sets_options.toml		diff \| blob \| history
src/options/smt_options.toml		diff \| blob \| history
src/options/strings_options.toml		diff \| blob \| history
src/preprocessing/passes/ite_simp.cpp		diff \| blob \| history
src/preprocessing/passes/ite_simp.h		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.cpp		diff \| blob \| history
src/theory/quantifiers/equality_query.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_modules.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_preprocess.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_state.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_statistics.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_statistics.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
test/regress/cli/regress0/arith/issue7984-quant-trans.smt2		diff \| blob \| history
test/regress/cli/regress0/decision/issue8296-sk-def-before-assert.smt2		diff \| blob \| history
test/regress/cli/regress0/nl/nta/issue8294-2-double-solve.smt2		diff \| blob \| history
test/regress/cli/regress0/quantifiers/issue5693-prenex.smt2		diff \| blob \| history
test/regress/cli/regress0/strings/issue6604-re-elim.smt2		diff \| blob \| history
test/regress/cli/regress0/strings/issue8295-star-union-char.smt2		diff \| blob \| history
test/regress/cli/regress0/strings/regexp_inclusion.smt2		diff \| blob \| history
test/regress/cli/regress0/strings/regexp_inclusion_reduction.smt2		diff \| blob \| history
test/regress/cli/regress1/fmf/fib-core.smt2		diff \| blob \| history
test/regress/cli/regress1/fmf/jasmin-cdt-crash.smt2		diff \| blob \| history
test/regress/cli/regress1/fmf/loopy_coda.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue4021-ind-opts.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/proj-issue155.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/qcft-smtlib3dbc51.smt2		diff \| blob \| history
test/regress/cli/regress1/rr-verify/bool-crci.sy		diff \| blob \| history
test/regress/cli/regress1/rr-verify/bv-term-32.sy		diff \| blob \| history
test/regress/cli/regress1/rr-verify/bv-term.sy		diff \| blob \| history
test/regress/cli/regress1/rr-verify/fp-arith.sy		diff \| blob \| history
test/regress/cli/regress1/rr-verify/fp-bool.sy		diff \| blob \| history
test/regress/cli/regress1/rr-verify/string-term.sy		diff \| blob \| history
test/regress/cli/regress1/seq/issue8148-const-mv.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/issue2982.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/issue6604-2.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/issue6635-rre.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/issue6653-4-rre.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/issue6653-rre-small.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/issue6653-rre.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/issue6766-re-elim-bv.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/issue6973-dup-lemma-conc.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/non_termination_regular_expression4.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/nt6-dd.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/policy_variable.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/proj254-re-elim-agg.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/query4674.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/query8485.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/re-agg-total1.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/re-agg-total2.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/re-all-char-hard.smt2		diff \| blob \| history
test/regress/cli/regress1/strings/re-elim-exact.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue3947-agg-miniscope.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/issue4083-var-shadow.smt2		diff \| blob \| history
test/regress/cli/regress1/sygus/proj-issue165.smt2		diff \| blob \| history
test/regress/cli/regress2/strings/issue918.smt2		diff \| blob \| history
test/regress/cli/regress2/strings/non_termination_regular_expression6.smt2		diff \| blob \| history
test/regress/cli/regress2/strings/small-1.smt2		diff \| blob \| history
test/regress/cli/regress3/regex-rrv.sy		diff \| blob \| history
test/regress/cli/regress4/unsat-circ-reduce.smt2		diff \| blob \| history
test/regress/cli/run_regression.py		diff \| blob \| history

RSS Atom