1
2 /*
3 * File NameArray.cpp.
4 *
5 * This file is part of the source code of the software program
6 * Vampire. It is protected by applicable
7 * copyright laws.
8 *
9 * This source code is distributed under the licence found here
10 * https://vprover.github.io/license.html
11 * and in the source directory
12 *
13 * In summary, you are allowed to use Vampire for non-commercial
14 * purposes but not allowed to distribute, modify, copy, create derivatives,
15 * or use in competitions.
16 * For other uses of Vampire please contact developers for a different
17 * licence, which we will make an effort to provide.
18 */
19 /**
20 * @file NameArray.cpp
21 * Implements ordered immutable arrays of integers.
22 * Previously they were used in Options.
23 *
24 * @since 21/04/2005 Manchester
25 */
26
27 #include <cstring>
28
29 #include "Exception.hpp"
30 #include "NameArray.hpp"
31 #include "Debug/Tracer.hpp"
32
33 namespace Lib {
34
NameArray(const char * array[],int len)35 NameArray::NameArray (const char* array[],int len)
36 : length(len),
37 _array(array)
38 {
39 #if VDEBUG
40 for (int i=1; i<len; i++) {
41 ASS_REP2(strcmp(array[i-1],array[i]) < 0,
42 array[i-1],
43 array[i]);
44 }
45 #endif
46 } // NameArray::NameArray
47
48 /**
49 * Find the index of a string in the name array. Throw a
50 * ValueNotFoundException if it is not present.
51 *
52 * @return the index
53 * @since 12/11/2004 Manchester
54 */
find(const char * value) const55 int NameArray::find (const char* value) const
56 {
57 CALL("NameArray::find");
58
59 int res=tryToFind(value);
60 if(res==-1) {
61 throw ValueNotFoundException();
62 }
63 return res;
64 } // Options::find
65
66 /**
67 * Find the index of a string in the name array. Return -1
68 * if it is not present.
69 */
tryToFind(const char * value) const70 int NameArray::tryToFind(const char* value) const
71 {
72 CALL("NameArray::tryToFind");
73
74 int from = 0;
75 int to = length;
76 while (from < to) {
77 int mid = (from+to)/2;
78 int comp = strcmp(_array[mid],value);
79 if (comp < 0) {
80 from = mid+1;
81 }
82 else if (comp == 0) {
83 return mid;
84 }
85 else { // comp > 0
86 to = mid;
87 }
88 }
89 return -1;
90 }
91
92 } // namespace Lib
93