Incorrect model

[AnzhelaSukhanova]

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.

[hgvk94]

I am working on fixing #5882. Looks like inlined predicates are interpreted as the least model whereas all the predicates that reach Spacer are interpreted as True. The interpretation for each predicate can be extended to a model, but they can't be combined as is.

[NikolajBjorner]

Have you tried changes like this:

@@ -449,7 +449,7 @@ namespace datalog {
             }
         }
         if (modified) {
-            datalog::del_rule(m_mc, *r0, l_false);
+            datalog::del_rule(m_mc, *r0, l_undef);
         }
 
         return modified;
@@ -568,7 +568,7 @@ namespace datalog {
                 goto process_next_tail;
             }
             if (!try_to_inline_rule(*r, *inlining_candidate, ti, res)) {
-                datalog::del_rule(m_mc, *r, l_false);
+                datalog::del_rule(m_mc, *r, l_undef);
                 res = nullptr;
             }
             return true;

It is unlikely to really address the core issues, but the calls to del_rule with l_true/l_false are not well motivated in the inliner.
A more serious analysis will be useful. The transformations can be justified as inferences with corresponding model transformations.

             r: B => P(x),   there is no clause B' => Q(x) in H such that P(y) in B' and B & B' & P(x)  & x = y is satisfiable
             ----------------------------------------------
             remove r from H, add B => P(x) to model trail.

then for model reconstruction given a model M for P, Q, R and B => P(x) in the model trail
the model for P(x) has to be updated to satisfy B => P(x).
The simplest way to update the model for P is by adding the interpretation for B as a disjunction to P.
It isn't clear this is generally correct, though. Suppose P occurs in B. Then just adding a single unfolding isn't sound.
Example, P has two arguments, and the rule is P(x, y), x = false, y =< 0, y' = y - 1 => P(x, y'), while the other rules that contain P in their bodies are of the form P(true, y),
If we augment the interpretation of P(x, y) := y = 0 by substituting it into the body and x = false, y <= 0, y' = y - 1 we get the interpretation P(x,y) := y = 0 or y = -1. The satisfying interpretation is P(x,y) := y <= 0.

So patching the model reconstruction code may be possible for some bugs, it should be hitting some more serious limitations where we don't already have the mechanisms to address them.

[hgvk94]

Yes, changing the 3rd argument to del_rule solves #5882. Probably #5887 and #5880 can be fixed with similar changes, which I am confident I can patch up.

I tried to go deeper and got stuck immediately. Right now, we are assigning interpretations to specific predicates before actually solving the CHCs. This causes problems when the interpretations are put together to get a model. I couldn't think of an easy way out. So I guess I will just put a comment. I will submit a PR shortly.

[hgvk94]

I think the problem is with the inlining step:

-------- [dl] apply src/muz/transforms/dl_mk_rule_inliner.cpp:122 ---------
tgt (0): 
<null>:
P1(#1,#2,#0) :- 
 P3(#1,#2,#0).
src:
<null>;<null>:
P3(#0,#0,1) :- 
 P1(#0,#1,#2).
res
<null>;<null>;<null>:
P1(#0,#0,1) :- 
 P1(#0,#1,#2).

After which we

Replace <null>:
P1(#1,#2,#0) :- 
P3(#1,#2,#0).
with <null>;<null>;<null>:
P1(#0,#0,1) :- 
P1(#0,#1,#2).

Not sure how to reconstruct models after such a replacement.

[NikolajBjorner]

In this case it should be that the model for P3 is determined by src.
As hinted at in the comment above, I don't think the general strategy for model repair is on a sound footing.
Maybe some special cases can be worked out, but it is better done on the drawing board.

[NikolajBjorner]

Maybe "drawing board" = "a solid honor's thesis".
The transformations take various shortcuts with batching, topological sorting, so a simple code review isn't going to give reasonable confidence in the model transformations.
Some inlining rules allow to add the removed Horn clause to the model reconstruction trail.
For other rules it works to just add the constraints to the reconstruction trail (not the predicates).

[NikolajBjorner]

#5920