From 36fb4dcec8fb09a48da59261eda0582da68348cd Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 23 Oct 2018 17:21:09 -0700 Subject: Sketch of refactoring the Commands to use new API 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`. --- src/parser/smt2/Smt2.g | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'src/parser/smt2/Smt2.g') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d9b0f622b..77de8d0c2 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -112,6 +112,7 @@ namespace CVC4 { #include #include +#include "api/cvc4cpp.h" #include "base/output.h" #include "expr/expr.h" #include "expr/kind.h" @@ -403,7 +404,9 @@ command [std::unique_ptr* cmd] | /* value query */ GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,expr] RPAREN_TOK - { cmd->reset(new GetValueCommand(terms)); } + { + cmd->reset(new GetValueCommand(api::Solver::exprVectorToTerms(terms))); + } | ~LPAREN_TOK { PARSER_STATE->parseError("The get-value command expects a list of " "terms. Perhaps you forgot a pair of " -- cgit v1.2.3