SMTFD is back (#4676)

src/cmd_context/check_logic.cpp

@@ -197,6 +197,14 @@ 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;
         }

src/tactic/fd_solver/CMakeLists.txt

@@ -4,8 +4,10 @@ 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
 )

src/tactic/fd_solver/smtfd_solver.h

@@ -0,0 +1,33 @@
+/*++
+Copyright (c) 2019 Microsoft Corporation
+
+Module Name:
+
+    smtfd_solver.h
+
+Abstract:
+
+    SMT reduction to Finite domain solver.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2019-09-03
+
+Notes:
+   
+--*/
+#pragma once
+
+#include "ast/ast.h"
+#include "util/params.h"
+
+class solver;
+class tactic;
+
+solver * mk_smtfd_solver(ast_manager & m, params_ref const & p);
+tactic * mk_smtfd_tactic(ast_manager & m, params_ref const & p);
+
+/*
+    ADD_TACTIC("smtfd", "builtin strategy for solving SMT problems by reduction to FD.", "mk_smtfd_tactic(m, p)")
+*/
+

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -34,6 +34,7 @@ Notes:
 #include "tactic/smtlogics/nra_tactic.h"
 #include "tactic/portfolio/default_tactic.h"
 #include "tactic/fd_solver/fd_solver.h"
+#include "tactic/fd_solver/smtfd_solver.h"
 #include "tactic/ufbv/ufbv_tactic.h"
 #include "tactic/fpa/qffp_tactic.h"
 #include "muz/fp/horn_tactic.h"
@@ -107,6 +108,8 @@ static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p
     parallel_params pp(p);
     if ((logic == "QF_FD" || logic == "SAT") && !m.proofs_enabled() && !pp.enable())
         return mk_fd_solver(m, p);
+    if (logic == "SMTFD" && !m.proofs_enabled() && !pp.enable())
+        return mk_smtfd_solver(m, p);
     return nullptr;
 }