deleted unnecessary files

2 files changed, 0 insertions, 222 deletions

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

-; -------------------------------------------------------------------------