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

use Pseudo-cost in parallel search; change automata to automaton in cp_model.proto

Browse Source
This commit is contained in:
Laurent Perron
2019-02-01 18:32:13 +01:00
parent 86ab8bbd8f
commit fec0768323
16 changed files with 107 additions and 95 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
ortools/flatzinc/cp_model_fz_solver.cc
View File

@@ -403,7 +403,7 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
for (const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(var);
for (const int64 value : fz_ct.arguments[1].values) arg->add_values(value);
} else if (fz_ct.type == "regular") {
auto* arg = ct->mutable_automata();
auto* arg = ct->mutable_automaton();
for (const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(var);
int count = 0;

12
ortools/sat/cp_model.cc
View File

@@ -233,9 +233,9 @@ void ReservoirConstraint::AddOptionalEvent(IntVar time, int64 demand,
void AutomatonConstraint::AddTransition(int tail, int head,
int64 transition_label) {
proto_->mutable_automata()->add_transition_tail(tail);
proto_->mutable_automata()->add_transition_head(head);
proto_->mutable_automata()->add_transition_label(transition_label);
proto_->mutable_automaton()->add_transition_tail(tail);
proto_->mutable_automaton()->add_transition_head(head);
proto_->mutable_automaton()->add_transition_label(transition_label);
}
void NoOverlap2DConstraint::AddRectangle(IntervalVar x_coordinate,
@@ -584,11 +584,11 @@ AutomatonConstraint CpModelBuilder::AddAutomaton(
absl::Span<const int> final_states) {
ConstraintProto* const proto = cp_model_.add_constraints();
for (const IntVar& var : transition_variables) {
proto->mutable_automata()->add_vars(GetOrCreateIntegerIndex(var.index_));
proto->mutable_automaton()->add_vars(GetOrCreateIntegerIndex(var.index_));
}
proto->mutable_automata()->set_starting_state(starting_state);
proto->mutable_automaton()->set_starting_state(starting_state);
for (const int final_state : final_states) {
proto->mutable_automata()->add_final_states(final_state);
proto->mutable_automaton()->add_final_states(final_state);
}
return AutomatonConstraint(proto);
}

2
ortools/sat/cp_model.h
View File

@@ -576,7 +576,7 @@ class CpModelBuilder {
// and 'label' is the label of an arc from 'head' to 'tail',
// corresponding to the value of one variable in the list of variables.
//
// This automata will be unrolled into a flow with n + 1 phases. Each phase
// This automaton will be unrolled into a flow with n + 1 phases. Each phase
// contains the possible states of the automaton. The first state contains the
// initial state. The last phase contains the final states.
//

13
ortools/sat/cp_model.proto
View File

@@ -222,10 +222,11 @@ message InverseConstraintProto {
repeated int32 f_inverse = 2;
}
// This constraint forces a sequence of variables to be accepted by an automata.
message AutomataConstraintProto {
// This constraint forces a sequence of variables to be accepted by an
// automaton.
message AutomatonConstraintProto {
// A state is identified by a non-negative number. It is preferable to keep
// all the states dense in says [0, num_states). The automata starts at
// all the states dense in says [0, num_states). The automaton starts at
// starting_state and must finish in any of the final states.
int64 starting_state = 2;
repeated int64 final_states = 3;
@@ -237,7 +238,7 @@ message AutomataConstraintProto {
repeated int64 transition_head = 5;
repeated int64 transition_label = 6;
// The sequence of variables. The automata is ran for vars_size() "steps" and
// The sequence of variables. The automaton is ran for vars_size() "steps" and
// the value of vars[i] corresponds to the transition label at step i.
repeated int32 vars = 7;
}
@@ -330,9 +331,9 @@ message ConstraintProto {
// take.
TableConstraintProto table = 16;
// The automata constraint forces a sequence of variables to be accepted
// The automaton constraint forces a sequence of variables to be accepted
// by an automaton.
AutomataConstraintProto automata = 17;
AutomatonConstraintProto automaton = 17;
// The inverse constraint forces two arrays to be inverses of each other:
// the values of one are the indices of the other, and vice versa.

24
ortools/sat/cp_model_checker.cc
View File

@@ -497,22 +497,22 @@ class ConstraintChecker {
return ct.table().negated();
}
bool AutomataConstraintIsFeasible(const ConstraintProto& ct) {
bool AutomatonConstraintIsFeasible(const ConstraintProto& ct) {
// Build the transition table {tail, label} -> head.
absl::flat_hash_map<std::pair<int64, int64>, int64> transition_map;
const int num_transitions = ct.automata().transition_tail().size();
const int num_transitions = ct.automaton().transition_tail().size();
for (int i = 0; i < num_transitions; ++i) {
transition_map[{ct.automata().transition_tail(i),
ct.automata().transition_label(i)}] =
ct.automata().transition_head(i);
transition_map[{ct.automaton().transition_tail(i),
ct.automaton().transition_label(i)}] =
ct.automaton().transition_head(i);
}
// Walk the automata.
int64 current_state = ct.automata().starting_state();
const int num_steps = ct.automata().vars_size();
// Walk the automaton.
int64 current_state = ct.automaton().starting_state();
const int num_steps = ct.automaton().vars_size();
for (int i = 0; i < num_steps; ++i) {
const std::pair<int64, int64> key = {current_state,
Value(ct.automata().vars(i))};
Value(ct.automaton().vars(i))};
if (!gtl::ContainsKey(transition_map, key)) {
return false;
}
@@ -520,7 +520,7 @@ class ConstraintChecker {
}
// Check we are now in a final state.
for (const int64 final : ct.automata().final_states()) {
for (const int64 final : ct.automaton().final_states()) {
if (current_state == final) return true;
}
return false;
@@ -782,8 +782,8 @@ bool SolutionIsFeasible(const CpModelProto& model,
case ConstraintProto::ConstraintCase::kTable:
is_feasible = checker.TableConstraintIsFeasible(ct);
break;
case ConstraintProto::ConstraintCase::kAutomata:
is_feasible = checker.AutomataConstraintIsFeasible(ct);
case ConstraintProto::ConstraintCase::kAutomaton:
is_feasible = checker.AutomatonConstraintIsFeasible(ct);
break;
case ConstraintProto::ConstraintCase::kCircuit:
is_feasible = checker.CircuitConstraintIsFeasible(ct);

20
ortools/sat/cp_model_loader.cc
View File

@@ -1061,23 +1061,23 @@ void LoadTableConstraint(const ConstraintProto& ct, Model* m) {
}
}
void LoadAutomataConstraint(const ConstraintProto& ct, Model* m) {
void LoadAutomatonConstraint(const ConstraintProto& ct, Model* m) {
auto* mapping = m->GetOrCreate<CpModelMapping>();
const std::vector<IntegerVariable> vars =
mapping->Integers(ct.automata().vars());
mapping->Integers(ct.automaton().vars());
const int num_transitions = ct.automata().transition_tail_size();
const int num_transitions = ct.automaton().transition_tail_size();
std::vector<std::vector<int64>> transitions;
transitions.reserve(num_transitions);
for (int i = 0; i < num_transitions; ++i) {
transitions.push_back({ct.automata().transition_tail(i),
ct.automata().transition_label(i),
ct.automata().transition_head(i)});
transitions.push_back({ct.automaton().transition_tail(i),
ct.automaton().transition_label(i),
ct.automaton().transition_head(i)});
}
const int64 starting_state = ct.automata().starting_state();
const int64 starting_state = ct.automaton().starting_state();
const std::vector<int64> final_states =
ValuesFromProto(ct.automata().final_states());
ValuesFromProto(ct.automaton().final_states());
m->Add(TransitionConstraint(vars, transitions, starting_state, final_states));
}
@@ -1269,8 +1269,8 @@ bool LoadConstraint(const ConstraintProto& ct, Model* m) {
case ConstraintProto::ConstraintProto::kTable:
LoadTableConstraint(ct, m);
return true;
case ConstraintProto::ConstraintProto::kAutomata:
LoadAutomataConstraint(ct, m);
case ConstraintProto::ConstraintProto::kAutomaton:
LoadAutomatonConstraint(ct, m);
return true;
case ConstraintProto::ConstraintProto::kCircuit:
LoadCircuitConstraint(ct, m);

2
ortools/sat/cp_model_loader.h
View File

@@ -190,7 +190,7 @@ void LoadElementConstraintBounds(const ConstraintProto& ct, Model* m);
void LoadElementConstraintAC(const ConstraintProto& ct, Model* m);
void LoadElementConstraint(const ConstraintProto& ct, Model* m);
void LoadTableConstraint(const ConstraintProto& ct, Model* m);
void LoadAutomataConstraint(const ConstraintProto& ct, Model* m);
void LoadAutomatonConstraint(const ConstraintProto& ct, Model* m);
void LoadCircuitConstraint(const ConstraintProto& ct, Model* m);
void LoadRoutesConstraint(const ConstraintProto& ct, Model* m);
void LoadCircuitCoveringConstraint(const ConstraintProto& ct, Model* m);

10
ortools/sat/cp_model_search.cc
View File

@@ -297,12 +297,18 @@ SatParameters DiversifySearchParameters(const SatParameters& params,
*name = "fixed";
return new_params;
}
} else {
// TODO(user): Disable lp_br if linear part is small or empty.
if (--index == 0) {
new_params.set_search_branching(SatParameters::LP_SEARCH);
*name = "lp_br";
return new_params;
}
}
// TODO(user): Disable lp_br if linear part is small or empty.
if (--index == 0) {
new_params.set_search_branching(SatParameters::PSEUDO_COST_SEARCH);
*name = "lp_br";
*name = "pseudo_cost";
return new_params;
}

10
ortools/sat/cp_model_solver.cc
View File

@@ -154,8 +154,8 @@ class FullEncodingFixedPointComputer {
return PropagateElement(ct);
case ConstraintProto::ConstraintProto::kTable:
return PropagateTable(ct);
case ConstraintProto::ConstraintProto::kAutomata:
return PropagateAutomata(ct);
case ConstraintProto::ConstraintProto::kAutomaton:
return PropagateAutomaton(ct);
case ConstraintProto::ConstraintProto::kInverse:
return PropagateInverse(ct);
case ConstraintProto::ConstraintProto::kLinear:
@@ -209,7 +209,7 @@ class FullEncodingFixedPointComputer {
bool PropagateElement(const ConstraintProto* ct);
bool PropagateTable(const ConstraintProto* ct);
bool PropagateAutomata(const ConstraintProto* ct);
bool PropagateAutomaton(const ConstraintProto* ct);
bool PropagateInverse(const ConstraintProto* ct);
bool PropagateLinear(const ConstraintProto* ct);
@@ -268,9 +268,9 @@ bool FullEncodingFixedPointComputer::PropagateTable(const ConstraintProto* ct) {
return true;
}
bool FullEncodingFixedPointComputer::PropagateAutomata(
bool FullEncodingFixedPointComputer::PropagateAutomaton(
const ConstraintProto* ct) {
for (const int variable : ct->automata().vars()) {
for (const int variable : ct->automaton().vars()) {
FullyEncode(variable);
}
return true;

16
ortools/sat/cp_model_utils.cc
View File

@@ -93,8 +93,8 @@ void AddReferencesUsedByConstraint(const ConstraintProto& ct,
case ConstraintProto::ConstraintCase::kTable:
AddIndices(ct.table().vars(), &output->variables);
break;
case ConstraintProto::ConstraintCase::kAutomata:
AddIndices(ct.automata().vars(), &output->variables);
case ConstraintProto::ConstraintCase::kAutomaton:
AddIndices(ct.automaton().vars(), &output->variables);
break;
case ConstraintProto::ConstraintCase::kInterval:
output->variables.insert(ct.interval().start());
@@ -177,7 +177,7 @@ void ApplyToAllLiteralIndices(const std::function<void(int*)>& f,
break;
case ConstraintProto::ConstraintCase::kTable:
break;
case ConstraintProto::ConstraintCase::kAutomata:
case ConstraintProto::ConstraintCase::kAutomaton:
break;
case ConstraintProto::ConstraintCase::kInterval:
break;
@@ -251,8 +251,8 @@ void ApplyToAllVariableIndices(const std::function<void(int*)>& f,
case ConstraintProto::ConstraintCase::kTable:
APPLY_TO_REPEATED_FIELD(table, vars);
break;
case ConstraintProto::ConstraintCase::kAutomata:
APPLY_TO_REPEATED_FIELD(automata, vars);
case ConstraintProto::ConstraintCase::kAutomaton:
APPLY_TO_REPEATED_FIELD(automaton, vars);
break;
case ConstraintProto::ConstraintCase::kInterval:
APPLY_TO_SINGULAR_FIELD(interval, start);
@@ -311,7 +311,7 @@ void ApplyToAllIntervalIndices(const std::function<void(int*)>& f,
break;
case ConstraintProto::ConstraintCase::kTable:
break;
case ConstraintProto::ConstraintCase::kAutomata:
case ConstraintProto::ConstraintCase::kAutomaton:
break;
case ConstraintProto::ConstraintCase::kInterval:
break;
@@ -372,8 +372,8 @@ std::string ConstraintCaseName(
return "kReservoir";
case ConstraintProto::ConstraintCase::kTable:
return "kTable";
case ConstraintProto::ConstraintCase::kAutomata:
return "kAutomata";
case ConstraintProto::ConstraintCase::kAutomaton:
return "kAutomaton";
case ConstraintProto::ConstraintCase::kInterval:
return "kInterval";
case ConstraintProto::ConstraintCase::kNoOverlap:

12
ortools/sat/csharp/CpModel.cs
View File

@@ -402,12 +402,12 @@ public class CpModel
return ct;
}
public Constraint AddAutomata(IEnumerable<IntVar> vars,
public Constraint AddAutomaton(IEnumerable<IntVar> vars,
long starting_state,
long[,] transitions,
IEnumerable<long> final_states) {
Constraint ct = new Constraint(model_);
AutomataConstraintProto aut = new AutomataConstraintProto();
AutomatonConstraintProto aut = new AutomatonConstraintProto();
foreach (IntVar var in vars)
{
aut.Vars.Add(var.Index);
@@ -424,17 +424,17 @@ public class CpModel
aut.TransitionHead.Add(transitions[i, 2]);
}
ct.Proto.Automata = aut;
ct.Proto.Automaton = aut;
return ct;
}
public Constraint AddAutomata(
public Constraint AddAutomaton(
IEnumerable<IntVar> vars,
long starting_state,
IEnumerable<Tuple<long, long, long>> transitions,
IEnumerable<long> final_states) {
Constraint ct = new Constraint(model_);
AutomataConstraintProto aut = new AutomataConstraintProto();
AutomatonConstraintProto aut = new AutomatonConstraintProto();
foreach (IntVar var in vars)
{
aut.Vars.Add(var.Index);
@@ -452,7 +452,7 @@ public class CpModel
aut.TransitionTail.Add(transition.Item3);
}
ct.Proto.Automata = aut;
ct.Proto.Automaton = aut;
return ct;
}

21
ortools/sat/integer.cc
View File

@@ -353,6 +353,9 @@ void IntegerEncoder::AssociateToIntegerEqualValue(Literal literal,
return;
}
const IntegerLiteral ge = IntegerLiteral::GreaterOrEqual(var, value);
const IntegerLiteral le = IntegerLiteral::LowerOrEqual(var, value);
// Special case for the first and last value.
if (value == domain.Min()) {
// Note that this will recursively call AssociateToIntegerEqualValue() but
@@ -360,24 +363,26 @@ void IntegerEncoder::AssociateToIntegerEqualValue(Literal literal,
// stop there. When a domain has just 2 values, this allows to call just
// once AssociateToIntegerEqualValue() and also associate the other value to
// the negation of the given literal.
AssociateToIntegerLiteral(literal,
IntegerLiteral::LowerOrEqual(var, value));
AssociateToIntegerLiteral(literal, le);
return;
}
if (value == domain.Max()) {
AssociateToIntegerLiteral(literal,
IntegerLiteral::GreaterOrEqual(var, value));
AssociateToIntegerLiteral(literal, ge);
return;
}
// (var == value) <=> (var >= value) and (var <= value).
const Literal a(
GetOrCreateAssociatedLiteral(IntegerLiteral::GreaterOrEqual(var, value)));
const Literal b(
GetOrCreateAssociatedLiteral(IntegerLiteral::LowerOrEqual(var, value)));
const Literal a(GetOrCreateAssociatedLiteral(ge));
const Literal b(GetOrCreateAssociatedLiteral(le));
sat_solver_->AddBinaryClause(a, literal.Negated());
sat_solver_->AddBinaryClause(b, literal.Negated());
sat_solver_->AddProblemClause({a.Negated(), b.Negated(), literal});
// Update reverse encoding.
const int new_size = 1 + literal.Index().value();
if (new_size > reverse_encoding_.size()) reverse_encoding_.resize(new_size);
reverse_encoding_[literal.Index()].push_back(le);
reverse_encoding_[literal.Index()].push_back(ge);
}
// TODO(user): The hard constraints we add between associated literals seems to

4
ortools/sat/pseudo_costs.cc
View File

@@ -126,7 +126,7 @@ std::vector<PseudoCosts::VariableBoundChange> GetBoundChanges(
if (decision == kNoLiteralIndex) return bound_changes;
auto* encoder = model->GetOrCreate<IntegerEncoder>();
auto* integer_trail = model->GetOrCreate<IntegerTrail>();
// TODO(user): Support equality decisions.
// NOTE: We ignore negation of equality decisions.
for (const IntegerLiteral l :
encoder->GetIntegerLiterals(Literal(decision))) {
if (l.var == kNoIntegerVariable) continue;
@@ -134,7 +134,7 @@ std::vector<PseudoCosts::VariableBoundChange> GetBoundChanges(
PseudoCosts::VariableBoundChange var_bound_change;
var_bound_change.var = l.var;
const IntegerValue current_lb = integer_trail->LowerBound(l.var);
var_bound_change.lower_bound_change = Subtract(l.bound, current_lb);
var_bound_change.lower_bound_change = Subtract(l.bound, current_lb);
bound_changes.push_back(var_bound_change);
}

32
ortools/sat/python/cp_model.py
View File

@@ -764,7 +764,7 @@ class CpModel(object):
and 'transition' is the label of an arc from 'head' to 'tail',
corresponding to the value of one variable in the list of variables.
This automata will be unrolled into a flow with n + 1 phases. Each phase
This automaton will be unrolled into a flow with n + 1 phases. Each phase
contains the possible states of the automaton. The first state contains the
initial state. The last phase contains the final states.
@@ -782,10 +782,10 @@ class CpModel(object):
Args:
transition_variables: A non empty list of variables whose values
correspond to the labels of the arcs traversed by the automata.
starting_state: The initial state of the automata.
correspond to the labels of the arcs traversed by the automaton.
starting_state: The initial state of the automaton.
final_states: A non empty list of admissible final states.
transition_triples: A list of transition for the automata, in the
transition_triples: A list of transition for the automaton, in the
following format (current_state, variable_value, next_state).
Returns:
@@ -798,23 +798,23 @@ class CpModel(object):
if not transition_variables:
raise ValueError(
'AddAutomata expects a non empty transition_variables '
'AddAutomaton expects a non empty transition_variables '
'array')
if not final_states:
raise ValueError('AddAutomata expects some final states')
raise ValueError('AddAutomaton expects some final states')
if not transition_triples:
raise ValueError('AddAutomata expects some transtion triples')
raise ValueError('AddAutomaton expects some transtion triples')
ct = Constraint(self.__model.constraints)
model_ct = self.__model.constraints[ct.Index()]
model_ct.automata.vars.extend(
model_ct.automaton.vars.extend(
[self.GetOrMakeIndex(x) for x in transition_variables])
cp_model_helper.AssertIsInt64(starting_state)
model_ct.automata.starting_state = starting_state
model_ct.automaton.starting_state = starting_state
for v in final_states:
cp_model_helper.AssertIsInt64(v)
model_ct.automata.final_states.append(v)
model_ct.automaton.final_states.append(v)
for t in transition_triples:
if len(t) != 3:
raise TypeError('Tuple ' + str(t) +
@@ -822,9 +822,9 @@ class CpModel(object):
cp_model_helper.AssertIsInt64(t[0])
cp_model_helper.AssertIsInt64(t[1])
cp_model_helper.AssertIsInt64(t[2])
model_ct.automata.transition_tail.append(t[0])
model_ct.automata.transition_label.append(t[1])
model_ct.automata.transition_head.append(t[2])
model_ct.automaton.transition_tail.append(t[0])
model_ct.automaton.transition_label.append(t[1])
model_ct.automaton.transition_head.append(t[2])
return ct
def AddInverse(self, variables, inverse_variables):
@@ -1558,7 +1558,7 @@ class ObjectiveSolutionPrinter(CpSolverSolutionCallback):
best_bound = self.BestObjectiveBound()
obj_lb = min(objective, best_bound)
obj_ub = max(objective, best_bound)
print('Solution %i, time = %.2f s, objective = [%i, %i]' %
(self.__solution_count, current_time - self.__start_time,
obj_lb, obj_ub))
print('Solution %i, time = %f s, objective = [%i, %i]' %
(self.__solution_count, current_time - self.__start_time, obj_lb,
obj_ub))
self.__solution_count += 1

16
ortools/sat/table.cc
View File

@@ -393,7 +393,7 @@ std::function<void(Model*)> LiteralTableConstraint(
std::function<void(Model*)> TransitionConstraint(
const std::vector<IntegerVariable>& vars,
const std::vector<std::vector<int64>>& automata, int64 initial_state,
const std::vector<std::vector<int64>>& automaton, int64 initial_state,
const std::vector<int64>& final_states) {
return [=](Model* model) {
IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
@@ -403,7 +403,7 @@ std::function<void(Model*)> TransitionConstraint(
// Test precondition.
{
std::set<std::pair<int64, int64>> unique_transition_checker;
for (const std::vector<int64>& transition : automata) {
for (const std::vector<int64>& transition : automaton) {
CHECK_EQ(transition.size(), 3);
const std::pair<int64, int64> p{transition[0], transition[1]};
CHECK(!gtl::ContainsKey(unique_transition_checker, p))
@@ -417,7 +417,7 @@ std::function<void(Model*)> TransitionConstraint(
std::vector<absl::flat_hash_set<int64>> possible_values(n);
for (int time = 0; time < n; ++time) {
const auto domain = integer_trail->InitialVariableDomain(vars[time]);
for (const std::vector<int64>& transition : automata) {
for (const std::vector<int64>& transition : automaton) {
// TODO(user): quadratic algo, improve!
if (domain.Contains(transition[1])) {
possible_values[time].insert(transition[1]);
@@ -435,7 +435,7 @@ std::function<void(Model*)> TransitionConstraint(
// TODO(user): filter using the domain of vars[time] that may not contain
// all the possible transitions.
for (int time = 0; time + 1 < n; ++time) {
for (const std::vector<int64>& transition : automata) {
for (const std::vector<int64>& transition : automaton) {
if (!gtl::ContainsKey(reachable_states[time], transition[0])) continue;
if (!gtl::ContainsKey(possible_values[time], transition[1])) continue;
reachable_states[time + 1].insert(transition[2]);
@@ -445,7 +445,7 @@ std::function<void(Model*)> TransitionConstraint(
// Backward.
for (int time = n - 1; time > 0; --time) {
std::set<int64> new_set;
for (const std::vector<int64>& transition : automata) {
for (const std::vector<int64>& transition : automaton) {
if (!gtl::ContainsKey(reachable_states[time], transition[0])) continue;
if (!gtl::ContainsKey(possible_values[time], transition[1])) continue;
if (!gtl::ContainsKey(reachable_states[time + 1], transition[2]))
@@ -455,7 +455,7 @@ std::function<void(Model*)> TransitionConstraint(
reachable_states[time].swap(new_set);
}
// We will model at each time step the current automata state using Boolean
// We will model at each time step the current automaton state using Boolean
// variables. We will have n+1 time step. At time zero, we start in the
// initial state, and at time n we should be in one of the final states. We
// don't need to create Booleans at at time when there is just one possible
@@ -465,13 +465,13 @@ std::function<void(Model*)> TransitionConstraint(
absl::flat_hash_map<IntegerValue, Literal> out_encoding;
for (int time = 0; time < n; ++time) {
// All these vector have the same size. We will use them to enforce a
// local table constraint representing one step of the automata at the
// local table constraint representing one step of the automaton at the
// given time.
std::vector<Literal> tuple_literals;
std::vector<IntegerValue> in_states;
std::vector<IntegerValue> transition_values;
std::vector<IntegerValue> out_states;
for (const std::vector<int64>& transition : automata) {
for (const std::vector<int64>& transition : automaton) {
if (!gtl::ContainsKey(reachable_states[time], transition[0])) continue;
if (!gtl::ContainsKey(possible_values[time], transition[1])) continue;
if (!gtl::ContainsKey(reachable_states[time + 1], transition[2]))

6
ortools/sat/table.h
View File

@@ -57,10 +57,10 @@ std::function<void(Model*)> LiteralTableConstraint(
void CompressTuples(const std::vector<int64>& domain_sizes, int64 any_value,
std::vector<std::vector<int64>>* tuples);
// Given an automata defined by a set of 3-tuples:
// Given an automaton defined by a set of 3-tuples:
// (state, transition_with_value_as_label, next_state)
// this accepts the sequences of vars.size() variables that are recognized by
// this automata. That is:
// this automaton. That is:
// - We start from the initial state.
// - For each variable, we move along the transition labeled by this variable
// value. Moreover, the variable must take a value that correspond to a
@@ -71,7 +71,7 @@ void CompressTuples(const std::vector<int64>& domain_sizes, int64 any_value,
// See the test for some examples.
std::function<void(Model*)> TransitionConstraint(
const std::vector<IntegerVariable>& vars,
const std::vector<std::vector<int64>>& automata, int64 initial_state,
const std::vector<std::vector<int64>>& automaton, int64 initial_state,
const std::vector<int64>& final_states);
} // namespace sat