diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-20 17:59:33 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-20 17:59:33 +0000 |
commit | 3d2b33d66998261f9369cccc098140f64bc8b417 (patch) | |
tree | 9176ad2684415f8fb95f75a5655e8b17dcdf9793 /src/expr/pickle_data.cpp | |
parent | 92155f5e40ed2cf452dc5e2f618e7be6542293e8 (diff) |
portfolio merge
Diffstat (limited to 'src/expr/pickle_data.cpp')
-rw-r--r-- | src/expr/pickle_data.cpp | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp new file mode 100644 index 000000000..1de8f2cf7 --- /dev/null +++ b/src/expr/pickle_data.cpp @@ -0,0 +1,60 @@ +/********************* */ +/*! \file pickle_data.cpp + ** \verbatim + ** Original author: kshitij + ** Major contributors: taking, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This is a "pickle" for expressions, CVC4-internal view + ** + ** This is the CVC4-internal view (private data structure) for a + ** "pickle" for expressions. The public-facing view is a "Pickle", + ** which just points to a PickleData. A pickle is a binary + ** serialization of an expression that can be converted back into an + ** expression in the same or another ExprManager. + **/ + +#include <iostream> +#include <sstream> +#include <string> + +#include "expr/pickle_data.h" +#include "expr/expr.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "expr/node_value.h" +#include "expr/expr_manager_scope.h" +#include "expr/variable_type_map.h" +#include "util/Assert.h" +#include "expr/kind.h" +#include "expr/metakind.h" + +namespace CVC4 { +namespace expr { +namespace pickle { + +void PickleData::writeToStringStream(std::ostringstream& oss) const { + BlockDeque::const_iterator i = d_blocks.begin(), end = d_blocks.end(); + for(; i != end; ++i) { + Block b = *i; + Assert(sizeof(b) * 8 == NBITS_BLOCK); + oss << b.d_body.d_data << " "; + } +} + +std::string PickleData::toString() const { + std::ostringstream oss; + oss.flags(std::ios::oct | std::ios::showbase); + writeToStringStream(oss); + return oss.str(); +} + +}/* CVC4::expr::pickle namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ |