From 81b749c73c43def5c5010e41b88cd437adce9915 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Mon, 2 Feb 2015 16:49:09 +1100
Subject: [PATCH] Remove old annbitset code
---
src/lib/MiscSolver.ml | 257 -----------------------------------------
src/lib/MiscSolver.mli | 27 -----
2 files changed, 284 deletions(-)
diff --git a/src/lib/MiscSolver.ml b/src/lib/MiscSolver.ml
index c0435fa..9ab4046 100644
--- a/src/lib/MiscSolver.ml
+++ b/src/lib/MiscSolver.ml
@@ -335,216 +335,6 @@ let foldBS f bs init =
done;
!res
-(*
-
-(** Represents a set of annotated formulae as a bit vector.
- All sets contain the formula True, that is bstrue,
- which is needed to detect whether False, that is bsfalse,
- is inserted.
- *)
-type annbitset = int array
-
-(** The number of elements that are stored in one integer of the array.
- It has to be strictly smaller than the bitsize of the system
- divided by two since we need two bits per entry
- (the "strictly" is due to the way ocaml handles integers).
- *)
-let annbsintsize = bsintsize / 2
-
-(** Constant for "element not contained in annotated bitset".
- *)
-let absNotIn = 0
-
-(** Constant for "element contained but not annotated in annotated bitset".
- *)
-let absUnAnn = 3
-
-(** Constant for "element contained and annotated with 1 in annotated bitset".
- *)
-let absAnn1 = 1
-
-(** Constant for "element contained and annotated with 2 in annotated bitset".
- *)
-let absAnn2 = 2
-
-(** The size of the arrays implementing the annotated bitsets.
- *)
-let abssize = ref (-1)
-
-(** The greatest index of the arrays implementing the annotated bitsets.
- It must hold that abssize = absindex + 1.
- *)
-let absindex = ref (-1)
-
-(** A dummy annotated bitset that can be used if an annotated bitset is needed
- before this module is initialised.
- It must never been actually used.
- *)
-let dummyABS = Array.make 0 0
-
-(** Copies the content of one annotated bitset to another annotated bitset.
- @param src The source annotated bitset.
- @param trg The target annotated bitset.
- *)
-let blitABS (src : annbitset) trg = Array.blit src 0 trg 0 !abssize
-
-(** Creates a clone of an annotated bitset.
- @param abs An annotated bitset.
- @return A new annotated bitset with the same content as abs.
- *)
-let copyABS (abs : annbitset) = Array.copy abs
-
-(** Compares two annotated bitsets. The order is (more or less) lexicographic.
- @param abs1 The first annotated bitset.
- @param abs2 The second annotated bitset.
- @param i The current index of the array.
- @return -1 if abs1 is smaller than abs2, 1 if abs1 is greater than abs2,
- and 0 if the sets are equal.
- *)
-let rec intern_compABS (abs1 : annbitset) abs2 i =
- if i >= 0 then
- let n1 = abs1.(i) in
- let n2 = abs2.(i) in
- if n1 = n2 then intern_compABS abs1 abs2 (pred i)
- else if n1 < n2 then (-1) else 1
- else 0
-
-let compareABS (abs1 : annbitset) abs2 = intern_compABS abs1 abs2 !absindex
-
-(** Computes a hash value for an annotated bitset.
- It implements the One-at-a-Time hash invented by Bob Jenkins.
- @param abs An annotated bitset.
- @param acc The hash value computed so far.
- @param i The current index of the array.
- @return The hash value of bs.
- *)
-let rec intern_hashABS abs acc i =
- if i >= 0 then
- let acc1 = acc + abs.(i) in
- let acc2 = acc1 + (acc1 lsl 10) in
- let acc3 = acc2 lxor (acc2 lsr 6) in
- intern_hashABS abs acc3 (pred i)
- else
- let acc1 = acc + (acc lsl 3) in
- let acc2 = acc1 lxor (acc1 lsr 11) in
- acc2 + (acc lsl 15)
-
-let hashABS abs = intern_hashABS abs 0 !absindex
-
-(** Tests whether a formula is an element of an annotated set of formulae
- and, if yes, determines its annotation.
- @param abs An annotated bitset of formulae.
- @param f The integer representation of a formula.
- @return The appropriate return code
- (one of absNotIn, absUnAnn, absAnn1, absAnn2).
- *)
-let getAnnABS abs f =
- let idx = f / annbsintsize in
- let pos = (f mod annbsintsize) lsl 1 in
- (abs.(idx) lsr pos) land 3
-
-(** Sets the annotation status of a formula in an annotated set of formulae.
- The old annotation status is overridden.
- @param abs An annotated bitset of formulae.
- @param f The integer representation of a formula
- whose annotation status is to be set.
- @param ann The (new) annotation status of f
- (must be one of absNotIn, absUnAnn, absAnn1, absAnn2).
- *)
-let setAnnABS abs f ann =
- let idx = f / annbsintsize in
- let pos = (f mod annbsintsize) lsl 1 in
- let pset = abs.(idx) in
- let pset1 = pset land ((-1) lxor (3 lsl pos)) in
- let pattern = (ann land 3) lsl pos in
- let npset = pset1 lor pattern in
- if npset <> pset then abs.(idx) <- npset else ()
-
-(** Tests whether a formula is an element of an annotated set of formulae.
- @param abs An annotated bitset of formulae.
- @param f The integer representation of a formula.
- @return True iff f is an element of abs (annotated or not).
- *)
-let memABS abs f =
- let idx = f / annbsintsize in
- let pos = (f mod annbsintsize) lsl 1 in
- (abs.(idx) land (3 lsl pos)) <> 0
-
-(** Removes a formula from an annotated bitset.
- @param abs An annotated bitset of formulae.
- @param f The integer representation of a formula
- which must not be bstrue.
- *)
-let remABS abs f =
- let idx = f / annbsintsize in
- let pos = (f mod annbsintsize) lsl 1 in
- let pset = abs.(idx) in
- let pattern = (-1) lxor (3 lsl pos) in
- let npset = pset land pattern in
- if npset <> pset then abs.(idx) <- npset else ()
-
-(** Adds a formula without annotation to an annotated set of formulae
- if it is not already contained in the set (annotated or not).
- @param abs An annotated bitset of formulae.
- @param f The integer representation of a formula that is to be added to abs.
- @return True iff inserting f leads to a new contradiction.
- *)
-let addABS abs f =
- let idx = f / annbsintsize in
- let pos = (f mod annbsintsize) lsl 1 in
- let pset = abs.(idx) in
- let pattern = 3 lsl pos in
- if (pset land pattern) = 0 then begin
- abs.(idx) <- pset lor pattern;
- let f1 = !arrayNeg.(f) in
- f1 >= 0 && f1 < !nrFormulae && memABS abs f1
- end
- else false
-
-(** Adds a formula to two sets of formulae
- if it is not already contained in the second one.
- @param bs A bitset of formulae.
- @param abs An annotated bitset of formulae.
- @param f The integer representation of a formula that is to be added to bs and abs.
- @return True iff inserting f into abs leads to a new contradiction.
- *)
-let addBSa bs abs f =
- let idx = f / annbsintsize in
- let pos = (f mod annbsintsize) lsl 1 in
- let apset = abs.(idx) in
- let pattern = 3 lsl pos in
- if (apset land pattern) = 0 then begin
- abs.(idx) <- apset lor pattern;
- addBSNoChk bs f;
- let f1 = !arrayNeg.(f) in
- f1 >= 0 && f1 < !nrFormulae && memABS abs f1
- end
- else false
-
-(** Creates an "empty" annotated bitset.
- @return An annotated bitset which only contains bstrue (unannotated).
- *)
-let makeABS () =
- let abs = Array.make !abssize 0 in
- setAnnABS abs !bstrue absUnAnn;
- abs
-
-(** "Empties" an annotated bitset such that it only contains bstrue (unannotated).
- @param abs An annotated bitset.
- *)
-let emptyABS abs =
- Array.fill abs 0 !abssize 0;
- setAnnABS abs !bstrue absUnAnn
-
-(** Copies the content of an annotated bitset to a bitset.
- @param src The annotated source bitset.
- @param trg The target bitset.
- *)
-let blitBSa (src : annbitset) (trg : bitset) =
- for i = 0 to pred !nrFormulae do
- if memABS src i then addBSNoChk trg i else ()
- done
-*)
(** Selects a principal formula from a set of formulae if possible.
@param bs A bitset of formulae.
@@ -591,23 +381,6 @@ let rec intern_mkEXList bs bnd acc i =
let mkEXList bs = intern_mkEXList bs !lposEX [] !hposEX
-(*
-(** Constructs a list of all EX-formulae of a set of annotated formulae.
- @param abs The annotated bitset of formulae.
- @param bnd The greatest integer representing an EX-formula.
- @param acc A list of EX-formulae gathered till now.
- @param i The current index of the array.
- @return A list of all EX-formulae f (in decreasing order) in abs.
- *)
-let rec intern_mkEXListAnn abs bnd acc i =
- if i >= bnd then
- if memABS abs i then intern_mkEXListAnn abs bnd (i::acc) (pred i)
- else intern_mkEXListAnn abs bnd acc (pred i)
- else acc
-
-let mkEXListAnn abs = intern_mkEXListAnn abs !lposEX [] !hposEX
-*)
-
(** Prints a "collection" as a set.
@param ps A string prefixing the set.
@param f A function converting the collection c into a list of strings.
@@ -639,31 +412,6 @@ let exportFSet expF bs = foldBS (fun i acc -> (expF i)::acc) bs []
!res
*)
-(*
-(** Converts an annotated set of formulae into a list of strings
- where each string represents one formula of the set and its annotation.
- @param expF A function which converts the formula in integer
- representations into a readable string.
- @param abs An annotated bitset of formulae.
- @return A list of string representations of the formulae in abs
- and their annotation.
- *)
-let exportAnnFSet expF abs =
- let res = ref [] in
- for i = 0 to pred !nrFormulae do
- let ann = getAnnABS abs i in
- if ann <> absNotIn then
- let fstr = expF i in
- let afstr =
- if ann = absAnn1 then fstr ^ "(1)"
- else if ann = absAnn2 then fstr ^ "(2)"
- else fstr
- in
- res := afstr::!res
- else ()
- done;
- !res
-*)
(** Initialises the global fields of this module
with the exception of the tables.
@@ -681,11 +429,6 @@ let initMisc size bsf bst lEX nrEX nrAX =
bssize := (size - 1) / bsintsize + 1;
assert (!bssize <= Sys.max_array_length);
bsindex := pred !bssize;
- (*
- abssize := (size - 1) / annbsintsize + 1;
- assert (!abssize <= Sys.max_array_length);
- absindex := pred !abssize;
- *)
bsfalse := bsf;
bstrue := bst;
lposEX := lEX;
diff --git a/src/lib/MiscSolver.mli b/src/lib/MiscSolver.mli
index 32fb381..bd3b497 100644
--- a/src/lib/MiscSolver.mli
+++ b/src/lib/MiscSolver.mli
@@ -37,33 +37,6 @@ val unionBSNoChk : bitset -> bitset -> bitset
val iterBS : (int -> unit) -> bitset -> unit
val foldBS : (int -> 'a -> 'a) -> bitset -> 'a -> 'a
-(*
- Annotated bitsets aren't used anymore and will be removed soon.
-
-type annbitset
-val absNotIn : int
-val absUnAnn : int
-val absAnn1 : int
-val absAnn2 : int
-val dummyABS : annbitset
-val makeABS : unit -> annbitset
-val blitABS : annbitset -> annbitset -> unit
-val copyABS : annbitset -> annbitset
-val emptyABS : annbitset -> unit
-val compareABS : annbitset -> annbitset -> int
-val hashABS : annbitset -> int
-val getAnnABS : annbitset -> int -> int
-val setAnnABS : annbitset -> int -> int -> unit
-val memABS : annbitset -> int -> bool
-val remABS : annbitset -> int -> unit
-val addABS : annbitset -> int -> bool
-val addBSa : bitset -> annbitset -> int -> bool
-val blitBSa : annbitset -> bitset -> unit
-
-val mkEXListAnn : annbitset -> int list
-val exportAnnFSet : (int -> string) -> annbitset -> string list
-*)
-
val getPFinclEX : bitset -> int
val getPFexclEX : bitset -> int
--
GitLab