More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.

4 files changed, 56 insertions, 7 deletions

diff --git a/src/printer/model_format_mode.cpp b/src/printer/modes.cpp
index a8f946a8d..4f7242318 100644
--- a/src/printer/model_format_mode.cpp
+++ b/src/printer/modes.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file model_format_mode.cpp
+/*! \file modes.cpp
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Andrew Reynolds
@@ -15,7 +15,7 @@
  ** \todo document this file
  **/
 
-#include "printer/model_format_mode.h"
+#include "printer/modes.h"
 
 namespace CVC4 {
 
@@ -34,4 +34,18 @@ std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) {
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out, InstFormatMode mode) {
+  switch(mode) {
+  case INST_FORMAT_MODE_DEFAULT:
+    out << "INST_FORMAT_MODE_DEFAULT";
+    break;
+  case INST_FORMAT_MODE_SZS:
+    out << "INST_FORMAT_MODE_SZS";
+    break;
+  default:
+    out << "InstFormatMode:UNKNOWN![" << unsigned(mode) << "]";
+  }
+  return out;
+}
+
 }/* CVC4 namespace */
diff --git a/src/printer/model_format_mode.h b/src/printer/modes.h
index c729c6e5d..9673f791c 100644
--- a/src/printer/model_format_mode.h
+++ b/src/printer/modes.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file model_format_mode.h
+/*! \file modes.h
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: Andrew Reynolds
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__PRINTER__MODEL_FORMAT_MODE_H
-#define __CVC4__PRINTER__MODEL_FORMAT_MODE_H
+#ifndef __CVC4__PRINTER__MODES_H
+#define __CVC4__PRINTER__MODES_H
 
 #include <iostream>
 
@@ -32,7 +32,16 @@ typedef enum {
   MODEL_FORMAT_MODE_TABLE,
 } ModelFormatMode;
 
+/** Enumeration of inst_format modes (how to print models from get-model command). */
+typedef enum {
+  /** default mode (print expressions in the output language format) */
+  INST_FORMAT_MODE_DEFAULT,
+  /** print as SZS proof */
+  INST_FORMAT_MODE_SZS,
+} InstFormatMode;
+
 std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, InstFormatMode mode) CVC4_PUBLIC;
 
 }/* CVC4 namespace */
 
diff --git a/src/printer/options b/src/printer/options
index 7e1b67986..4daa9c77d 100644
--- a/src/printer/options
+++ b/src/printer/options
@@ -5,7 +5,10 @@
 
 module PRINTER "printer/options.h" Printing
 
-option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::printer::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "printer/model_format_mode.h" :handler-include "printer/options_handlers.h"
+option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::printer::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "printer/modes.h" :handler-include "printer/options_handlers.h"
  print format mode for models, see --model-format=help
 
+option instFormatMode --inst-format=MODE InstFormatMode :handler CVC4::printer::stringToInstFormatMode :default INST_FORMAT_MODE_DEFAULT :read-write :include "printer/modes.h" :handler-include "printer/options_handlers.h"
+ print format mode for instantiations, see --inst-format=help
+
 endmodule
diff --git a/src/printer/options_handlers.h b/src/printer/options_handlers.h
index 97d0e64c9..2a89a8d38 100644
--- a/src/printer/options_handlers.h
+++ b/src/printer/options_handlers.h
@@ -19,7 +19,7 @@
 #ifndef __CVC4__PRINTER__OPTIONS_HANDLERS_H
 #define __CVC4__PRINTER__OPTIONS_HANDLERS_H
 
-#include "printer/model_format_mode.h"
+#include "printer/modes.h"
 
 namespace CVC4 {
 namespace printer {
@@ -34,6 +34,16 @@ table\n\
 + Print functional expressions over finite domains in a table format.\n\
 ";
 
+static const std::string instFormatHelp = "\
+Inst format modes currently supported by the --model-format option:\n\
+\n\
+default \n\
++ Print instantiations as a list in the output language format.\n\
+\n\
+szs\n\
++ Print instantiations as SZS compliant proof.\n\
+";
+
 inline ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "default") {
     return MODEL_FORMAT_MODE_DEFAULT;
@@ -48,6 +58,19 @@ inline ModelFormatMode stringToModelFormatMode(std::string option, std::string o
   }
 }
 
+inline InstFormatMode stringToInstFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "default") {
+    return INST_FORMAT_MODE_DEFAULT;
+  } else if(optarg == "szs") {
+    return INST_FORMAT_MODE_SZS;
+  } else if(optarg == "help") {
+    puts(instFormatHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --inst-format: `") +
+                          optarg + "'.  Try --inst-format help.");
+  }
+}
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */