From cd2d17df93a214a2261063f494551b0233b4495f Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Mon, 13 Jul 2015 16:45:46 -0700 Subject: [PATCH] support regular_nfa --- examples/flatzinc/regular_test.fzn | 14 +++++++ src/flatzinc/constraints.cc | 62 +++++++++++++++++++++++++++-- src/flatzinc/model.cc | 9 +++++ src/flatzinc/model.h | 3 ++ src/flatzinc/mznlib/regular_nfa.mzn | 2 + src/flatzinc/parser.yy | 8 +++- 6 files changed, 93 insertions(+), 5 deletions(-) create mode 100644 examples/flatzinc/regular_test.fzn create mode 100644 src/flatzinc/mznlib/regular_nfa.mzn diff --git a/examples/flatzinc/regular_test.fzn b/examples/flatzinc/regular_test.fzn new file mode 100644 index 0000000000..fad10bb43e --- /dev/null +++ b/examples/flatzinc/regular_test.fzn @@ -0,0 +1,14 @@ +array [1..18] of set of int: d = [{2,4},5..5,{4,6},{1,3,5},{2,6},5..5,{2,8},{1,5,7},{2,4,6,8},{1,3,7,9},{2,8},{3,5,9},{4,8},5..5,{4,6},{5,7,9},{6,8},5..5]; +var 1..2: X_INTRODUCED_0; +var 1..2: X_INTRODUCED_1; +var 1..2: X_INTRODUCED_2; +array [1..3] of var 1..2: x:: output_array([1..3]) = [X_INTRODUCED_0,X_INTRODUCED_1,X_INTRODUCED_2]; +constraint regular_nfa(x,9,2,d,1,9..9); +solve :: int_search(x,input_order,indomain_min,complete) satisfy; + +// Should return (with -a) +// x = array1d(1..3, [1, 1, 2]); +// ---------- +// x = array1d(1..3, [1, 2, 2]); +// ---------- +// x = array1d(1..3, [2, 1, 2]); diff --git a/src/flatzinc/constraints.cc b/src/flatzinc/constraints.cc index 31563eb6f6..b3cd78cda3 100644 --- a/src/flatzinc/constraints.cc +++ b/src/flatzinc/constraints.cc @@ -32,12 +32,12 @@ DECLARE_bool(fz_verbose); // - k-dimensional diffn // - geost // - network_flow -// - regular with NFAs // Not necessary?: // - knapsack // Done: // - symmetric all different // - disjunctive: +// - regular with NFAs // Later: // optional scheduling constraints: alternative, span, disjunctive, cumulative // functional versions of many global constraints @@ -2242,8 +2242,8 @@ void ExtractRegular(FzSolver* fzsolver, FzConstraint* ct) { const std::vector& array_transitions = ct->Arg(3).values; IntTupleSet tuples(3); int count = 0; - for (int q = 1; q <= num_states; ++q) { - for (int s = 1; s <= num_values; ++s) { + for (int64 q = 1; q <= num_states; ++q) { + for (int64 s = 1; s <= num_values; ++s) { const int64 next = array_transitions[count++]; if (next != 0) { tuples.Insert3(q, s, next); @@ -2276,6 +2276,60 @@ void ExtractRegular(FzSolver* fzsolver, FzConstraint* ct) { AddConstraint(solver, ct, constraint); } +void ExtractRegularNfa(FzSolver* fzsolver, FzConstraint* ct) { + Solver* const solver = fzsolver->solver(); + + const std::vector variables = fzsolver->GetVariableArray(ct->Arg(0)); + const int64 num_states = ct->Arg(1).Value(); + const int64 num_values = ct->Arg(2).Value(); + + const std::vector& array_transitions = ct->Arg(3).domains; + IntTupleSet tuples(3); + int count = 0; + for (int64 q = 1; q <= num_states; ++q) { + for (int64 s = 1; s <= num_values; ++s) { + const FzDomain& next = array_transitions[count++]; + if (next.is_interval) { + for (int64 v = next.values[0]; v <= next.values[1]; ++v) { + if (v != 0) { + tuples.Insert3(q, s, v); + } + } + } else { + for (int64 v : next.values) { + if (v != 0) { + tuples.Insert3(q, s, v); + } + } + } + } + } + + const int64 initial_state = ct->Arg(4).Value(); + + std::vector final_states; + switch (ct->Arg(5).type) { + case FzArgument::INT_VALUE: { + final_states.push_back(ct->Arg(5).values[0]); + break; + } + case FzArgument::INT_INTERVAL: { + for (int v = ct->Arg(5).values[0]; v <= ct->Arg(5).values[1]; ++v) { + final_states.push_back(v); + } + break; + } + case FzArgument::INT_LIST: { + final_states = ct->Arg(5).values; + break; + } + default: { LOG(FATAL) << "Wrong constraint " << ct->DebugString(); } + } + Constraint* const constraint = solver->MakeTransitionConstraint( + variables, tuples, initial_state, final_states); + AddConstraint(solver, ct, constraint); +} + void ExtractSetIn(FzSolver* fzsolver, FzConstraint* ct) { Solver* const solver = fzsolver->solver(); IntExpr* const expr = fzsolver->GetExpression(ct->Arg(0)); @@ -2574,6 +2628,8 @@ void FzSolver::ExtractConstraint(FzConstraint* ct) { ExtractNvalue(this, ct); } else if (type == "regular") { ExtractRegular(this, ct); + } else if (type == "regular_nfa") { + ExtractRegularNfa(this, ct); } else if (type == "set_in" || type == "int_in") { ExtractSetIn(this, ct); } else if (type == "set_in_reif") { diff --git a/src/flatzinc/model.cc b/src/flatzinc/model.cc index fca7258881..9794def9fd 100644 --- a/src/flatzinc/model.cc +++ b/src/flatzinc/model.cc @@ -245,6 +245,13 @@ FzArgument FzArgument::IntegerList(std::vector* values) { return result; } +FzArgument FzArgument::DomainList(const std::vector& domains) { + FzArgument result; + result.type = DOMAIN_LIST; + result.domains = domains; + return result; +} + FzArgument FzArgument::IntVarRef(FzIntegerVariable* const var) { FzArgument result; result.type = INT_VAR_REF; @@ -287,6 +294,8 @@ std::string FzArgument::DebugString() const { values[1]); case INT_LIST: return StringPrintf("[%s]", strings::Join(values, ", ").c_str()); + case DOMAIN_LIST: + return StringPrintf("[%s]", JoinDebugString(domains, ", ").c_str()); case INT_VAR_REF: return variables[0]->name; case INT_VAR_REF_ARRAY: { diff --git a/src/flatzinc/model.h b/src/flatzinc/model.h index 70dcd21ab4..fb8245adcb 100644 --- a/src/flatzinc/model.h +++ b/src/flatzinc/model.h @@ -133,6 +133,7 @@ struct FzArgument { INT_VALUE, INT_INTERVAL, INT_LIST, + DOMAIN_LIST, INT_VAR_REF, INT_VAR_REF_ARRAY, VOID_ARGUMENT, @@ -142,6 +143,7 @@ struct FzArgument { static FzArgument Interval(int64 imin, int64 imax); static FzArgument IntegerList(const std::vector& values); static FzArgument IntegerList(std::vector* values); + static FzArgument DomainList(const std::vector& domains); static FzArgument IntVarRef(FzIntegerVariable* const var); static FzArgument IntVarRefArray(const std::vector& vars); static FzArgument VoidArgument(); @@ -152,6 +154,7 @@ struct FzArgument { Type type; std::vector values; std::vector variables; + std::vector domains; // Helpers diff --git a/src/flatzinc/mznlib/regular_nfa.mzn b/src/flatzinc/mznlib/regular_nfa.mzn new file mode 100644 index 0000000000..8852a21cb0 --- /dev/null +++ b/src/flatzinc/mznlib/regular_nfa.mzn @@ -0,0 +1,2 @@ +predicate regular_nfa(array[int] of var int: x, int: Q, int: S, + array[int,int] of set of int: d, int: q0, set of int: F); \ No newline at end of file diff --git a/src/flatzinc/parser.yy b/src/flatzinc/parser.yy index d2c224fe96..8ae2a04d08 100644 --- a/src/flatzinc/parser.yy +++ b/src/flatzinc/parser.yy @@ -598,10 +598,14 @@ argument: $$ = FzArgument::IntVarRef(FindOrDie(context->variable_map, id)); } else if (ContainsKey(context->variable_array_map, id)) { $$ = FzArgument::IntVarRefArray(FindOrDie(context->variable_array_map, id)); - } else { - CHECK(ContainsKey(context->domain_map, id)) << "Unknown identifier: " << id; + } else if (ContainsKey(context->domain_map, id)) { const FzDomain& d = FindOrDie(context->domain_map, id); $$ = FzArgument::FromDomain(d); + } else { + CHECK(ContainsKey(context->domain_array_map, id)) << "Unknown identifier: " + << id; + const std::vector& d = FindOrDie(context->domain_array_map, id); + $$ = FzArgument::DomainList(d); } } | IDENTIFIER '[' IVALUE ']' {