MCPcopy Create free account
hub / github.com/NeuralNetworkVerification/Marabou / update

Method update

deps/CVC4/context/context.cpp:138–195  ·  view source on GitHub ↗

Source from the content-addressed store, hash-verified

136}
137
138void ContextObj::update()
139{
140 Debug("context") << "before update(" << this << "):" << std::endl
141 << "context is " << getContext() << std::endl
142 << *getContext() << std::endl;
143
144 // Call save() to save the information in the current object
145 ContextObj* pContextObjSaved = save(d_pScope->getCMM());
146
147 Debug("context") << "in update(" << this << ") with restore "
148 << pContextObjSaved << ": waypoint 1" << std::endl
149 << *getContext() << std::endl;
150
151 // Check that base class data was saved
152 Assert((pContextObjSaved->d_pContextObjNext == d_pContextObjNext
153 && pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev
154 && pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore
155 && pContextObjSaved->d_pScope == d_pScope))
156 << "save() did not properly copy information in base class";
157
158 // Link the "saved" object in place of this ContextObj in the scope
159 // we're moving it FROM.
160 Debug("context") << "in update(" << this
161 << "): next() == " << next() << std::endl;
162 if(next() != NULL) {
163 Debug("context") << "in update(" << this
164 << "): next()->prev() == " << next()->prev() << std::endl;
165 next()->prev() = &pContextObjSaved->next();
166 Debug("context") << "in update(" << this
167 << "): next()->prev() is now "
168 << next()->prev() << std::endl;
169 }
170 Debug("context") << "in update(" << this
171 << "): prev() == " << prev() << std::endl;
172 Debug("context") << "in update(" << this
173 << "): *prev() == " << *prev() << std::endl;
174 *prev() = pContextObjSaved;
175 Debug("context") << "in update(" << this
176 << "): *prev() is now " << *prev() << std::endl;
177
178 Debug("context") << "in update(" << this << ") with restore "
179 << pContextObjSaved << ": waypoint 3" << std::endl
180 << *getContext() << std::endl;
181
182 // Update Scope pointer to current top Scope
183 d_pScope = d_pScope->getContext()->getTopScope();
184
185 // Store the saved copy in the restore pointer
186 d_pContextObjRestore = pContextObjSaved;
187
188 // Insert object into the list of objects that need to be restored when this
189 // Scope is popped.
190 d_pScope->addToChain(this);
191
192 Debug("context") << "after update(" << this << ") with restore "
193 << pContextObjSaved << ":" << std::endl
194 << *getContext() << std::endl;
195}

Callers 2

updateModelMethod · 0.80
getObjectiveBoundMethod · 0.80

Calls 6

prevMethod · 0.80
getTopScopeMethod · 0.80
addToChainMethod · 0.80
getCMMMethod · 0.45
nextMethod · 0.45
getContextMethod · 0.45

Tested by

no test coverage detected