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/model_format_mode.h | |
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/model_format_mode.h')
-rw-r--r-- | src/printer/model_format_mode.h | 39 |
1 files changed, 0 insertions, 39 deletions
diff --git a/src/printer/model_format_mode.h b/src/printer/model_format_mode.h deleted file mode 100644 index c729c6e5d..000000000 --- a/src/printer/model_format_mode.h +++ /dev/null @@ -1,39 +0,0 @@ -/********************* */ -/*! \file model_format_mode.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__PRINTER__MODEL_FORMAT_MODE_H -#define __CVC4__PRINTER__MODEL_FORMAT_MODE_H - -#include <iostream> - -namespace CVC4 { - -/** Enumeration of model_format modes (how to print models from get-model command). */ -typedef enum { - /** default mode (print expressions in the output language format) */ - MODEL_FORMAT_MODE_DEFAULT, - /** print functional values in a table format */ - MODEL_FORMAT_MODE_TABLE, -} ModelFormatMode; - -std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* __CVC4__PRINTER__MODEL_FORMAT_H */ |