always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[SAT/Java] ILiteral -> Literal; [SAT] fix a few english mistakes

Browse Source
This commit is contained in:
Laurent Perron
2018-09-14 13:24:34 +02:00
parent 01815e2d6d
commit 53863acd62
31 changed files with 102 additions and 103 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
ortools/com/google/ortools/sat/Constraint.java
View File

@@ -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());
}
}

38
ortools/com/google/ortools/sat/CpModel.java
View File

@@ -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),

2
ortools/com/google/ortools/sat/CpSolver.java
View File

@@ -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;

2
ortools/com/google/ortools/sat/CpSolverSolutionCallback.java
View File

@@ -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());
}

4
ortools/com/google/ortools/sat/IntVar.java
View File

@@ -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);
}

4
ortools/com/google/ortools/sat/ILiteral.java → ortools/com/google/ortools/sat/Literal.java
View File

@@ -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();

6
ortools/com/google/ortools/sat/NotBooleanVariable.java
View File

@@ -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;
}

3
ortools/sat/circuit.h
View File

@@ -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<int>* tails, std::vector<int>* heads,
std::vector<Literal>* literals);

2
ortools/sat/clause.cc
View File

@@ -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;
}

2
ortools/sat/cp_model.proto
View File

@@ -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;

10
ortools/sat/cp_model_presolve.cc
View File

@@ -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<std::string, int> sorted_rules(context.stats_by_rule_name.begin(),
context.stats_by_rule_name.end());
for (const auto& entry : sorted_rules) {

6
ortools/sat/cp_model_solver.cc
View File

@@ -293,7 +293,7 @@ class ModelWithMapping {
// Used to return a feasible solution for the unused variables.
std::vector<int64> 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<const ConstraintProto*> 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<SatSolver>()->Propagate();
// Probing Boolean variables. Because we don't have a good deterministic time

16
ortools/sat/doc/boolean_logic.md
View File

@@ -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()});
}
}
```

16
ortools/sat/doc/scheduling.md
View File

@@ -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<ILiteral> list = new ArrayList<>();
List<Literal> 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);

2
ortools/sat/drat_checker.h
View File

@@ -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).

8
ortools/sat/integer.cc
View File

@@ -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.

2
ortools/sat/integer.h
View File

@@ -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<int>& watch_indices) {
LOG(FATAL) << "Not implemented.";

4
ortools/sat/lp_utils.cc
View File

@@ -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.

8
ortools/sat/optimization.cc
View File

@@ -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;

2
ortools/sat/pb_constraint.cc
View File

@@ -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;

6
ortools/sat/pb_constraint.h
View File

@@ -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()) {

4
ortools/sat/samples/BoolOrSample.java
View File

@@ -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()});
}
}

4
ortools/sat/samples/LiteralSample.java
View File

@@ -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());
}
}

4
ortools/sat/samples/OptionalIntervalSample.java
View File

@@ -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");

12
ortools/sat/samples/RankingSample.java
View File

@@ -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<ILiteral> list = new ArrayList<>();
List<Literal> 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);

8
ortools/sat/samples/ReifiedSample.java
View File

@@ -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()});
}
}

2
ortools/sat/sat_parameters.proto
View File

@@ -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];
}

10
ortools/sat/sat_solver.cc
View File

@@ -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<Literal> 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

8
ortools/sat/sat_solver.h
View File

@@ -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<SatPropagator> 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<Literal>& 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 {

2
ortools/sat/theta_tree.h
View File

@@ -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) =

2
ortools/sat/util.h
View File

@@ -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,