diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-09-08 14:25:25 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-09-08 14:25:25 +0000 |
commit | cfa9e2cbbdf77a325791b5548b41093a0781311c (patch) | |
tree | e843d38afe4b197a2dd81316998477cedac26c52 /src/main/command_executer.h | |
parent | 6935324f45bd7f2c735ca4120a9e800ef8903442 (diff) |
Single driver for both sequential and portfolio
A "command executer" layer between parsing commands and invoking them.
New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.
Diffstat (limited to 'src/main/command_executer.h')
-rw-r--r-- | src/main/command_executer.h | 69 |
1 files changed, 69 insertions, 0 deletions
diff --git a/src/main/command_executer.h b/src/main/command_executer.h new file mode 100644 index 000000000..245857c04 --- /dev/null +++ b/src/main/command_executer.h @@ -0,0 +1,69 @@ +/********************* */ +/*! \file command_executer.cpp + ** \verbatim + ** Original author: kshitij + ** Major contributors: mdeters + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief An additional layer between commands and invoking them. + **/ + +#ifndef __CVC4__COMMAND_EXECUTER_H +#define __CVC4__COMMAND_EXECUTER_H + +#include "expr/expr_manager.h" +#include "smt/smt_engine.h" + +namespace CVC4 { + +namespace main { + +class CommandExecuter { + +protected: + ExprManager& d_exprMgr; + SmtEngine d_smtEngine; + Options& d_options; + +public: + // Note: though the options are not cached (instead a reference is + // used), the portfolio command executer currently parses them + // during initalization, creating thread-specific options and + // storing them + CommandExecuter(ExprManager &exprMgr, Options &options); + + ~CommandExecuter() {} + + /** + * Executes a command. Recursively handles if cmd is a command + * sequence. Eventually uses doCommandSingleton (which can be + * overridden by a derived class). + */ + bool doCommand(CVC4::Command* cmd); + + virtual std::string getSmtEngineStatus(); + +protected: + /** Executes treating cmd as a singleton */ + virtual bool doCommandSingleton(CVC4::Command* cmd); + +private: + CommandExecuter(); + +}; + +bool smtEngineInvoke(SmtEngine* smt, + Command* cmd, + std::ostream *out); + + +}/*main namespace*/ +}/*CVC4 namespace*/ + +#endif /* __CVC4__COMMAND_EXECUTER_H */ |