<!-- iframe showing the search results (closed by default) -->
<divid="MSearchResultsWindow">
<iframesrc="javascript:void(0)"frameborder="0"
name="MSearchResults" id="MSearchResults">
</iframe>
</div>
<divclass="header">
<divclass="headertitle">
<divclass="title">presolve_context.h</div></div>
</div><!--header-->
<divclass="contents">
<ahref="presolve__context_8h.html">Go to the documentation of this file.</a><divclass="fragment"><divclass="line"><aname="l00001"></a><spanclass="lineno"> 1</span> <spanclass="comment">// Copyright 2010-2018 Google LLC</span></div>
<divclass="line"><aname="l00002"></a><spanclass="lineno"> 2</span> <spanclass="comment">// Licensed under the Apache License, Version 2.0 (the "License");</span></div>
<divclass="line"><aname="l00003"></a><spanclass="lineno"> 3</span> <spanclass="comment">// you may not use this file except in compliance with the License.</span></div>
<divclass="line"><aname="l00004"></a><spanclass="lineno"> 4</span> <spanclass="comment">// You may obtain a copy of the License at</span></div>
<divclass="line"><aname="l00008"></a><spanclass="lineno"> 8</span> <spanclass="comment">// Unless required by applicable law or agreed to in writing, software</span></div>
<divclass="line"><aname="l00009"></a><spanclass="lineno"> 9</span> <spanclass="comment">// distributed under the License is distributed on an "AS IS" BASIS,</span></div>
<divclass="line"><aname="l00010"></a><spanclass="lineno"> 10</span> <spanclass="comment">// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.</span></div>
<divclass="line"><aname="l00011"></a><spanclass="lineno"> 11</span> <spanclass="comment">// See the License for the specific language governing permissions and</span></div>
<divclass="line"><aname="l00012"></a><spanclass="lineno"> 12</span> <spanclass="comment">// limitations under the License.</span></div>
<divclass="line"><aname="l00032"></a><spanclass="lineno"> 32</span> <spanclass="comment">// We use some special constraint index in our variable <-> constraint graph.</span></div>
<divclass="line"><aname="l00045"></a><spanclass="lineno"> 45</span> <spanclass="comment">// When storing a reference to a literal, it is important not to forget when</span></div>
<divclass="line"><aname="l00046"></a><spanclass="lineno"> 46</span> <spanclass="comment">// reading it back to take its representative. Otherwise, we might introduce</span></div>
<divclass="line"><aname="l00047"></a><spanclass="lineno"> 47</span> <spanclass="comment">// literal that have already been removed, which will break invariants in a</span></div>
<divclass="line"><aname="l00048"></a><spanclass="lineno"> 48</span> <spanclass="comment">// bunch of places.</span></div>
<divclass="line"><aname="l00070"></a><spanclass="lineno"> 70</span> <spanclass="comment">// Wrap the CpModelProto we are presolving with extra data structure like the</span></div>
<divclass="line"><aname="l00071"></a><spanclass="lineno"> 71</span> <spanclass="comment">// in-memory domain of each variables and the constraint variable graph.</span></div>
<divclass="line"><aname="l00077"></a><spanclass="lineno"> 77</span> <spanclass="comment">// Helpers to adds new variables to the presolved model.</span></div>
<divclass="line"><aname="l00088"></a><spanclass="lineno"> 88</span> <spanclass="comment">// Helpers to query the current domain of a variable.</span></div>
<divclass="line"><aname="l00099"></a><spanclass="lineno"> 99</span> <spanclass="comment">// Helpers to query the current domain of a linear expression.</span></div>
<divclass="line"><aname="l00100"></a><spanclass="lineno"> 100</span> <spanclass="comment">// This doesn't check for integer overflow, but our linear expression</span></div>
<divclass="line"><aname="l00101"></a><spanclass="lineno"> 101</span> <spanclass="comment">// should be such that this cannot happen (tested at validation).</span></div>
<divclass="line"><aname="l00105"></a><spanclass="lineno"> 105</span> <spanclass="comment">// This function takes a positive variable reference.</span></div>
<divclass="line"><aname="l00110"></a><spanclass="lineno"> 110</span> <spanclass="comment">// Returns true if this ref only appear in one constraint.</span></div>
<divclass="line"><aname="l00113"></a><spanclass="lineno"> 113</span> <spanclass="comment">// Returns true if this ref no longer appears in the model.</span></div>
<divclass="line"><aname="l00116"></a><spanclass="lineno"> 116</span> <spanclass="comment">// Functions to make sure that once we remove a variable, we no longer reuse</span></div>
<divclass="line"><aname="l00121"></a><spanclass="lineno"> 121</span> <spanclass="comment">// Same as VariableIsUniqueAndRemovable() except that in this case the</span></div>
<divclass="line"><aname="l00122"></a><spanclass="lineno"> 122</span> <spanclass="comment">// variable also appear in the objective in addition to a single constraint.</span></div>
<divclass="line"><aname="l00125"></a><spanclass="lineno"> 125</span> <spanclass="comment">// Returns true if an integer variable is only appearing in the rhs of</span></div>
<divclass="line"><aname="l00126"></a><spanclass="lineno"> 126</span> <spanclass="comment">// constraints of the form lit => var in domain. When this is the case, then</span></div>
<divclass="line"><aname="l00127"></a><spanclass="lineno"> 127</span> <spanclass="comment">// we can usually remove this variable and replace these constraints with</span></div>
<divclass="line"><aname="l00128"></a><spanclass="lineno"> 128</span> <spanclass="comment">// the proper constraints on the enforcement literals.</span></div>
<divclass="line"><aname="l00131"></a><spanclass="lineno"> 131</span> <spanclass="comment">// Returns false if the new domain is empty. Sets 'domain_modified' (if</span></div>
<divclass="line"><aname="l00132"></a><spanclass="lineno"> 132</span> <spanclass="comment">// provided) to true iff the domain is modified otherwise does not change it.</span></div>
<divclass="line"><aname="l00136"></a><spanclass="lineno"> 136</span> <spanclass="comment">// Returns false if the 'lit' doesn't have the desired value in the domain.</span></div>
<divclass="line"><aname="l00140"></a><spanclass="lineno"> 140</span> <spanclass="comment">// This function always return false. It is just a way to make a little bit</span></div>
<divclass="line"><aname="l00141"></a><spanclass="lineno"> 141</span> <spanclass="comment">// more sure that we abort right away when infeasibility is detected.</span></div>
<divclass="line"><aname="l00144"></a><spanclass="lineno"> 144</span> <spanclass="comment">// TODO(user): Report any explanation for the client in a nicer way?</span></div>
<divclass="line"><aname="l00152"></a><spanclass="lineno"> 152</span> <spanclass="comment">// Stores a description of a rule that was just applied to have a summary of</span></div>
<divclass="line"><aname="l00153"></a><spanclass="lineno"> 153</span> <spanclass="comment">// what the presolve did at the end.</span></div>
<divclass="line"><aname="l00156"></a><spanclass="lineno"> 156</span> <spanclass="comment">// Updates the constraints <-> variables graph. This needs to be called each</span></div>
<divclass="line"><aname="l00157"></a><spanclass="lineno"> 157</span> <spanclass="comment">// time a constraint is modified.</span></div>
<divclass="line"><aname="l00160"></a><spanclass="lineno"> 160</span> <spanclass="comment">// At the beginning of the presolve, we delay the costly creation of this</span></div>
<divclass="line"><aname="l00161"></a><spanclass="lineno"> 161</span> <spanclass="comment">// "graph" until we at least ran some basic presolve. This is because during</span></div>
<divclass="line"><aname="l00162"></a><spanclass="lineno"> 162</span> <spanclass="comment">// a LNS neighbhorhood, many constraints will be reduced significantly by</span></div>
<divclass="line"><aname="l00163"></a><spanclass="lineno"> 163</span> <spanclass="comment">// this "simple" presolve.</span></div>
<divclass="line"><aname="l00166"></a><spanclass="lineno"> 166</span> <spanclass="comment">// Calls UpdateConstraintVariableUsage() on all newly created constraints.</span></div>
<divclass="line"><aname="l00169"></a><spanclass="lineno"> 169</span> <spanclass="comment">// Returns true if our current constraints <-> variables graph is ok.</span></div>
<divclass="line"><aname="l00170"></a><spanclass="lineno"> 170</span> <spanclass="comment">// This is meant to be used in DEBUG mode only.</span></div>
<divclass="line"><aname="l00173"></a><spanclass="lineno"> 173</span> <spanclass="comment">// Regroups fixed variables with the same value.</span></div>
<divclass="line"><aname="l00174"></a><spanclass="lineno"> 174</span> <spanclass="comment">// TODO(user): Also regroup cte and -cte?</span></div>
<divclass="line"><aname="l00177"></a><spanclass="lineno"> 177</span> <spanclass="comment">// Adds the relation (ref_x = coeff * ref_y + offset) to the repository.</span></div>
<divclass="line"><aname="l00178"></a><spanclass="lineno"> 178</span> <spanclass="comment">// Once the relation is added, it doesn't need to be enforced by a constraint</span></div>
<divclass="line"><aname="l00179"></a><spanclass="lineno"> 179</span> <spanclass="comment">// in the model proto, since we will propagate such relation directly and add</span></div>
<divclass="line"><aname="l00180"></a><spanclass="lineno"> 180</span> <spanclass="comment">// them to the proto at the end of the presolve.</span></div>
<divclass="line"><aname="l00182"></a><spanclass="lineno"> 182</span> <spanclass="comment">// Returns true if the relation was added.</span></div>
<divclass="line"><aname="l00183"></a><spanclass="lineno"> 183</span> <spanclass="comment">// In some rare case, like if x = 3*z and y = 5*t are already added, we</span></div>
<divclass="line"><aname="l00184"></a><spanclass="lineno"> 184</span> <spanclass="comment">// currently cannot add x = 2 * y and we will return false in these case. So</span></div>
<divclass="line"><aname="l00185"></a><spanclass="lineno"> 185</span> <spanclass="comment">// when this returns false, the relation needs to be enforced by a separate</span></div>
<divclass="line"><aname="l00188"></a><spanclass="lineno"> 188</span> <spanclass="comment">// If the relation was added, both variables will be marked to appear in the</span></div>
<divclass="line"><aname="l00189"></a><spanclass="lineno"> 189</span> <spanclass="comment">// special kAffineRelationConstraint. This will allow to identify when a</span></div>
<divclass="line"><aname="l00190"></a><spanclass="lineno"> 190</span> <spanclass="comment">// variable is no longer needed (only appear there and is not a</span></div>
<divclass="line"><aname="l00194"></a><spanclass="lineno"> 194</span> <spanclass="comment">// Adds the fact that ref_a == ref_b using StoreAffineRelation() above.</span></div>
<divclass="line"><aname="l00195"></a><spanclass="lineno"> 195</span> <spanclass="comment">// This should never fail, so the relation will always be added.</span></div>
<divclass="line"><aname="l00198"></a><spanclass="lineno"> 198</span> <spanclass="comment">// Stores/Get the relation target_ref = abs(ref); The first function returns</span></div>
<divclass="line"><aname="l00199"></a><spanclass="lineno"> 199</span> <spanclass="comment">// false if it already exist and the second false if it is not present.</span></div>
<divclass="line"><aname="l00203"></a><spanclass="lineno"> 203</span> <spanclass="comment">// Returns the representative of a literal.</span></div>
<divclass="line"><aname="l00206"></a><spanclass="lineno"> 206</span> <spanclass="comment">// Returns another reference with exactly the same value.</span></div>
<divclass="line"><aname="l00213"></a><spanclass="lineno"> 213</span> <spanclass="comment">// This makes sure that the affine relation only uses one of the</span></div>
<divclass="line"><aname="l00214"></a><spanclass="lineno"> 214</span> <spanclass="comment">// representative from the var_equiv_relations.</span></div>
<divclass="line"><aname="l00217"></a><spanclass="lineno"> 217</span> <spanclass="comment">// Makes sure the domain of ref and of its representative are in sync.</span></div>
<divclass="line"><aname="l00218"></a><spanclass="lineno"> 218</span> <spanclass="comment">// Returns false on unsat.</span></div>
<divclass="line"><aname="l00221"></a><spanclass="lineno"> 221</span> <spanclass="comment">// Creates the internal structure for any new variables in working_model.</span></div>
<divclass="line"><aname="l00227"></a><spanclass="lineno"> 227</span> <spanclass="comment">// Inserts the given literal to encode ref == value.</span></div>
<divclass="line"><aname="l00228"></a><spanclass="lineno"> 228</span> <spanclass="comment">// If an encoding already exists, it adds the two implications between</span></div>
<divclass="line"><aname="l00229"></a><spanclass="lineno"> 229</span> <spanclass="comment">// the previous encoding and the new encoding.</span></div>
<divclass="line"><aname="l00231"></a><spanclass="lineno"> 231</span> <spanclass="comment">// Important: This does not update the constraint<->variable graph, so</span></div>
<divclass="line"><aname="l00232"></a><spanclass="lineno"> 232</span> <spanclass="comment">// ConstraintVariableGraphIsUpToDate() will be false until</span></div>
<divclass="line"><aname="l00233"></a><spanclass="lineno"> 233</span> <spanclass="comment">// UpdateNewConstraintsVariableUsage() is called.</span></div>
<divclass="line"><aname="l00236"></a><spanclass="lineno"> 236</span> <spanclass="comment">// Gets the associated literal if it is already created. Otherwise</span></div>
<divclass="line"><aname="l00237"></a><spanclass="lineno"> 237</span> <spanclass="comment">// create it, add the corresponding constraints and returns it.</span></div>
<divclass="line"><aname="l00239"></a><spanclass="lineno"> 239</span> <spanclass="comment">// Important: This does not update the constraint<->variable graph, so</span></div>
<divclass="line"><aname="l00240"></a><spanclass="lineno"> 240</span> <spanclass="comment">// ConstraintVariableGraphIsUpToDate() will be false until</span></div>
<divclass="line"><aname="l00241"></a><spanclass="lineno"> 241</span> <spanclass="comment">// UpdateNewConstraintsVariableUsage() is called.</span></div>
<divclass="line"><aname="l00244"></a><spanclass="lineno"> 244</span> <spanclass="comment">// If not already done, adds a Boolean to represent any integer variables that</span></div>
<divclass="line"><aname="l00245"></a><spanclass="lineno"> 245</span> <spanclass="comment">// take only two values. Make sure all the relevant affine and encoding</span></div>
<divclass="line"><aname="l00246"></a><spanclass="lineno"> 246</span> <spanclass="comment">// relations are updated.</span></div>
<divclass="line"><aname="l00248"></a><spanclass="lineno"> 248</span> <spanclass="comment">// Note that this might create a new Boolean variable.</span></div>
<divclass="line"><aname="l00251"></a><spanclass="lineno"> 251</span> <spanclass="comment">// Returns true if a literal attached to ref == var exists.</span></div>
<divclass="line"><aname="l00252"></a><spanclass="lineno"> 252</span> <spanclass="comment">// It assigns the corresponding to `literal` if non null.</span></div>
<divclass="line"><aname="l00255"></a><spanclass="lineno"> 255</span> <spanclass="comment">// Stores the fact that literal implies var == value.</span></div>
<divclass="line"><aname="l00256"></a><spanclass="lineno"> 256</span> <spanclass="comment">// It returns true if that information is new.</span></div>
<divclass="line"><aname="l00259"></a><spanclass="lineno"> 259</span> <spanclass="comment">// Stores the fact that literal implies var != value.</span></div>
<divclass="line"><aname="l00260"></a><spanclass="lineno"> 260</span> <spanclass="comment">// It returns true if that information is new.</span></div>
<divclass="line"><aname="l00263"></a><spanclass="lineno"> 263</span> <spanclass="comment">// Objective handling functions. We load it at the beginning so that during</span></div>
<divclass="line"><aname="l00264"></a><spanclass="lineno"> 264</span> <spanclass="comment">// presolve we can work on the more efficient hash_map representation.</span></div>
<divclass="line"><aname="l00266"></a><spanclass="lineno"> 266</span> <spanclass="comment">// Note that ReadObjectiveFromProto() makes sure that var_to_constraints of</span></div>
<divclass="line"><aname="l00267"></a><spanclass="lineno"> 267</span> <spanclass="comment">// all the variable that appear in the objective contains -1. This is later</span></div>
<divclass="line"><aname="l00268"></a><spanclass="lineno"> 268</span> <spanclass="comment">// enforced by all the functions modifying the objective.</span></div>
<divclass="line"><aname="l00270"></a><spanclass="lineno"> 270</span> <spanclass="comment">// Note(user): Because we process affine relation only on</span></div>
<divclass="line"><aname="l00271"></a><spanclass="lineno"> 271</span> <spanclass="comment">// CanonicalizeObjective(), it is possible that when processing a</span></div>
<divclass="line"><aname="l00272"></a><spanclass="lineno"> 272</span> <spanclass="comment">// canonicalized linear constraint, we don't detect that a variable in affine</span></div>
<divclass="line"><aname="l00273"></a><spanclass="lineno"> 273</span> <spanclass="comment">// relation is in the objective. For now this is fine, because when this is</span></div>
<divclass="line"><aname="l00274"></a><spanclass="lineno"> 274</span> <spanclass="comment">// the case, we also have an affine linear constraint, so we can't really do</span></div>
<divclass="line"><aname="l00275"></a><spanclass="lineno"> 275</span> <spanclass="comment">// anything with that variable since it appear in at least two constraints.</span></div>
<divclass="line"><aname="l00280"></a><spanclass="lineno"> 280</span> <spanclass="comment">// Given a variable defined by the given inequality that also appear in the</span></div>
<divclass="line"><aname="l00281"></a><spanclass="lineno"> 281</span> <spanclass="comment">// objective, remove it from the objective by transferring its cost to other</span></div>
<divclass="line"><aname="l00282"></a><spanclass="lineno"> 282</span> <spanclass="comment">// variables in the equality.</span></div>
<divclass="line"><aname="l00284"></a><spanclass="lineno"> 284</span> <spanclass="comment">// If new_vars_in_objective is not nullptr, it will be filled with "new"</span></div>
<divclass="line"><aname="l00285"></a><spanclass="lineno"> 285</span> <spanclass="comment">// variables that where not in the objective before and are after</span></div>
<divclass="line"><aname="l00301"></a><spanclass="lineno"> 301</span> <spanclass="comment">// Advanced usage. This should be called when a variable can be removed from</span></div>
<divclass="line"><aname="l00302"></a><spanclass="lineno"> 302</span> <spanclass="comment">// the problem, so we don't count it as part of an affine relation anymore.</span></div>
<divclass="line"><aname="l00307"></a><spanclass="lineno"> 307</span> <spanclass="comment">// The vector list is sorted and contains unique elements.</span></div>
<divclass="line"><aname="l00309"></a><spanclass="lineno"> 309</span> <spanclass="comment">// Important: To properly handle the objective, var_to_constraints[objective]</span></div>
<divclass="line"><aname="l00310"></a><spanclass="lineno"> 310</span> <spanclass="comment">// contains -1 so that if the objective appear in only one constraint, the</span></div>
<divclass="line"><aname="l00311"></a><spanclass="lineno"> 311</span> <spanclass="comment">// constraint cannot be simplified.</span></div>
<divclass="line"><aname="l00325"></a><spanclass="lineno"> 325</span> <spanclass="comment">// Make sure we never delete an "assumption" literal by using a special</span></div>
<divclass="line"><aname="l00326"></a><spanclass="lineno"> 326</span> <spanclass="comment">// constraint for that.</span></div>
<divclass="line"><aname="l00333"></a><spanclass="lineno"> 333</span> <spanclass="comment">// For each variables, list the constraints that just enforce a lower bound</span></div>
<divclass="line"><aname="l00334"></a><spanclass="lineno"> 334</span> <spanclass="comment">// (resp. upper bound) on that variable. If all the constraints in which a</span></div>
<divclass="line"><aname="l00335"></a><spanclass="lineno"> 335</span> <spanclass="comment">// variable appear are in the same direction, then we can usually fix a</span></div>
<divclass="line"><aname="l00336"></a><spanclass="lineno"> 336</span> <spanclass="comment">// variable to one of its bound (modulo its cost).</span></div>
<divclass="line"><aname="l00338"></a><spanclass="lineno"> 338</span> <spanclass="comment">// TODO(user): Keeping these extra vector of hash_set seems inefficient. Come</span></div>
<divclass="line"><aname="l00339"></a><spanclass="lineno"> 339</span> <spanclass="comment">// up with a better way to detect if a variable is only constrainted in one</span></div>
<divclass="line"><aname="l00347"></a><spanclass="lineno"> 347</span> <spanclass="comment">// Indicate if we are allowed to remove irrelevant feasible solution from the</span></div>
<divclass="line"><aname="l00348"></a><spanclass="lineno"> 348</span> <spanclass="comment">// set of feasible solution. For example, if a variable is unused, can we fix</span></div>
<divclass="line"><aname="l00349"></a><spanclass="lineno"> 349</span> <spanclass="comment">// it to an arbitrary value (or its mimimum objective one)? This must be true</span></div>
<divclass="line"><aname="l00350"></a><spanclass="lineno"> 350</span> <spanclass="comment">// if the client wants to enumerate all solutions or wants correct tightened</span></div>
<divclass="line"><aname="l00351"></a><spanclass="lineno"> 351</span> <spanclass="comment">// bounds in the response.</span></div>
<divclass="line"><aname="l00354"></a><spanclass="lineno"> 354</span> <spanclass="comment">// If true, fills stats_by_rule_name, otherwise do not do that. This can take</span></div>
<divclass="line"><aname="l00355"></a><spanclass="lineno"> 355</span> <spanclass="comment">// a few percent of the run time with a lot of LNS threads.</span></div>
<divclass="line"><aname="l00358"></a><spanclass="lineno"> 358</span> <spanclass="comment">// Just used to display statistics on the presolve rules that were used.</span></div>
<divclass="line"><aname="l00361"></a><spanclass="lineno"> 361</span> <spanclass="comment">// Number of "rules" applied. This should be equal to the sum of all numbers</span></div>
<divclass="line"><aname="l00362"></a><spanclass="lineno"> 362</span> <spanclass="comment">// in stats_by_rule_name. This is used to decide if we should do one more pass</span></div>
<divclass="line"><aname="l00363"></a><spanclass="lineno"> 363</span> <spanclass="comment">// of the presolve or not. Note that depending on the presolve transformation,</span></div>
<divclass="line"><aname="l00364"></a><spanclass="lineno"> 364</span> <spanclass="comment">// a rule can correspond to a tiny change or a big change. Because of that,</span></div>
<divclass="line"><aname="l00365"></a><spanclass="lineno"> 365</span> <spanclass="comment">// this isn't a perfect proxy for the efficacy of the presolve.</span></div>
<divclass="line"><aname="l00374"></a><spanclass="lineno"> 374</span> <spanclass="comment">// Each time a domain is modified this is set to true.</span></div>
<divclass="line"><aname="l00377"></a><spanclass="lineno"> 377</span> <spanclass="comment">// Advanced presolve. See this class comment.</span></div>
<divclass="line"><aname="l00381"></a><spanclass="lineno"> 381</span> <spanclass="comment">// Helper to add an affine relation x = c.y + o to the given repository.</span></div>
<divclass="line"><aname="l00387"></a><spanclass="lineno"> 387</span> <spanclass="comment">// Returns true iff the variable is not the representative of an equivalence</span></div>
<divclass="line"><aname="l00388"></a><spanclass="lineno"> 388</span> <spanclass="comment">// class of size at least 2.</span></div>
<divclass="line"><aname="l00391"></a><spanclass="lineno"> 391</span> <spanclass="comment">// Process encoding_remap_queue_ and updates the encoding maps. This could</span></div>
<divclass="line"><aname="l00392"></a><spanclass="lineno"> 392</span> <spanclass="comment">// lead to UNSAT being detected, in which case it will return false.</span></div>
<divclass="line"><aname="l00395"></a><spanclass="lineno"> 395</span> <spanclass="comment">// Makes sure we only insert encoding about the current representative.</span></div>
<divclass="line"><aname="l00397"></a><spanclass="lineno"> 397</span> <spanclass="comment">// Returns false if ref cannot take the given value (it might not have been</span></div>
<divclass="line"><aname="l00401"></a><spanclass="lineno"> 401</span> <spanclass="comment">// Inserts an half reified var value encoding (literal => var ==/!= value).</span></div>
<divclass="line"><aname="l00402"></a><spanclass="lineno"> 402</span> <spanclass="comment">// It returns true if the new state is different from the old state.</span></div>
<divclass="line"><aname="l00403"></a><spanclass="lineno"> 403</span> <spanclass="comment">// Not that if imply_eq is false, the literal will be stored in its negated</span></div>
<divclass="line"><aname="l00406"></a><spanclass="lineno"> 406</span> <spanclass="comment">// Thus, if you detect literal <=> var == value, then two calls must be made:</span></div>
<divclass="line"><aname="l00407"></a><spanclass="lineno"> 407</span> <spanclass="comment">// InsertHalfVarValueEncoding(literal, var, value, true);</span></div>
<divclass="line"><aname="l00408"></a><spanclass="lineno"> 408</span> <spanclass="comment">// InsertHalfVarValueEncoding(NegatedRef(literal), var, value, false);</span></div>
<divclass="line"><aname="l00416"></a><spanclass="lineno"> 416</span> <spanclass="comment">// Initially false, and set to true on the first inconsistency.</span></div>
<divclass="line"><aname="l00422"></a><spanclass="lineno"> 422</span> <spanclass="comment">// Internal representation of the objective. During presolve, we first load</span></div>
<divclass="line"><aname="l00423"></a><spanclass="lineno"> 423</span> <spanclass="comment">// the objective in this format in order to have more efficient substitution</span></div>
<divclass="line"><aname="l00424"></a><spanclass="lineno"> 424</span> <spanclass="comment">// on large problems (also because the objective is often dense). At the end</span></div>
<divclass="line"><aname="l00425"></a><spanclass="lineno"> 425</span> <spanclass="comment">// we re-convert it to its proto form.</span></div>
<divclass="line"><aname="l00437"></a><spanclass="lineno"> 437</span> <spanclass="comment">// Number of constraints of the form [lit =>] var in domain.</span></div>
<divclass="line"><aname="l00441"></a><spanclass="lineno"> 441</span> <spanclass="comment">// We maintain how many time each interval is used.</span></div>
<divclass="line"><aname="l00448"></a><spanclass="lineno"> 448</span> <spanclass="comment">// For each constant variable appearing in the model, we maintain a reference</span></div>
<divclass="line"><aname="l00449"></a><spanclass="lineno"> 449</span> <spanclass="comment">// variable with the same constant value. If two variables end up having the</span></div>
<divclass="line"><aname="l00450"></a><spanclass="lineno"> 450</span> <spanclass="comment">// same fixed value, then we can detect it using this and add a new</span></div>
<divclass="line"><aname="l00451"></a><spanclass="lineno"> 451</span> <spanclass="comment">// equivalence relation. See ExploitFixedDomain().</span></div>
<divclass="line"><aname="l00454"></a><spanclass="lineno"> 454</span> <spanclass="comment">// When a "representative" gets a new representative, it should be enqueued</span></div>
<divclass="line"><aname="l00455"></a><spanclass="lineno"> 455</span> <spanclass="comment">// here so that we can lazily update the *encoding_ maps below.</span></div>
<divclass="line"><aname="l00458"></a><spanclass="lineno"> 458</span> <spanclass="comment">// Contains variables with some encoded value: encoding_[i][v] points</span></div>
<divclass="line"><aname="l00459"></a><spanclass="lineno"> 459</span> <spanclass="comment">// to the literal attached to the value v of the variable i.</span></div>
<divclass="line"><aname="l00462"></a><spanclass="lineno"> 462</span> <spanclass="comment">// Contains the currently collected half value encodings:</span></div>
<divclass="line"><aname="l00463"></a><spanclass="lineno"> 463</span> <spanclass="comment">// i.e.: literal => var ==/!= value</span></div>
<divclass="line"><aname="l00464"></a><spanclass="lineno"> 464</span> <spanclass="comment">// The state is accumulated (adding x => var == value then !x => var != value)</span></div>
<divclass="line"><aname="l00465"></a><spanclass="lineno"> 465</span> <spanclass="comment">// will deduce that x equivalent to var == value.</span></div>
<divclass="line"><aname="l00471"></a><spanclass="lineno"> 471</span> <spanclass="comment">// This regroups all the affine relations between variables. Note that the</span></div>
<divclass="line"><aname="l00472"></a><spanclass="lineno"> 472</span> <spanclass="comment">// constraints used to detect such relations will not be removed from the</span></div>
<divclass="line"><aname="l00473"></a><spanclass="lineno"> 473</span> <spanclass="comment">// model at detection time (thus allowing proper domain propagation). However,</span></div>
<divclass="line"><aname="l00474"></a><spanclass="lineno"> 474</span> <spanclass="comment">// if the arity of a variable becomes one, then such constraint will be</span></div>
<divclass="line"><aname="l00481"></a><spanclass="lineno"> 481</span> <spanclass="comment">// Used by SetVariableAsRemoved() and VariableWasRemoved().</span></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_a1aadaad9b8af16ab5a208c682e2e1717"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#a1aadaad9b8af16ab5a208c682e2e1717">operations_research::sat::PresolveContext::AddImplication</a></div><divclass="ttdeci">void AddImplication(int a, int b)</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8cc_source.html#l00054">presolve_context.cc:54</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_afad3c5370d5ef3338d7a5455198e6364"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#afad3c5370d5ef3338d7a5455198e6364">operations_research::sat::PresolveContext::StoreAffineRelation</a></div><divclass="ttdeci">bool StoreAffineRelation(int ref_x, int ref_y, int64 coeff, int64 offset)</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8cc_source.html#l00534">presolve_context.cc:534</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_a4d724b2f4bd1d1cab7b11dafd3448d8b"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#a4d724b2f4bd1d1cab7b11dafd3448d8b">operations_research::sat::PresolveContext::ConstraintToVars</a></div><divclass="ttdeci">const std::vector< int >& ConstraintToVars(int c) const</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8h_source.html#l00312">presolve_context.h:312</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_acf72cafd3dab9ac4b5e5b1a3aaa75192"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#acf72cafd3dab9ac4b5e5b1a3aaa75192">operations_research::sat::PresolveContext::VarToConstraints</a></div><divclass="ttdeci">const absl::flat_hash_set< int >& VarToConstraints(int var) const</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8h_source.html#l00316">presolve_context.h:316</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_a3dc318518f2e4259ed03b5d1c95316ef"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#a3dc318518f2e4259ed03b5d1c95316ef">operations_research::sat::PresolveContext::StoreLiteralImpliesVarEqValue</a></div><divclass="ttdeci">bool StoreLiteralImpliesVarEqValue(int literal, int var, int64 value)</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8cc_source.html#l01040">presolve_context.cc:1040</a></div></div>
<divclass="ttc"id="anamespaceoperations__research_html"><divclass="ttname"><ahref="namespaceoperations__research.html">operations_research</a></div><divclass="ttdoc">The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...</div><divclass="ttdef"><b>Definition:</b><ahref="dense__doubly__linked__list_8h_source.html#l00021">dense_doubly_linked_list.h:21</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1_domain_html"><divclass="ttname"><ahref="classoperations__research_1_1_domain.html">operations_research::Domain</a></div><divclass="ttdoc">We call domain any subset of Int64 = [kint64min, kint64max].</div><divclass="ttdef"><b>Definition:</b><ahref="sorted__interval__list_8h_source.html#l00081">sorted_interval_list.h:81</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1_time_limit_html"><divclass="ttname"><ahref="classoperations__research_1_1_time_limit.html">operations_research::TimeLimit</a></div><divclass="ttdoc">A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...</div><divclass="ttdef"><b>Definition:</b><ahref="time__limit_8h_source.html#l00105">time_limit.h:105</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_a23aa815e8a7a860998c4d35760fa087e"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#a23aa815e8a7a860998c4d35760fa087e">operations_research::sat::PresolveContext::var_to_lb_only_constraints</a></div><divclass="ttdeci">std::vector< absl::flat_hash_set< int >> var_to_lb_only_constraints</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8h_source.html#l00342">presolve_context.h:342</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_a31d9b7763fd739fe805438b464096c32"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#a31d9b7763fd739fe805438b464096c32">operations_research::sat::PresolveContext::ObjectiveDomain</a></div><divclass="ttdeci">const Domain & ObjectiveDomain() const</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8h_source.html#l00293">presolve_context.h:293</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_a8fc1d49d1e1bf7261f15ccc6c23c4b10"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#a8fc1d49d1e1bf7261f15ccc6c23c4b10">operations_research::sat::PresolveContext::StoreBooleanEqualityRelation</a></div><divclass="ttdeci">void StoreBooleanEqualityRelation(int ref_a, int ref_b)</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8cc_source.html#l00649">presolve_context.cc:649</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_a8abe16435f55971a49965eb6616c5783"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#a8abe16435f55971a49965eb6616c5783">operations_research::sat::PresolveContext::stats_by_rule_name</a></div><divclass="ttdeci">absl::flat_hash_map< std::string, int > stats_by_rule_name</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8h_source.html#l00359">presolve_context.h:359</a></div></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_abe4ecb2ef8f498b18a55fbcbbf54e550"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#abe4ecb2ef8f498b18a55fbcbbf54e550">operations_research::sat::kAssumptionsConstraint</a></div><divclass="ttdeci">constexpr int kAssumptionsConstraint</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8h_source.html#l00035">presolve_context.h:35</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_aeb77639debea43978becf1d990581537"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#aeb77639debea43978becf1d990581537">operations_research::sat::PresolveContext::tmp_literal_set</a></div><divclass="ttdeci">absl::flat_hash_set< int > tmp_literal_set</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8h_source.html#l00372">presolve_context.h:372</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_a436752c51b5f6010033151b7bd7966da"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#a436752c51b5f6010033151b7bd7966da">operations_research::sat::PresolveContext::tmp_literals</a></div><divclass="ttdeci">std::vector< int > tmp_literals</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8h_source.html#l00369">presolve_context.h:369</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_a06f0856b91c0399720273b5da85ce280"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#a06f0856b91c0399720273b5da85ce280">operations_research::sat::PresolveContext::StoreAbsRelation</a></div><divclass="ttdeci">bool StoreAbsRelation(int target_ref, int ref)</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8cc_source.html#l00675">presolve_context.cc:675</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_a90674fa816d7a066e251337852214e84"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#a90674fa816d7a066e251337852214e84">operations_research::sat::PresolveContext::IntervalUsage</a></div><divclass="ttdeci">int IntervalUsage(int c) const</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8h_source.html#l00320">presolve_context.h:320</a></div></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_aca25bc3ffa54b3f2668c6eeddffd8d1d"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#aca25bc3ffa54b3f2668c6eeddffd8d1d">operations_research::sat::kObjectiveConstraint</a></div><divclass="ttdeci">constexpr int kObjectiveConstraint</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8h_source.html#l00033">presolve_context.h:33</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_af97bdc26758ff0f27314cafb7c2d7044"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#af97bdc26758ff0f27314cafb7c2d7044">operations_research::sat::PresolveContext::GetAbsRelation</a></div><divclass="ttdeci">bool GetAbsRelation(int target_ref, int *ref)</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8cc_source.html#l00690">presolve_context.cc:690</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_a31ade354475e7f6052e62f7befc21cf8"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#a31ade354475e7f6052e62f7befc21cf8">operations_research::sat::PresolveContext::StoreLiteralImpliesVarNEqValue</a></div><divclass="ttdeci">bool StoreLiteralImpliesVarNEqValue(int literal, int var, int64 value)</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8cc_source.html#l01048">presolve_context.cc:1048</a></div></div>
<divclass="ttc"id="aclassoperations__research_1_1sat_1_1_presolve_context_html_a47714f887512a3d7acebfcb4a348291a"><divclass="ttname"><ahref="classoperations__research_1_1sat_1_1_presolve_context.html#a47714f887512a3d7acebfcb4a348291a">operations_research::sat::PresolveContext::var_to_ub_only_constraints</a></div><divclass="ttdeci">std::vector< absl::flat_hash_set< int >> var_to_ub_only_constraints</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8h_source.html#l00341">presolve_context.h:341</a></div></div>
<divclass="ttc"id="anamespaceoperations__research_1_1sat_html_a55963ffe87280b37dce97b9a8cbd03ae"><divclass="ttname"><ahref="namespaceoperations__research_1_1sat.html#a55963ffe87280b37dce97b9a8cbd03ae">operations_research::sat::kAffineRelationConstraint</a></div><divclass="ttdeci">constexpr int kAffineRelationConstraint</div><divclass="ttdef"><b>Definition:</b><ahref="presolve__context_8h_source.html#l00034">presolve_context.h:34</a></div></div>
