diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-10-10 08:25:24 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-10 08:25:24 -0500 |
| commit | 9e481faf7dfce8f992ae6730ad49f6db335b6432 (patch) | |
| tree | 2261c38ea1af96a9832bb99f5a6eba93513f20b7 /src/smt/command.h | |
| parent | e6c9674d9a7d2ffd5f4093ddd2db64fb45b470d2 (diff) | |
Provide API version of some SMT Commands. (#5222)
This PR provides an SMT version of the following SMT commands:
get-instantiations
block-model
block-model-values
get-qe
get-qe-disjunct
command.cpp now calls those functions instead of their SmtEngine counterparts. In addition, SEXPR is now an API kind.
Diffstat (limited to 'src/smt/command.h')
| -rw-r--r-- | src/smt/command.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/command.h b/src/smt/command.h index 81a736407..b823b5730 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1070,7 +1070,7 @@ class CVC4_PUBLIC GetInstantiationsCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; protected: - SmtEngine* d_smtEngine; + api::Solver* d_solver; }; /* class GetInstantiationsCommand */ class CVC4_PUBLIC GetSynthSolutionCommand : public Command |