Sketch of refactoring the Commands to use new APInewApiForCommands

This commit is a sketch of how we can transform `Command`s to use the
new API and transform the parser bit-by-bit. The overall idea is that
`Command::invoke()` now takes an `Solver*` as an argument instead of an
`SmtEngine*`. The default implementation `Command::invoke()` just calls
the old implementation. As an example, the PR transforms the
`GetValueCommand`.

1 files changed, 3 insertions, 2 deletions

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 6b88a109c..e31ab44bc 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -20,6 +20,7 @@
 #include <typeinfo>
 #include <vector>
 
+#include "api/cvc4cpp.h"  // for ExprSetDepth etc..
 #include "expr/expr.h" // for ExprSetDepth etc..
 #include "expr/node_manager_attributes.h" // for VarNameAttr
 #include "options/language.h" // for LANG_AST
@@ -340,8 +341,8 @@ static void toStream(std::ostream& out, const SimplifyCommand* c)
 static void toStream(std::ostream& out, const GetValueCommand* c)
 {
   out << "GetValue( << ";
-  const vector<Expr>& terms = c->getTerms();
-  copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, ", "));
+  const vector<api::Term>& terms = c->getTerms();
+  copy(terms.begin(), terms.end(), ostream_iterator<api::Term>(out, ", "));
   out << ">> )";
 }