diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/refcount24.cvc')
-rw-r--r-- | test/regress/regress0/quantifiers/refcount24.cvc | 112 |
1 files changed, 0 insertions, 112 deletions
diff --git a/test/regress/regress0/quantifiers/refcount24.cvc b/test/regress/regress0/quantifiers/refcount24.cvc deleted file mode 100644 index 21c9a3cfe..000000000 --- a/test/regress/regress0/quantifiers/refcount24.cvc +++ /dev/null @@ -1,112 +0,0 @@ -% Preamble -------------- -DATATYPE UNIT = Unit END; -DATATYPE BOOL = Truth | Falsity END; - -% Decls -------------- -resource$type: TYPE; -process$type: TYPE; -null: resource$type; -S$elem$type: TYPE = process$type; -S$t$type: TYPE; -S$empty: S$t$type; -S$mem:(S$elem$type, S$t$type) -> BOOL; -S$add:(S$elem$type, S$t$type) -> S$t$type; -S$remove:(S$elem$type, S$t$type) -> S$t$type; -S$cardinality:(S$t$type) -> INT; -S$mem_empty: BOOLEAN = (FORALL (e: S$elem$type): (NOT ((S$mem((e), (S$empty))) = - (Truth)))); -ASSERT S$mem_empty; -S$mem_add: BOOLEAN = (FORALL (x: S$elem$type, y: S$elem$type, s: S$t$type): - ((S$mem((x), (S$add((y), (s))))) = (IF (((x) = (y)) OR - ((S$mem((x), (s))) = - (Truth))) THEN - (Truth) ELSE - (Falsity) ENDIF))); -ASSERT S$mem_add; -S$mem_remove: BOOLEAN = (FORALL (x: S$elem$type, y: S$elem$type, s: S$t$type): - ((S$mem((x), (S$remove((y), (s))))) = (IF ((NOT - ((x) = - (y))) AND - ((S$mem( - (x), (s))) = - (Truth))) THEN - (Truth) ELSE - (Falsity) ENDIF))); -ASSERT S$mem_remove; -S$card_empty: BOOLEAN = ((S$cardinality((S$empty))) = (0)); -ASSERT S$card_empty; -S$card_zero: BOOLEAN = (FORALL (s: S$t$type): (((S$cardinality((s))) = (0)) => - ((s) = (S$empty)))); -ASSERT S$card_zero; -S$card_non_negative: BOOLEAN = (FORALL (s: S$t$type): ((S$cardinality((s))) >= - (0))); -ASSERT S$card_non_negative; -S$card_add: BOOLEAN = (FORALL (x: S$elem$type, s: S$t$type): ((S$cardinality( - (S$add( - (x), (s))))) = - (IF ((S$mem( - (x), (s))) = - (Truth)) THEN - (S$cardinality( - (s))) ELSE ( - (S$cardinality( - (s))) + - (1)) ENDIF))); -ASSERT S$card_add; -S$card_remove: BOOLEAN = (FORALL (x: S$elem$type, s: S$t$type): ((S$cardinality( - (S$remove( - (x), (s))))) = - (IF ( - (S$mem( - (x), (s))) = - (Truth)) THEN ( - (S$cardinality( - (s))) - - (1)) ELSE - (S$cardinality( - (s))) ENDIF))); -ASSERT S$card_remove; - -% Var Decls -------------- -count: ARRAY resource$type OF INT; -ref: ARRAY process$type OF resource$type; -valid: ARRAY resource$type OF BOOL; -destroy$r: resource$type; -valid$1: ARRAY resource$type OF BOOL; - -% Asserts -------------- -ASSERT (NOT ((FORALL (p: process$type): ((NOT - ( - ( - (ref)[ - (p)]) = - (null))) => - (( - (valid)[ - ( - (ref)[ - (p)])]) = - (Truth)))) => - ((NOT ((destroy$r) = (null))) => - ((((valid)[(destroy$r)]) = (Truth)) => - ((((count)[(destroy$r)]) = (0)) => - (((valid$1) = ((valid) WITH [(destroy$r)] := - (Falsity))) => (FORALL - ( - p: process$type): - ( - (NOT - ( - ( - (ref)[ - (p)]) = - (null))) => - ( - ( - (valid$1)[ - ( - (ref)[ - (p)])]) = - (Truth)))))))))); - -CHECKSAT; |