merge from fmf-devel branch. more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models

1 files changed, 24 insertions, 0 deletions

diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 925f86d48..fb6cd84d8 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -150,6 +150,16 @@ none\n\
 + do not perform nonclausal simplification\n\
 ";
 
+static const std::string modelFormatHelp = "\
+Model format modes currently supported by the --model-format option:\n\
+\n\
+default \n\
++ Print model as expressions in the output language format.\n\
+\n\
+table\n\
++ Print functional expressions over finite domains in a table format.\n\
+";
+
 inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
 #ifdef CVC4_DUMPING
   char* optargPtr = strdup(optarg.c_str());
@@ -231,6 +241,20 @@ inline SimplificationMode stringToSimplificationMode(std::string option, std::st
   }
 }
 
+inline ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "default") {
+    return MODEL_FORMAT_MODE_DEFAULT;
+  } else if(optarg == "table") {
+    return MODEL_FORMAT_MODE_TABLE;
+  } else if(optarg == "help") {
+    puts(modelFormatHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --model-format: `") +
+                          optarg + "'.  Try --model-format help.");
+  }
+}
+
 // This macro is used for setting :regular-output-channel and :diagnostic-output-channel
 // to redirect a stream.  It maintains all attributes set on the stream.
 #define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \