diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-14 01:45:58 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-14 10:45:58 +0200 |
| commit | 292b2c5712ce31282ac3ec564f268ee7f0aa3506 (patch) | |
| tree | 7333ca654b5716f5829a5c8bb00e7f7f98d1db08 /src/expr | |
| parent | 88adf5e1416fb0c533fe3a24da5fce50aa5a2c0b (diff) | |
exportTo only if needed for --sygus-rr-synth-check (#2168)
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/expr_manager_template.cpp | 10 | ||||
| -rw-r--r-- | src/expr/expr_template.cpp | 5 | ||||
| -rw-r--r-- | src/expr/type_node.cpp | 1 |
3 files changed, 15 insertions, 1 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 33b06ead4..457e54d9b 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -1023,6 +1023,16 @@ TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, Expr } else if(n.getKind() == kind::BITVECTOR_TYPE) { return to->mkBitVectorType(n.getConst<BitVectorSize>()); } + else if (n.getKind() == kind::FLOATINGPOINT_TYPE) + { + return to->mkFloatingPointType(n.getConst<FloatingPointSize>()); + } + else if (n.getNumChildren() == 0) + { + std::stringstream msg; + msg << "export of type " << n << " not supported"; + throw ExportUnsupportedException(msg.str().c_str()); + } Type from_t = from->toType(n); Type& to_t = vmap.d_typeMap[from_t]; if(! to_t.isNull()) { diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 1344935af..3a0d31b2d 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -248,8 +248,11 @@ public: children.push_back(exportInternal(*i)); } if(Debug.isOn("export")) { - ExprManagerScope ems(*to); Debug("export") << "children for export from " << n << std::endl; + + // `n` belongs to the `from` ExprManager, so begin ExprManagerScope + // after printing `n` + ExprManagerScope ems(*to); for(std::vector<Node>::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) { Debug("export") << " child: " << *i << std::endl; } diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index b3e5c5a83..d6cf12d41 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -342,6 +342,7 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { // t1.getKind() == kind::TYPE_CONSTANT switch(t0.getKind()) { case kind::BITVECTOR_TYPE: + case kind::FLOATINGPOINT_TYPE: case kind::SORT_TYPE: case kind::CONSTRUCTOR_TYPE: case kind::SELECTOR_TYPE: |