From 4e810852928a06d398264343585a365a27c2eef9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 21 Jan 2020 10:29:42 -0600
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/basic_cmds.cpp          | 30 -------------------------
 src/cmd_context/extra_cmds/dbg_cmds.cpp | 30 +++++++++++++++++++++++++
 2 files changed, 30 insertions(+), 30 deletions(-)

diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index dd30ca634..3ce523b02 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -31,8 +31,6 @@ Notes:
 #include "cmd_context/cmd_util.h"
 #include "cmd_context/simplify_cmd.h"
 #include "cmd_context/eval_cmd.h"
-#include "qe/qe_mbp.h"
-#include "qe/qe_mbi.h"
 
 class help_cmd : public cmd {
     svector<symbol> m_cmds;
@@ -851,33 +849,6 @@ public:
     void finalize(cmd_context & ctx) override {}
 };
 
-class get_interpolant_cmd : public cmd {
-    expr* m_a;
-    expr* m_b;
-public:
-    get_interpolant_cmd():cmd("get-interpolant") {}
-    char const * get_usage() const override { return "<expr> <expr>"; }
-    char const * get_descr(cmd_context & ctx) const override { return "perform model based interpolation"; }
-    unsigned get_arity() const override { return 2; }
-    cmd_arg_kind next_arg_kind(cmd_context& ctx) const override {
-        return CPK_EXPR; 
-    }
-    void set_next_arg(cmd_context& ctx, expr * arg) override { 
-        if (m_a == nullptr) 
-            m_a = arg; 
-        else 
-            m_b = arg; 
-    }
-    void prepare(cmd_context & ctx) override { m_a = nullptr; m_b = nullptr;  }
-    void execute(cmd_context & ctx) override { 
-        ast_manager& m = ctx.m();
-        qe::interpolator mbi(m);
-        expr_ref itp(m);
-        lbool res = mbi.pogo(ctx.get_solver_factory(), m_a, m_b, itp);
-        ctx.regular_stream() << itp << "\n";
-    }
-};
-
 
 // provides "help" for builtin cmds
 class builtin_cmd : public cmd {
@@ -928,7 +899,6 @@ void install_ext_basic_cmds(cmd_context & ctx) {
     ctx.insert(alloc(echo_cmd));
     ctx.insert(alloc(labels_cmd));
     ctx.insert(alloc(declare_map_cmd));
-    ctx.insert(alloc(get_interpolant_cmd));
     ctx.insert(alloc(builtin_cmd, "reset", nullptr, "reset the shell (all declarations and assertions will be erased)"));
     install_simplify_cmd(ctx);
     install_eval_cmd(ctx);
diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp
index a8e027bb0..47a2f65ee 100644
--- a/src/cmd_context/extra_cmds/dbg_cmds.cpp
+++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp
@@ -376,6 +376,35 @@ public:
     }
 };
 
+class get_interpolant_cmd : public cmd {
+    expr* m_a;
+    expr* m_b;
+public:
+    get_interpolant_cmd():cmd("get-interpolant") {}
+    char const * get_usage() const override { return "<expr> <expr>"; }
+    char const * get_descr(cmd_context & ctx) const override { return "perform model based interpolation"; }
+    unsigned get_arity() const override { return 2; }
+    cmd_arg_kind next_arg_kind(cmd_context& ctx) const override {
+        return CPK_EXPR; 
+    }
+    void set_next_arg(cmd_context& ctx, expr * arg) override { 
+        if (m_a == nullptr) 
+            m_a = arg; 
+        else 
+            m_b = arg; 
+    }
+    void prepare(cmd_context & ctx) override { m_a = nullptr; m_b = nullptr;  }
+    void execute(cmd_context & ctx) override { 
+        ast_manager& m = ctx.m();
+        qe::interpolator mbi(m);
+        expr_ref itp(m);
+        lbool res = mbi.pogo(ctx.get_solver_factory(), m_a, m_b, itp);
+        ctx.regular_stream() << itp << "\n";
+    }
+};
+
+
+
 class mbi_cmd : public cmd {
     expr* m_a;
     expr* m_b;
@@ -550,6 +579,7 @@ void install_dbg_cmds(cmd_context & ctx) {
     ctx.insert(alloc(instantiate_cmd));
     ctx.insert(alloc(instantiate_nested_cmd));
     ctx.insert(alloc(set_next_id));
+    ctx.insert(alloc(get_interpolant_cmd));
     ctx.insert(alloc(mbp_cmd));
     ctx.insert(alloc(mbi_cmd));
     ctx.insert(alloc(euf_project_cmd));