slow check-sat with Array Int (Option (Set Int))

After trying to represent finite maps in Liquid Haskell with `Array Int (Option (Set Int))`, I arrived at an SMTLIB query that takes 16 seconds. This is the result of minimizing a query that takes hours. I guess I could use some help understanding why it takes so long, and whether there is something that could be done to speed it up.

Tested with z3 4.15.0 in nixos.

Slow version:
<details>

```
(set-option :smt.mbqi false)

(set-option :auto-config false)
(set-option :model true)
(declare-datatype Option (par (a) (None (Some (someVal a)))))
(declare-datatypes ((SubstFormula.Formula 0)) (((SubstFormula.Conj (SubstFormula.Conj$35$$35$lqdc$35$$35$$36$select$35$$35$SubstFormula.Conj$35$$35$1 SubstFormula.Formula) (SubstFormula.Conj$35$$35$lqdc$35$$35$$36$select$35$$35$SubstFormula.Conj$35$$35$2 SubstFormula.Formula)) (SubstFormula.Eq))))
(declare-datatypes ((State.State 2)) ((par (T0 T1) ((junk$35$$35$State.State (junk$35$$35$State.State$35$$35$0 T0) (junk$35$$35$State.State$35$$35$1 T1)) (State.State (lqdc$35$$35$$36$select$35$$35$State.State$35$$35$1 Int))))))
(declare-fun lq_anf$36$$35$$35$7205759403792799984$35$$35$d1EY () (State.State (Array Int (Option (Set Int))) SubstFormula.Formula))
(declare-fun x () SubstFormula.Formula)
(declare-fun w () (Array Int (Option (Set Int))))
(declare-fun f1$35$$35$a1D1 () SubstFormula.Formula)
(declare-fun SubstFormula.consistentScopes () Int)
(declare-fun sf$35$$35$a1D0 () (Array Int Bool))
(declare-fun SubstFormula.skolemize () Int)
(declare-fun ds_d1Ex () SubstFormula.Formula)

(push 1)
(declare-fun apply$35$$35$0 (Int SubstFormula.Formula) Bool)
(declare-fun apply$35$$35$1 (Int (Array Int (Option (Set Int)))) Int)
(declare-fun apply$35$$35$3 (Int (Array Int Bool)) Int)
(declare-fun apply$35$$35$2 (Int SubstFormula.Formula) (State.State (Array Int (Option (Set Int))) SubstFormula.Formula))
(define-fun b$36$$35$$35$110 () Bool (= lq_anf$36$$35$$35$7205759403792799984$35$$35$d1EY (apply$35$$35$2 (apply$35$$35$3 SubstFormula.skolemize sf$35$$35$a1D0) f1$35$$35$a1D1)))
(push 1)
(push 1)
(assert
  (and
    (exists ((VV$35$$35$1 (Array Int (Option (Set Int)))))
      (and
        (= ((as const (Array Int Bool)) true) ((_ map =>) sf$35$$35$a1D0 ((as const (Array Int Bool)) false)))
        (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$1) ds_d1Ex)
      )
    )
  (exists ((lq_karg$36$lq_tmp$36$x$35$$35$1124$35$$35$k_$35$$35$1122 SubstFormula.Formula))
    (and
      (= lq_karg$36$lq_tmp$36$x$35$$35$1124$35$$35$k_$35$$35$1122 x)
      (exists ((lq_tmp$36$x$35$$35$1124 SubstFormula.Formula) (VV$35$$35$19 (Array Int (Option (Set Int)))))
        (and
          (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$19) lq_tmp$36$x$35$$35$1124)
          (= lq_karg$36$lq_tmp$36$x$35$$35$1124$35$$35$k_$35$$35$1122 lq_tmp$36$x$35$$35$1124)
        )
      )
    )
  )
  (exists ((lq_tmp$36$x$35$$35$1027 SubstFormula.Formula) (VV$35$$35$55 (Array Int (Option (Set Int)))))
    (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$55) lq_tmp$36$x$35$$35$1027)
  )
  (exists ((lq_tmp$36$x$35$$35$1124 SubstFormula.Formula) (VV$35$$35$19 (Array Int (Option (Set Int)))))
    (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$19) lq_tmp$36$x$35$$35$1124)
  )
  (exists ((lq_karg$36$lq_tmp$36$x$35$$35$1124$35$$35$k_$35$$35$1122 SubstFormula.Formula))
    (exists ((lq_tmp$36$x$35$$35$1124 SubstFormula.Formula) (VV$35$$35$19 (Array Int (Option (Set Int)))))
      (and
        (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$19) lq_tmp$36$x$35$$35$1124)
        (= lq_karg$36$lq_tmp$36$x$35$$35$1124$35$$35$k_$35$$35$1122 lq_tmp$36$x$35$$35$1124)
      )
    )
  )
  (exists ((VV$35$$35$1 (Array Int (Option (Set Int)))))
    (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$1) ds_d1Ex)
  )
  (exists ((lq_karg$36$VV$35$$35$1121$35$$35$k_$35$$35$1122 (Array Int (Option (Set Int)))))
    (exists ((lq_tmp$36$x$35$$35$1124 SubstFormula.Formula) (VV$35$$35$19 (Array Int (Option (Set Int)))))
      (and
        (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$19) lq_tmp$36$x$35$$35$1124)
        (= lq_karg$36$VV$35$$35$1121$35$$35$k_$35$$35$1122 VV$35$$35$19)
      )
    )
  )
  (exists ((lq_karg$36$lq_tmp$36$x$35$$35$1027$35$$35$k_$35$$35$1025 SubstFormula.Formula))
    (exists ((lq_tmp$36$x$35$$35$1027 SubstFormula.Formula) (VV$35$$35$55 (Array Int (Option (Set Int)))))
      (and
        (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$55) lq_tmp$36$x$35$$35$1027)
        (= lq_karg$36$lq_tmp$36$x$35$$35$1027$35$$35$k_$35$$35$1025 lq_tmp$36$x$35$$35$1027)
      )
    )
  )
  (exists ((lq_karg$36$VV$35$$35$1024$35$$35$k_$35$$35$1025 (Array Int (Option (Set Int)))))
    (exists ((lq_tmp$36$x$35$$35$1027 SubstFormula.Formula) (VV$35$$35$55 (Array Int (Option (Set Int)))))
      (and
        (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$55) lq_tmp$36$x$35$$35$1027)
        (= lq_karg$36$VV$35$$35$1024$35$$35$k_$35$$35$1025 VV$35$$35$55)
      )
    )
  )
  (exists ((lq_karg$36$VV$35$$35$1024$35$$35$k_$35$$35$1025 (Array Int (Option (Set Int)))) (lq_karg$36$lq_tmp$36$x$35$$35$1027$35$$35$k_$35$$35$1025 SubstFormula.Formula))
    (exists ((lq_tmp$36$x$35$$35$1027 SubstFormula.Formula) (VV$35$$35$55 (Array Int (Option (Set Int)))))
      (and
        (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$55) lq_tmp$36$x$35$$35$1027)
        (= lq_karg$36$VV$35$$35$1024$35$$35$k_$35$$35$1025 VV$35$$35$55)
        (= lq_karg$36$lq_tmp$36$x$35$$35$1027$35$$35$k_$35$$35$1025 lq_tmp$36$x$35$$35$1027)
      )
    )
  )
  (exists ((lq_karg$36$VV$35$$35$1121$35$$35$k_$35$$35$1122 (Array Int (Option (Set Int)))) (lq_karg$36$lq_tmp$36$x$35$$35$1124$35$$35$k_$35$$35$1122 SubstFormula.Formula))
    (exists ((lq_tmp$36$x$35$$35$1124 SubstFormula.Formula) (VV$35$$35$19 (Array Int (Option (Set Int)))))
      (and
        (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$19) lq_tmp$36$x$35$$35$1124)
        (= lq_karg$36$VV$35$$35$1121$35$$35$k_$35$$35$1122 VV$35$$35$19)
        (= lq_karg$36$lq_tmp$36$x$35$$35$1124$35$$35$k_$35$$35$1122 lq_tmp$36$x$35$$35$1124)
      )
    )
  )

  b$36$$35$$35$110
  )
)
(push 1)
(assert (not false))
(check-sat)
; SMT Says: Sat
(pop 1)
(pop 1)
(pop 1)
(pop 1)
```
</details>

