From 4cd85e08c4b0be67ae80a36f7f3d5d87aba4d1d5 Mon Sep 17 00:00:00 2001 From: Corentin Le Molgat Date: Wed, 18 Nov 2020 16:11:32 +0100 Subject: [PATCH] Export Google update --- ortools/algorithms/samples/Knapsack.java | 3 +- ortools/constraint_solver/doc/routing_svg.py | 3 +- .../java/com/google/ortools/sat/CpModel.java | 55 +++++++++---------- .../samples/linear_programming_example.py | 1 - ortools/sat/BUILD | 1 - ortools/sat/cp_model_presolve.cc | 4 ++ ortools/sat/doc/README.md | 1 - ortools/sat/doc/boolean_logic.md | 1 - ortools/sat/doc/integer_arithmetic.md | 1 - ortools/sat/doc/model.md | 1 - ortools/sat/doc/scheduling.md | 4 -- ortools/sat/doc/solver.md | 4 -- ortools/sat/samples/binpacking_problem_sat.py | 1 - ortools/sat/samples/bool_or_sample_sat.py | 1 - .../sat/samples/boolean_product_sample_sat.py | 1 - ortools/sat/samples/channeling_sample_sat.py | 1 - .../earliness_tardiness_cost_sample_sat.py | 1 - ortools/sat/samples/interval_sample_sat.py | 1 - ortools/sat/samples/literal_sample_sat.py | 1 - ortools/sat/samples/minimal_jobshop_sat.py | 1 - ortools/sat/samples/multiple_knapsack_sat.py | 1 - ortools/sat/samples/no_overlap_sample_sat.py | 1 - .../samples/optional_interval_sample_sat.py | 1 - .../sat/samples/rabbits_and_pheasants_sat.py | 1 - ortools/sat/samples/ranking_sample_sat.py | 1 - ortools/sat/samples/reified_sample_sat.py | 1 - .../scheduling_with_calendar_sample_sat.py | 1 - .../search_for_all_solutions_sample_sat.py | 1 - ortools/sat/samples/simple_sat_program.py | 1 - .../samples/solution_hinting_sample_sat.py | 1 - ...print_intermediate_solutions_sample_sat.py | 1 - .../solve_with_time_limit_sample_sat.py | 1 - .../sat/samples/step_function_sample_sat.py | 1 - .../stop_after_n_solutions_sample_sat.py | 1 - ortools/sat/sat_solver.h | 6 ++ 35 files changed, 40 insertions(+), 67 deletions(-) diff --git a/ortools/algorithms/samples/Knapsack.java b/ortools/algorithms/samples/Knapsack.java index a18a832e4b..cf8c9563a7 100644 --- a/ortools/algorithms/samples/Knapsack.java +++ b/ortools/algorithms/samples/Knapsack.java @@ -19,7 +19,8 @@ import com.google.ortools.algorithms.KnapsackSolver; import java.util.ArrayList; // [END import] -/** Sample showing how to model using the knapsack solver. +/** + * Sample showing how to model using the knapsack solver. */ public class Knapsack { private Knapsack() {} diff --git a/ortools/constraint_solver/doc/routing_svg.py b/ortools/constraint_solver/doc/routing_svg.py index 7469575516..934602bb80 100755 --- a/ortools/constraint_solver/doc/routing_svg.py +++ b/ortools/constraint_solver/doc/routing_svg.py @@ -19,6 +19,7 @@ from ortools.constraint_solver import pywrapcp from ortools.constraint_solver import routing_enums_pb2 # [END import] + # [START data_model] class DataModel(object): # pylint: disable=too-many-instance-attributes """Stores the data for the problem.""" @@ -571,7 +572,7 @@ class SVGPrinter(object): # pylint: disable=too-many-instance-attributes # First print route previous_loc_idx = None for loc_idx in route: - if previous_loc_idx != None and previous_loc_idx != loc_idx: + if previous_loc_idx and previous_loc_idx != loc_idx: self._svg.draw_polyline(self._data.locations[previous_loc_idx], self._data.locations[loc_idx], self._stroke_width, color, colorname) diff --git a/ortools/java/com/google/ortools/sat/CpModel.java b/ortools/java/com/google/ortools/sat/CpModel.java index cfea396749..d69150ae1a 100644 --- a/ortools/java/com/google/ortools/sat/CpModel.java +++ b/ortools/java/com/google/ortools/sat/CpModel.java @@ -23,7 +23,6 @@ import com.google.ortools.sat.CumulativeConstraintProto; import com.google.ortools.sat.DecisionStrategyProto; import com.google.ortools.sat.ElementConstraintProto; import com.google.ortools.sat.IntegerArgumentProto; -import com.google.ortools.sat.IntegerVariableProto; import com.google.ortools.sat.InverseConstraintProto; import com.google.ortools.sat.LinearConstraintProto; import com.google.ortools.sat.NoOverlap2DConstraintProto; @@ -640,49 +639,52 @@ public final class CpModel { /** Adds {@code target == num / denom}, rounded towards 0. */ public Constraint addDivisionEquality(IntVar target, IntVar num, IntVar denom) { Constraint ct = new Constraint(modelBuilder); - IntegerArgumentProto.Builder intDiv = ct.getBuilder().getIntDivBuilder(); - intDiv.setTarget(target.getIndex()); - intDiv.addVars(num.getIndex()); - intDiv.addVars(denom.getIndex()); + ct.getBuilder() + .getIntDivBuilder() + .setTarget(target.getIndex()) + .addVars(num.getIndex()) + .addVars(denom.getIndex()); return ct; } /** Adds {@code target == Abs(var)}. */ public Constraint addAbsEquality(IntVar target, IntVar var) { Constraint ct = new Constraint(modelBuilder); - IntegerArgumentProto.Builder intMax = ct.getBuilder() - .getIntMaxBuilder() - .setTarget(target.getIndex()) - .addVars(var.getIndex()) - .addVars(-var.getIndex() - 1); + ct.getBuilder() + .getIntMaxBuilder() + .setTarget(target.getIndex()) + .addVars(var.getIndex()) + .addVars(-var.getIndex() - 1); return ct; } /** Adds {@code target == var % mod}. */ public Constraint addModuloEquality(IntVar target, IntVar var, IntVar mod) { Constraint ct = new Constraint(modelBuilder); - IntegerArgumentProto.Builder intMod = ct.getBuilder().getIntModBuilder(); - intMod.setTarget(target.getIndex()); - intMod.addVars(var.getIndex()); - intMod.addVars(mod.getIndex()); + ct.getBuilder() + .getIntModBuilder() + .setTarget(target.getIndex()) + .addVars(var.getIndex()) + .addVars(mod.getIndex()); return ct; } /** Adds {@code target == var % mod}. */ public Constraint addModuloEquality(IntVar target, IntVar var, long mod) { Constraint ct = new Constraint(modelBuilder); - IntegerArgumentProto.Builder intMod = ct.getBuilder().getIntModBuilder(); - intMod.setTarget(target.getIndex()); - intMod.addVars(var.getIndex()); - intMod.addVars(indexFromConstant(mod)); + ct.getBuilder() + .getIntModBuilder() + .setTarget(target.getIndex()) + .addVars(var.getIndex()) + .addVars(indexFromConstant(mod)); return ct; } /** Adds {@code target == Product(vars)}. */ public Constraint addProductEquality(IntVar target, IntVar[] vars) { Constraint ct = new Constraint(modelBuilder); - IntegerArgumentProto.Builder intProd = ct.getBuilder().getIntProdBuilder(); - intProd.setTarget(target.getIndex()); + IntegerArgumentProto.Builder intProd = + ct.getBuilder().getIntProdBuilder().setTarget(target.getIndex()); for (IntVar var : vars) { intProd.addVars(var.getIndex()); } @@ -960,8 +962,7 @@ public final class CpModel { public void minimize(LinearExpr expr) { CpObjectiveProto.Builder obj = modelBuilder.getObjectiveBuilder(); for (int i = 0; i < expr.numElements(); ++i) { - obj.addVars(expr.getVariable(i).getIndex()); - obj.addCoeffs(expr.getCoefficient(i)); + obj.addVars(expr.getVariable(i).getIndex()).addCoeffs(expr.getCoefficient(i)); } } @@ -969,8 +970,7 @@ public final class CpModel { public void maximize(LinearExpr expr) { CpObjectiveProto.Builder obj = modelBuilder.getObjectiveBuilder(); for (int i = 0; i < expr.numElements(); ++i) { - obj.addVars(expr.getVariable(i).getIndex()); - obj.addCoeffs(-expr.getCoefficient(i)); + obj.addVars(expr.getVariable(i).getIndex()).addCoeffs(-expr.getCoefficient(i)); } obj.setScalingFactor(-1.0); } @@ -985,8 +985,7 @@ public final class CpModel { for (IntVar var : variables) { ds.addVariables(var.getIndex()); } - ds.setVariableSelectionStrategy(varStr); - ds.setDomainReductionStrategy(domStr); + ds.setVariableSelectionStrategy(varStr).setDomainReductionStrategy(domStr); } /** Returns some statistics on model as a string. */ @@ -1016,9 +1015,7 @@ public final class CpModel { int indexFromConstant(long constant) { int index = modelBuilder.getVariablesCount(); - IntegerVariableProto.Builder cst = modelBuilder.addVariablesBuilder(); - cst.addDomain(constant); - cst.addDomain(constant); + modelBuilder.addVariablesBuilder().addDomain(constant).addDomain(constant); return index; } diff --git a/ortools/linear_solver/samples/linear_programming_example.py b/ortools/linear_solver/samples/linear_programming_example.py index 2d4431b32b..0bf6809795 100644 --- a/ortools/linear_solver/samples/linear_programming_example.py +++ b/ortools/linear_solver/samples/linear_programming_example.py @@ -14,7 +14,6 @@ # [START program] # [START import] from ortools.linear_solver import pywraplp - # [END import] diff --git a/ortools/sat/BUILD b/ortools/sat/BUILD index 1b203991d2..27b4002157 100644 --- a/ortools/sat/BUILD +++ b/ortools/sat/BUILD @@ -85,7 +85,6 @@ cc_library( ) cc_library( - name = "synchronization", srcs = ["synchronization.cc"], hdrs = ["synchronization.h"], diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 40034f8960..40f9beb90b 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -1233,6 +1233,10 @@ bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto* ct) { // constraint by expanding its rhs. context_->UpdateRuleStats( "linear: singleton column in equality and in objective."); + + // TODO(b/173280761): Prevent potential overflow here. Even if coeff + // divide objective_coeff, we might add big coefficients to the objective + // this way which will break our linear expression overflow precondition. context_->SubstituteVariableInObjective(var, coeff, *ct); rhs = new_rhs; index_to_erase.insert(i); diff --git a/ortools/sat/doc/README.md b/ortools/sat/doc/README.md index a564448288..b586c60d68 100644 --- a/ortools/sat/doc/README.md +++ b/ortools/sat/doc/README.md @@ -45,7 +45,6 @@ The Python interface to the CP-SAT solver is implemented using two classes. ```python """Simple solve.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/doc/boolean_logic.md b/ortools/sat/doc/boolean_logic.md index efcf60d901..713abb8922 100644 --- a/ortools/sat/doc/boolean_logic.md +++ b/ortools/sat/doc/boolean_logic.md @@ -252,7 +252,6 @@ then is written as Or(not b, x) and Or(not b, not y). ```python """Simple model with a reified constraint.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/doc/integer_arithmetic.md b/ortools/sat/doc/integer_arithmetic.md index 8248e440c6..e3a341f77e 100644 --- a/ortools/sat/doc/integer_arithmetic.md +++ b/ortools/sat/doc/integer_arithmetic.md @@ -149,7 +149,6 @@ rabbits and pheasants are there? ```python """Rabbits and Pheasants quizz.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/doc/model.md b/ortools/sat/doc/model.md index e657eb1be9..49827967ed 100644 --- a/ortools/sat/doc/model.md +++ b/ortools/sat/doc/model.md @@ -87,7 +87,6 @@ Some remarks: ```python """Code sample that solves a model using solution hinting.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/doc/scheduling.md b/ortools/sat/doc/scheduling.md index 4df9f35950..4ceafec40f 100644 --- a/ortools/sat/doc/scheduling.md +++ b/ortools/sat/doc/scheduling.md @@ -178,7 +178,6 @@ understand these presence literals, and correctly ignore inactive intervals. ```python """Code sample to demonstrates how to build an optional interval.""" - from ortools.sat.python import cp_model @@ -307,7 +306,6 @@ weekends, making the final day as early as possible. ```python """Code sample to demonstrate how to build a NoOverlap constraint.""" - from ortools.sat.python import cp_model @@ -602,7 +600,6 @@ number of other intervals that precede it. ```python """Code sample to demonstrates how to rank intervals.""" - from ortools.sat.python import cp_model @@ -1246,7 +1243,6 @@ The following code displays: ```python """Code sample to demonstrate how an interval can span across a break.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/doc/solver.md b/ortools/sat/doc/solver.md index 81d5993521..90904bd825 100644 --- a/ortools/sat/doc/solver.md +++ b/ortools/sat/doc/solver.md @@ -42,7 +42,6 @@ solver. The most useful one is the time limit. ```python """Solves a problem with a time limit.""" - from ortools.sat.python import cp_model @@ -217,7 +216,6 @@ The exact implementation depends on the target language. ```python """Solves an optimization problem and displays all intermediate solutions.""" - from ortools.sat.python import cp_model @@ -463,7 +461,6 @@ To search for all solutions, use the SearchForAllSolutions method. ```python """Code sample that solves a model and displays all solutions.""" - from ortools.sat.python import cp_model @@ -700,7 +697,6 @@ CpSolverSolutionCallback.OnSolutionCallback(). ```python """Code sample that solves a model and displays a small number of solutions.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/binpacking_problem_sat.py b/ortools/sat/samples/binpacking_problem_sat.py index 2bde2c35eb..455976e136 100644 --- a/ortools/sat/samples/binpacking_problem_sat.py +++ b/ortools/sat/samples/binpacking_problem_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Solves a binpacking problem using the CP-SAT solver.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/bool_or_sample_sat.py b/ortools/sat/samples/bool_or_sample_sat.py index d7bc928297..45ffc80acf 100644 --- a/ortools/sat/samples/bool_or_sample_sat.py +++ b/ortools/sat/samples/bool_or_sample_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Code sample to demonstrates a simple Boolean constraint.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/boolean_product_sample_sat.py b/ortools/sat/samples/boolean_product_sample_sat.py index 05a6e1b8c5..149ba2334e 100644 --- a/ortools/sat/samples/boolean_product_sample_sat.py +++ b/ortools/sat/samples/boolean_product_sample_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Code sample that encodes the product of two Boolean variables.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/channeling_sample_sat.py b/ortools/sat/samples/channeling_sample_sat.py index ca30e39719..448a3e3b94 100644 --- a/ortools/sat/samples/channeling_sample_sat.py +++ b/ortools/sat/samples/channeling_sample_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Link integer constraints together.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/earliness_tardiness_cost_sample_sat.py b/ortools/sat/samples/earliness_tardiness_cost_sample_sat.py index cc30a2e679..b7b172cb86 100644 --- a/ortools/sat/samples/earliness_tardiness_cost_sample_sat.py +++ b/ortools/sat/samples/earliness_tardiness_cost_sample_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Encodes an convex piecewise linear function.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/interval_sample_sat.py b/ortools/sat/samples/interval_sample_sat.py index 096b571031..38460000af 100644 --- a/ortools/sat/samples/interval_sample_sat.py +++ b/ortools/sat/samples/interval_sample_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Code sample to demonstrates how to build an interval.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/literal_sample_sat.py b/ortools/sat/samples/literal_sample_sat.py index 831a7e3692..2e49f31da3 100644 --- a/ortools/sat/samples/literal_sample_sat.py +++ b/ortools/sat/samples/literal_sample_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Code sample to demonstrate Boolean variable and literals.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/minimal_jobshop_sat.py b/ortools/sat/samples/minimal_jobshop_sat.py index 32c47171ac..0992660d09 100644 --- a/ortools/sat/samples/minimal_jobshop_sat.py +++ b/ortools/sat/samples/minimal_jobshop_sat.py @@ -13,7 +13,6 @@ """Minimal jobshop example.""" # [START program] - import collections # [START model] diff --git a/ortools/sat/samples/multiple_knapsack_sat.py b/ortools/sat/samples/multiple_knapsack_sat.py index 36fe3ff7f6..35d22a77c9 100644 --- a/ortools/sat/samples/multiple_knapsack_sat.py +++ b/ortools/sat/samples/multiple_knapsack_sat.py @@ -14,7 +14,6 @@ """Solves a multiple knapsack problem using the CP-SAT solver.""" # [START import] - from ortools.sat.python import cp_model # [END import] diff --git a/ortools/sat/samples/no_overlap_sample_sat.py b/ortools/sat/samples/no_overlap_sample_sat.py index 659a3bcb8a..bc459e0286 100644 --- a/ortools/sat/samples/no_overlap_sample_sat.py +++ b/ortools/sat/samples/no_overlap_sample_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Code sample to demonstrate how to build a NoOverlap constraint.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/optional_interval_sample_sat.py b/ortools/sat/samples/optional_interval_sample_sat.py index 6cc1e094a9..f0ea7a2e21 100644 --- a/ortools/sat/samples/optional_interval_sample_sat.py +++ b/ortools/sat/samples/optional_interval_sample_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Code sample to demonstrates how to build an optional interval.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/rabbits_and_pheasants_sat.py b/ortools/sat/samples/rabbits_and_pheasants_sat.py index 2772dcb03b..5ce4ff9479 100644 --- a/ortools/sat/samples/rabbits_and_pheasants_sat.py +++ b/ortools/sat/samples/rabbits_and_pheasants_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Rabbits and Pheasants quizz.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/ranking_sample_sat.py b/ortools/sat/samples/ranking_sample_sat.py index 0691df57ca..fcdc64dfab 100644 --- a/ortools/sat/samples/ranking_sample_sat.py +++ b/ortools/sat/samples/ranking_sample_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Code sample to demonstrates how to rank intervals.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/reified_sample_sat.py b/ortools/sat/samples/reified_sample_sat.py index e13751a49a..540a0991cb 100644 --- a/ortools/sat/samples/reified_sample_sat.py +++ b/ortools/sat/samples/reified_sample_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Simple model with a reified constraint.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/scheduling_with_calendar_sample_sat.py b/ortools/sat/samples/scheduling_with_calendar_sample_sat.py index 9da45ce203..bfc62dee56 100644 --- a/ortools/sat/samples/scheduling_with_calendar_sample_sat.py +++ b/ortools/sat/samples/scheduling_with_calendar_sample_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Code sample to demonstrate how an interval can span across a break.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/search_for_all_solutions_sample_sat.py b/ortools/sat/samples/search_for_all_solutions_sample_sat.py index ec22830969..2949181c02 100644 --- a/ortools/sat/samples/search_for_all_solutions_sample_sat.py +++ b/ortools/sat/samples/search_for_all_solutions_sample_sat.py @@ -13,7 +13,6 @@ """Code sample that solves a model and displays all solutions.""" # [START program] - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/simple_sat_program.py b/ortools/sat/samples/simple_sat_program.py index b5a76de3f6..f949e39925 100644 --- a/ortools/sat/samples/simple_sat_program.py +++ b/ortools/sat/samples/simple_sat_program.py @@ -13,7 +13,6 @@ """Simple solve.""" # [START program] - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/solution_hinting_sample_sat.py b/ortools/sat/samples/solution_hinting_sample_sat.py index a15215f21b..eeefd4912f 100644 --- a/ortools/sat/samples/solution_hinting_sample_sat.py +++ b/ortools/sat/samples/solution_hinting_sample_sat.py @@ -13,7 +13,6 @@ """Code sample that solves a model using solution hinting.""" # [START program] - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.py b/ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.py index bba2005c3d..8168060299 100644 --- a/ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.py +++ b/ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.py @@ -13,7 +13,6 @@ """Solves an optimization problem and displays all intermediate solutions.""" # [START program] - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/solve_with_time_limit_sample_sat.py b/ortools/sat/samples/solve_with_time_limit_sample_sat.py index 2e9f4630ee..e77467f423 100644 --- a/ortools/sat/samples/solve_with_time_limit_sample_sat.py +++ b/ortools/sat/samples/solve_with_time_limit_sample_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Solves a problem with a time limit.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/step_function_sample_sat.py b/ortools/sat/samples/step_function_sample_sat.py index 0469831fef..b482292f64 100644 --- a/ortools/sat/samples/step_function_sample_sat.py +++ b/ortools/sat/samples/step_function_sample_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Implements a step function.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/samples/stop_after_n_solutions_sample_sat.py b/ortools/sat/samples/stop_after_n_solutions_sample_sat.py index 2192e4588e..c44ce44ca6 100644 --- a/ortools/sat/samples/stop_after_n_solutions_sample_sat.py +++ b/ortools/sat/samples/stop_after_n_solutions_sample_sat.py @@ -12,7 +12,6 @@ # limitations under the License. """Code sample that solves a model and displays a small number of solutions.""" - from ortools.sat.python import cp_model diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h index db3dd158db..75cc14be86 100644 --- a/ortools/sat/sat_solver.h +++ b/ortools/sat/sat_solver.h @@ -430,6 +430,12 @@ class SatSolver { // Simplifies the problem when new variables are assigned at level 0. void ProcessNewlyFixedVariables(); + int64 NumFixedVariables() const { + if (!decisions_.empty()) return decisions_[0].trail_index; + CHECK_EQ(CurrentDecisionLevel(), 0); + return trail_->Index(); + } + private: // Calls Propagate() and returns true if no conflict occurred. Otherwise, // learns the conflict, backtracks, enqueues the consequence of the learned