diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-08-18 17:52:25 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-18 17:52:25 -0500 |
| commit | bcbef9dfa053a14ac48f176fe4bde9a1aa2b4931 (patch) | |
| tree | e01bff53c1dfc1b91d605714c1a8a53aa4dda631 /src/api/cvc4cpp.h | |
| parent | 77fdb2327ae969a7d97b6eb67ad3526d78867b3a (diff) | |
Refactor functions that print commands (Part 2) (#4905)
This PR is a step towards migrating commands to the Term/Sort level. It replaces the dynamic casts for printing commands with direct calls to corresponding functions. Those functions now take node level arguments instead of commands to make them available for internal code.
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 7e91b3b99..6c84b73bc 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -44,6 +44,8 @@ class Datatype; class DatatypeConstructor; class DatatypeConstructorArg; class ExprManager; +class GetAbductCommand; +class GetInterpolCommand; class NodeManager; class SmtEngine; class SynthFunCommand; @@ -1950,8 +1952,10 @@ std::ostream& operator<<(std::ostream& out, */ class CVC4_PUBLIC Grammar { - friend class Solver; + friend class CVC4::GetAbductCommand; + friend class CVC4::GetInterpolCommand; friend class CVC4::SynthFunCommand; + friend class Solver; public: /** |