Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC proofs.

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;