support regular_nfa

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]);

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<int64>& 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<IntVar*> 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<FzDomain>& 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<int64> 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") {

src/flatzinc/model.cc

@@ -245,6 +245,13 @@ FzArgument FzArgument::IntegerList(std::vector<int64>* values) {
   return result;
 }
 
+FzArgument FzArgument::DomainList(const std::vector<FzDomain>& 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: {

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<int64>& values);
   static FzArgument IntegerList(std::vector<int64>* values);
+  static FzArgument DomainList(const std::vector<FzDomain>& domains);
   static FzArgument IntVarRef(FzIntegerVariable* const var);
   static FzArgument IntVarRefArray(const std::vector<FzIntegerVariable*>& vars);
   static FzArgument VoidArgument();
@@ -152,6 +154,7 @@ struct FzArgument {
   Type type;
   std::vector<int64> values;
   std::vector<FzIntegerVariable*> variables;
+  std::vector<FzDomain> domains;
 
   // Helpers
 

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

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<FzDomain>& d = FindOrDie(context->domain_array_map, id);
+    $$ = FzArgument::DomainList(d);
   }
 }
 | IDENTIFIER '[' IVALUE ']' {