Stream concrete values for variable agnostic enumerators (#2526)

4 files changed, 887 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 9948b0ec9..afc8c0f1b 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -524,6 +524,8 @@ libcvc4_add_sources(
   theory/quantifiers/sygus/cegis.h
   theory/quantifiers/sygus/cegis_unif.cpp
   theory/quantifiers/sygus/cegis_unif.h
+  theory/quantifiers/sygus/enum_stream_substitution.cpp
+  theory/quantifiers/sygus/enum_stream_substitution.h
   theory/quantifiers/sygus/sygus_eval_unfold.cpp
   theory/quantifiers/sygus/sygus_eval_unfold.h
   theory/quantifiers/sygus/sygus_explain.cpp
diff --git a/src/Makefile.am b/src/Makefile.am
index 77cfccda5..0a32cb645 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -534,6 +534,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/sygus/cegis_unif.h \
 	theory/quantifiers/sygus/ce_guided_single_inv.cpp \
 	theory/quantifiers/sygus/ce_guided_single_inv.h \
+	theory/quantifiers/sygus/enum_stream_substitution.cpp \
+	theory/quantifiers/sygus/enum_stream_substitution.h \
 	theory/quantifiers/sygus/sygus_pbe.cpp \
 	theory/quantifiers/sygus/sygus_pbe.h \
 	theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp \
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
new file mode 100644
index 000000000..3a879640f
--- /dev/null
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -0,0 +1,602 @@
+/*********************                                                        */
+/*! \file enum_stream_substitution.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief class for streaming concrete values (through substitutions) from
+ ** enumerated abstract ones
+ **/
+
+#include "theory/quantifiers/sygus/enum_stream_substitution.h"
+
+#include "options/base_options.h"
+#include "options/quantifiers_options.h"
+#include "printer/printer.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+
+#include <numeric>  // for std::iota
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+EnumStreamPermutation::EnumStreamPermutation(quantifiers::TermDbSygus* tds)
+    : d_tds(tds)
+{
+}
+
+void EnumStreamPermutation::reset(Node value)
+{
+  // clean state
+  d_var_classes.clear();
+  d_var_tn_cons.clear();
+  d_first = true;
+  d_perm_state_class.clear();
+  d_perm_values.clear();
+  d_value = value;
+  // get variables in value's type
+  TypeNode tn = value.getType();
+  Node var_list = Node::fromExpr(tn.getDatatype().getSygusVarList());
+  NodeManager* nm = NodeManager::currentNM();
+  // get subtypes in value's type
+  std::vector<TypeNode> sf_types;
+  d_tds->getSubfieldTypes(tn, sf_types);
+  // associate variables with constructors in all subfield types
+  std::map<Node, Node> cons_var;
+  for (const Node& v : var_list)
+  {
+    // collect constructors for variable in all subtypes
+    for (const TypeNode& stn : sf_types)
+    {
+      const Datatype& dt = stn.getDatatype();
+      for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
+      {
+        if (dt[i].getNumArgs() == 0 && Node::fromExpr(dt[i].getSygusOp()) == v)
+        {
+          Node cons = nm->mkNode(APPLY_CONSTRUCTOR, dt[i].getConstructor());
+          d_var_tn_cons[v][stn] = cons;
+          cons_var[cons] = v;
+        }
+      }
+    }
+  }
+  // collect variables occurring in value
+  std::vector<Node> vars;
+  std::unordered_set<Node, NodeHashFunction> visited;
+  collectVars(value, vars, visited);
+  // partition permutation variables
+  d_curr_ind = 0;
+  Trace("synth-stream-concrete") << " ..permutting vars :";
+  std::unordered_set<Node, NodeHashFunction> seen_vars;
+  for (const Node& v_cons : vars)
+  {
+    Assert(cons_var.find(v_cons) != cons_var.end());
+    Node var = cons_var[v_cons];
+    if (seen_vars.insert(var).second)
+    {
+      // do not add repeated vars
+      d_var_classes[d_tds->getSubclassForVar(tn, var)].push_back(var);
+    }
+  }
+  for (const std::pair<unsigned, std::vector<Node>>& p : d_var_classes)
+  {
+    d_perm_state_class.push_back(PermutationState(p.second));
+    if (Trace.isOn("synth-stream-concrete"))
+    {
+      Trace("synth-stream-concrete") << " " << p.first << " -> [";
+      for (const Node& var : p.second)
+      {
+        std::stringstream ss;
+        Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, var);
+        Trace("synth-stream-concrete") << " " << ss.str();
+      }
+      Trace("synth-stream-concrete") << " ]";
+    }
+  }
+  Trace("synth-stream-concrete") << "\n";
+}
+
+Node EnumStreamPermutation::getNext()
+{
+  if (Trace.isOn("synth-stream-concrete"))
+  {
+    std::stringstream ss;
+    Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_value);
+    Trace("synth-stream-concrete")
+        << " ....streaming next permutation for value : " << ss.str()
+        << " with " << d_perm_state_class.size() << " permutation classes\n";
+  }
+  // initial value
+  if (d_first)
+  {
+    d_first = false;
+    Node bultin_value = d_tds->sygusToBuiltin(d_value, d_value.getType());
+    d_perm_values.insert(
+        d_tds->getExtRewriter()->extendedRewrite(bultin_value));
+    return d_value;
+  }
+  unsigned n_classes = d_perm_state_class.size();
+  Node perm_value, bultin_perm_value;
+  do
+  {
+    bool new_perm = false;
+    while (!new_perm && d_curr_ind < n_classes)
+    {
+      if (d_perm_state_class[d_curr_ind].getNextPermutation())
+      {
+        new_perm = true;
+        Trace("synth-stream-concrete-debug2")
+            << " ....class " << d_curr_ind << " has new perm\n";
+        d_curr_ind = 0;
+      }
+      else
+      {
+        Trace("synth-stream-concrete-debug2")
+            << " ....class " << d_curr_ind << " reset\n";
+        d_perm_state_class[d_curr_ind].reset();
+        d_curr_ind++;
+      }
+    }
+    // no new permutation
+    if (!new_perm)
+    {
+      Trace("synth-stream-concrete") << " ....no new perm, return null\n";
+      return Node::null();
+    }
+    // building substitution
+    std::vector<Node> domain_sub, range_sub;
+    for (unsigned i = 0, size = d_perm_state_class.size(); i < size; ++i)
+    {
+      Trace("synth-stream-concrete") << " ..perm for class " << i << " is";
+      std::vector<Node> raw_sub;
+      d_perm_state_class[i].getLastPerm(raw_sub);
+      // retrieve variables for substitution domain
+      const std::vector<Node>& domain_sub_class =
+          d_perm_state_class[i].getVars();
+      Assert(domain_sub_class.size() == raw_sub.size());
+      // build proper substitution based on variables types and constructors
+      for (unsigned j = 0, size_j = raw_sub.size(); j < size_j; ++j)
+      {
+        for (std::pair<const TypeNode, Node>& p :
+             d_var_tn_cons[domain_sub_class[j]])
+        {
+          // get constructor of type p.first from variable being permuted
+          domain_sub.push_back(p.second);
+          // get constructor of type p.first from variable to be permuted for
+          range_sub.push_back(d_var_tn_cons[raw_sub[j]][p.first]);
+          Trace("synth-stream-concrete-debug2")
+              << "\n ....{ adding " << domain_sub.back() << " ["
+              << domain_sub.back().getType() << "] -> " << range_sub.back()
+              << " [" << range_sub.back().getType() << "] }";
+        }
+      }
+      Trace("synth-stream-concrete") << "\n";
+    }
+    perm_value = d_value.substitute(domain_sub.begin(),
+                                    domain_sub.end(),
+                                    range_sub.begin(),
+                                    range_sub.end());
+    bultin_perm_value = d_tds->sygusToBuiltin(perm_value, perm_value.getType());
+    Trace("synth-stream-concrete-debug")
+        << " ......perm builtin is " << bultin_perm_value;
+    bultin_perm_value =
+        d_tds->getExtRewriter()->extendedRewrite(bultin_perm_value);
+    Trace("synth-stream-concrete-debug")
+        << " and rewrites to " << bultin_perm_value << "\n";
+    // if permuted value is equivalent modulo rewriting to a previous one, look
+    // for another
+  } while (!d_perm_values.insert(bultin_perm_value).second);
+  if (Trace.isOn("synth-stream-concrete"))
+  {
+    std::stringstream ss;
+    Printer::getPrinter(options::outputLanguage())
+        ->toStreamSygus(ss, perm_value);
+    Trace("synth-stream-concrete")
+        << " ....return new perm " << ss.str() << "\n";
+  }
+  return perm_value;
+}
+
+const std::vector<Node>& EnumStreamPermutation::getVarsClass(unsigned id) const
+{
+  std::map<unsigned, std::vector<Node>>::const_iterator it =
+      d_var_classes.find(id);
+  Assert(it != d_var_classes.end());
+  return it->second;
+}
+
+unsigned EnumStreamPermutation::getVarClassSize(unsigned id) const
+{
+  std::map<unsigned, std::vector<Node>>::const_iterator it =
+      d_var_classes.find(id);
+  if (it == d_var_classes.end())
+  {
+    return 0;
+  }
+  return it->second.size();
+}
+
+void EnumStreamPermutation::collectVars(
+    Node n,
+    std::vector<Node>& vars,
+    std::unordered_set<Node, NodeHashFunction>& visited)
+{
+  if (visited.find(n) != visited.end())
+  {
+    return;
+  }
+  visited.insert(n);
+  if (n.getNumChildren() > 0)
+  {
+    for (const Node& ni : n)
+    {
+      collectVars(ni, vars, visited);
+    }
+    return;
+  }
+  if (d_tds->sygusToBuiltin(n, n.getType()).getKind() == kind::BOUND_VARIABLE)
+  {
+    if (std::find(vars.begin(), vars.end(), n) == vars.end())
+    {
+      vars.push_back(n);
+    }
+    return;
+  }
+}
+
+EnumStreamPermutation::PermutationState::PermutationState(
+    const std::vector<Node>& vars)
+{
+  d_vars = vars;
+  d_curr_ind = 0;
+  d_seq.resize(vars.size());
+  std::fill(d_seq.begin(), d_seq.end(), 0);
+  // initialize variable indices
+  d_last_perm.resize(vars.size());
+  std::iota(d_last_perm.begin(), d_last_perm.end(), 0);
+}
+
+void EnumStreamPermutation::PermutationState::reset()
+{
+  d_curr_ind = 0;
+  std::fill(d_seq.begin(), d_seq.end(), 0);
+  std::iota(d_last_perm.begin(), d_last_perm.end(), 0);
+}
+
+const std::vector<Node>& EnumStreamPermutation::PermutationState::getVars()
+    const
+{
+  return d_vars;
+}
+
+void EnumStreamPermutation::PermutationState::getLastPerm(
+    std::vector<Node>& vars)
+{
+  for (unsigned i = 0, size = d_last_perm.size(); i < size; ++i)
+  {
+    if (Trace.isOn("synth-stream-concrete"))
+    {
+      std::stringstream ss;
+      Printer::getPrinter(options::outputLanguage())
+          ->toStreamSygus(ss, d_vars[d_last_perm[i]]);
+      Trace("synth-stream-concrete") << " " << ss.str();
+    }
+    vars.push_back(d_vars[d_last_perm[i]]);
+  }
+}
+
+bool EnumStreamPermutation::PermutationState::getNextPermutation()
+{
+  // exhausted permutations
+  if (d_curr_ind == d_vars.size())
+  {
+    Trace("synth-stream-concrete-debug2") << "exhausted perms, ";
+    return false;
+  }
+  if (d_seq[d_curr_ind] >= d_curr_ind)
+  {
+    d_seq[d_curr_ind] = 0;
+    d_curr_ind++;
+    return getNextPermutation();
+  }
+  if (d_curr_ind % 2 == 0)
+  {
+    // swap with first element
+    std::swap(d_last_perm[0], d_last_perm[d_curr_ind]);
+  }
+  else
+  {
+    // swap with element in index in sequence of current index
+    std::swap(d_last_perm[d_seq[d_curr_ind]], d_last_perm[d_curr_ind]);
+  }
+  d_seq[d_curr_ind] += 1;
+  d_curr_ind = 0;
+  return true;
+}
+
+EnumStreamSubstitution::EnumStreamSubstitution(quantifiers::TermDbSygus* tds)
+    : d_tds(tds), d_stream_permutations(tds)
+{
+}
+
+void EnumStreamSubstitution::initialize(TypeNode tn)
+{
+  d_tn = tn;
+  // get variables in value's type
+  Node var_list = Node::fromExpr(tn.getDatatype().getSygusVarList());
+  // get subtypes in value's type
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<TypeNode> sf_types;
+  d_tds->getSubfieldTypes(tn, sf_types);
+  // associate variables with constructors in all subfield types
+  for (const Node& v : var_list)
+  {
+    // collect constructors for variable in all subtypes
+    for (const TypeNode& stn : sf_types)
+    {
+      const Datatype& dt = stn.getDatatype();
+      for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
+      {
+        if (dt[i].getNumArgs() == 0 && Node::fromExpr(dt[i].getSygusOp()) == v)
+        {
+          d_var_tn_cons[v][stn] =
+              nm->mkNode(APPLY_CONSTRUCTOR, dt[i].getConstructor());
+        }
+      }
+    }
+  }
+  // split initial variables into classes
+  for (const Node& v : var_list)
+  {
+    Assert(d_tds->getSubclassForVar(tn, v) > 0);
+    d_var_classes[d_tds->getSubclassForVar(tn, v)].push_back(v);
+  }
+}
+
+void EnumStreamSubstitution::resetValue(Node value)
+{
+  if (Trace.isOn("synth-stream-concrete"))
+  {
+    std::stringstream ss;
+    Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, value);
+    Trace("synth-stream-concrete")
+        << " * Streaming concrete: registering value " << ss.str() << "\n";
+  }
+  d_last = Node::null();
+  d_value = value;
+  // reset permutation util
+  d_stream_permutations.reset(value);
+  // reset combination utils
+  d_curr_ind = 0;
+  d_comb_state_class.clear();
+  Trace("synth-stream-concrete") << " ..combining vars  :";
+  for (const std::pair<unsigned, std::vector<Node>>& p : d_var_classes)
+  {
+    // ignore classes without variables being permuted
+    unsigned perm_var_class_sz = d_stream_permutations.getVarClassSize(p.first);
+    if (perm_var_class_sz == 0)
+    {
+      continue;
+    }
+    d_comb_state_class.push_back(CombinationState(
+        p.second.size(), perm_var_class_sz, p.first, p.second));
+    if (Trace.isOn("synth-stream-concrete"))
+    {
+      Trace("synth-stream-concrete")
+          << " " << p.first << " -> " << perm_var_class_sz << " from [ ";
+      for (const Node& var : p.second)
+      {
+        std::stringstream ss;
+        Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, var);
+        Trace("synth-stream-concrete") << " " << ss.str();
+      }
+      Trace("synth-stream-concrete") << " ]";
+    }
+  }
+  Trace("synth-stream-concrete") << "\n";
+}
+
+Node EnumStreamSubstitution::getNext()
+{
+  if (Trace.isOn("synth-stream-concrete"))
+  {
+    std::stringstream ss;
+    Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_value);
+    Trace("synth-stream-concrete")
+        << " ..streaming next combination of " << ss.str() << "\n";
+  }
+  unsigned n_classes = d_comb_state_class.size();
+  // intial case
+  if (d_last.isNull())
+  {
+    d_last = d_stream_permutations.getNext();
+  }
+  else
+  {
+    bool new_comb = false;
+    while (!new_comb && d_curr_ind < n_classes)
+    {
+      if (d_comb_state_class[d_curr_ind].getNextCombination())
+      {
+        new_comb = true;
+        Trace("synth-stream-concrete-debug2")
+            << " ....class " << d_curr_ind << " has new comb\n";
+        d_curr_ind = 0;
+      }
+      else
+      {
+        Trace("synth-stream-concrete-debug2")
+            << " ....class " << d_curr_ind << " reset\n";
+        d_comb_state_class[d_curr_ind].reset();
+        d_curr_ind++;
+      }
+    }
+    // no new combination
+    if (!new_comb)
+    {
+      Trace("synth-stream-concrete")
+          << " ..no new comb, get next permutation\n ....total combs until "
+             "here : "
+          << d_comb_values.size() << "\n";
+      d_last = d_stream_permutations.getNext();
+      // exhausted permutations
+      if (d_last.isNull())
+      {
+        Trace("synth-stream-concrete") << " ..no new comb, return null\n";
+        return Node::null();
+      }
+      // reset combination classes for next permutation
+      d_curr_ind = 0;
+      for (unsigned i = 0, size = d_comb_state_class.size(); i < size; ++i)
+      {
+        d_comb_state_class[i].reset();
+      }
+    }
+  }
+  if (Trace.isOn("synth-stream-concrete-debug"))
+  {
+    std::stringstream ss;
+    Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_last);
+    Trace("synth-stream-concrete-debug")
+        << " ..using base perm " << ss.str() << "\n";
+  }
+  // building substitution
+  std::vector<Node> domain_sub, range_sub;
+  for (unsigned i = 0, size = d_comb_state_class.size(); i < size; ++i)
+  {
+    Trace("synth-stream-concrete")
+        << " ..comb for class " << d_comb_state_class[i].getSubclassId()
+        << " is";
+    std::vector<Node> raw_sub;
+    d_comb_state_class[i].getLastComb(raw_sub);
+    // retrieve variables for substitution domain
+    const std::vector<Node>& domain_sub_class =
+        d_stream_permutations.getVarsClass(
+            d_comb_state_class[i].getSubclassId());
+    Assert(domain_sub_class.size() == raw_sub.size());
+    // build proper substitution based on variables types and constructors
+    for (unsigned j = 0, size_j = raw_sub.size(); j < size_j; ++j)
+    {
+      for (std::pair<const TypeNode, Node>& p :
+           d_var_tn_cons[domain_sub_class[j]])
+      {
+        // get constructor of type p.first from variable being permuted
+        domain_sub.push_back(p.second);
+        // get constructor of type p.first from variable to be permuted for
+        range_sub.push_back(d_var_tn_cons[raw_sub[j]][p.first]);
+        Trace("synth-stream-concrete-debug2")
+            << "\n ....{ adding " << domain_sub.back() << " ["
+            << domain_sub.back().getType() << "] -> " << range_sub.back()
+            << " [" << range_sub.back().getType() << "] }";
+      }
+    }
+    Trace("synth-stream-concrete") << "\n";
+  }
+  Node comb_value = d_last.substitute(
+      domain_sub.begin(), domain_sub.end(), range_sub.begin(), range_sub.end());
+  // the new combination value should be fresh, modulo rewriting, by
+  // construction (unless it's equiv to a constant, e.g. true / false)
+  Node builtin_comb_value = d_tds->getExtRewriter()->extendedRewrite(
+      d_tds->sygusToBuiltin(comb_value, comb_value.getType()));
+  if (Trace.isOn("synth-stream-concrete"))
+  {
+    std::stringstream ss;
+    Printer::getPrinter(options::outputLanguage())
+        ->toStreamSygus(ss, comb_value);
+    Trace("synth-stream-concrete")
+        << " ....register new comb value " << ss.str()
+        << " with rewritten form " << builtin_comb_value
+        << (builtin_comb_value.isConst() ? " (isConst)" : "") << "\n";
+  }
+  if (!builtin_comb_value.isConst()
+      && !d_comb_values.insert(builtin_comb_value).second)
+  {
+    std::stringstream ss, ss1;
+    Printer::getPrinter(options::outputLanguage())
+        ->toStreamSygus(ss, comb_value);
+    Trace("synth-stream-concrete")
+        << " ..term " << ss.str() << " is REDUNDANT with " << builtin_comb_value
+        << "\n ..excluding all other concretizations (had "
+        << d_comb_values.size() << " already)\n\n";
+    return Node::null();
+  }
+  if (Trace.isOn("synth-stream-concrete"))
+  {
+    std::stringstream ss;
+    Printer::getPrinter(options::outputLanguage())
+        ->toStreamSygus(ss, comb_value);
+    Trace("synth-stream-concrete")
+        << " ..return new comb " << ss.str() << "\n\n";
+  }
+  return comb_value;
+}
+
+EnumStreamSubstitution::CombinationState::CombinationState(
+    unsigned n, unsigned k, unsigned subclass_id, const std::vector<Node>& vars)
+    : d_n(n), d_k(k)
+{
+  Assert(!vars.empty());
+  Assert(k <= n);
+  d_last_comb.resize(k);
+  std::iota(d_last_comb.begin(), d_last_comb.end(), 0);
+  d_vars = vars;
+  d_subclass_id = subclass_id;
+}
+
+const unsigned EnumStreamSubstitution::CombinationState::getSubclassId() const
+{
+  return d_subclass_id;
+}
+
+void EnumStreamSubstitution::CombinationState::reset()
+{
+  std::iota(d_last_comb.begin(), d_last_comb.end(), 0);
+}
+
+void EnumStreamSubstitution::CombinationState::getLastComb(
+    std::vector<Node>& vars)
+{
+  for (unsigned i = 0, size = d_last_comb.size(); i < size; ++i)
+  {
+    if (Trace.isOn("synth-stream-concrete"))
+    {
+      std::stringstream ss;
+      Printer::getPrinter(options::outputLanguage())
+          ->toStreamSygus(ss, d_vars[d_last_comb[i]]);
+      Trace("synth-stream-concrete") << " " << ss.str();
+    }
+    vars.push_back(d_vars[d_last_comb[i]]);
+  }
+}
+
+bool EnumStreamSubstitution::CombinationState::getNextCombination()
+{
+  // find what to increment
+  bool new_comb = false;
+  for (int i = d_k - 1; i >= 0; --i)
+  {
+    if (d_last_comb[i] < d_n - d_k + i)
+    {
+      unsigned j = d_last_comb[i] + 1;
+      while (static_cast<unsigned>(i) <= d_k - 1)
+      {
+        d_last_comb[i++] = j++;
+      }
+      new_comb = true;
+      break;
+    }
+  }
+  return new_comb;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h
new file mode 100644
index 000000000..5d3daa538
--- /dev/null
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h
@@ -0,0 +1,281 @@
+/*********************                                                        */
+/*! \file enum_stream_substitution.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief class for streaming concrete values (through substitutions) from
+ ** enumerated abstract ones
+ **/
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
+
+#include "expr/node.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Streamer of different values according to variable permutations
+ *
+ * Generates a new value (modulo rewriting) when queried in which its variables
+ * are permuted (see EnumStreamSubstitution for more details).
+ */
+class EnumStreamPermutation
+{
+ public:
+  EnumStreamPermutation(quantifiers::TermDbSygus* tds);
+  ~EnumStreamPermutation() {}
+  /** resets utility
+   *
+   * for each subset of the variables in value (according to their
+   * subclasses_classes), a permutation utility is initialized
+   */
+  void reset(Node value);
+  /** computes next permutation, if any, of value
+   *
+   * a "next" permutation is determined by having at least one new permutation
+   * in one of the variable subclasses in the value.
+   *
+   * For example, if the variables of value (OP x1 x2 x3 x4) are partioned into
+   * {{x1, x4}, {x2, x3}} then the sequence of getNext() is
+   *
+   * (OP x4 x2 x3 x1)
+   * (OP x1 x3 x2 x4)
+   * (OP x4 x3 x2 x1)
+   *
+   * Moreover, new values are only considered if they are unique modulo
+   * rewriting. If for example OP were "+", then no next value would exist,
+   * while if OP were "-" the only next value would be: (- x4 x2 x3 x1)
+   *
+   * Since the same variable can occur in different subfield types (and
+   * therefore their datatype equivalents would have different types) a map from
+   * variables to sets of constructors (see var_cons) is used to build
+   * substitutions in a proper way when generating different combinations.
+   */
+  Node getNext();
+  /** retrieve variables in class with given id */
+  const std::vector<Node>& getVarsClass(unsigned id) const;
+  /** retrieve number of variables being permuted from subclass with given id */
+  unsigned getVarClassSize(unsigned id) const;
+
+ private:
+  /** sygus term database of current quantifiers engine */
+  quantifiers::TermDbSygus* d_tds;
+  /** maps subclass ids to subset of d_vars with that subclass id */
+  std::map<unsigned, std::vector<Node>> d_var_classes;
+  /** maps variables to subfield types with constructors for
+   * the that variable, which are themselves associated with the respective
+   * constructors */
+  std::map<Node, std::map<TypeNode, Node>> d_var_tn_cons;
+  /** whether first query */
+  bool d_first;
+  /** value to which we are generating permutations */
+  Node d_value;
+  /** generated permutations (modulo rewriting) */
+  std::unordered_set<Node, NodeHashFunction> d_perm_values;
+  /** retrieves variables occurring in value */
+  void collectVars(Node n,
+                   std::vector<Node>& vars,
+                   std::unordered_set<Node, NodeHashFunction>& visited);
+  /** Utility for stepwise application of Heap's algorithm for permutation
+   *
+   * see https://en.wikipedia.org/wiki/Heap%27s_algorithm
+   */
+  class PermutationState
+  {
+   public:
+    PermutationState(const std::vector<Node>& vars);
+    /** computes next permutation, i.e. execute one step of Heap's algorithm
+     *
+     * returns true if one exists, false otherwise
+     *
+     * when a new permutation is generated the the new variable arrangement is
+     * stored in d_last_perm (in terms of d_vars' indices)
+     */
+    bool getNextPermutation();
+    /** resets permutation state to initial variable ordering */
+    void reset();
+    /** retrieves last variable permutation
+     *
+     * vars is populated with the new variable arrangement
+     */
+    void getLastPerm(std::vector<Node>& vars);
+    /** retrieve variables being permuted */
+    const std::vector<Node>& getVars() const;
+
+   private:
+    /** variables being permuted */
+    std::vector<Node> d_vars;
+    /** last computed permutation of variables */
+    std::vector<unsigned> d_last_perm;
+    /** auxiliary position list for generating permutations */
+    std::vector<unsigned> d_seq;
+    /** current index being permuted */
+    unsigned d_curr_ind;
+  };
+  /** permutation state of each variable subclass */
+  std::vector<PermutationState> d_perm_state_class;
+  /** current variable subclass being permuted */
+  unsigned d_curr_ind;
+};
+
+/** Streamer of concrete values for enumerator
+ *
+ * When a given enumerator is "variable agnostic", only values in which
+ * variables are ordered are chosen for it (see
+ * TermDbSygus::registerEnumerator). If such values are seen as "abstract", in
+ * the sense that each represent a set of values, this class can be used to
+ * stream all the concrete values that correspond to them.
+ *
+ * For example a variable agnostic enumerator that contains three variables, x1,
+ * x2, x3, in which x1 < x2 < x3, for which an "abstract" value (OP x1 x2) is
+ * derived, will lead to the stream of "concrete" values
+ *
+ * (OP x1 x2)
+ * (OP x1 x3)
+ * (OP x2 x3)
+ *
+ * (OP x2 x1)
+ * (OP x3 x1)
+ * (OP x3 x2)
+ *
+ * in which for each permutation of the variables in the abstract value ([x1,
+ * x2] and [x2, x1] in the above) we generate all the substitutions through
+ * ordered combinations of the variables of the enumerator ([x1, x2], [x1, x3],
+ * and [x2, x3] in the above).
+ *
+ * Moreover the permutations are generated modulo rewriting, s.t. if two
+ * permutations are equivalent, only one is used.
+ *
+ * It should be noted that the variables of a variable agnostic enumerator are
+ * kept in independent "subclasses" (see TermDbSygus::getSubclassForVar).
+ * Therefore when streaming concrete values, permutations and combinations are
+ * generated by the product of the permutations and combinations of each class.
+ */
+class EnumStreamSubstitution
+{
+ public:
+  EnumStreamSubstitution(quantifiers::TermDbSygus* tds);
+  ~EnumStreamSubstitution() {}
+  /** initializes utility
+   *
+   * the combinations are generated from a initial set of variables (for now all
+   * variables in given type).
+   */
+  void initialize(TypeNode tn);
+  /** resets value for which substitutions will be generated through
+   * combinations
+   *
+   * For each variable subclass in this utility, a subset is chosen with as
+   * many variables as in the same variable subclass of value's variables.
+   *
+   * The combinations are performed modulo subclasses. For each subclass of the
+   * given variables, a combination utility is initialized.
+   *
+   * For example, if the initial variable set is partioned into
+   *
+   * {1 -> {x1, x4}, 2 -> {x2, x3, x6}, 3 -> {x5}}
+   *
+   * and value's variables into
+   *
+   * {1 -> {x1, x4}, 2 -> {x2}, 3 -> {}}
+   *
+   * then the combination utilities are initialized such that for class 1 all
+   * ordered subsets with two variables are chosen; for class 2 all ordered
+   * subsets with one variable; and for class 3 no combination can be chosen.
+   */
+  void resetValue(Node value);
+  /** computes next combination, if any, of value
+   *
+   * a "next" combination is determined by having at least one new combination
+   * in one of the variable subclasses in the initial set of variables. If no
+   * new combination exists, the cycle restarts with a new base value generated
+   * by EnumStreamPermutation::getNext() (see above).
+   *
+   * This layered approach (of deriving all combinations for each permutation)
+   * allows to consider only ordered combinations to generate all possible
+   * variations of the base value. See the example in EnumStreamSubstitution for
+   * further details.
+   */
+  Node getNext();
+
+ private:
+  /** sygus term database of current quantifiers engine */
+  quantifiers::TermDbSygus* d_tds;
+  /** type this utility has been initialized for */
+  TypeNode d_tn;
+  /** current value */
+  Node d_value;
+  /** maps subclass ids to d_tn's variables with that subclass id */
+  std::map<unsigned, std::vector<Node>> d_var_classes;
+  /** maps variables to subfield types with constructors for
+   * the that variable, which are themselves associated with the respective
+   * constructors */
+  std::map<Node, std::map<TypeNode, Node>> d_var_tn_cons;
+  /** last value generated after a combination
+   *
+   * If getNext() has been called, this is the return value of the most recent
+   * call to getNext(). Otherwise, this value is null.
+   */
+  Node d_last;
+  /** generated combinations */
+  std::unordered_set<Node, NodeHashFunction> d_comb_values;
+  /** permutation utility */
+  EnumStreamPermutation d_stream_permutations;
+  /** Utility for stepwise generation of ordered subsets of size k from n
+   * variables */
+  class CombinationState
+  {
+   public:
+    CombinationState(unsigned n,
+                     unsigned k,
+                     unsigned subclass_id,
+                     const std::vector<Node>& vars);
+    /** computes next combination
+     *
+     * returns true if one exists, false otherwise
+     */
+    bool getNextCombination();
+    /** resets combination state to first k variables in vars */
+    void reset();
+    /** retrieves last variable combination
+     *
+     * variables in new combination are stored in argument vars
+     */
+    void getLastComb(std::vector<Node>& vars);
+    /** retrieve subclass id */
+    const unsigned getSubclassId() const;
+
+   private:
+    /** subclass id of variables being combined */
+    unsigned d_subclass_id;
+    /** number of variables */
+    unsigned d_n;
+    /** size of subset */
+    unsigned d_k;
+    /** last combination state */
+    std::vector<unsigned> d_last_comb;
+    /** variables from which combination is extracted */
+    std::vector<Node> d_vars;
+  };
+  /** combination state for each variable subclass */
+  std::vector<CombinationState> d_comb_state_class;
+  /** current class being combined */
+  unsigned d_curr_ind;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif