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.

1 files changed, 24 insertions, 1 deletions

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 */