diff options
| author |  rustanleino <unknown> | 2010-08-10 02:16:29 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-08-10 02:16:29 +0000 |
| commit | 554fb3a6780c412b81dc935835c2760e4cbe0b4d (patch) | |
| tree | b50aa3dbbb369a52751bfcb9f142c9c928e591ae /Binaries | |
| parent | c2aa0b56fce36a101c3bef7ce901b8f26dcb5f08 (diff) | |
Boogie: Added boolean code expressions (sans well-formedness checks on the input).
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/TypedUnivBackPred2.sx | 4 | ||||
| -rw-r--r-- | Binaries/UnivBackPred2.sx | 2 |
2 files changed, 6 insertions, 0 deletions
diff --git a/Binaries/TypedUnivBackPred2.sx b/Binaries/TypedUnivBackPred2.sx index 5ee200f1..450e658a 100644 --- a/Binaries/TypedUnivBackPred2.sx +++ b/Binaries/TypedUnivBackPred2.sx @@ -10,6 +10,8 @@ (DEFOP <: U U $bool) ; used for translation with type premisses
(DEFOP <:: T U U $bool) ; used for translation with type arguments
+(DEFOP tickleBool $bool $bool) ; used in triggers to exhaustively instantiate quantifiers over booleans
+
(BG_PUSH (AND
; false is not true
@@ -126,6 +128,8 @@ ; Reflect plus
(FORALL (a b) (PATS (Reflect$Add a b)) (EQ (Reflect$Add a b) (+ a b)))
+ (tickleBool FALSE)
+ (tickleBool TRUE)
)) ;; AND, BG_PUSH
; End Boogie universal background predicate
; -------------------------------------------------------------------------
diff --git a/Binaries/UnivBackPred2.sx b/Binaries/UnivBackPred2.sx index 7c3dac8e..7e30017b 100644 --- a/Binaries/UnivBackPred2.sx +++ b/Binaries/UnivBackPred2.sx @@ -80,6 +80,8 @@ ; Reflect plus
(FORALL (a b) (PATS (Reflect$Add a b)) (EQ (Reflect$Add a b) (+ a b)))
+ (EQ (tickleBool |@false|) |@true|)
+ (EQ (tickleBool |@true|) |@true|)
)) ;; AND, BG_PUSH
; End Boogie universal background predicate
; -------------------------------------------------------------------------
|