projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: daee9d4) | patch
Make datatype selector expansion to its own accessible method (#7069)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 26 Aug 2021 16:20:43 +0000 (11:20 -0500)
committerGitHub <noreply@github.com>
Thu, 26 Aug 2021 16:20:43 +0000 (16:20 +0000)
commit44989759e897b74256f406606dd2a61a8eced365
treea05c8325a29a2d3250b7fcac12b089cb8da2713ctree
parentdaee9d4ec0c9e7c5054345c4156c4debe815e045commit | diff
Make datatype selector expansion to its own accessible method (#7069)

This eliminates another call to currentSmtEngine.

After this, there are only two remaining calls (one for normalizing sygus grammars wrt user define-funs, and the other for Rewriter::rewrite).
src/theory/datatypes/datatypes_rewriter.cpp diff | blob | history
src/theory/datatypes/datatypes_rewriter.h diff | blob | history
src/theory/quantifiers/ematching/candidate_generator.cpp diff | blob | history