add finite sets to datatype recursion, delay initialize finite_set plugin, fix bugs in are_distinct and equality simplification

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/theory_finite_set_size.cpp

@@ -470,6 +470,7 @@ namespace smt {
         }
     }
 
+
     std::ostream& theory_finite_set_size::display(std::ostream& out) const {
         if (m_solver)
             m_solver->display(out << "set.size-solver\n");