test/regress/regress0/fmf/quant_real_univ.cvc


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

% EXPECT: sat
OPTION "fmf-bound";
OPTION "sets-ext";
Atom : TYPE;
REAL_UNIVERSE : SET OF [REAL];
ATOM_UNIVERSE : SET OF [Atom];
ASSERT REAL_UNIVERSE = UNIVERSE :: SET OF [REAL];
ASSERT ATOM_UNIVERSE = UNIVERSE :: SET OF [Atom];

levelVal : SET OF [Atom, REAL];
ASSERT FORALL (s : Atom, v1, v2 : REAL) : 
			(TUPLE(s) IS_IN ATOM_UNIVERSE AND TUPLE(v1) IS_IN REAL_UNIVERSE AND TUPLE(v2) IS_IN REAL_UNIVERSE) 
			=> (((s, v1) IS_IN levelVal AND (s, v2) IS_IN levelVal) => (v1 = v2));

CHECKSAT;