projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b1ef625) | patch
Expand definitions in sygus operators at the SMT level (#7077)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 27 Aug 2021 18:03:41 +0000 (13:03 -0500)
committerGitHub <noreply@github.com>
Fri, 27 Aug 2021 18:03:41 +0000 (18:03 +0000)
commita698b522d619c800a3401c7294cf1c6c663d7acc
treeff63fd9c775e39279d12858217ca1efea1a762cftree
parentb1ef6257c9f4c30fd71f42942107b029c569c316commit | diff
Expand definitions in sygus operators at the SMT level (#7077)

Eliminates another call to currentSmtEngine.

This PR ensures we remember the mapping between operators that are embedded in sygus datatypes during preprocessing, instead of computing this within the sygus datatypes utilities when solving.
src/smt/smt_engine.cpp diff | blob | history
src/smt/sygus_solver.cpp diff | blob | history
src/smt/sygus_solver.h diff | blob | history
src/theory/datatypes/sygus_datatype_utils.cpp diff | blob | history
src/theory/datatypes/sygus_datatype_utils.h diff | blob | history
src/theory/quantifiers/sygus/type_info.cpp diff | blob | history