Eldarica returns inconsistent result

Question

Eldarica returns inconsistent result

Closed this issue 4 months ago · 3 comments

Hello everyone,

eldarica's behavior for the following code seems inconsistent to me:

( declare-datatypes ( ( f 0 ) ) ( ( ( g ) ( h ( i Int ) ( j f ) ) ) ) )
( declare-datatypes ( ( d1 0 ) ) ( ( ( b ( c d1 ) ( d1 d1 ) ) ( e ) ) ) )
( declare-fun n ( f ) Bool )
( declare-fun mmin ( f ) Bool )
( declare-fun p ( f d1 f ) Bool )
( assert ( forall ( ( q f ) ) ( => ( and ( mmin q ) ( n q ) ) false ) ) )
( assert ( forall ( ( s f ) ( w d1 ) ( y d1 ) ( z f ) ) ( => ( and ( p s w s ) ( p z y z ) ) ( p s ( b w y ) z ) ) ) )
( assert ( forall ( ( q f ) ) ( p q e q ) ) )
( assert ( forall ( ( q f ) ) ( => ( p q e g ) ( n q ) ) ) )
( assert ( mmin ( h 0 g ) ) )
(check-sat)

If I execute
~/eldarica/eld -assert -ssol test.smt2
eldarica returns SAT + a model (which differs however non-deterministically).
If I now replace the predicate declaration for p with the model definition returned by eldarica:

( declare-datatypes ( ( f 0 ) ) ( ( ( g ) ( h ( i Int ) ( j f ) ) ) ) )
( declare-datatypes ( ( d1 0 ) ) ( ( ( b ( c d1 ) ( d1 d1 ) ) ( e ) ) ) )
( declare-fun n ( f ) Bool )
( declare-fun mmin ( f ) Bool )
(define-fun p ((A f) (B d1) (C f)) Bool (or (or (and (and (= (_size A) (_size C)) (= (_size B) 1)) (>= (_size C) 1)) (and (and (and (is-b B) (= (_size B) 3)) (and (>= (_size A) 1) (>= (_size C) 1))) (is-b B))) (and (and (and (is-b B) (and (and (and (or (and (is-g A) (>= (_size B) 4)) (and (is-h A) (>= (+ (- 1) (_size B)) 4))) (or (and (is-g A) (>= (_size B) 5)) (and (is-h A) (>= (+ 1 (_size B)) 5)))) (>= (_size A) 1)) (>= (_size C) 1))) (is-b B)) (= (mod (+ 1 (_size C)) 2) 0))))
( assert ( forall ( ( q f ) ) ( => ( and ( mmin q ) ( n q ) ) false ) ) )
( assert ( forall ( ( s f ) ( w d1 ) ( y d1 ) ( z f ) ) ( => ( and ( p s w s ) ( p z y z ) ) ( p s ( b w y ) z ) ) ) )
( assert ( forall ( ( q f ) ) ( p q e q ) ) )
( assert ( forall ( ( q f ) ) ( => ( p q e g ) ( n q ) ) ) )
( assert ( mmin ( h 0 g ) ) )
(check-sat)

and execute eldarica with the same command as above on this code, I get "unsat".
Is the model invalid even though debug assertions are enabled?

Answer 1 · 2024-08-26T10:53:05.000Z

In the meantime I have been able to minimize the returned model (the set of assertions is already minimized):

(define-fun p ((A f) (B d1) (C f)) Bool
    (or (and (= (_size A) (_size C)) (= (_size B) 1))
        (= (_size B) 3)
        (and 
             (>= (_size B) 5)
             (= (mod (+ 1 (_size C)) 2) 0))) )

This should be logically equivalent to the definition of p in my previous report. Eldarica can even prove that.
Maybe this helps for debugging.

Answer 2 · 2024-08-26T16:22:25.000Z

Great catch! This was really a bug of the translation to SMT-LIB; the internal solution was correct, but in the pretty-printing some de Brujin indexes were handled incorrectly, resulting in (_size C) instead of (_size B) being printed in the last line. This should be fixed in the latest version.

Answer 3 · 2024-08-27T08:48:57.000Z

Thanks for checking and fixing