search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.4k stars 1.47k forks source link

Issues with models of Horn clauses #5920

Open NikolajBjorner opened 2 years ago

NikolajBjorner commented 2 years ago

This issue collects several separate filings. They are all or mostly related to rule in-lining and model transformation.

There are comments associated with closed issues that can give more information. The work required to close these issues is beyond basic bug fixing and will require planning. At this point it seems more productive to spend efforts developing the appropriate theory for fixing this.

The high level:

Preprocessing transformations add and delete Horn clauses. The (addition and) deletion can be tracked in a trail such that a model for the transformed Horn clauses is translated to a model of the original clauses. There are some different cases for when Horn clauses are deleted. The rules for fixing models depend on the cases and should be worked out clearly. The code for inlining also performs some shortcuts (topological sorting) and the rules for fixing models have to consider this.

It is worth writing a paper on and then changing/overhauling the code. It is probably less useful to poke at more bugs: models can be checked and if they fail, then disable the transformation rules that don't record model reconstruction. The overall soundness of SAT vs. UNSAT seems not be at stake.

NikolajBjorner commented 2 years ago

Hello!

For the instance

(set-logic HORN)

(declare-fun P1 (Int  Bool) Bool)
(declare-fun P2 (Int  Bool) Bool)
(declare-fun P3 (Int  Int) Bool)
(declare-fun P4 (Int) Bool)
(declare-fun P5 (Int) Bool)
(declare-fun P6 (Int  Int) Bool)
(declare-fun P7 (Int  Int  Int  Int) Bool)
(declare-fun P8 (Int  Int) Bool)
(declare-fun P9 (Int) Bool)

(assert (forall ((v1 Int) (v2 Bool))
  (=> (and (P4 v1) v2) (P1 v1 v2))))

(assert (forall ((v1 Int) (v2 Int) (v3 Int) (v4 Bool))
  (=> (and (P2 v3 v4) (= (+ 1 v1) v2) (>= v2 1))
      (P4 v1))))

(assert (forall ((v1 Int) (v2 Bool) (v3 Int))
  (=> (and (P8 3 v3) (= v2 (>= v1 0)))
      (P2 v1 v2))))

(assert (forall ((v1 Int) (v2 Int))
  (=> (and (P4 v1)) (P3 v1 v2))))

(assert (forall ((v1 Int)) (=> (P8 3 v1) (P4 v1))))

(assert (forall ((v1 Int) (v2 Int) (v3 Int))
  (=> (and (P5 v3)) (P8 v1 v2))))

(assert (forall ((v1 Int))
  (=> (P6 0 v1) (P5 v1))))

(assert (forall ((v1 Int) (v2 Int) (v3 Int) (v4 Int))
  (=> (and (P7 v4 0 v1 v2)
           (P9 v4)
           (= (+ 1 v3) v4)
           (<= 1 v4))
      (P6 v1 v2))))

(assert (forall ((v1 Int) (v2 Int) (v3 Int) (v4 Int))
  (=> (and (= v2 1)) (P7 v1 v2 v3 v4))))

(assert (forall ((v1 Int) (v2 Int))
  (=> (and (P9 v1) (<= v1 0)) (P8 v1 v2))))

(assert (forall ((v1 Int) (v2 Int)) (=> (and (>= v2 1)) (P9 v1))))

(assert (forall ((v1 Int)) (=> (= v1 3) (P9 v1))))

(check-sat)
(get-model)
(exit)

z3 returns

sat
(
  (define-fun P8 ((x!0 Int) (x!1 Int)) Bool
    true)
  (define-fun P5 ((x!0 Int)) Bool
    false)
  (define-fun P4 ((x!0 Int)) Bool
    (exists ((x!1 Int) (x!2 Int) (x!3 Bool))
      (! (and (= x!3 (>= x!2 0)) (>= x!1 1) (= x!0 (+ (- 1) x!1))) :weight 0)))
  (define-fun P1 ((x!0 Int) (x!1 Bool)) Bool
    false)
  (define-fun P7 ((x!0 Int) (x!1 Int) (x!2 Int) (x!3 Int)) Bool
    (= x!1 1))
  (define-fun P2 ((x!0 Int) (x!1 Bool)) Bool
    (= x!1 (>= x!0 0)))
  (define-fun P6 ((x!0 Int) (x!1 Int)) Bool
    false)
  (define-fun P3 ((x!0 Int) (x!1 Int)) Bool
    (exists ((x!2 Int) (x!3 Int) (x!4 Bool))
      (! (and (= x!4 (>= x!3 0)) (>= x!2 1) (= x!0 (+ (- 1) x!2))) :weight 0)))
  (define-fun P9 ((x!0 Int)) Bool
    true)
)

