88 lines
3.3 KiB
Diff
88 lines
3.3 KiB
Diff
--- ./src/encoding_pred.ml.orig 2012-07-19 12:33:10.000000000 -0600
|
|
+++ ./src/encoding_pred.ml 2012-07-31 15:35:10.506221997 -0600
|
|
@@ -266,11 +266,6 @@ let rec push d =
|
|
| Pnamed (s, p) ->
|
|
Pnamed (s, translate_eq p)
|
|
| p -> p in
|
|
- let rec lifted l p =
|
|
- match l with [] -> p
|
|
- | (_,a)::q ->
|
|
- lifted q (Forall(false, Ident.create a, Ident.create a, ut, [], p))
|
|
- in
|
|
Queue.add (Dgoal
|
|
(loc, is_lemma, expl, name,
|
|
Env.empty_scheme
|
|
--- ./src/encoding_rec.ml.orig 2012-07-19 12:33:10.000000000 -0600
|
|
+++ ./src/encoding_rec.ml 2012-07-31 15:35:10.506221997 -0600
|
|
@@ -397,11 +397,6 @@ let rec push d =
|
|
| Tconst (ConstUnit) as t -> plunge fv t PTunit
|
|
| Tconst (ConstFloat _) as t -> plunge fv t PTreal
|
|
| _ as t -> t in
|
|
- let rec lifted l p =
|
|
- match l with [] -> p
|
|
- | (_,a)::q ->
|
|
- lifted q (Forall(false, Ident.create a, Ident.create a, ut, [], p))
|
|
- in
|
|
Queue.add (Dgoal
|
|
(loc, is_lemma, expl, name,
|
|
Env.empty_scheme
|
|
--- ./src/theoryreducer.ml.orig 2012-07-19 12:33:10.000000000 -0600
|
|
+++ ./src/theoryreducer.ml 2012-07-31 15:35:10.507222001 -0600
|
|
@@ -191,11 +191,6 @@ struct
|
|
(** symbols the result **)
|
|
let symbolsSet = ref StringSet.empty in
|
|
let rec collect formula =
|
|
- let rec collectIntoAList l = match l with
|
|
- [] -> ()
|
|
- | p :: r ->
|
|
- collect p ;
|
|
- collectIntoAList r in
|
|
match formula with
|
|
| Papp (id, [a; b], _) when is_eq id || is_neq id || id == t_zwf_zero->
|
|
symbolsSet := StringSet.union (functionalSymbolsCollect a)
|
|
--- ./src/vcg.ml.orig 2012-07-19 12:33:10.000000000 -0600
|
|
+++ ./src/vcg.ml 2012-07-31 15:35:10.507222001 -0600
|
|
@@ -615,13 +615,6 @@ let occur_as_var id = function
|
|
| Spred _ -> false
|
|
|
|
let clean_sequent hyps concl =
|
|
- (* if a variable appears twice, we remove the first and its dependencies *)
|
|
- let rec filter_up_to x = function
|
|
- | [] -> []
|
|
- | Svar (y, _) :: _ as hl when x = y -> hl
|
|
- | Spred (_, p) :: hl when occur_predicate x p -> filter_up_to x hl
|
|
- | h :: hl -> h :: filter_up_to x hl
|
|
- in
|
|
(* we remove variables not occuring at all in hypotheses or conclusion *)
|
|
let rec clean = function
|
|
| [] ->
|
|
--- ./src/theory_filtering.ml.orig 2012-07-19 12:33:10.000000000 -0600
|
|
+++ ./src/theory_filtering.ml 2012-07-31 15:35:10.507222001 -0600
|
|
@@ -180,11 +180,6 @@ let symbols f =
|
|
(** symbols the result **)
|
|
let symbolsSet = ref Int_set.empty in
|
|
let rec collect formula =
|
|
- let rec collectIntoAList l = match l with
|
|
- [] -> ()
|
|
- | p :: r ->
|
|
- collect p ;
|
|
- collectIntoAList r in
|
|
match formula with
|
|
| Papp (id, [a; b], _) when is_eq id || is_neq id || id == t_zwf_zero->
|
|
symbolsSet := Int_set.union (functional_symbols a)
|
|
--- ./jc/jc_iterators.ml.orig 2012-07-19 12:33:10.000000000 -0600
|
|
+++ ./jc/jc_iterators.ml 2012-07-31 15:35:52.481285428 -0600
|
|
@@ -1057,13 +1057,6 @@ let replace_sub_expr e el =
|
|
| None -> None,el
|
|
| Some _ -> let e1,r = pop el in Some e1,r
|
|
in
|
|
- let rec popn n el =
|
|
- if n > 0 then
|
|
- let e,r = pop el in
|
|
- let el1,el2 = popn (n-1) r in
|
|
- e :: el1, el2
|
|
- else [],el
|
|
- in
|
|
let enode = match e#node with
|
|
| JCEconst _ | JCEvar _ | JCEassert _ | JCEreturn_void as enode -> enode
|
|
| JCEcontract(req,dec,vi_result,behs,_e) ->
|