From 22ef16d1108dd0e42da203ca4d453fbdd128a8d6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 26 Jul 2021 20:52:15 -0500 Subject: [PATCH] Miscellaneous fixes from proof-new (#6914) --- src/expr/bound_var_manager.h | 2 +- src/printer/smt2/smt2_printer.cpp | 11 +++++++++-- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h index b619a36e2..507cebab3 100644 --- a/src/expr/bound_var_manager.h +++ b/src/expr/bound_var_manager.h @@ -77,7 +77,7 @@ class BoundVarManager Node mkBoundVar(Node n, const std::string& name, TypeNode tn) { Node v = mkBoundVar(n, tn); - setNameAttr(n, name); + setNameAttr(v, name); return v; } //---------------------------------- utilities for computing Node hash diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b5a8472e6..bf26b80ee 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -824,8 +824,8 @@ void Smt2Printer::toStream(std::ostream& out, case kind::PRODUCT: case kind::TRANSPOSE: case kind::TCLOSURE: - out << smtKindString(k, d_variant) << " "; - break; + case kind::IDEN: + case kind::JOIN_IMAGE: out << smtKindString(k, d_variant) << " "; break; case kind::COMPREHENSION: out << smtKindString(k, d_variant) << " "; break; case kind::SINGLETON: { @@ -1237,6 +1237,11 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right"; case kind::INT_TO_BITVECTOR: return "int2bv"; + // datatypes theory + case kind::APPLY_TESTER: return "is"; + case kind::APPLY_UPDATER: return "update"; + + // set theory case kind::UNION: return "union"; case kind::INTERSECTION: return "intersection"; case kind::SETMINUS: return "setminus"; @@ -1254,6 +1259,8 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::PRODUCT: return "product"; case kind::TRANSPOSE: return "transpose"; case kind::TCLOSURE: return "tclosure"; + case kind::IDEN: return "iden"; + case kind::JOIN_IMAGE: return "join_image"; // bag theory case kind::BAG_TYPE: return "Bag"; -- 2.30.2