diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 8 | ||||
-rw-r--r-- | src/expr/command.h | 7 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 14 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 9 | ||||
-rw-r--r-- | src/expr/expr_template.h | 13 | ||||
-rw-r--r-- | src/expr/pickler.cpp | 9 | ||||
-rw-r--r-- | src/expr/pickler.h | 12 |
7 files changed, 45 insertions, 27 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 938f28635..a62a9421f 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -1273,12 +1273,8 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { } Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - throw ExportToUnsupportedException(); - // vector<DatatypeType> params; - // transform(d_datatypes.begin(), d_datatypes.end(), back_inserter(params), - // ExportTransformer(exprManager, variableMap)); - // DatatypeDeclarationCommand* c = new DatatypeDeclarationCommand(params); - // return c; + throw ExportUnsupportedException + ("export of DatatypeDeclarationCommand unsupported"); } Command* DatatypeDeclarationCommand::clone() const { diff --git a/src/expr/command.h b/src/expr/command.h index 5786f4e71..e120deed6 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -50,13 +50,6 @@ std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC; std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC; std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC; -class CVC4_PUBLIC ExportToUnsupportedException : public Exception { -public: - ExportToUnsupportedException() throw() : - Exception("exportTo unsupported for command") { - } -};/* class ExportToUnsupportedException */ - /** The status an SMT benchmark can have */ enum BenchmarkStatus { /** Benchmark is satisfiable */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index be2804fd5..457491445 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -928,13 +928,21 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) { Debug("export") << "type: " << n << std::endl; - Assert(n.getKind() == kind::SORT_TYPE || - n.getMetaKind() != kind::metakind::PARAMETERIZED, - "PARAMETERIZED-kinded types (other than SORT_KIND) not supported"); + if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) { + throw ExportUnsupportedException + ("export of types belonging to theory of DATATYPES kinds unsupported"); + } + if(n.getMetaKind() == kind::metakind::PARAMETERIZED && + n.getKind() != kind::SORT_TYPE) { + throw ExportUnsupportedException + ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported"); + } if(n.getKind() == kind::TYPE_CONSTANT) { return to->mkTypeConst(n.getConst<TypeConstant>()); } else if(n.getKind() == kind::BITVECTOR_TYPE) { return to->mkBitVectorType(n.getConst<BitVectorSize>()); + } else if(n.getKind() == kind::SUBRANGE_TYPE) { + return to->mkSubrangeType(n.getSubrangeBounds()); } Type from_t = from->toType(n); Type& to_t = vmap.d_typeMap[from_t]; diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index f39c0e7ea..2f9e27c0c 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -114,7 +114,12 @@ namespace expr { static Node exportConstant(TNode n, NodeManager* to); Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap) { - if(n.isConst()) { + if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) { + throw ExportUnsupportedException + ("export of node belonging to theory of DATATYPES kinds unsupported"); + } + + if(n.getMetaKind() == metakind::CONSTANT) { return exportConstant(n, NodeManager::fromExprManager(to)); } else if(n.isVar()) { Expr from_e(from, new Node(n)); @@ -132,7 +137,7 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC // a check that mkVar isn't called internally NodeManagerScope nullScope(NULL); - if(n.getKind() == kind::BOUND_VAR_LIST) { + if(n.getKind() == kind::BOUND_VAR_LIST || n.getKind() == kind::BOUND_VARIABLE) { to_e = to->mkBoundVar(name, type);// FIXME thread safety } else if(n.getKind() == kind::VARIABLE) { to_e = to->mkVar(name, type);// FIXME thread safety diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 96c7cfadf..4255e3454 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -132,6 +132,19 @@ public: friend class ExprManager; };/* class TypeCheckingException */ +/** + * Exception thrown in case of failure to export + */ +class CVC4_PUBLIC ExportUnsupportedException : public Exception { +public: + ExportUnsupportedException() throw(): + Exception("export unsupported") { + } + ExportUnsupportedException(const char* msg) throw(): + Exception(msg) { + } +};/* class DatatypeExportUnsupportedException */ + std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) CVC4_PUBLIC; diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp index a41db794d..6548cf98a 100644 --- a/src/expr/pickler.cpp +++ b/src/expr/pickler.cpp @@ -129,7 +129,7 @@ Pickler::~Pickler() { } void Pickler::toPickle(Expr e, Pickle& p) - throw(AssertionException, PicklingException) { + throw(PicklingException) { Assert(NodeManager::fromExprManager(e.getExprManager()) == d_private->d_nm); Assert(d_private->atDefaultState()); @@ -471,6 +471,13 @@ Pickle::~Pickle() { delete d_data; } +uint64_t MapPickler::variableFromMap(uint64_t x) const +{ + VarMap::const_iterator i = d_fromMap.find(x); + Assert(i != d_fromMap.end()); + return i->second; +} + }/* CVC4::expr::pickle namespace */ }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/expr/pickler.h b/src/expr/pickler.h index a6427ad47..dee4f06e6 100644 --- a/src/expr/pickler.h +++ b/src/expr/pickler.h @@ -67,7 +67,7 @@ class CVC4_PUBLIC Pickler { protected: virtual uint64_t variableToMap(uint64_t x) const - throw(AssertionException, PicklingException) { + throw(PicklingException) { return x; } virtual uint64_t variableFromMap(uint64_t x) const { @@ -87,7 +87,7 @@ public: * * @return the pickle, which should be dispose()'d when you're done with it */ - void toPickle(Expr e, Pickle& p) throw(AssertionException, PicklingException); + void toPickle(Expr e, Pickle& p) throw(PicklingException); /** * Constructs a node from a Pickle. @@ -116,7 +116,7 @@ public: protected: virtual uint64_t variableToMap(uint64_t x) const - throw(AssertionException, PicklingException) { + throw(PicklingException) { VarMap::const_iterator i = d_toMap.find(x); if(i != d_toMap.end()) { return i->second; @@ -125,11 +125,7 @@ protected: } } - virtual uint64_t variableFromMap(uint64_t x) const { - VarMap::const_iterator i = d_fromMap.find(x); - Assert(i != d_fromMap.end()); - return i->second; - } + virtual uint64_t variableFromMap(uint64_t x) const; };/* class MapPickler */ }/* CVC4::expr::pickle namespace */ |