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

1 files changed, 42 insertions, 0 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 9341c9828..34cdd2e30 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1048,6 +1048,48 @@ std::string GetProofCommand::getCommandName() const throw() {
   return "get-proof";
 }
 
+/* class GetInstantiationsCommand */
+
+GetInstantiationsCommand::GetInstantiationsCommand() throw() {
+}
+
+void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    smtEngine->printInstantiations();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+//Instantiations* GetInstantiationsCommand::getResult() const throw() {
+//  return d_result;
+//}
+
+void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out, verbosity);
+  } else {
+    //d_result->toStream(out);
+  }
+}
+
+Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetInstantiationsCommand* c = new GetInstantiationsCommand();
+  //c->d_result = d_result;
+  return c;
+}
+
+Command* GetInstantiationsCommand::clone() const {
+  GetInstantiationsCommand* c = new GetInstantiationsCommand();
+  //c->d_result = d_result;
+  return c;
+}
+
+std::string GetInstantiationsCommand::getCommandName() const throw() {
+  return "get-instantiations";
+}
+
 /* class GetUnsatCoreCommand */
 
 GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {