Interpret: Use the new TermPrinter for printing models and interpolants

src/bin/Interpret.cc

@@ -30,6 +30,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 #include "ArithLogic.h"
 #include "LogicFactory.h"
 #include "Substitutor.h"
+#include "TermPrinter.h"
 
 #include <string>
 #include <sstream>
@@ -791,10 +792,10 @@ std::string Interpret::printDefinitionSmtlib(const TemplateFunction & templateFu
     const vec<PTRef>& args = templateFun.getArgs();
     for (int i = 0; i < args.size(); i++) {
         auto sortString = logic->printSort(logic->getSortRef(args[i]));
-        ss << "(" << logic->pp(args[i]) << " " << sortString << ")" << (i == args.size()-1 ? "" : " ");
+        ss << "(" << TermPrinter(*logic).print(args[i]) << " " << sortString << ")" << (i == args.size()-1 ? "" : " ");
     }
     ss << ")" << " " << logic->printSort(templateFun.getRetSort()) << "\n";
-    ss << "    " << logic->pp(templateFun.getBody()) << ")\n";
+    ss << "    " << TermPrinter(*logic).print(templateFun.getBody()) << ")\n";
     return ss.str();
 }
 
@@ -1284,7 +1285,7 @@ void Interpret::getInterpolants(const ASTNode& n)
     }
 
     for (int j = 0; j < itps.size(); j++) {
-        auto itp = logic->pp(itps[j]);
+        auto itp = TermPrinter(*logic).print(itps[j]);
         notify_formatted(false, "%s%s%s",
                          (j == 0 ? "(" : " "), itp.c_str(), (j == itps.size() - 1 ? ")" : ""));
     }