projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 90fe2a0) | patch
Fix bugs related to printing Sygus commands (#3804)
authorAbdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Mon, 24 Feb 2020 20:30:02 +0000 (14:30 -0600)
committerGitHub <noreply@github.com>
Mon, 24 Feb 2020 20:30:02 +0000 (14:30 -0600)
commitc4f2ca4c1931f91a9647f0daa032ee9417f1b382
treea2396581d7de09b033fd44c8f7ad3310280bd5f6tree
parent90fe2a057cdcdaea34f0a03f837159d9adb45914commit | diff
Fix bugs related to printing Sygus commands (#3804)

With this commit, most Sygus problems should print correctly. The current printing functionality was tested on 158 Sygus regress files (0, 1, and 2) and 153 of them were printed in Sygus2 format and contained "(check-synth)". The printing functionality was tested again on the generated files and gave almost the same results.
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history