Simplify nlsat code by removing redundant else statements

Remove unnecessary 'else' keywords after early return statements in recently merged nlsat code (PR #8498). This improves code clarity by eliminating redundant control flow statements.

Changes:
- src/nlsat/nlsat_solver.cpp: Removed 7 redundant else statements
- src/nlsat/nlsat_explain.cpp: Removed 1 redundant else statement
- src/nlsat/tactic/goal2nlsat.cpp: Removed 1 redundant else statement
- src/nlsat/tactic/nlsat_tactic.cpp: Removed 1 redundant else statement

All simplifications preserve exact functionality - only control flow clarity improved.
Tests: All unit tests pass (./test-z3 /a)
Build: Clean compilation with no warnings

src/nlsat/nlsat_explain.cpp

@@ -567,8 +567,7 @@ namespace nlsat {
             atom * a  = m_atoms[l.var()];
             if (a != nullptr)
                 return a->max_var();
-            else
-                return null_var;
+            return null_var;
         }
 
         /**

src/nlsat/nlsat_solver.cpp

@@ -422,8 +422,7 @@ namespace nlsat {
         var max_var(bool_var b) const {
             if (!is_arith_atom(b))
                 return null_var;
-            else
-                return m_atoms[b]->max_var();
+            return m_atoms[b]->max_var();
         }
 
         var max_var(literal l) const {
@@ -1439,8 +1438,7 @@ namespace nlsat {
             bool_var b = l.var();
             if (l.sign())
                 return ~m_bvalues[b];
-            else
-                return m_bvalues[b];
+            return m_bvalues[b];
         }
 
         /**
@@ -1747,8 +1745,7 @@ namespace nlsat {
                 return true;
             if (m_xk == null_var)
                 return process_boolean_clause(cls);
-            else
-                return process_arith_clause(cls, satisfy_learned);
+            return process_arith_clause(cls, satisfy_learned);
         }
 
         /**
@@ -3880,8 +3877,7 @@ namespace nlsat {
             std::ostream& operator()(std::ostream & out, var x) const override {
                 if (m_x == x)
                     return out << "#1";
-                else
-                    return out << "x" << x; 
+                return out << "x" << x; 
             }
         };
 
@@ -3904,8 +3900,7 @@ namespace nlsat {
         std::ostream& display(std::ostream & out, atom const & a, display_var_proc const & proc) const {
             if (a.is_ineq_atom())
                 return display_ineq(out, static_cast<ineq_atom const &>(a), proc);
-            else
-                return display_root(out, static_cast<root_atom const &>(a), proc);
+            return display_root(out, static_cast<root_atom const &>(a), proc);
         }
 
         std::ostream& display(std::ostream & out, atom const & a) const {
@@ -3915,15 +3910,13 @@ namespace nlsat {
         std::ostream& display_mathematica(std::ostream & out, atom const & a) const {
             if (a.is_ineq_atom())
                 return display_mathematica(out, static_cast<ineq_atom const &>(a));
-            else
-                return display_mathematica(out, static_cast<root_atom const &>(a));
+            return display_mathematica(out, static_cast<root_atom const &>(a));
         }
 
         std::ostream& display_smt2(std::ostream & out, atom const & a, display_var_proc const & proc) const {
             if (a.is_ineq_atom())
                 return display_ineq_smt2(out, static_cast<ineq_atom const &>(a), proc);
-            else
-                return display_root_smt2(out, static_cast<root_atom const &>(a), proc);
+            return display_root_smt2(out, static_cast<root_atom const &>(a), proc);
         }
 
         std::ostream& display_atom(std::ostream & out, bool_var b, display_var_proc const & proc) const {

src/nlsat/tactic/goal2nlsat.cpp

@@ -180,8 +180,7 @@ struct goal2nlsat::imp {
         if (m.is_eq(f)) {
             if (m_util.is_int_real(to_app(f)->get_arg(0)))
                 return process_eq(to_app(f));
-            else
-                return nlsat::literal(process_bvar(f), false);                
+            return nlsat::literal(process_bvar(f), false);                
         }
         else if (m_util.is_le(f)) {
             return process_le(to_app(f));

src/nlsat/tactic/nlsat_tactic.cpp

@@ -35,8 +35,7 @@ class nlsat_tactic : public tactic {
         std::ostream& operator()(std::ostream & out, nlsat::var x) const override {
             if (x < m_var2expr.size())
                 return out << mk_ismt2_pp(m_var2expr.get(x), m); 
-            else
-                return out << "x!" << x;
+            return out << "x!" << x;
         }
     };