diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
commit | 0b2f9943d55152e0958369083649dd71340864c9 (patch) | |
tree | cd040f1dd12816c6af37548597bd674cafb45271 /src/printer | |
parent | 8ebd49cb903ba19f9330820d02af08e226c9b791 (diff) |
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.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/modes.cpp (renamed from src/printer/model_format_mode.cpp) | 18 | ||||
-rw-r--r-- | src/printer/modes.h (renamed from src/printer/model_format_mode.h) | 15 | ||||
-rw-r--r-- | src/printer/options | 5 | ||||
-rw-r--r-- | src/printer/options_handlers.h | 25 |
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 */ |