From 181bdb681529b9457652acee5612788e3f11547a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 2 Nov 2012 14:18:12 -0700
Subject: [PATCH] removed dead files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/cmd_context/strategic_solver_cmd.cpp      | 34 ----------------
 src/cmd_context/strategic_solver_cmd.h        | 40 -------------------
 src/tactic/portfolio/smt_strategic_solver.cpp |  2 +-
 3 files changed, 1 insertion(+), 75 deletions(-)
 delete mode 100644 src/cmd_context/strategic_solver_cmd.cpp
 delete mode 100644 src/cmd_context/strategic_solver_cmd.h

diff --git a/src/cmd_context/strategic_solver_cmd.cpp b/src/cmd_context/strategic_solver_cmd.cpp
deleted file mode 100644
index 3bb820e0d..000000000
--- a/src/cmd_context/strategic_solver_cmd.cpp
+++ /dev/null
@@ -1,34 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
-    strategic_solver_cmd.h
-
-Abstract:
-
-    Specialization of the strategic solver that
-    used cmd_context to access the assertion set.
-
-Author:
-
-    Leonardo (leonardo) 2012-11-01
-
-Notes:
-
---*/
-#include"strategic_solver_cmd.h"
-#include"cmd_context.h"
-
-strategic_solver_cmd::strategic_solver_cmd(cmd_context & ctx):
-    m_ctx(ctx) {
-}
-
-unsigned strategic_solver_cmd::get_num_assertions() const {
-    return static_cast<unsigned>(m_ctx.end_assertions() - m_ctx.begin_assertions());
-}
-
-expr * strategic_solver_cmd::get_assertion(unsigned idx) const {
-    SASSERT(idx < get_num_assertions());
-    return m_ctx.begin_assertions()[idx];
-}
diff --git a/src/cmd_context/strategic_solver_cmd.h b/src/cmd_context/strategic_solver_cmd.h
deleted file mode 100644
index 014d2dee6..000000000
--- a/src/cmd_context/strategic_solver_cmd.h
+++ /dev/null
@@ -1,40 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
-    strategic_solver_cmd.h
-
-Abstract:
-
-    Specialization of the strategic solver that
-    used cmd_context to access the assertion set.
-
-Author:
-
-    Leonardo (leonardo) 2012-11-01
-
-Notes:
-
---*/
-#ifndef _STRATEGIC_SOLVER_CMD_H_
-#define _STRATEGIC_SOLVER_CMD_H_
-
-#include"strategic_solver.h"
-
-class cmd_context;
-
-/**
-   Specialization for the SMT 2.0 command language frontend.
-
-   The strategic solver does not have to maintain a copy of the assertion set in the cmd_context.
-*/
-class strategic_solver_cmd : public strategic_solver_core {
-    cmd_context &        m_ctx;
-public:
-    strategic_solver_cmd(cmd_context & ctx);
-    virtual unsigned get_num_assertions() const;
-    virtual expr * get_assertion(unsigned idx) const;
-};
-
-#endif 
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 1cf43a45c..b958c42b9 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -18,7 +18,7 @@ Notes:
 
 --*/
 #include"cmd_context.h"
-#include"strategic_solver_cmd.h"
+#include"strategic_solver.h"
 #include"qfbv_tactic.h"
 #include"qflia_tactic.h"
 #include"qfnia_tactic.h"