Skip to content

Commit

Permalink
updated answers
Browse files Browse the repository at this point in the history
  • Loading branch information
@pruemmer
pruemmer committed Aug 27, 2024
1 parent e88e9b4 commit ceeddef
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 5 deletions.
2 changes: 1 addition & 1 deletion regression-tests/horn-adt/Answers
View file
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ sat
de-brujin-bug.smt2
sat
(define-fun mmin ((A f)) Bool (= (h 0 g) A))
(define-fun n ((A f)) Bool (or (or (and (and (= (_size A) (_size g)) (= (_size e) 1)) (>= (_size g) 1)) (and (and (and (is-b e) (= (_size e) 3)) (and (>= (_size A) 1) (>= (_size g) 1))) (is-b e))) (and (and (and (is-b e) (and (and (and (and (or (and (is-g A) (>= (_size e) 4)) (and (is-h A) (>= (_size e) 5))) (or (and (is-g A) (>= (_size e) 5)) (and (is-h A) (>= (_size e) 4)))) (>= (+ (_size A) (_size e)) 6)) (>= (_size A) 1)) (>= (_size g) 1))) (is-b e)) (= (mod (+ 1 (_size e)) 2) 0))))
(define-fun n ((A f)) Bool (= (_size A) 1))
(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 (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) (_size B)) 6)) (>= (_size A) 1)) (>= (_size C) 1))) (is-b B)) (= (mod (+ 1 (_size B)) 2) 0))))

list-synasc-unsat.smt2
Expand Down
8 changes: 4 additions & 4 deletions regression-tests/horn-arrays/Answers
View file
Original file line number Diff line number Diff line change
Expand Up @@ -224,8 +224,8 @@ sat
(define-fun preds0 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool (= A 1))
(define-fun preds1 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (= A 1) (or (= D 0) (and (= D 1) (= (select C 0) (select B 0))))))
(define-fun preds2 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (or (= D 0) (and (= D 1) (= (select C 0) (select B 0))))) (= 1 A)))
(define-fun preds3 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (exists ((var0 (Array Int Int))) (= (store var0 D 1) B)) (and (<= D 0) (= D 0))) (exists ((var0 (Array Int Int))) (and (= (store var0 D 1) B) (and (<= D 0) (and (= D 1) (= (select C 0) (select var0 0))))))) (= 1 A)))
(define-fun preds4 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (exists ((var0 (Array Int Int))) (= (store var0 D 1) C)) (and (exists ((var0 (Array Int Int))) (= (store var0 D 1) B)) (and (<= D 0) (= D 0)))) (exists ((var0 (Array Int Int))) (and (= (store var0 D 1) C) (exists ((var1 (Array Int Int))) (and (= (store var1 D 1) B) (and (<= D 0) (and (= D 1) (= (select var0 0) (select var1 0))))))))) (= 1 A)))
(define-fun preds3 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select B D) 1) (and (<= D 0) (= D 0))) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= 0 D) (= (select C 0) (select B 0))))))) (= 1 A)))
(define-fun preds4 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (= D 0)))) (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (= 0 D))))) (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= 0 D) (= (select C 0) (select B 0))))))))) (= 1 A)))
(define-fun preds5 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool (and (= (select C 0) (select B 0)) (= 1 A)))
(define-fun preds6 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (= A 1) (and (and (<= D 1) (>= D 0)) (= (select C 0) (select B 0)))))
(define-fun preds7 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (and (and (<= D 1) (>= D 0)) (= (select C 0) (select B 0)))) (= 1 A)))
Expand Down Expand Up @@ -294,8 +294,8 @@ sat
(define-fun preds0 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool (= A 1))
(define-fun preds1 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (= A 1) (or (= D 0) (and (= D 1) (= (select C 0) (select B 0))))))
(define-fun preds2 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (or (= D 0) (and (= D 1) (= (select C 0) (select B 0))))) (= 1 A)))
(define-fun preds3 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (exists ((var0 (Array Int Int))) (= (store var0 D 1) B)) (and (<= D 0) (= D 0))) (exists ((var0 (Array Int Int))) (and (= (store var0 D 1) B) (and (<= D 0) (and (= D 1) (= (select C 0) (select var0 0))))))) (= 1 A)))
(define-fun preds4 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (exists ((var0 (Array Int Int))) (= (store var0 D 1) C)) (and (exists ((var0 (Array Int Int))) (= (store var0 D 1) B)) (and (<= D 0) (= D 0)))) (exists ((var0 (Array Int Int))) (and (= (store var0 D 1) C) (exists ((var1 (Array Int Int))) (and (= (store var1 D 1) B) (and (<= D 0) (and (= D 1) (= (select var0 0) (select var1 0))))))))) (= 1 A)))
(define-fun preds3 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select B D) 1) (and (<= D 0) (= D 0))) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= 0 D) (= (select C 0) (select B 0))))))) (= 1 A)))
(define-fun preds4 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (= D 0)))) (or (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (= 0 D))))) (and (= (select C D) 1) (and (= (select B D) 1) (and (<= D 0) (and (= D 1) (or (= 0 D) (= (select C 0) (select B 0))))))))) (= 1 A)))
(define-fun preds5 ((A Int) (B (Array Int Int)) (C (Array Int Int))) Bool (and (= (select C 0) (select B 0)) (= 1 A)))
(define-fun preds6 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (= A 1) (and (and (<= D 1) (>= D 0)) (= (select C 0) (select B 0)))))
(define-fun preds7 ((A Int) (B (Array Int Int)) (C (Array Int Int)) (D Int)) Bool (and (and (<= D 0) (and (and (<= D 1) (>= D 0)) (= (select C 0) (select B 0)))) (= 1 A)))
Expand Down

0 comments on commit ceeddef

Please sign in to comment.