The assertion has a few nested existentials of the form
```
(and
  ...
  (exists (a) (exists (b)) exp)
  (exists (c) (exists (d)) exp)
  ...
)
```
If I combine those as in
```
(and
  ...
  (exists (a b) exp)
  (exists (c d) exp)
  ...
)
```
then the test runs in 60 ms!

Fast version:

<details>

```

(set-option :smt.mbqi false)

(set-option :auto-config false)
(set-option :model true)
(declare-datatype Option (par (a) (None (Some (someVal a)))))
(declare-datatypes ((SubstFormula.Formula 0)) (((SubstFormula.Conj (SubstFormula.Conj$35$$35$lqdc$35$$35$$36$select$35$$35$SubstFormula.Conj$35$$35$1 SubstFormula.Formula) (SubstFormula.Conj$35$$35$lqdc$35$$35$$36$select$35$$35$SubstFormula.Conj$35$$35$2 SubstFormula.Formula)) (SubstFormula.Eq))))
(declare-datatypes ((State.State 2)) ((par (T0 T1) ((junk$35$$35$State.State (junk$35$$35$State.State$35$$35$0 T0) (junk$35$$35$State.State$35$$35$1 T1)) (State.State (lqdc$35$$35$$36$select$35$$35$State.State$35$$35$1 Int))))))
(declare-fun lq_anf$36$$35$$35$7205759403792799984$35$$35$d1EY () (State.State (Array Int (Option (Set Int))) SubstFormula.Formula))
(declare-fun x () SubstFormula.Formula)
(declare-fun w () (Array Int (Option (Set Int))))
(declare-fun f1$35$$35$a1D1 () SubstFormula.Formula)
(declare-fun SubstFormula.consistentScopes () Int)
(declare-fun sf$35$$35$a1D0 () (Array Int Bool))
(declare-fun SubstFormula.skolemize () Int)
(declare-fun ds_d1Ex () SubstFormula.Formula)

(push 1)
(declare-fun apply$35$$35$0 (Int SubstFormula.Formula) Bool)
(declare-fun apply$35$$35$1 (Int (Array Int (Option (Set Int)))) Int)
(declare-fun apply$35$$35$3 (Int (Array Int Bool)) Int)
(declare-fun apply$35$$35$2 (Int SubstFormula.Formula) (State.State (Array Int (Option (Set Int))) SubstFormula.Formula))
(define-fun b$36$$35$$35$110 () Bool (= lq_anf$36$$35$$35$7205759403792799984$35$$35$d1EY (apply$35$$35$2 (apply$35$$35$3 SubstFormula.skolemize sf$35$$35$a1D0) f1$35$$35$a1D1)))
(push 1)
(push 1)
(assert
  (and
    (exists ((VV$35$$35$1 (Array Int (Option (Set Int)))))
      (and
        (= ((as const (Array Int Bool)) true) ((_ map =>) sf$35$$35$a1D0 ((as const (Array Int Bool)) false)))
        (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$1) ds_d1Ex)
      )
    )
  (exists ((lq_karg$36$lq_tmp$36$x$35$$35$1124$35$$35$k_$35$$35$1122 SubstFormula.Formula))
    (and
      (= lq_karg$36$lq_tmp$36$x$35$$35$1124$35$$35$k_$35$$35$1122 x)
      (exists ((lq_tmp$36$x$35$$35$1124 SubstFormula.Formula) (VV$35$$35$19 (Array Int (Option (Set Int)))))
        (and
          (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$19) lq_tmp$36$x$35$$35$1124)
          (= lq_karg$36$lq_tmp$36$x$35$$35$1124$35$$35$k_$35$$35$1122 lq_tmp$36$x$35$$35$1124)
        )
      )
    )
  )
  (exists ((lq_tmp$36$x$35$$35$1027 SubstFormula.Formula) (VV$35$$35$55 (Array Int (Option (Set Int)))))
    (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$55) lq_tmp$36$x$35$$35$1027)
  )
  (exists ((lq_tmp$36$x$35$$35$1124 SubstFormula.Formula) (VV$35$$35$19 (Array Int (Option (Set Int)))))
    (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$19) lq_tmp$36$x$35$$35$1124)
  )
  (exists ((lq_karg$36$lq_tmp$36$x$35$$35$1124$35$$35$k_$35$$35$1122 SubstFormula.Formula) (lq_tmp$36$x$35$$35$1124 SubstFormula.Formula) (VV$35$$35$19 (Array Int (Option (Set Int)))))
    (and
      (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$19) lq_tmp$36$x$35$$35$1124)
      (= lq_karg$36$lq_tmp$36$x$35$$35$1124$35$$35$k_$35$$35$1122 lq_tmp$36$x$35$$35$1124)
    )
  )
  (exists ((VV$35$$35$1 (Array Int (Option (Set Int)))))
    (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$1) ds_d1Ex)
  )
  (exists ((lq_karg$36$VV$35$$35$1121$35$$35$k_$35$$35$1122 (Array Int (Option (Set Int)))) (lq_tmp$36$x$35$$35$1124 SubstFormula.Formula) (VV$35$$35$19 (Array Int (Option (Set Int)))))
    (and
      (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$19) lq_tmp$36$x$35$$35$1124)
      (= lq_karg$36$VV$35$$35$1121$35$$35$k_$35$$35$1122 VV$35$$35$19)
    )
  )
  (exists ((lq_karg$36$lq_tmp$36$x$35$$35$1027$35$$35$k_$35$$35$1025 SubstFormula.Formula) (lq_tmp$36$x$35$$35$1027 SubstFormula.Formula) (VV$35$$35$55 (Array Int (Option (Set Int)))))
    (and
      (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$55) lq_tmp$36$x$35$$35$1027)
      (= lq_karg$36$lq_tmp$36$x$35$$35$1027$35$$35$k_$35$$35$1025 lq_tmp$36$x$35$$35$1027)
    )
  )
  (exists ((lq_karg$36$VV$35$$35$1024$35$$35$k_$35$$35$1025 (Array Int (Option (Set Int)))) (lq_tmp$36$x$35$$35$1027 SubstFormula.Formula) (VV$35$$35$55 (Array Int (Option (Set Int)))))
    (and
      (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$55) lq_tmp$36$x$35$$35$1027)
      (= lq_karg$36$VV$35$$35$1024$35$$35$k_$35$$35$1025 VV$35$$35$55)
    )
  )
  (exists ((lq_karg$36$VV$35$$35$1024$35$$35$k_$35$$35$1025 (Array Int (Option (Set Int)))) (lq_karg$36$lq_tmp$36$x$35$$35$1027$35$$35$k_$35$$35$1025 SubstFormula.Formula) (lq_tmp$36$x$35$$35$1027 SubstFormula.Formula) (VV$35$$35$55 (Array Int (Option (Set Int)))))
    (and
      (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$55) lq_tmp$36$x$35$$35$1027)
      (= lq_karg$36$VV$35$$35$1024$35$$35$k_$35$$35$1025 VV$35$$35$55)
      (= lq_karg$36$lq_tmp$36$x$35$$35$1027$35$$35$k_$35$$35$1025 lq_tmp$36$x$35$$35$1027)
    )
  )
  (exists ((lq_karg$36$VV$35$$35$1121$35$$35$k_$35$$35$1122 (Array Int (Option (Set Int)))) (lq_karg$36$lq_tmp$36$x$35$$35$1124$35$$35$k_$35$$35$1122 SubstFormula.Formula) (lq_tmp$36$x$35$$35$1124 SubstFormula.Formula) (VV$35$$35$19 (Array Int (Option (Set Int)))))
    (and
      (apply$35$$35$0 (apply$35$$35$1 SubstFormula.consistentScopes VV$35$$35$19) lq_tmp$36$x$35$$35$1124)
      (= lq_karg$36$VV$35$$35$1121$35$$35$k_$35$$35$1122 VV$35$$35$19)
      (= lq_karg$36$lq_tmp$36$x$35$$35$1124$35$$35$k_$35$$35$1122 lq_tmp$36$x$35$$35$1124)
    )
  )

  b$36$$35$$35$110
  )
)
(push 1)
(assert (not false))
(check-sat)
; SMT Says: Sat
(pop 1)
(pop 1)
(pop 1)
(pop 1)
```
</details>

Looks like both variants should be equally fast to check.

A third variant that runs in 15 ms is to change the `Option` datatype as in
```diff
-(declare-datatype Option (par (a) (None (Some (someVal a)))))
+(declare-datatype Option (par (a) (None (Some (someVal Int)))))
```


Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

slow check-sat with Array Int (Option (Set Int)) #7770

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

slow check-sat with Array Int (Option (Set Int)) #7770

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions