UnsupportedOperationException for one/lone quantifiers

[philippemerle]

Describe the bug

UnsupportedOperationException is thrown when executing the following Alloy specification:
sig A { id: Int }
pred P1 [p : set A]
{
one a: p | a.id = 1
}
pred P2[p : set A] {
P1[ { x : p | x.id > 0 } ]
}
run {
some a : set A | P2[a]
}

If one is replaced by lone then the exception is also thrown.
If one is replaced by no/some/all then no exception is thrown.

To Reproduce

Expected behavior

Screenshots

Desktop (please complete the following information):

Smartphone (please complete the following information):

Additional context

Issue copied from philippemerle#5

[mudathirmahgoub]

The Java exception is fixed in master. However there is still a problem with this alloy model. There is a comprehension expression in predicate P2 with one free variable p. This forces the translator to universally quantify over sets of uninterpreted infinite type.
CVC4 does not have strong support for quantification over sets of infinite type. It returns unknown answer for the following:

(set-logic ALL)
(set-option :tlimit 0)
(set-option :produce-unsat-cores false)
(set-option :block-models literals)
(set-option :finite-model-find true)
(set-option :produce-models true)
(set-option :incremental true)
(set-option :sets-ext true)
(declare-sort Atom 0)
(assert
 (forall ((S (Set (Tuple Atom))))
  (= (as emptyset (Set (Tuple Atom))) S)
 )
)
(check-sat)
(get-model)

For the given alloy model, the comprehension in P2 can be avoided in several ways. One way is to introduce an auxiliary field to signature A as follows:

sig A { id: Int, g: Int }
fact 
{
   -- g is the same as id except non positive values
   all x: A, y: Int | 
	(x-> y in id and y > 0) <=> (x->y in g)
}
pred P1 [p : set A]
{
all a: p | a.id = 1
}
pred P2[p : set A] {
P1[ p &(g.Int) ]
}
run {
some a : set A | #a >= 2 and P2[a]
}

This version can be solved by CVC4.