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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Mon, 17 Jan 2022 19:05:55 +0000 (13:05 -0600)
committer	GitHub <noreply@github.com>
	Mon, 17 Jan 2022 19:05:55 +0000 (16:05 -0300)
commit	6a3ead1cca025ad4d07976b10fc3c3eda2bf8220
tree	e312262024789bcbc65870bd8fc18dd61fa3d2f0	tree
parent	12f3384db0d6afade79252c28532ee6830fe767f	commit \| diff

Refactor options related to rewriting and symmetry breaking in sygus (#7949)

Note this also corrects a few inconsistencies in how the rewriter is invoked in fast / variable agnostic enumeration.

Notably, fast enumeration now leverages the term datatype sygus for rewriting, meaning it can evaluate recursive functions for enumerated terms.

17 files changed:

src/options/datatypes_options.toml		diff \| blob \| history
src/options/quantifiers_options.toml		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/enum_stream_substitution.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/enum_value_manager.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator_callback.h		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
test/regress/regress1/rr-verify/bool-crci.sy		diff \| blob \| history
test/regress/regress1/rr-verify/bv-term-32.sy		diff \| blob \| history
test/regress/regress1/rr-verify/bv-term.sy		diff \| blob \| history
test/regress/regress1/rr-verify/fp-arith.sy		diff \| blob \| history
test/regress/regress1/rr-verify/fp-bool.sy		diff \| blob \| history
test/regress/regress1/rr-verify/string-term.sy		diff \| blob \| history
test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2		diff \| blob \| history

RSS Atom