Illegal clauses - Githubissues

AdrienChampion commented 6 years ago

The following benchmarks produce errors of the form

z3.z3types.Z3Exception: Rule contains negative predicate <null>:
P!!2(#0,#1,#2) :-
 not INV_REC_f__2_PRE(#3),
 (= (:var 3) (- (:var 0) 2)).

which seems to mean that the Horn clauses are not Horn clauses since some have shape

(=> (and ...  (not <pred_app>) ...) <pred_app>)

agurfinkel commented 6 years ago

@mattulbrich , is that a clausification problem or are the predicates really negated?

AdrienChampion commented 6 years ago

At least some of them have a .muz counterpart.

But the first one (smt2/arrays/heap__heap_call.array.smt2), for instance, does not.

mattulbrich commented 6 years ago

There is no intentional negation.

@AdrienChampion , could you please point out on an example how this negation arises from the smt2? I do not see it.

Which tool are you using? The above examples did not raise parser exceptions and either Z3 or eldarica was able to find a solution for them.

AdrienChampion commented 6 years ago

(Warning: ugly verbose post.)

@mattulbrich

On smt2/arrays/libc__sbrk_1.array.smt2, z3 complains about this clause

(forall ((increment$1_0_old Int)
         (HEAP$1_old (Array Int Int))
         (increment$2_0_old Int)
         (HEAP$2_old (Array Int Int)))
  (let ((a!1 (forall ((call$1_0 Int)
                      (call$2_0 Int)
                      (HEAP$1_res (Array Int Int))
                      (HEAP$2_res (Array Int Int)))
               (let ((a!1 (=> (not (< call$2_0 0))
                              (=> (not (= increment$2_0_old 0))
                                  (INV_MAIN_0 increment$1_0_old
                                              HEAP$1_res
                                              increment$2_0_old
                                              HEAP$2_res)))))
               (let ((a!2 (=> (not (< call$1_0 0))
                              (=> (not (= increment$1_0_old 0)) a!1))))
                 (=> (=> (and (= 0 0) (= HEAP$1_old HEAP$2_old))
                         (and (= call$1_0 call$2_0) (= HEAP$1_res HEAP$2_res)))
                     a!2))))))
  (let ((a!2 (=> (= (select HEAP$2_old (- 9)) 0) a!1)))
  (let ((a!3 (=> (= (select HEAP$1_old (- 9)) 0) a!2)))
    (=> (and (= increment$1_0_old increment$2_0_old) (= HEAP$1_old HEAP$2_old))
        a!3)))))

It says

z3.z3types.Z3Exception: Rule contains negative predicate <null>:
query!21() :-
 not INV_MAIN_0(#3,#6,#1,#7),
 (not (< (:var 5) 0)),
 (not (= (:var 3) 0)),
 (not (< (:var 4) 0)),
 (=> (and (= 0 0) (= (:var 2) (:var 0)))
    (and (= (:var 4) (:var 5)) (= (:var 6) (:var 7)))),
 (= (select (:var 0) (- 9)) 0),
 (= (:var 3) (:var 1)),
 (= (select (:var 2) (- 9)) 0),
 (= (:var 2) (:var 0)),
 (not (= (:var 1) 0)).

I'm not sure that's the real problem here though. When I inline the let bindings from the clause above I get (omitting the inner forall):

(assert
  (forall
    ( (increment$1_0_old Int)
      (HEAP$1_old (Array Int Int))
      (increment$2_0_old Int)
      (HEAP$2_old (Array Int Int))
    )

    (=>
      (and
        (= increment$1_0_old increment$2_0_old)
        (= HEAP$1_old HEAP$2_old)
      )
      (=>
        (= (select HEAP$1_old (- 9)) 0)
        (=> (= (select HEAP$2_old (- 9)) 0)
          (=>
            (=> (and (= 0 0) (= HEAP$1_old HEAP$2_old))
                (and (= call$1_0 call$2_0) (= HEAP$1_res HEAP$2_res))
            )
            (=> (not (< call$1_0 0))
                (=>
                  (not (= increment$1_0_old 0))
                  (=> (not (< call$2_0 0))
                      (=> (not (= increment$2_0_old 0))
                          (INV_MAIN_0
                            increment$1_0_old
                            HEAP$1_res
                            increment$2_0_old
                            HEAP$2_res
                          )
; skipping remaining closing parents.

So unless I messed up the inlining (which is possible), INV_MAIN_0 seems to be appearing positively...

mattulbrich commented 6 years ago

I take it then, that it is the Z3 translation which seems to be problematic and not our input in this case?

mattulbrich commented 6 years ago

Ah! :bulb:

This error message only reaches surface if -v:X for a sufficiently high X is chosen. We did receive plenty of unknown results by spacer, perhaps because these parsing errors occurred. ~~Z3's duality engine can parse these files.~~ In more recent versions, duality also chokes on the SMT input.

mattulbrich commented 6 years ago

I believe it is a belated quantifier that irritates the parser.

We produce clauses of the form

(forall ((...)) (=> (pred ...) (forall ((...)) ...)))

which is equivalent to mentioning all variables in the front.
Now: Is this illegal input or should the normalisation be able to take care of that?

/cc @cocreature

agurfinkel commented 6 years ago

The competition format is very strict to simplify parsing for the most tools. You can see the details here: https://chc-comp.github.io/2018/format.html

Instead of forcing all benchmarks to follow the format (which might not be desirable in the long run), we have developed a normalization script based on Z3. The script is limited but simple. On these examples, it was not able to normalize the input into desired format.

Ideally, the normalizer would be fixed to work. In practice, however, it is unlikely that we will invest time in that right now. If you have normalized inputs, please commit them as well.

I also noticed that @pruemmer submitted a PR that normalized some of the inputs with Eldarica. This might be sufficient.

chc-comp / llreve-bench

Illegal clauses #2