1 /******************************************
2 Copyright (c) 2016, Mate Soos
3
4 Permission is hereby granted, free of charge, to any person obtaining a copy
5 of this software and associated documentation files (the "Software"), to deal
6 in the Software without restriction, including without limitation the rights
7 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8 copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10
11 The above copyright notice and this permission notice shall be included in
12 all copies or substantial portions of the Software.
13
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20 THE SOFTWARE.
21 ***********************************************/
22
23 #ifndef __WATCHALGOS_H__
24 #define __WATCHALGOS_H__
25
26 #include "watched.h"
27 #include "watcharray.h"
28 #include "clauseallocator.h"
29
30 namespace CMSat {
31
32 //////////////////
33 // NORMAL Clause
34 //////////////////
findWCl(watch_subarray_const ws,const ClOffset c)35 static inline bool findWCl(watch_subarray_const ws, const ClOffset c)
36 {
37 const Watched* i = ws.begin(), *end = ws.end();
38 for (; i != end && (!i->isClause() || i->get_offset() != c); i++);
39 return i != end;
40 }
41
removeWCl(watch_subarray ws,const ClOffset c)42 static inline void removeWCl(watch_subarray ws, const ClOffset c)
43 {
44 Watched* i = ws.begin(), *end = ws.end();
45 for (; i != end && (!i->isClause() || i->get_offset() != c); i++);
46 assert(i != end);
47 Watched* j = i;
48 i++;
49 for (; i != end; j++, i++) *j = *i;
50 ws.shrink_(1);
51 }
52
53 //////////////////
54 // BINARY Clause
55 //////////////////
56
removeWBin(watch_array & wsFull,const Lit lit1,const Lit lit2,const bool red)57 inline void removeWBin(
58 watch_array &wsFull
59 , const Lit lit1
60 , const Lit lit2
61 , const bool red
62 ) {
63 watch_subarray ws = wsFull[lit1];
64 Watched *i = ws.begin(), *end = ws.end();
65 for (; i != end && (
66 !i->isBin()
67 || i->lit2() != lit2
68 || i->red() != red
69 ); i++);
70
71 assert(i != end);
72 Watched *j = i;
73 i++;
74 for (; i != end; j++, i++) *j = *i;
75 ws.shrink_(1);
76 }
77
removeWBin_change_order(watch_array & wsFull,const Lit lit1,const Lit lit2,const bool red)78 inline void removeWBin_change_order(
79 watch_array &wsFull
80 , const Lit lit1
81 , const Lit lit2
82 , const bool red
83 ) {
84 watch_subarray ws = wsFull[lit1];
85 Watched *i = ws.begin(), *end = ws.end();
86 for (; i != end && (
87 !i->isBin()
88 || i->lit2() != lit2
89 || i->red() != red
90 ); i++);
91
92 assert(i != end);
93 *i = ws[ws.size()-1];
94 ws.shrink_(1);
95 }
96
removeWBin_except_marked(watch_array & wsFull,const Lit lit1,const Lit lit2,const bool red)97 inline bool removeWBin_except_marked(
98 watch_array &wsFull
99 , const Lit lit1
100 , const Lit lit2
101 , const bool red
102 ) {
103 watch_subarray ws = wsFull[lit1];
104 Watched *i = ws.begin(), *end = ws.end();
105 for (; i != end && (
106 !i->isBin()
107 || i->lit2() != lit2
108 || i->red() != red
109 ); i++);
110 assert(i != end);
111
112 if (i->bin_cl_marked()) {
113 return false;
114 }
115
116 Watched *j = i;
117 i++;
118 for (; i != end; j++, i++) *j = *i;
119 ws.shrink_(1);
120
121 return true;
122 }
123
findWatchedOfBin(const watch_array & wsFull,const Lit lit1,const Lit lit2,const bool red)124 inline const Watched& findWatchedOfBin(
125 const watch_array& wsFull
126 , const Lit lit1
127 , const Lit lit2
128 , const bool red
129 ) {
130 watch_subarray_const ws = wsFull[lit1];
131 for (const Watched *i = ws.begin(), *end = ws.end(); i != end; i++) {
132 if (i->isBin() && i->lit2() == lit2 && i->red() == red)
133 return *i;
134 }
135
136 assert(false);
137 return *ws.begin();
138 }
139
findWatchedOfBin(watch_array & wsFull,const Lit lit1,const Lit lit2,const bool red)140 inline Watched& findWatchedOfBin(
141 watch_array& wsFull
142 , const Lit lit1
143 , const Lit lit2
144 , const bool red
145 ) {
146 watch_subarray ws = wsFull[lit1];
147 for (Watched *i = ws.begin(), *end = ws.end(); i != end; i++) {
148 if (i->isBin() && i->lit2() == lit2 && i->red() == red)
149 return *i;
150 }
151
152 assert(false);
153 return *ws.begin();
154 }
155
removeWXCl(watch_array & wsFull,const Lit lit,const ClOffset offs)156 static inline void removeWXCl(watch_array& wsFull
157 , const Lit lit
158 , const ClOffset offs
159 ) {
160 watch_subarray ws = wsFull[lit];
161 Watched *i = ws.begin(), *end = ws.end();
162 for (; i != end && (!i->isClause() || i->get_offset() != offs); i++);
163 assert(i != end);
164 Watched *j = i;
165 i++;
166 for (; i != end; j++, i++) *j = *i;
167 ws.shrink_(1);
168 }
169
170 } //end namespace
171
172
173 #endif //__WATCHALGOS_H__
174