In this interpretation the first clause is equivalent to the implication true => false if v2 is true and v1 >= 0.

NikolajBjorner commented 2 years ago

Hello, For the instance

(set-logic HORN)

(declare-fun P1 (Int Int Int) Bool)

(declare-fun P2 (Int) Bool)

(declare-fun P3 (Int Int Int) Bool)

(declare-fun P4 (Int Int Int Int Int Int Int) Bool)

(declare-fun P5 (Int Int Int) Bool)

(assert (forall ((v1 Int) (v2 Int) (v3 Int))
  (=> (and (P5 v3 v2 v1))
      (P3 v3 v2 v1))))

(assert (forall ((v1 Int) (v2 Int) (v3 Int) (v4 Int)
                 (v5 Int) (v6 Int) (v7 Int) (v8 Int))
  (let ((a!1 (= (not (= 0 v7)) (and (not (= 0 v6))))))
  (let ((a!2 (and a!1
                  (= (not (= 0 v6)) (>= v5 0))
                  (= v5 (+ v4))
                  (= v4 v3)
                  (not (not (= 0 v7)))
                  (P5 v3 v2 v1))))
    (=> a!2 (P2 v8))))))

(assert (forall ((v1 Int) (v2 Int) (v3 Int))
  (let ((a!1 (and (not (not (= 0 v1)))
                  (P5 v3 v2 v1))))
    (=> a!1
        (P3 v3 v2 v1)))))

(assert (forall ((v1 Int) (v2 Int) (v3 Int) (v4 Int)
                 (v5 Int) (v6 Int) (v7 Int))
  (=> (and (P3 v2 v1 v7))
      (P4 v6 v5 v4 v3 v2 v1 v7))))

(assert (forall ((v1 Int) (v2 Int) (v3 Int))
  (=> (and (P3 v2 v1 v3))
      (P1 v2 v1 v3))))

(assert (forall ((v1 Int) (v2 Int) (v3 Int) (v4 Int) (v5 Int))
  (=> (and (= v5 v3)
           (= v4 1)
           (P1 v3 v2 v1))
      (P5 v5 v3 v4))))

(assert (not (exists ((v1 Int))
       (and (P2 v1)))))

(assert (forall ((v1 Int) (v2 Int) (v3 Int) (v4 Int) (v5 Int))
  (let ((a!1 (= (not (= 0 v5)) (and (not (= 0 v4))))))
  (let ((a!2 (and a!1
                  (= (not (= 0 v4)) (>= v1 0))
                  (not (= 0 v5)))))
    (=> a!2
        (P1 v1 v3 v2))))))

(check-sat)
(get-model)
(exit)

z3 returns

sat
(
  (define-fun P3 ((x!0 Int) (x!1 Int) (x!2 Int)) Bool
    true)
  (define-fun P4 ((x!0 Int)
   (x!1 Int)
   (x!2 Int)
   (x!3 Int)
   (x!4 Int)
   (x!5 Int)
   (x!6 Int)) Bool
    true)
  (define-fun P2 ((x!0 Int)) Bool
    false)
  (define-fun P1 ((x!0 Int) (x!1 Int) (x!2 Int)) Bool
    (>= x!0 0))
  (define-fun P5 ((x!0 Int) (x!1 Int) (x!2 Int)) Bool
    (and (>= x!0 0) (= x!1 x!0) (= x!2 1)))
)

If v2 < 0 in the fifth clause, this interpretation is incorrect.

NikolajBjorner commented 2 years ago

Hello, For instance

(set-logic HORN)

(declare-fun P (Int) Bool)
(declare-fun Q (Bool  Int  Int  Bool  Int  Int) Bool)
(declare-fun R (Bool  Int  Int) Bool)

(assert (not (exists ((v1 Int)) (P v1))))

(assert (forall ((v1 Int) (v2 Int) (v3 Bool)
                 (v4 Int) (v5 Int) (v6 Int))
  (=> (and (Q v3 v4 v2 true v5 v6)
           (>= v2 1))
      (P v1))))

