From 53863acd623108b2c918f092b4bd07c9a64d8abf Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Fri, 14 Sep 2018 13:24:34 +0200 Subject: [PATCH] [SAT/Java] ILiteral -> Literal; [SAT] fix a few english mistakes --- .../com/google/ortools/sat/Constraint.java | 6 +-- ortools/com/google/ortools/sat/CpModel.java | 38 +++++++++---------- ortools/com/google/ortools/sat/CpSolver.java | 2 +- .../ortools/sat/CpSolverSolutionCallback.java | 2 +- ortools/com/google/ortools/sat/IntVar.java | 4 +- .../sat/{ILiteral.java => Literal.java} | 4 +- .../ortools/sat/NotBooleanVariable.java | 6 +-- ortools/sat/circuit.h | 3 +- ortools/sat/clause.cc | 2 +- ortools/sat/cp_model.proto | 2 +- ortools/sat/cp_model_presolve.cc | 10 ++--- ortools/sat/cp_model_solver.cc | 6 +-- ortools/sat/doc/boolean_logic.md | 16 ++++---- ortools/sat/doc/scheduling.md | 16 ++++---- ortools/sat/drat_checker.h | 2 +- ortools/sat/integer.cc | 8 ++-- ortools/sat/integer.h | 2 +- ortools/sat/lp_utils.cc | 4 +- ortools/sat/optimization.cc | 8 ++-- ortools/sat/pb_constraint.cc | 2 +- ortools/sat/pb_constraint.h | 6 +-- ortools/sat/samples/BoolOrSample.java | 4 +- ortools/sat/samples/LiteralSample.java | 4 +- .../sat/samples/OptionalIntervalSample.java | 4 +- ortools/sat/samples/RankingSample.java | 12 +++--- ortools/sat/samples/ReifiedSample.java | 8 ++-- ortools/sat/sat_parameters.proto | 2 +- ortools/sat/sat_solver.cc | 10 ++--- ortools/sat/sat_solver.h | 8 ++-- ortools/sat/theta_tree.h | 2 +- ortools/sat/util.h | 2 +- 31 files changed, 102 insertions(+), 103 deletions(-) rename ortools/com/google/ortools/sat/{ILiteral.java => Literal.java} (94%) diff --git a/ortools/com/google/ortools/sat/Constraint.java b/ortools/com/google/ortools/sat/Constraint.java index 446e78a4c8..e503eb6f6c 100644 --- a/ortools/com/google/ortools/sat/Constraint.java +++ b/ortools/com/google/ortools/sat/Constraint.java @@ -29,13 +29,13 @@ public class Constraint { } /** Adds a literal to the constraint. */ - public void onlyEnforceIf(ILiteral lit) { + public void onlyEnforceIf(Literal lit) { constraintBuilder.addEnforcementLiteral(lit.getIndex()); } /** Adds a list of literals to the constraint. */ - public void onlyEnforceIf(ILiteral[] lits) { - for (ILiteral lit : lits) { + public void onlyEnforceIf(Literal[] lits) { + for (Literal lit : lits) { constraintBuilder.addEnforcementLiteral(lit.getIndex()); } } diff --git a/ortools/com/google/ortools/sat/CpModel.java b/ortools/com/google/ortools/sat/CpModel.java index ef47293c16..302e0fc172 100644 --- a/ortools/com/google/ortools/sat/CpModel.java +++ b/ortools/com/google/ortools/sat/CpModel.java @@ -107,38 +107,38 @@ public class CpModel { // Boolean Constraints. /** Adds {@code Or(literals) == true}. */ - public Constraint addBoolOr(ILiteral[] literals) { + public Constraint addBoolOr(Literal[] literals) { Constraint ct = new Constraint(modelBuilder); BoolArgumentProto.Builder boolOr = ct.builder().getBoolOrBuilder(); - for (ILiteral lit : literals) { + for (Literal lit : literals) { boolOr.addLiterals(lit.getIndex()); } return ct; } /** Adds {@code And(literals) == true}. */ - public Constraint addBoolAnd(ILiteral[] literals) { + public Constraint addBoolAnd(Literal[] literals) { Constraint ct = new Constraint(modelBuilder); BoolArgumentProto.Builder boolOr = ct.builder().getBoolAndBuilder(); - for (ILiteral lit : literals) { + for (Literal lit : literals) { boolOr.addLiterals(lit.getIndex()); } return ct; } /** Adds {@code XOr(literals) == true}. */ - public Constraint addBoolXor(ILiteral[] literals) { + public Constraint addBoolXor(Literal[] literals) { Constraint ct = new Constraint(modelBuilder); BoolArgumentProto.Builder boolOr = ct.builder().getBoolXorBuilder(); - for (ILiteral lit : literals) { + for (Literal lit : literals) { boolOr.addLiterals(lit.getIndex()); } return ct; } /** Adds {@code a => b}. */ - public Constraint addImplication(ILiteral a, ILiteral b) { - return addBoolOr(new ILiteral[] {a.not(), b}); + public Constraint addImplication(Literal a, Literal b) { + return addBoolOr(new Literal[] {a.not(), b}); } // Linear constraints. @@ -448,7 +448,7 @@ public class CpModel { * @return an instance of the Constraint class * @throws MismatchedArrayLengths if the arrays have different sizes */ - public Constraint addCircuit(int[] tails, int[] heads, ILiteral[] literals) + public Constraint addCircuit(int[] tails, int[] heads, Literal[] literals) throws MismatchedArrayLengths { if (tails.length != heads.length) { throw new MismatchedArrayLengths("addCircuit", "tails", "heads"); @@ -465,7 +465,7 @@ public class CpModel { for (int h : heads) { circuit.addHeads(h); } - for (ILiteral lit : literals) { + for (Literal lit : literals) { circuit.addLiterals(lit.getIndex()); } return ct; @@ -697,7 +697,7 @@ public class CpModel { } /** Adds {@code var == i + offset <=> booleans[i] == true for all i in [0, booleans.length)}. */ - public void addMapDomain(IntVar var, ILiteral[] booleans, long offset) { + public void addMapDomain(IntVar var, Literal[] booleans, long offset) { for (int i = 0; i < booleans.length; ++i) { addEquality(var, offset + i).onlyEnforceIf(booleans[i]); addDifferent(var, offset + i).onlyEnforceIf(booleans[i].not()); @@ -845,7 +845,7 @@ public class CpModel { * @return an IntervalVar object */ public IntervalVar newOptionalIntervalVar( - IntVar start, IntVar size, IntVar end, ILiteral isPresent, String name) { + IntVar start, IntVar size, IntVar end, Literal isPresent, String name) { return new IntervalVar( modelBuilder, start.getIndex(), @@ -858,10 +858,10 @@ public class CpModel { /** * Creates an optional interval with a fixed end. * - * @see #newOptionalIntervalVar(IntVar, IntVar, IntVar, ILiteral, String) newOptionalIntervalVar + * @see #newOptionalIntervalVar(IntVar, IntVar, IntVar, Literal, String) newOptionalIntervalVar */ public IntervalVar newOptionalIntervalVar( - IntVar start, IntVar size, long end, ILiteral isPresent, String name) { + IntVar start, IntVar size, long end, Literal isPresent, String name) { return new IntervalVar( modelBuilder, start.getIndex(), @@ -874,10 +874,10 @@ public class CpModel { /** * Creates an optional interval with a fixed size. * - * @see #newOptionalIntervalVar(IntVar, IntVar, IntVar, ILiteral, String) newOptionalIntervalVar + * @see #newOptionalIntervalVar(IntVar, IntVar, IntVar, Literal, String) newOptionalIntervalVar */ public IntervalVar newOptionalIntervalVar( - IntVar start, long size, IntVar end, ILiteral isPresent, String name) { + IntVar start, long size, IntVar end, Literal isPresent, String name) { return new IntervalVar( modelBuilder, start.getIndex(), @@ -889,7 +889,7 @@ public class CpModel { /** Creates an optional interval with a fixed start. */ public IntervalVar newOptionalIntervalVar( - long start, IntVar size, IntVar end, ILiteral isPresent, String name) { + long start, IntVar size, IntVar end, Literal isPresent, String name) { return new IntervalVar( modelBuilder, indexFromConstant(start), @@ -902,10 +902,10 @@ public class CpModel { /** * Creates an optional fixed interval from start and size. * - * @see #newOptionalIntervalVar(IntVar, IntVar, IntVar, ILiteral, String) newOptionalIntervalVar + * @see #newOptionalIntervalVar(IntVar, IntVar, IntVar, Literal, String) newOptionalIntervalVar */ public IntervalVar newOptionalFixedInterval( - long start, long size, ILiteral isPresent, String name) { + long start, long size, Literal isPresent, String name) { return new IntervalVar( modelBuilder, indexFromConstant(start), diff --git a/ortools/com/google/ortools/sat/CpSolver.java b/ortools/com/google/ortools/sat/CpSolver.java index cb9fbc3404..05ff66a264 100644 --- a/ortools/com/google/ortools/sat/CpSolver.java +++ b/ortools/com/google/ortools/sat/CpSolver.java @@ -73,7 +73,7 @@ public class CpSolver { } /** Returns the Boolean value of a literal in the last solution found. */ - public Boolean booleanValue(ILiteral var) { + public Boolean booleanValue(Literal var) { int index = var.getIndex(); if (index >= 0) { return solveResponse.getSolution(index) != 0; diff --git a/ortools/com/google/ortools/sat/CpSolverSolutionCallback.java b/ortools/com/google/ortools/sat/CpSolverSolutionCallback.java index 3239252dd4..0782fd7be8 100644 --- a/ortools/com/google/ortools/sat/CpSolverSolutionCallback.java +++ b/ortools/com/google/ortools/sat/CpSolverSolutionCallback.java @@ -44,7 +44,7 @@ public class CpSolverSolutionCallback extends SolutionCallback { } /** Returns the Boolean value of the literal in the current solution. */ - public Boolean booleanValue(ILiteral literal) { + public Boolean booleanValue(Literal literal) { return solutionBooleanValue(literal.getIndex()); } diff --git a/ortools/com/google/ortools/sat/IntVar.java b/ortools/com/google/ortools/sat/IntVar.java index de15fa4985..f3ce46ecb6 100644 --- a/ortools/com/google/ortools/sat/IntVar.java +++ b/ortools/com/google/ortools/sat/IntVar.java @@ -17,7 +17,7 @@ import com.google.ortools.sat.CpModelProto; import com.google.ortools.sat.IntegerVariableProto; /** An integer variable. */ -public class IntVar implements ILiteral { +public class IntVar implements Literal { IntVar(CpModelProto.Builder builder, long lb, long ub, String name) { this.modelBuilder = builder; this.variableIndex = modelBuilder.getVariablesCount(); @@ -87,7 +87,7 @@ public class IntVar implements ILiteral { /** Returns the negation of a boolean variable. */ @Override - public ILiteral not() { + public Literal not() { if (negation_ == null) { negation_ = new NotBooleanVariable(this); } diff --git a/ortools/com/google/ortools/sat/ILiteral.java b/ortools/com/google/ortools/sat/Literal.java similarity index 94% rename from ortools/com/google/ortools/sat/ILiteral.java rename to ortools/com/google/ortools/sat/Literal.java index 5fa67c23b0..7266e780fa 100644 --- a/ortools/com/google/ortools/sat/ILiteral.java +++ b/ortools/com/google/ortools/sat/Literal.java @@ -14,11 +14,11 @@ package com.google.ortools.sat; /** Interface to describe a boolean variable or its negation. */ -public interface ILiteral { +public interface Literal { int getIndex(); /** Returns the Boolean negation of the current literal. */ - public ILiteral not(); + public Literal not(); /** Returns a short string to describe the literal. */ public String getShortString(); diff --git a/ortools/com/google/ortools/sat/NotBooleanVariable.java b/ortools/com/google/ortools/sat/NotBooleanVariable.java index 8700aa55db..f60c94ce3c 100644 --- a/ortools/com/google/ortools/sat/NotBooleanVariable.java +++ b/ortools/com/google/ortools/sat/NotBooleanVariable.java @@ -14,10 +14,10 @@ package com.google.ortools.sat; /** - * The negation of a boolean variable. This class should not be used directly, ILiteral must be used + * The negation of a boolean variable. This class should not be used directly, Literal must be used * instead. */ -public class NotBooleanVariable implements ILiteral { +public class NotBooleanVariable implements Literal { public NotBooleanVariable(IntVar boolvar) { boolVar = boolvar; } @@ -30,7 +30,7 @@ public class NotBooleanVariable implements ILiteral { /** Returns the negation of this literal. */ @Override - public ILiteral not() { + public Literal not() { return boolVar; } diff --git a/ortools/sat/circuit.h b/ortools/sat/circuit.h index 2a53c50c0e..bc860f445d 100644 --- a/ortools/sat/circuit.h +++ b/ortools/sat/circuit.h @@ -167,8 +167,7 @@ class CircuitCoveringPropagator : PropagatorInterface, ReversibleInterface { // ============================================================================ // Changes the node indices so that we get a graph in [0, num_nodes) where every -// nodes has at least one incoming or outgoing arcs. Returns the number of -// nodes. +// node has at least one incoming or outgoing arc. Returns the number of nodes. int ReindexArcs(std::vector* tails, std::vector* heads, std::vector* literals); diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc index 05ce16dd70..797e0e2709 100644 --- a/ortools/sat/clause.cc +++ b/ortools/sat/clause.cc @@ -365,7 +365,7 @@ bool BinaryImplicationGraph::PropagateOnTrue(Literal true_literal, // enqueued after the true_literal on the trail. This property is // important for ComputeFirstUIPConflict() to work since it needs the // trail order to be a topological order for the deduction graph. - // But the performance where not too good... + // But the performance was not too good... continue; } diff --git a/ortools/sat/cp_model.proto b/ortools/sat/cp_model.proto index d68a89d0d4..615478a322 100644 --- a/ortools/sat/cp_model.proto +++ b/ortools/sat/cp_model.proto @@ -514,7 +514,7 @@ message CpSolverResponse { // If the problem has some variables that are not fixed at the end of the // search (because of a particular search strategy in the CpModelProto) then // this will be used instead of filling the solution above. The two fields - // will then contains the lower and upper bound of each variable as they where + // will then contains the lower and upper bounds of each variable as they were // when the best "solution" was found. repeated int64 solution_lower_bounds = 18; repeated int64 solution_upper_bounds = 19; diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 5557227e33..91811134a3 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -201,7 +201,7 @@ struct PresolveContext { } // Because we always replace equivalent literals before preprocessing a - // constraint, we should never run into a case where one of the literal is + // constraint, we should never run into a case where one of the literals is // fixed but the other is not updated. So this can be called without the need // to keep around the constraints that detected this relation. void AddBooleanEqualityRelation(int ref_a, int ref_b) { @@ -616,7 +616,7 @@ bool PresolveIntProd(ConstraintProto* ct, PresolveContext* context) { } } - // For now, we only presolve the case where all variable are Booleans. + // For now, we only presolve the case where all variables are Booleans. const int target_ref = ct->int_prod().target(); if (!RefIsPositive(target_ref)) return false; for (const int var : ct->int_prod().vars()) { @@ -2328,10 +2328,10 @@ void PresolveCpModel(bool log_info, CpModelProto* presolved_model, // Stats and checks. if (log_info) { LOG(INFO) << "- " << context.affine_relations.NumRelations() - << " affine relations where detected. " << num_affine_relations - << " where kept."; + << " affine relations were detected. " << num_affine_relations + << " were kept."; LOG(INFO) << "- " << context.var_equiv_relations.NumRelations() - << " variable equivalence relations where detected."; + << " variable equivalence relations were detected."; std::map sorted_rules(context.stats_by_rule_name.begin(), context.stats_by_rule_name.end()); for (const auto& entry : sorted_rules) { diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 7dc724290b..4c6a827819 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -293,7 +293,7 @@ class ModelWithMapping { // Used to return a feasible solution for the unused variables. std::vector lower_bounds_; - // Set of constraints to ignore because they where already dealt with by + // Set of constraints to ignore because they were already dealt with by // ExtractEncoding(). std::unordered_set ct_to_ignore_; }; @@ -2455,7 +2455,7 @@ CpSolverResponse SolveCpModelInternal( } } if (num_ignored_constraints > 0) { - VLOG(2) << num_ignored_constraints << " constraints where skipped."; + VLOG(2) << num_ignored_constraints << " constraints were skipped."; } if (!unsupported_types.empty()) { VLOG(1) << "There is unsuported constraints types in this model: "; @@ -2552,7 +2552,7 @@ CpSolverResponse SolveCpModelInternal( } // Note that we do one last propagation at level zero once all the constraints - // where added. + // were added. model->GetOrCreate()->Propagate(); // Probing Boolean variables. Because we don't have a good deterministic time diff --git a/ortools/sat/doc/boolean_logic.md b/ortools/sat/doc/boolean_logic.md index 97e9062cd5..47c52724e7 100644 --- a/ortools/sat/doc/boolean_logic.md +++ b/ortools/sat/doc/boolean_logic.md @@ -79,8 +79,8 @@ int main() { ```java import com.google.ortools.sat.CpModel; -import com.google.ortools.sat.ILiteral; import com.google.ortools.sat.IntVar; +import com.google.ortools.sat.Literal; public class LiteralSample { @@ -89,7 +89,7 @@ public class LiteralSample { public static void main(String[] args) throws Exception { CpModel model = new CpModel(); IntVar x = model.newBoolVar("x"); - ILiteral notX = x.not(); + Literal notX = x.not(); System.out.println(notX.getShortString()); } } @@ -201,8 +201,8 @@ int main() { ```java import com.google.ortools.sat.CpModel; -import com.google.ortools.sat.ILiteral; import com.google.ortools.sat.IntVar; +import com.google.ortools.sat.Literal; public class BoolOrSample { @@ -212,7 +212,7 @@ public class BoolOrSample { CpModel model = new CpModel(); IntVar x = model.newBoolVar("x"); IntVar y = model.newBoolVar("y"); - model.addBoolOr(new ILiteral[] {x, y.not()}); + model.addBoolOr(new Literal[] {x, y.not()}); } } ``` @@ -356,8 +356,8 @@ int main() { ```java import com.google.ortools.sat.CpModel; -import com.google.ortools.sat.ILiteral; import com.google.ortools.sat.IntVar; +import com.google.ortools.sat.Literal; /** * Reification is the action of associating a Boolean variable to a constraint. This boolean @@ -381,15 +381,15 @@ public class ReifiedSample { IntVar b = model.newBoolVar("b"); // Version 1: a half-reified boolean and. - model.addBoolAnd(new ILiteral[] {x, y.not()}).onlyEnforceIf(b); + model.addBoolAnd(new Literal[] {x, y.not()}).onlyEnforceIf(b); // Version 2: implications. model.addImplication(b, x); model.addImplication(b, y.not()); // Version 3: boolean or. - model.addBoolOr(new ILiteral[] {b.not(), x}); - model.addBoolOr(new ILiteral[] {b.not(), y.not()}); + model.addBoolOr(new Literal[] {b.not(), x}); + model.addBoolOr(new Literal[] {b.not(), y.not()}); } } ``` diff --git a/ortools/sat/doc/scheduling.md b/ortools/sat/doc/scheduling.md index 0f3d365a0d..e4b7cc6b85 100644 --- a/ortools/sat/doc/scheduling.md +++ b/ortools/sat/doc/scheduling.md @@ -251,9 +251,9 @@ int main() { ```java import com.google.ortools.sat.CpModel; -import com.google.ortools.sat.ILiteral; import com.google.ortools.sat.IntVar; import com.google.ortools.sat.IntervalVar; +import com.google.ortools.sat.Literal; public class OptionalIntervalSample { @@ -266,7 +266,7 @@ public class OptionalIntervalSample { IntVar endVar = model.newIntVar(0, horizon, "end"); // Java code supports IntVar or integer constants in intervals. int duration = 10; - ILiteral presence = model.newBoolVar("presence"); + Literal presence = model.newBoolVar("presence"); IntervalVar interval = model.newOptionalIntervalVar(startVar, duration, endVar, presence, "interval"); @@ -1063,9 +1063,9 @@ int main() { import com.google.ortools.sat.CpSolverStatus; import com.google.ortools.sat.CpModel; import com.google.ortools.sat.CpSolver; -import com.google.ortools.sat.ILiteral; import com.google.ortools.sat.IntVar; import com.google.ortools.sat.IntervalVar; +import com.google.ortools.sat.Literal; import java.util.ArrayList; import java.util.List; @@ -1077,11 +1077,11 @@ public class RankingSample { static { System.loadLibrary("jniortools"); } - static void rankTasks(CpModel model, IntVar[] starts, ILiteral[] presences, IntVar[] ranks) { + static void rankTasks(CpModel model, IntVar[] starts, Literal[] presences, IntVar[] ranks) { int numTasks = starts.length; // Creates precedence variables between pairs of intervals. - ILiteral[][] precedences = new ILiteral[numTasks][numTasks]; + Literal[][] precedences = new Literal[numTasks][numTasks]; for (int i = 0; i < numTasks; ++i) { for (int j = 0; j < numTasks; ++j) { if (i == j) { @@ -1098,7 +1098,7 @@ public class RankingSample { // Create optional intervals. for (int i = 0; i < numTasks - 1; ++i) { for (int j = i + 1; j < numTasks; ++j) { - List list = new ArrayList<>(); + List list = new ArrayList<>(); list.add(precedences[i][j]); list.add(precedences[j][i]); list.add(presences[i].not()); @@ -1112,7 +1112,7 @@ public class RankingSample { // The following boolOr will enforce that for any two intervals: // i precedes j or j precedes i or at least one interval is not // performed. - model.addBoolOr(list.toArray(new ILiteral[0])); + model.addBoolOr(list.toArray(new Literal[0])); // For efficiency, we add a redundant constraint declaring that only one of i precedes j and // j precedes i are true. This will speed up the solve because the reason of this // propagation is shorter that using interval bounds is true. @@ -1144,7 +1144,7 @@ public class RankingSample { IntVar[] starts = new IntVar[numTasks]; IntVar[] ends = new IntVar[numTasks]; IntervalVar[] intervals = new IntervalVar[numTasks]; - ILiteral[] presences = new ILiteral[numTasks]; + Literal[] presences = new Literal[numTasks]; IntVar[] ranks = new IntVar[numTasks]; IntVar trueVar = model.newConstant(1); diff --git a/ortools/sat/drat_checker.h b/ortools/sat/drat_checker.h index a1e4558725..02a89ee5de 100644 --- a/ortools/sat/drat_checker.h +++ b/ortools/sat/drat_checker.h @@ -203,7 +203,7 @@ class DratChecker { ClauseIndex source_clause_index); // Marks the given clause as needed to check the DRAT proof, as well as the - // other clauses which where used to check this clause (these are found from + // other clauses which were used to check this clause (these are found from // 'unit_stack_', containing the clauses that became unit in // AssignAndPropagate, and from 'assignment_source_', containing for each // variable the clause that caused its assignment). diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc index 20442da774..debfbc8caf 100644 --- a/ortools/sat/integer.cc +++ b/ortools/sat/integer.cc @@ -899,9 +899,9 @@ bool IntegerTrail::Enqueue(IntegerLiteral i_lit, return false; } else { // Note(user): We never make the bound of an optional literal cross. We - // used to have a bug where we propagated these bound and their associated - // literal, and we where reaching a conflict while propagating the - // associated literal instead of setting is_ignored below to false. + // used to have a bug where we propagated these bounds and their + // associated literals, and we were reaching a conflict while propagating + // the associated literal instead of setting is_ignored below to false. const Literal is_ignored = Literal(is_ignored_literals_[var]); if (integer_search_levels_.empty()) { trail_->EnqueueWithUnitReason(is_ignored); @@ -988,7 +988,7 @@ IntegerTrail::Dependencies(int trail_index) const { // // To detect if we already did the computation, we store the negated index. // Note that we will redo the computation in the corner case where all the - // given IntegerLiteral turn out to be assigned at level zero. + // given IntegerLiterals turn out to be assigned at level zero. // // TODO(user): We could check that the same IntegerVariable never appear // twice. And if it does the one with the lowest bound could be removed. diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index 188022ee32..ccd9a2c20a 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -787,7 +787,7 @@ class PropagatorInterface { // updated many times or if different watched literals have the same // watch_index. // - At level zero, it will not contain any indices associated with literals - // that where already fixed when the propagator was registered. Only the + // that were already fixed when the propagator was registered. Only the // indices of the literals modified after the registration will be present. virtual bool IncrementalPropagate(const std::vector& watch_indices) { LOG(FATAL) << "Not implemented."; diff --git a/ortools/sat/lp_utils.cc b/ortools/sat/lp_utils.cc index 7e2ce84934..56474cb540 100644 --- a/ortools/sat/lp_utils.cc +++ b/ortools/sat/lp_utils.cc @@ -98,10 +98,10 @@ bool ConvertMPModelProtoToCpModelProto(const MPModelProto& mp_model, } LOG_IF(WARNING, num_truncated_bounds > 0) - << num_truncated_bounds << " bounds where truncated to " + << num_truncated_bounds << " bounds were truncated to " << kMaxVariableBound << "."; LOG_IF(WARNING, num_small_domains > 0) - << num_small_domains << " continuous variable domain with less than " + << num_small_domains << " continuous variable domain with fewer than " << kSmallDomainSize << " values."; // Variables needed to scale the double coefficients into int64. diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc index 31304e6556..aa9369697d 100644 --- a/ortools/sat/optimization.cc +++ b/ortools/sat/optimization.cc @@ -581,7 +581,7 @@ SatSolver::Status SolveWithWPM1(LogBehavior log, const SatSolver::Status result = solver->ResetAndSolveWithGivenAssumptions(assumptions_subset); if (result == SatSolver::FEASIBLE) { - // If not all assumptions where taken, continue with a lower stratified + // If not all assumptions were taken, continue with a lower stratified // bound. Otherwise we have an optimal solution! // // TODO(user): Try more advanced variant where the bound is lowered by @@ -1052,7 +1052,7 @@ SatSolver::Status SolveWithCardinalityEncodingAndCore( upper_bound = obj + offset; } - // If not all assumptions where taken, continue with a lower stratified + // If not all assumptions were taken, continue with a lower stratified // bound. Otherwise we have an optimal solution. stratified_lower_bound = MaxNodeWeightSmallerThan(nodes, stratified_lower_bound); @@ -1603,7 +1603,7 @@ SatSolver::Status MinimizeWithCoreAndLazyEncoding( if (result == SatSolver::FEASIBLE) { process_solution(); if (cores.empty()) { - // If not all assumptions where taken, continue with a lower stratified + // If not all assumptions were taken, continue with a lower stratified // bound. Otherwise we have an optimal solution. stratified_threshold = next_stratified_threshold; if (stratified_threshold == 0) break; @@ -1856,7 +1856,7 @@ SatSolver::Status MinimizeWithHittingSetAndLazyEncoding( if (result == SatSolver::FEASIBLE) { process_solution(); if (cores.empty()) { - // If not all assumptions where taken, continue with a lower stratified + // If not all assumptions were taken, continue with a lower stratified // bound. Otherwise we have an optimal solution. stratified_threshold = next_stratified_threshold; if (stratified_threshold == 0) break; diff --git a/ortools/sat/pb_constraint.cc b/ortools/sat/pb_constraint.cc index 0b285c32f1..57f424da35 100644 --- a/ortools/sat/pb_constraint.cc +++ b/ortools/sat/pb_constraint.cc @@ -948,7 +948,7 @@ void PbConstraints::Untrail(const Trail& trail, int trail_index) { for (ConstraintIndexWithCoeff& update : to_update_[literal.Index()]) { thresholds_[update.index] += update.coefficient; - // Only the constraints which where inspected during Propagate() need + // Only the constraints which were inspected during Propagate() need // inspection during Untrail(). if (update.need_untrail_inspection) { update.need_untrail_inspection = false; diff --git a/ortools/sat/pb_constraint.h b/ortools/sat/pb_constraint.h index e378b778e9..6d7e621f18 100644 --- a/ortools/sat/pb_constraint.h +++ b/ortools/sat/pb_constraint.h @@ -234,7 +234,7 @@ class MutableUpperBoundedLinearConstraint { // Relaxes the constraint so that: // - ComputeSlackForTrailPrefix(trail, trail_index) == target; - // - All the variable that where propagated given the assignment < trail_index + // - All the variables that were propagated given the assignment < trail_index // are still propagated. // // As a precondition, ComputeSlackForTrailPrefix(trail, trail_index) >= target @@ -244,7 +244,7 @@ class MutableUpperBoundedLinearConstraint { // linear expression in 3 parts: // - P1: the true variables (only the one assigned < trail_index). // - P2: the other variables with a coeff > diff. - // Note that all these variables where the propagated ones. + // Note that all these variables were the propagated ones. // - P3: the other variables with a coeff <= diff. // We can then transform P1 + P2 + P3 <= rhs_ into P1 + P2' <= rhs_ - diff // Where P2' is the same sum as P2 with all the coefficient reduced by diff. @@ -537,7 +537,7 @@ class PbConstraints : public SatPropagator { // Changes the number of variables. void Resize(int num_variables) { - // Note that we avoid using up memory in the common case where there is no + // Note that we avoid using up memory in the common case where there are no // pb constraints at all. If there is 10 million variables, this vector // alone will take 480 MB! if (!constraints_.empty()) { diff --git a/ortools/sat/samples/BoolOrSample.java b/ortools/sat/samples/BoolOrSample.java index c768f13219..9afe4c6b09 100644 --- a/ortools/sat/samples/BoolOrSample.java +++ b/ortools/sat/samples/BoolOrSample.java @@ -12,8 +12,8 @@ // limitations under the License. import com.google.ortools.sat.CpModel; -import com.google.ortools.sat.ILiteral; import com.google.ortools.sat.IntVar; +import com.google.ortools.sat.Literal; public class BoolOrSample { @@ -23,6 +23,6 @@ public class BoolOrSample { CpModel model = new CpModel(); IntVar x = model.newBoolVar("x"); IntVar y = model.newBoolVar("y"); - model.addBoolOr(new ILiteral[] {x, y.not()}); + model.addBoolOr(new Literal[] {x, y.not()}); } } diff --git a/ortools/sat/samples/LiteralSample.java b/ortools/sat/samples/LiteralSample.java index 723fc5ae77..d3abba77bf 100644 --- a/ortools/sat/samples/LiteralSample.java +++ b/ortools/sat/samples/LiteralSample.java @@ -12,8 +12,8 @@ // limitations under the License. import com.google.ortools.sat.CpModel; -import com.google.ortools.sat.ILiteral; import com.google.ortools.sat.IntVar; +import com.google.ortools.sat.Literal; public class LiteralSample { @@ -22,7 +22,7 @@ public class LiteralSample { public static void main(String[] args) throws Exception { CpModel model = new CpModel(); IntVar x = model.newBoolVar("x"); - ILiteral notX = x.not(); + Literal notX = x.not(); System.out.println(notX.getShortString()); } } diff --git a/ortools/sat/samples/OptionalIntervalSample.java b/ortools/sat/samples/OptionalIntervalSample.java index bf5fc60872..329af9be08 100644 --- a/ortools/sat/samples/OptionalIntervalSample.java +++ b/ortools/sat/samples/OptionalIntervalSample.java @@ -12,9 +12,9 @@ // limitations under the License. import com.google.ortools.sat.CpModel; -import com.google.ortools.sat.ILiteral; import com.google.ortools.sat.IntVar; import com.google.ortools.sat.IntervalVar; +import com.google.ortools.sat.Literal; public class OptionalIntervalSample { @@ -27,7 +27,7 @@ public class OptionalIntervalSample { IntVar endVar = model.newIntVar(0, horizon, "end"); // Java code supports IntVar or integer constants in intervals. int duration = 10; - ILiteral presence = model.newBoolVar("presence"); + Literal presence = model.newBoolVar("presence"); IntervalVar interval = model.newOptionalIntervalVar(startVar, duration, endVar, presence, "interval"); diff --git a/ortools/sat/samples/RankingSample.java b/ortools/sat/samples/RankingSample.java index 8476b43ed6..2e493946ce 100644 --- a/ortools/sat/samples/RankingSample.java +++ b/ortools/sat/samples/RankingSample.java @@ -14,9 +14,9 @@ import com.google.ortools.sat.CpSolverStatus; import com.google.ortools.sat.CpModel; import com.google.ortools.sat.CpSolver; -import com.google.ortools.sat.ILiteral; import com.google.ortools.sat.IntVar; import com.google.ortools.sat.IntervalVar; +import com.google.ortools.sat.Literal; import java.util.ArrayList; import java.util.List; @@ -28,11 +28,11 @@ public class RankingSample { static { System.loadLibrary("jniortools"); } - static void rankTasks(CpModel model, IntVar[] starts, ILiteral[] presences, IntVar[] ranks) { + static void rankTasks(CpModel model, IntVar[] starts, Literal[] presences, IntVar[] ranks) { int numTasks = starts.length; // Creates precedence variables between pairs of intervals. - ILiteral[][] precedences = new ILiteral[numTasks][numTasks]; + Literal[][] precedences = new Literal[numTasks][numTasks]; for (int i = 0; i < numTasks; ++i) { for (int j = 0; j < numTasks; ++j) { if (i == j) { @@ -49,7 +49,7 @@ public class RankingSample { // Create optional intervals. for (int i = 0; i < numTasks - 1; ++i) { for (int j = i + 1; j < numTasks; ++j) { - List list = new ArrayList<>(); + List list = new ArrayList<>(); list.add(precedences[i][j]); list.add(precedences[j][i]); list.add(presences[i].not()); @@ -63,7 +63,7 @@ public class RankingSample { // The following boolOr will enforce that for any two intervals: // i precedes j or j precedes i or at least one interval is not // performed. - model.addBoolOr(list.toArray(new ILiteral[0])); + model.addBoolOr(list.toArray(new Literal[0])); // For efficiency, we add a redundant constraint declaring that only one of i precedes j and // j precedes i are true. This will speed up the solve because the reason of this // propagation is shorter that using interval bounds is true. @@ -95,7 +95,7 @@ public class RankingSample { IntVar[] starts = new IntVar[numTasks]; IntVar[] ends = new IntVar[numTasks]; IntervalVar[] intervals = new IntervalVar[numTasks]; - ILiteral[] presences = new ILiteral[numTasks]; + Literal[] presences = new Literal[numTasks]; IntVar[] ranks = new IntVar[numTasks]; IntVar trueVar = model.newConstant(1); diff --git a/ortools/sat/samples/ReifiedSample.java b/ortools/sat/samples/ReifiedSample.java index 9a825c028a..e8bf5a558c 100644 --- a/ortools/sat/samples/ReifiedSample.java +++ b/ortools/sat/samples/ReifiedSample.java @@ -12,8 +12,8 @@ // limitations under the License. import com.google.ortools.sat.CpModel; -import com.google.ortools.sat.ILiteral; import com.google.ortools.sat.IntVar; +import com.google.ortools.sat.Literal; /** * Reification is the action of associating a Boolean variable to a constraint. This boolean @@ -37,14 +37,14 @@ public class ReifiedSample { IntVar b = model.newBoolVar("b"); // Version 1: a half-reified boolean and. - model.addBoolAnd(new ILiteral[] {x, y.not()}).onlyEnforceIf(b); + model.addBoolAnd(new Literal[] {x, y.not()}).onlyEnforceIf(b); // Version 2: implications. model.addImplication(b, x); model.addImplication(b, y.not()); // Version 3: boolean or. - model.addBoolOr(new ILiteral[] {b.not(), x}); - model.addBoolOr(new ILiteral[] {b.not(), y.not()}); + model.addBoolOr(new Literal[] {b.not(), x}); + model.addBoolOr(new Literal[] {b.not(), y.not()}); } } diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto index f92a0a8b99..4054b5d51b 100644 --- a/ortools/sat/sat_parameters.proto +++ b/ortools/sat/sat_parameters.proto @@ -602,6 +602,6 @@ message SatParameters { // If true, we automatically detect variables whose constraint are always // enforced by the same literal and we mark them as optional. This allows - // to propagate them as if they where present in some situation. + // to propagate them as if they were present in some situation. optional bool use_optional_variables = 108 [default = true]; } diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc index 845612783d..56cd06770d 100644 --- a/ortools/sat/sat_solver.cc +++ b/ortools/sat/sat_solver.cc @@ -563,7 +563,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() { // PB resolution. // There is no point using this if the conflict and all the reasons involved - // in its resolution where clauses. + // in its resolution were clauses. bool compute_pb_conflict = false; if (parameters_->use_pb_resolution()) { compute_pb_conflict = (pb_constraints_.ConflictingConstraint() != nullptr); @@ -718,7 +718,7 @@ bool SatSolver::PropagateAndStopAfterOneConflictResolution() { // Note that we need to output the learned clause before cleaning the clause // database. This is because we already backtracked and some of the clauses - // that where needed to infer the conflict may not be "reasons" anymore and + // that were needed to infer the conflict may not be "reasons" anymore and // may be deleted. if (drat_proof_handler_ != nullptr) { drat_proof_handler_->AddClause(learned_conflict_); @@ -1252,7 +1252,7 @@ std::vector SatSolver::GetLastIncompatibleDecisions() { } // We reverse the assumptions so they are in the same order as the one in - // which the decision where made. + // which the decision were made. std::reverse(unsat_assumptions.begin(), unsat_assumptions.end()); return unsat_assumptions; } @@ -1753,13 +1753,13 @@ void SatSolver::ComputeFirstUIPConflict( // expand each of its literal using the reason for this literal assignement to // false. The is_marked_ set allow us to never expand the same literal twice. // - // The expansion is not done (i.e. stop) for literal that where assigned at a + // The expansion is not done (i.e. stop) for literals that were assigned at a // decision level below the current one. If the level of such literal is not // zero, it is added to the conflict clause. // // Now, the trick is that we use the trail to expand the literal of the // current level in a very specific order. Namely the reverse order of the one - // in which they where infered. We stop as soon as + // in which they were inferred. We stop as soon as // num_literal_at_highest_level_that_needs_to_be_processed is exactly one. // // This last literal will be the first UIP because by definition all the diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h index a06c8993d8..e6d03d4b84 100644 --- a/ortools/sat/sat_solver.h +++ b/ortools/sat/sat_solver.h @@ -131,7 +131,7 @@ class SatSolver { bool IsModelUnsat() const { return is_model_unsat_; } // Adds and registers the given propagator with the sat solver. Note that - // during propagation, they will be called in the order they where added. + // during propagation, they will be called in the order they were added. void AddPropagator(SatPropagator* propagator); void AddLastPropagator(SatPropagator* propagator); void TakePropagatorOwnership(std::unique_ptr propagator) { @@ -243,7 +243,7 @@ class SatSolver { // This function starts by calling EnqueueDecisionAndBackjumpOnConflict(). If // there is no conflict, it stops there. Otherwise, it tries to reapply all - // the decisions that where backjumped over until the first one that can't be + // the decisions that were backjumped over until the first one that can't be // taken because it is incompatible. Note that during this process, more // conflicts may happen and the trail may be backtracked even further. // @@ -428,7 +428,7 @@ class SatSolver { // See SaveDebugAssignment(). Note that these functions only consider the // variables at the time the debug_assignment_ was saved. If new variables - // where added since that time, they will be considered unassigned. + // were added since that time, they will be considered unassigned. bool ClauseIsValidUnderDebugAssignement( const std::vector& clause) const; bool PBConstraintIsValidUnderDebugAssignment( @@ -497,7 +497,7 @@ class SatSolver { // Returns true iff the clause is the reason for an assigned variable. // // TODO(user): With our current data structures, we could also return true - // for clauses that where just used as a reason (like just before an untrail). + // for clauses that were just used as a reason (like just before an untrail). // This may be beneficial, but should properly be defined so that we can // have the same behavior if we change the implementation. bool ClauseIsUsedAsReason(SatClause* clause) const { diff --git a/ortools/sat/theta_tree.h b/ortools/sat/theta_tree.h index 46125e6d38..b241d953d9 100644 --- a/ortools/sat/theta_tree.h +++ b/ortools/sat/theta_tree.h @@ -62,7 +62,7 @@ namespace sat { // initial_envelope(event) + sum_energy_min(event). // // We also maintain envelope_opt with is the maximum envelope a node could take -// if at most one of the event where at its maximum energy. +// if at most one of the events were at its maximum energy. // _ energy_delta(leaf) = energy_max(leaf) - energy_min(leaf) // _ max_energy_delta(node) = max_{leaf \in leaves(node)} energy_delta(leaf) // _ envelope_opt(node) = diff --git a/ortools/sat/util.h b/ortools/sat/util.h index 3bb8e9c3fa..402f875c4d 100644 --- a/ortools/sat/util.h +++ b/ortools/sat/util.h @@ -54,7 +54,7 @@ void RandomizeDecisionHeuristic(URBG* random, SatParameters* parameters); // // For a vector of size n, if we want to call this n times so that each literal // is last at least once, the sum of the size of the changed suffixes will be -// O(n log n). If we where to use a simpler algorithm (like moving the last +// O(n log n). If we were to use a simpler algorithm (like moving the last // unprocessed literal to the last position), this sum would be O(n^2). // // Returns the size of the common prefix of literals before and after the move,