Difference between Dependent type , refinement type and Hoare Logic

Question

I know little dependent type theory. From wikipedia :

A dependent type is a type whose definition depends on a value.

And from my Type theory course i recall that a dependent type is :

Family of types indexed by a type.

But i have a confusion regarding dependent types and refinement types and hoare logic.

Because from Depenedent vs refinement type the refinement types looks like a Hoare logic. What more power refinement types gives besides just allowing to state predicated that has to be satisfied (Which looks like nearly same as Hoare Logic)?

What additional thing that dependent type gives in comparison to refinement types ? And is Dependent type more powerful than Refinement types + Sat/Constraint solver.

can anyone clear the air with examples.