diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-01 08:40:06 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-01 08:40:06 -0500 |
| commit | 9c2a0ef0f00696eb4bbffcbbf23a43508c1c3987 (patch) | |
| tree | 404921e1b0f0d4972f5baf1ebdd46eab0ea2557f /src/preprocessing/assertion_pipeline.h | |
| parent | e145e9f16ca87eaa3955fb4308f8a6fad6bb158d (diff) | |
Make SygusSolver use sygus attributes directly (#5172)
Previously, the SmtEngine was using an interface through TheoryEngine to set user attributes to indicate that e.g. a synth-fun is associated with a given grammar. Since SmtEngine and its members are internal now, this can simply be done directly via attributes. This makes it so that SygusSolver does not depend on TheoryEngine nor does it require the TheoryEngine to be initialized at the time a synth-fun is created.
Diffstat (limited to 'src/preprocessing/assertion_pipeline.h')
0 files changed, 0 insertions, 0 deletions