diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-09 06:51:43 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-09 06:51:43 -0500 |
commit | cc01e2119801bbd4fd99548b79c297fa57a1977d (patch) | |
tree | cf9c64efbc286089a898d93abb3150e79138e5a7 /src/expr/command.h | |
parent | 88907b94e858b701e83bbee67f542ad0ee5ae626 (diff) |
Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC proofs.
Diffstat (limited to 'src/expr/command.h')
-rw-r--r-- | src/expr/command.h | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/expr/command.h b/src/expr/command.h index 0d173faf6..ad9cd1aa7 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -575,6 +575,20 @@ public: std::string getCommandName() const throw(); };/* class GetProofCommand */ +class CVC4_PUBLIC GetInstantiationsCommand : public Command { +protected: + //Instantiations* d_result; +public: + GetInstantiationsCommand() throw(); + ~GetInstantiationsCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + //Instantiations* getResult() const throw(); + void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class GetInstantiationsCommand */ + class CVC4_PUBLIC GetUnsatCoreCommand : public Command { protected: //UnsatCore* d_result; |