diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/quantifiers/refcount24.cvc | 112 | ||||
| -rw-r--r-- | test/unit/theory/theory_engine_white.h | 3 |
2 files changed, 115 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/refcount24.cvc b/test/regress/regress0/quantifiers/refcount24.cvc new file mode 100644 index 000000000..21c9a3cfe --- /dev/null +++ b/test/regress/regress0/quantifiers/refcount24.cvc @@ -0,0 +1,112 @@ +% 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; diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index eb6e5eefb..2a176e3d9 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -75,6 +75,9 @@ class FakeOutputChannel : public OutputChannel { void setIncomplete() throw(AssertionException) { Unimplemented(); } + void handleUserAttribute( const char* attr, Theory* t ){ + Unimplemented(); + } };/* class FakeOutputChannel */ template<TheoryId theory> |