projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ddf2ec6) | patch
Fix rewrite rule synthesis for 0-ary operators (#8221)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 4 Mar 2022 19:40:30 +0000 (13:40 -0600)
committerGitHub <noreply@github.com>
Fri, 4 Mar 2022 19:40:30 +0000 (19:40 +0000)
commit3bc29d4e86534f779f6d94d3cf947a2dded4566f
tree7b84d9d8b26d9479721e354fdf751f66f0748d2ftree
parentddf2ec6fbf35c8174c6d63a6de3a4993872019c9commit | diff
Fix rewrite rule synthesis for 0-ary operators (#8221)

Fixes cvc5/cvc5-projects#422.

Also changes the default setting for rewrite rule synthesis to check correct of rewrite rules by default.
src/options/quantifiers_options.toml diff | blob | history
src/preprocessing/passes/synth_rew_rules.cpp diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/quantifiers/sygus/type_info.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/rr-verify/bv-term-32.sy diff | blob | history
test/regress/regress1/sygus/issue8216-rr-input-re.smt2 [new file with mode: 0644] blob
test/unit/api/cpp/solver_black.cpp diff | blob | history