Predicate sentence using SMT2/Z3

I need to write the following sentence using SMT2/Z3, not sure of the difference.

For every person who has a parent, he/she must love his/her parent.

So far, I've written

(declare-const x Bool)
(declare-const y Bool)
(declare-const z Bool)
(declare-fun love () Bool)
      (assert =>
         ((forall (x) (y x) )
         (exists z)))

(check-sat)

But this is just giving me an error on arguments which I can't seem to fix.

My predicates are

Person(x) x is a person.

Parent(x, y) x is a parent of y.

Love(x, y) x loves y.

Any help greatly appreciated.

Solution

Here's one way:

(declare-sort Person 0)
(declare-fun parentOf (Person Person) Bool)
(declare-fun loves    (Person Person) Bool)

(assert
   (forall ((x Person) (y Person))
       (=> (parentOf x y)
           (loves x y))))

(check-sat)
(get-model)

z3 says:

sat
(model
  ;; universe for Person:
  ;;   Person!val!0
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun Person!val!0 () Person)
  ;; cardinality constraint:
  (forall ((x Person)) (= x Person!val!0))
  ;; -----------
  (define-fun loves ((x!0 Person) (x!1 Person)) Bool
    false)
  (define-fun parentOf ((x!0 Person) (x!1 Person)) Bool
    false)
)

Essentially, z3 is telling us that our constraints are satisfiable (that's the meaning of the output sat) and a (note: not the) satisfying assignment is a universe where there's:

Precisely one person, named Person!val!0
Nobody loves anyone
Nobody is the parent of anyone else

Which clearly satisfies all the constraints, but perhaps not the most interesting model out there. If you assert further facts, you can get richer models. (For instance, you can say there're at least 5 people, that nobody is their own parent, parenting relationship is not symmetric, everybody loves themselves, etc. depending on exactly what you're trying to model.)

Keep in mind that SMT solvers are not good for dealing with quantifiers. While statements like this will work just fine, extensive use of quantifiers and first-order logic will put theories into the semi-decidable territory, i.e., z3 can end up saying unknown. SMT solvers are best for quantifier-free combinations of theories such as arithmetic, arrays, datatypes, etc. For problems such as these, Prolog is probably your best bet for modeling purposes.