(assert (forall ((v1 Bool) (v2 Int) (v3 Int) (v4 Bool) (v5 Int)
                 (v6 Int) (v7 Int) (v8 Bool) (v9 Int) (v10 Int))
  (=> (and (Q v8 v9 v7 v1 v2 v10)
           (= (+ 1 v3) v7)
           (>= v7 1)
           (= v5 v2)
           (not v1)
           (not v4))
      (Q v1 v2 v3 v4 v5 v6))))

(assert (forall ((v1 Bool) (v2 Int) (v3 Int) (v4 Int)
         (v5 Bool) (v6 Int) (v7 Int))
  (=> (and (R v5 v6 v4)
           (Q v5 v6 v4 v1 v2 v7)
           (>= v4 1)
           (= (+ 1 v3) v4)
           (not v1))
      (R v1 v2 v3))))

(assert (forall ((v1 Bool) (v2 Int) (v3 Int) (v5 Bool) (v6 Int) (v7 Int))
  (=> (and (not v5))
      (Q v1 v2 v3 v5 v6 v7))))

(assert (forall ((v1 Bool) (v2 Int) (v3 Int))
  (=> (and (not v1)) 
      (R v1 v2 v3))))

(check-sat)
(get-model)
(exit)

z3 returns

sat
(
  (define-fun P ((x!0 Int)) Bool
    (exists ((x!1 Int)) (! (>= x!1 1) :weight 0)))
  (define-fun R ((x!0 Bool) (x!1 Int) (x!2 Int)) Bool
    true)
  (define-fun Q ((x!0 Bool) (x!1 Int) (x!2 Int) (x!3 Bool) (x!4 Int) (x!5 Int)) Bool
    true)
)

This interpretation is incorrect for the first clause.

NikolajBjorner commented 2 years ago

Hello!

For the instance

(set-logic HORN)

(set-option :fp.xform.inline_linear_branch true)
(set-option :fp.xform.inline_eager false)

(declare-fun P1 (Int Int) Bool)
(declare-fun P2 (Int Int Int) Bool)
(declare-fun P3 (Int) Bool)
(declare-fun P4 (Int Int) Bool)

(assert (forall ((v1 Int) (v2 Int))
  (=> (and (P4 v1 v2))
      (P3 v1))))

(assert (forall ((v1 Int) (v2 Int))
  (=> (and (= v2 0)) (P4 v2 v1))))

(assert (forall ((v1 Int) (v2 Int) (v3 Int))
  (=> (and (P1 v1 v3) (P4 v3 v2))
      (P2 v1 v3 v2))))

(assert (forall ((v1 Int) (v2 Int))
  (=> (and (P3 v2))
      (P1 v1 v2))))

(check-sat)
(get-model)
(exit)

z3 returns

sat
(
  (define-fun P3 ((x!0 Int)) Bool
    (= x!0 0))
  (define-fun P1 ((x!0 Int) (x!1 Int)) Bool
    true)
  (define-fun P4 ((x!0 Int) (x!1 Int)) Bool
    true)
  (define-fun P2 ((x!0 Int) (x!1 Int) (x!2 Int)) Bool
    true)
)

If in the first clause v1 != 0, this interpretation is incorrect. With fp.xform.inline_eager in true or fp.xform.inline_linear_branch in false, z3 returns correct model.

In this case, P3 is in-lined by the clause for P4 (v2 = 0). But P4 is sent to SPACER and set to true. SPACER does not see P3 or the dependency of P3 on P4. Unclear if a "simple" patch is possible based on the implementation. The model transformer has to ensure that when deleting a rule P3(x) :- P4(x,y), then the interpretation for P3 should contain P4. It deletes the rule without ensuring this, it just in-lines P3(x) :- x = 0. And then ensures that P3(x) contains at least x = 0. At this point, it serves possibly better as a use case for developing a formal account for model reconstruction than pointing to something immediately actionable in the code (because model reconstruction there was an after-thought I don't think it is the best idea to keep patching it). In principle, model reconstruction takes a trail of deleted and added Horn rules and updates the interpretation for predicates in the head. In practice, all deleted rules have to be tracked correctly and rules that involve recursion would need to be accounted for. Shortcuts may be possible if predicates are guaranteed to be unreachable and therefore can be interpreted as "true".