Incorrect model

[AnzhelaSukhanova]

Hello!

For

(set-logic HORN)

(declare-fun |state| ( Bool Bool Bool Bool Int Int Int ) Bool)

(assert (forall ((C Int) (D Int) (E Int)) (state false true false false C D E)))

(assert (forall ((A Bool)
         (B Bool)
         (C Bool)
         (D Bool)
         (E Bool)
         (F Bool)
         (G Int)
         (H Int)
         (I Int)
         (J Int)
         (K Int)
         (L Int)
         (M Bool)
         (N Bool))
  (let ((a!1 (and (state B A N M H J L)
                  (or M N (not A) (not B) (and F D (not C) (= H G)))
                  (or M A B)
                  (or M (not N) A)
                  (or N (not M) (not B))
                  (or M N B (and (not F) E (not D) (= G 1)))
                  (or M N A (and E D (not C) (= H G)))
                  (or N B (<= H 0)))))
    (or (not a!1) (state E D C F G I K)))))

(assert (forall ((C Int) (D Int) (E Int)) (not (state false false true true C D E))))

(check-sat)

eldarica returns

sat
(define-fun state ((A Bool) (B Bool) (C Bool) (D Bool) (E Int) (F Int) (G Int)) Bool (or (or (or (and (and (and (= A true) (= B true)) (not (= C true))) (>= E 1)) (and (and (= A true) (and (not (= B true)) (not (= D true)))) (>= E 1))) (and (= B true) (and (and (not (= A true)) (not (= C true))) (not (= D true))))) (and (and (= B true) (not (= C true))) (and (>= (- E D) 1) (>= (+ D E) 1)))))

It seems to me, this model isn't correct. Let's consider state definition. If A is True, B is True, C is False and E >= 1, then state is True. So, if in the second clause B is True, A is True, N is False and H >= 1, then (state B A N M H J L) is True. Conjunctions 2, 3, 5-7 in the a!1 is True too. Conjunction 4 is True if M is False, and conjunction 1 is True if F is True, D is True, C is False and H is G.

Thus, (state E D C F G I K) is (state E True False True G I K) where G >= 1 and (not a!1) is False. If E is False and G is 1, then (state E True False True G I K) is False too.

[pruemmer]

You are right, there is some weirdness here. The inequality (>= (- E D) 1) is ill-typed, and must stem from the fact that we internally encode Booleans as integers [0, 1]. We should add a post-processor for eliminating such expressions.

I don't think the solution is actually incorrect, since Eldarica can verify it internally (option -assert). You can also get a well-formed solution by adding the option -abstract:off (which can be verified independently using z3).

I'm leaving this issue open until I find time to fix this presentation problem.