projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: be6f9c2) | patch
Add -o sygus-grammar to print auto-generated SyGuS grammars (#7573)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 4 Nov 2021 23:50:55 +0000 (18:50 -0500)
committerGitHub <noreply@github.com>
Thu, 4 Nov 2021 23:50:55 +0000 (18:50 -0500)
commitf9d59828ebd150797682f1fbf5267aca7d15bb54
tree846371c0f52cb9749aaff333ab31ed7cb2fd81fdtree
parentbe6f9c2ee9201cc5181ce7ba27b6fe992ab3fff6commit | diff
Add -o sygus-grammar to print auto-generated SyGuS grammars (#7573)

Fixes #5341.
src/options/base_options.toml diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.h diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_cons.h diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/sygus/print-grammar.sy [new file with mode: 0644] blob