Make SygusSolver use sygus attributes directly (#5172)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 1 Oct 2020 13:40:06 +0000 (08:40 -0500)
committerGitHub <noreply@github.com>
Thu, 1 Oct 2020 13:40:06 +0000 (08:40 -0500)
commit9c2a0ef0f00696eb4bbffcbbf23a43508c1c3987
tree404921e1b0f0d4972f5baf1ebdd46eab0ea2557f
parente145e9f16ca87eaa3955fb4308f8a6fad6bb158d
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.
src/smt/sygus_solver.cpp
src/theory/quantifiers/quantifiers_attributes.cpp
src/theory/quantifiers/theory_quantifiers.cpp