Refactor DeclareSygusVarCommand and SynthFunCommand to use the API. (#5334)
authorAbdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Tue, 27 Oct 2020 18:19:11 +0000 (13:19 -0500)
committerGitHub <noreply@github.com>
Tue, 27 Oct 2020 18:19:11 +0000 (13:19 -0500)
commit70d6e3c33571807b7bb94bf4f462de4fdf7a369c
tree7bf85c35072f7a746de947d31d5f4a79acd6f279
parent88025001599c7e5ced8d55c3769e728758434f69
Refactor DeclareSygusVarCommand and SynthFunCommand to use the API. (#5334)

This PR is part of migrating commands. DeclareSygusVarCommand and SynthFunCommand now call public API function instead of their corresponding SmtEngine functions. Those two commands don't fully initialize the solver anymore. Some operations in SygusInterpol::solveInterpolation, which creates an interpolation sub-solver, depend on the solver being fully initialized and were affected by this change. Those operations are now executed by the main solver instead of the sub-solver, which is not fully initialized by the time they are needed.
src/api/cvc4cpp.cpp
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
src/smt/command.cpp
src/smt/smt_engine.cpp
src/theory/quantifiers/sygus/sygus_interpol.cpp
test/unit/api/solver_black.h