From 6d2d1c5060a9e99afbd14108f32f80a74493eaef Mon Sep 17 00:00:00 2001 From: Unknown Date: Thu, 4 Oct 2012 14:21:57 -0700 Subject: deleted unnecessary files --- Binaries/TypedUnivBackPred2.sx | 135 ----------------------------------------- Binaries/UnivBackPred2.sx | 87 -------------------------- 2 files changed, 222 deletions(-) delete mode 100644 Binaries/TypedUnivBackPred2.sx delete mode 100644 Binaries/UnivBackPred2.sx (limited to 'Binaries') diff --git a/Binaries/TypedUnivBackPred2.sx b/Binaries/TypedUnivBackPred2.sx deleted file mode 100644 index 450e658a..00000000 --- a/Binaries/TypedUnivBackPred2.sx +++ /dev/null @@ -1,135 +0,0 @@ -; ------------------------------------------------------------------------- -; Boogie 2 universal background predicate for Z3 (Simplify notation with types) -; Copyright (c) 2004-2009, Microsoft Corp. - -(DEFTYPE $int :BUILTIN Int) -(DEFTYPE $bool :BUILTIN bool) -(DEFTYPE U) -(DEFTYPE T) - -(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 - - (DISTINCT |@false| |@true|) - - ; we assume type correctness of the operations here - ; a-l>=0 ==> (v ++ w:l)[a:b] = v[a-l:b-l] - (FORALL (v lv w lw lvw a b) - (QID bv:e:c1) - (PATS ($bv_extract ($bv_concat v lv w lw) lvw a b)) - (IMPLIES - (>= (- a lw) 0) - (EQ ($bv_extract ($bv_concat v lv w lw) lvw a b) ($bv_extract v lv (- a lw) (- b lw))))) - - ; b<=l ==> (v ++ w:l)[a:b] = w[a:b] - (FORALL (v lv w lw lvw a b) - (QID bv:e:c2) - (PATS ($bv_extract ($bv_concat v lv w lw) lvw a b)) - (IMPLIES - (<= b lw) - (EQ ($bv_extract ($bv_concat v lv w lw) lvw a b) ($bv_extract w lw a b)))) - - ; v:l - ; a>=x || b<=y ==> (v[x:l] ++ w ++ v[0:y])[a:b] = v[a:b] - (FORALL (v lv x lxv w lw lwy y a b) - (QID bv:e:c3) - (PATS - ($bv_extract - ($bv_concat - ($bv_extract v lv x lv) lxv - ($bv_concat - w lw - ($bv_extract v lv 0 y) y) lwy) lv a b)) - (IMPLIES - (AND - (EQ lw (- x y)) - (EQ lxv (- lv x)) - (EQ lwy (+ w y)) - (OR (>= a x) (<= b y))) - (EQ - ($bv_extract - ($bv_concat - ($bv_extract v lv x lv) lxv - ($bv_concat - w lw - ($bv_extract v lv 0 y) y) lwy) lv a b) - ($bv_extract v lv a b)))) - - ; a>=x ==> (v[x:l] ++ w)[a:b] = v[a:b] - (FORALL (v lv x lxv w a b) - (QID bv:e:c4) - (PATS - ($bv_extract - ($bv_concat - ($bv_extract v lv x lv) lxv - w x) - lv a b)) - (IMPLIES - (AND - (EQ lxv (- lv x)) - (>= a x)) - (EQ - ($bv_extract - ($bv_concat - ($bv_extract v lv x lv) lxv - w x) - lv a b) - ($bv_extract v lv a b)))) - - (FORALL (v l) - (QID bv:e:0) - (PATS ($bv_extract v l 0 l)) - (EQ ($bv_extract v l 0 l) v)) - - (FORALL (n) - (QID bv:pow) - (PATS ($pow2 n)) - (IMPLIES (> n 0) (EQ ($pow2 n) (* 2 ($pow2 (- n 1)))))) - - (EQ ($pow2 0) 1) - - ; 0 <= v < 2^Y ==> 0bvX ++ v[0:Y] == v - (FORALL (v l a b) - (QID bv:e:pow) - (PATS ($bv_concat 0 b ($bv_extract v l 0 a) a)) - (IMPLIES - (AND - (<= 0 v) - (< v ($pow2 a)) - (EQ l (+ a b))) - (EQ ($bv_concat 0 b ($bv_extract v l 0 a) a) v))) - - ; X > 0 ==> 0bvX ++ v >= 0 - (FORALL (v a b) - (QID bv:e:pos) - (PATS ($bv_concat 0 b v a)) - (IMPLIES - (> b 0) - (>= ($bv_concat 0 b v a) 0))) - - ;; unsound? -; (FORALL (lv w lw) -; (QID bv:c:0) -; (PATS ($bv_concat 0 lv w lw)) -; (EQ ($bv_concat 0 lv w lw) w)) - ;; matching loop -; (FORALL (v l1 a b l2 c d) -; (QID bv:e:e) -; (PATS ($bv_extract ($bv_extract v l1 a b) l2 c d)) -; (EQ ($bv_extract ($bv_extract v l1 a b) l2 c d) ($bv_extract v l1 (+ c a) (+ d a)))) - - - ; 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 deleted file mode 100644 index 7e30017b..00000000 --- a/Binaries/UnivBackPred2.sx +++ /dev/null @@ -1,87 +0,0 @@ -; ------------------------------------------------------------------------- -; Boogie 2 universal background predicate -; Copyright (c) 2004-2008, Microsoft Corp. -(DEFPRED (<: t u)) ; used for translation with type premisses -(DEFPRED (<:: s t u)) ; used for translation with type arguments - -(BG_PUSH (AND - - ; formula/term axioms - - (FORALL (x y) - (IFF - (EQ (boolIff x y) |@true|) - (IFF (EQ x |@true|) (EQ y |@true|)))) - - (FORALL (x y) - (IFF - (EQ (boolImplies x y) |@true|) - (IMPLIES (EQ x |@true|) (EQ y |@true|)))) - - (FORALL (x y) - (IFF - (EQ (boolAnd x y) |@true|) - (AND (EQ x |@true|) (EQ y |@true|)))) - - (FORALL (x y) - (IFF - (EQ (boolOr x y) |@true|) - (OR (EQ x |@true|) (EQ y |@true|)))) - - (FORALL (x) - (PATS (boolNot x)) - (IFF - (EQ (boolNot x) |@true|) - (NEQ x |@true|))) - - (FORALL (x y) - (IFF - (EQ (anyEqual x y) |@true|) - (EQ x y))) - - (FORALL (x y) - (PATS (anyNeq x y)) - (IFF - (EQ (anyNeq x y) |@true|) - (NEQ x y))) - - (FORALL (x y) - (IFF - (EQ (intLess x y) |@true|) - (< x y))) - - (FORALL (x y) - (IFF - (EQ (intAtMost x y) |@true|) - (<= x y))) - - (FORALL (x y) - (IFF - (EQ (intAtLeast x y) |@true|) - (>= x y))) - - (FORALL (x y) - (IFF - (EQ (intGreater x y) |@true|) - (> x y))) - - ; false is not true - - (DISTINCT |@false| |@true|) - - ;; The following axiom gives a way to typed produce verification conditions, - ;; that is, verification conditions where the terms are typable. To use these, - ;; the VCExpressionGenerator.{CastTo,CastFrom} methods must be overridden. - ;; Look for USE_SORTED_LOGIC in VCGeneration/VCExpr.ssc. - ; (FORALL (val T U) - ; (PATS (TypeConvert (TypeConvert val T U) U T)) - ; (EQ (TypeConvert (TypeConvert val T U) U T) val)) - - ; 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 -; ------------------------------------------------------------------------- -- cgit v1.2.3