remove SMTFD

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Sep 2, 2020 · 54a75d6 · 54a75d6
1 parent 7c2fe46
commit 54a75d6
Show file tree

Hide file tree

Showing 5 changed files with 0 additions and 2,175 deletions.
diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp
@@ -197,14 +197,6 @@ struct check_logic::imp {
             m_dt          = true;
             m_nonlinear   = true; // non-linear 0-1 variables may get eliminated
         }
-        else if (logic == "SMTFD") {
-            m_bvs         = true;
-            m_uf          = true;
-            m_arrays      = true;
-            m_ints        = false;
-            m_dt          = false;
-            m_nonlinear   = false; 
-        }
         else {
             m_unknown_logic = true;
         }

diff --git a/src/tactic/fd_solver/CMakeLists.txt b/src/tactic/fd_solver/CMakeLists.txt
@@ -4,10 +4,8 @@ z3_add_component(fd_solver
     enum2bv_solver.cpp
     fd_solver.cpp
     pb2bv_solver.cpp
-    smtfd_solver.cpp
   COMPONENT_DEPENDENCIES
     sat_solver
   TACTIC_HEADERS
     fd_solver.h
-    smtfd_solver.h
 )