projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 30e5875) | patch
Optimize the rewriter for DT_SYGUS_EVAL (#3529)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 6 Dec 2019 19:12:12 +0000 (13:12 -0600)
committerAndres Noetzli <andres.noetzli@gmail.com>
Fri, 6 Dec 2019 19:12:12 +0000 (11:12 -0800)
commitec865a83596fd1285e033426b80ddfc1c35085cd
tree07a73efec0083b288bd94c39b301019400b92f3etree
parent30e5875e066e917b69d01189233aec26ce226cd6commit | diff
Optimize the rewriter for DT_SYGUS_EVAL (#3529)

This makes it so that we don't construct intermediate unfoldings of applications of DT_SYGUS_EVAL, which wastes time in node construction. It makes the sygusToBuiltin utility in TermDbSygus use this implementation.
src/theory/datatypes/datatypes_rewriter.cpp diff | blob | history
src/theory/datatypes/theory_datatypes_utils.cpp diff | blob | history
src/theory/datatypes/theory_datatypes_utils.h diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.cpp diff | blob | history