Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/enum_stream_substitution.cpp	Lines:	230	345	66.7 %
Date:	2021-05-22	Branches:	326	1118	29.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Haniel Barbosa, Andrew Reynolds, Gereon Kremer
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * Class for streaming concrete values (through substitutions) from
 * enumerated abstract ones.
 */

#include "theory/quantifiers/sygus/enum_stream_substitution.h"

#include "expr/dtype_cons.h"
#include "options/base_options.h"
#include "options/datatypes_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 cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

EnumStreamPermutation::EnumStreamPermutation(quantifiers::TermDbSygus* tds)
    : d_tds(tds), d_first(true), d_curr_ind(0)
{
}

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 = tn.getDType().getSygusVarList();
  NodeManager* nm = NodeManager::currentNM();
  // get subtypes in value's type
  SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
  std::vector<TypeNode> sf_types;
  ti.getSubfieldTypes(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 DType& dt = stn.getDType();
      for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
      {
        if (dt[i].getNumArgs() == 0 && 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> visited;
  collectVars(value, vars, visited);
  // partition permutation variables
  d_curr_ind = 0;
  Trace("synth-stream-concrete") << " ..permutting vars :";
  std::unordered_set<Node> 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[ti.getSubclassForVar(var)].push_back(var);
    }
  }
  for (const std::pair<const 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;
        TermDbSygus::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;
    TermDbSygus::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;
    if (options::sygusSymBreakDynamic())
    {
      bultin_perm_value =
          d_tds->getExtRewriter()->extendedRewrite(bultin_perm_value);
      Trace("synth-stream-concrete-debug")
          << " and rewrites to " << bultin_perm_value;
    }
    Trace("synth-stream-concrete-debug") << "\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;
    TermDbSygus::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>& 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;
      TermDbSygus::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), d_curr_ind(0)
{
}

void EnumStreamSubstitution::initialize(TypeNode tn)
{
  d_tn = tn;
  // get variables in value's type
  Node var_list = tn.getDType().getSygusVarList();
  // get subtypes in value's type
  NodeManager* nm = NodeManager::currentNM();
  SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
  std::vector<TypeNode> sf_types;
  ti.getSubfieldTypes(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 DType& dt = stn.getDType();
      for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
      {
        if (dt[i].getNumArgs() == 0 && 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(ti.getSubclassForVar(v) > 0);
    d_var_classes[ti.getSubclassForVar(v)].push_back(v);
  }
}

void EnumStreamSubstitution::resetValue(Node value)
{
  if (Trace.isOn("synth-stream-concrete"))
  {
    std::stringstream ss;
    TermDbSygus::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<const 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;
        TermDbSygus::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;
    TermDbSygus::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;
    TermDbSygus::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->sygusToBuiltin(comb_value, comb_value.getType());
  if (options::sygusSymBreakDynamic())
  {
    builtin_comb_value =
        d_tds->getExtRewriter()->extendedRewrite(builtin_comb_value);
  }
  if (Trace.isOn("synth-stream-concrete"))
  {
    std::stringstream ss;
    TermDbSygus::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)
  {
    if (Trace.isOn("synth-stream-concrete"))
    {
      std::stringstream ss, ss1;
      TermDbSygus::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;
    TermDbSygus::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;
      TermDbSygus::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;
}

void EnumStreamConcrete::initialize(Node e) { d_ess.initialize(e.getType()); }
void EnumStreamConcrete::addValue(Node v)
{
  d_ess.resetValue(v);
  d_currTerm = d_ess.getNext();
}
bool EnumStreamConcrete::increment()
{
  d_currTerm = d_ess.getNext();
  return !d_currTerm.isNull();
}
Node EnumStreamConcrete::getCurrent() { return d_currTerm; }
}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Haniel Barbosa, Andrew Reynolds, Gereon Kremer
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Class for streaming concrete values (through substitutions) from
14		* enumerated abstract ones.
15		*/
16
17		#include "theory/quantifiers/sygus/enum_stream_substitution.h"
18
19		#include "expr/dtype_cons.h"
20		#include "options/base_options.h"
21		#include "options/datatypes_options.h"
22		#include "options/quantifiers_options.h"
23		#include "printer/printer.h"
24		#include "theory/quantifiers/sygus/term_database_sygus.h"
25
26		#include <numeric> // for std::iota
27
28		using namespace cvc5::kind;
29
30		namespace cvc5 {
31		namespace theory {
32		namespace quantifiers {
33
34	1	EnumStreamPermutation::EnumStreamPermutation(quantifiers::TermDbSygus* tds)
35	1	: d_tds(tds), d_first(true), d_curr_ind(0)
36		{
37	1	}
38
39	1	void EnumStreamPermutation::reset(Node value)
40		{
41		// clean state
42	1	d_var_classes.clear();
43	1	d_var_tn_cons.clear();
44	1	d_first = true;
45	1	d_perm_state_class.clear();
46	1	d_perm_values.clear();
47	1	d_value = value;
48		// get variables in value's type
49	2	TypeNode tn = value.getType();
50	2	Node var_list = tn.getDType().getSygusVarList();
51	1	NodeManager* nm = NodeManager::currentNM();
52		// get subtypes in value's type
53	1	SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
54	2	std::vector<TypeNode> sf_types;
55	1	ti.getSubfieldTypes(sf_types);
56		// associate variables with constructors in all subfield types
57	2	std::map<Node, Node> cons_var;
58	3	for (const Node& v : var_list)
59		{
60		// collect constructors for variable in all subtypes
61	4	for (const TypeNode& stn : sf_types)
62		{
63	2	const DType& dt = stn.getDType();
64	8	for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
65		{
66	6	if (dt[i].getNumArgs() == 0 && dt[i].getSygusOp() == v)
67		{
68	4	Node cons = nm->mkNode(APPLY_CONSTRUCTOR, dt[i].getConstructor());
69	2	d_var_tn_cons[v][stn] = cons;
70	2	cons_var[cons] = v;
71		}
72		}
73		}
74		}
75		// collect variables occurring in value
76	2	std::vector<Node> vars;
77	2	std::unordered_set<Node> visited;
78	1	collectVars(value, vars, visited);
79		// partition permutation variables
80	1	d_curr_ind = 0;
81	1	Trace("synth-stream-concrete") << " ..permutting vars :";
82	2	std::unordered_set<Node> seen_vars;
83	2	for (const Node& v_cons : vars)
84		{
85	1	Assert(cons_var.find(v_cons) != cons_var.end());
86	2	Node var = cons_var[v_cons];
87	1	if (seen_vars.insert(var).second)
88		{
89		// do not add repeated vars
90	1	d_var_classes[ti.getSubclassForVar(var)].push_back(var);
91		}
92		}
93	2	for (const std::pair<const unsigned, std::vector<Node>>& p : d_var_classes)
94		{
95	1	d_perm_state_class.push_back(PermutationState(p.second));
96	1	if (Trace.isOn("synth-stream-concrete"))
97		{
98		Trace("synth-stream-concrete") << " " << p.first << " -> [";
99		for (const Node& var : p.second)
100		{
101		std::stringstream ss;
102		TermDbSygus::toStreamSygus(ss, var);
103		Trace("synth-stream-concrete") << " " << ss.str();
104		}
105		Trace("synth-stream-concrete") << " ]";
106		}
107		}
108	1	Trace("synth-stream-concrete") << "\n";
109	1	}
110
111	2	Node EnumStreamPermutation::getNext()
112		{
113	2	if (Trace.isOn("synth-stream-concrete"))
114		{
115		std::stringstream ss;
116		TermDbSygus::toStreamSygus(ss, d_value);
117		Trace("synth-stream-concrete")
118		<< " ....streaming next permutation for value : " << ss.str()
119		<< " with " << d_perm_state_class.size() << " permutation classes\n";
120		}
121		// initial value
122	2	if (d_first)
123		{
124	1	d_first = false;
125	2	Node bultin_value = d_tds->sygusToBuiltin(d_value, d_value.getType());
126	1	d_perm_values.insert(
127	2	d_tds->getExtRewriter()->extendedRewrite(bultin_value));
128	1	return d_value;
129		}
130	1	unsigned n_classes = d_perm_state_class.size();
131	2	Node perm_value, bultin_perm_value;
132		do
133		{
134	1	bool new_perm = false;
135	3	while (!new_perm && d_curr_ind < n_classes)
136		{
137	1	if (d_perm_state_class[d_curr_ind].getNextPermutation())
138		{
139		new_perm = true;
140		Trace("synth-stream-concrete-debug2")
141		<< " ....class " << d_curr_ind << " has new perm\n";
142		d_curr_ind = 0;
143		}
144		else
145		{
146	2	Trace("synth-stream-concrete-debug2")
147	1	<< " ....class " << d_curr_ind << " reset\n";
148	1	d_perm_state_class[d_curr_ind].reset();
149	1	d_curr_ind++;
150		}
151		}
152		// no new permutation
153	1	if (!new_perm)
154		{
155	1	Trace("synth-stream-concrete") << " ....no new perm, return null\n";
156	1	return Node::null();
157		}
158		// building substitution
159		std::vector<Node> domain_sub, range_sub;
160		for (unsigned i = 0, size = d_perm_state_class.size(); i < size; ++i)
161		{
162		Trace("synth-stream-concrete") << " ..perm for class " << i << " is";
163		std::vector<Node> raw_sub;
164		d_perm_state_class[i].getLastPerm(raw_sub);
165		// retrieve variables for substitution domain
166		const std::vector<Node>& domain_sub_class =
167		d_perm_state_class[i].getVars();
168		Assert(domain_sub_class.size() == raw_sub.size());
169		// build proper substitution based on variables types and constructors
170		for (unsigned j = 0, size_j = raw_sub.size(); j < size_j; ++j)
171		{
172		for (std::pair<const TypeNode, Node>& p :
173		d_var_tn_cons[domain_sub_class[j]])
174		{
175		// get constructor of type p.first from variable being permuted
176		domain_sub.push_back(p.second);
177		// get constructor of type p.first from variable to be permuted for
178		range_sub.push_back(d_var_tn_cons[raw_sub[j]][p.first]);
179		Trace("synth-stream-concrete-debug2")
180		<< "\n ....{ adding " << domain_sub.back() << " ["
181		<< domain_sub.back().getType() << "] -> " << range_sub.back()
182		<< " [" << range_sub.back().getType() << "] }";
183		}
184		}
185		Trace("synth-stream-concrete") << "\n";
186		}
187		perm_value = d_value.substitute(domain_sub.begin(),
188		domain_sub.end(),
189		range_sub.begin(),
190		range_sub.end());
191		bultin_perm_value = d_tds->sygusToBuiltin(perm_value, perm_value.getType());
192		Trace("synth-stream-concrete-debug")
193		<< " ......perm builtin is " << bultin_perm_value;
194		if (options::sygusSymBreakDynamic())
195		{
196		bultin_perm_value =
197		d_tds->getExtRewriter()->extendedRewrite(bultin_perm_value);
198		Trace("synth-stream-concrete-debug")
199		<< " and rewrites to " << bultin_perm_value;
200		}
201		Trace("synth-stream-concrete-debug") << "\n";
202		// if permuted value is equivalent modulo rewriting to a previous one, look
203		// for another
204		} while (!d_perm_values.insert(bultin_perm_value).second);
205		if (Trace.isOn("synth-stream-concrete"))
206		{
207		std::stringstream ss;
208		TermDbSygus::toStreamSygus(ss, perm_value);
209		Trace("synth-stream-concrete")
210		<< " ....return new perm " << ss.str() << "\n";
211		}
212		return perm_value;
213		}
214
215	2	const std::vector<Node>& EnumStreamPermutation::getVarsClass(unsigned id) const
216		{
217		std::map<unsigned, std::vector<Node>>::const_iterator it =
218	2	d_var_classes.find(id);
219	2	Assert(it != d_var_classes.end());
220	2	return it->second;
221		}
222
223	1	unsigned EnumStreamPermutation::getVarClassSize(unsigned id) const
224		{
225		std::map<unsigned, std::vector<Node>>::const_iterator it =
226	1	d_var_classes.find(id);
227	1	if (it == d_var_classes.end())
228		{
229		return 0;
230		}
231	1	return it->second.size();
232		}
233
234	1	void EnumStreamPermutation::collectVars(Node n,
235		std::vector<Node>& vars,
236		std::unordered_set<Node>& visited)
237		{
238	1	if (visited.find(n) != visited.end())
239		{
240		return;
241		}
242	1	visited.insert(n);
243	1	if (n.getNumChildren() > 0)
244		{
245		for (const Node& ni : n)
246		{
247		collectVars(ni, vars, visited);
248		}
249		return;
250		}
251	1	if (d_tds->sygusToBuiltin(n, n.getType()).getKind() == kind::BOUND_VARIABLE)
252		{
253	1	if (std::find(vars.begin(), vars.end(), n) == vars.end())
254		{
255	1	vars.push_back(n);
256		}
257	1	return;
258		}
259		}
260
261	1	EnumStreamPermutation::PermutationState::PermutationState(
262	1	const std::vector<Node>& vars)
263		{
264	1	d_vars = vars;
265	1	d_curr_ind = 0;
266	1	d_seq.resize(vars.size());
267	1	std::fill(d_seq.begin(), d_seq.end(), 0);
268		// initialize variable indices
269	1	d_last_perm.resize(vars.size());
270	1	std::iota(d_last_perm.begin(), d_last_perm.end(), 0);
271	1	}
272
273	1	void EnumStreamPermutation::PermutationState::reset()
274		{
275	1	d_curr_ind = 0;
276	1	std::fill(d_seq.begin(), d_seq.end(), 0);
277	1	std::iota(d_last_perm.begin(), d_last_perm.end(), 0);
278	1	}
279
280		const std::vector<Node>& EnumStreamPermutation::PermutationState::getVars()
281		const
282		{
283		return d_vars;
284		}
285
286		void EnumStreamPermutation::PermutationState::getLastPerm(
287		std::vector<Node>& vars)
288		{
289		for (unsigned i = 0, size = d_last_perm.size(); i < size; ++i)
290		{
291		if (Trace.isOn("synth-stream-concrete"))
292		{
293		std::stringstream ss;
294		TermDbSygus::toStreamSygus(ss, d_vars[d_last_perm[i]]);
295		Trace("synth-stream-concrete") << " " << ss.str();
296		}
297		vars.push_back(d_vars[d_last_perm[i]]);
298		}
299		}
300
301	2	bool EnumStreamPermutation::PermutationState::getNextPermutation()
302		{
303		// exhausted permutations
304	2	if (d_curr_ind == d_vars.size())
305		{
306	1	Trace("synth-stream-concrete-debug2") << "exhausted perms, ";
307	1	return false;
308		}
309	1	if (d_seq[d_curr_ind] >= d_curr_ind)
310		{
311	1	d_seq[d_curr_ind] = 0;
312	1	d_curr_ind++;
313	1	return getNextPermutation();
314		}
315		if (d_curr_ind % 2 == 0)
316		{
317		// swap with first element
318		std::swap(d_last_perm[0], d_last_perm[d_curr_ind]);
319		}
320		else
321		{
322		// swap with element in index in sequence of current index
323		std::swap(d_last_perm[d_seq[d_curr_ind]], d_last_perm[d_curr_ind]);
324		}
325		d_seq[d_curr_ind] += 1;
326		d_curr_ind = 0;
327		return true;
328		}
329
330	1	EnumStreamSubstitution::EnumStreamSubstitution(quantifiers::TermDbSygus* tds)
331	1	: d_tds(tds), d_stream_permutations(tds), d_curr_ind(0)
332		{
333	1	}
334
335	1	void EnumStreamSubstitution::initialize(TypeNode tn)
336		{
337	1	d_tn = tn;
338		// get variables in value's type
339	2	Node var_list = tn.getDType().getSygusVarList();
340		// get subtypes in value's type
341	1	NodeManager* nm = NodeManager::currentNM();
342	1	SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
343	2	std::vector<TypeNode> sf_types;
344	1	ti.getSubfieldTypes(sf_types);
345		// associate variables with constructors in all subfield types
346	3	for (const Node& v : var_list)
347		{
348		// collect constructors for variable in all subtypes
349	4	for (const TypeNode& stn : sf_types)
350		{
351	2	const DType& dt = stn.getDType();
352	8	for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
353		{
354	6	if (dt[i].getNumArgs() == 0 && dt[i].getSygusOp() == v)
355		{
356	2	d_var_tn_cons[v][stn] =
357	4	nm->mkNode(APPLY_CONSTRUCTOR, dt[i].getConstructor());
358		}
359		}
360		}
361		}
362		// split initial variables into classes
363	3	for (const Node& v : var_list)
364		{
365	2	Assert(ti.getSubclassForVar(v) > 0);
366	2	d_var_classes[ti.getSubclassForVar(v)].push_back(v);
367		}
368	1	}
369
370	1	void EnumStreamSubstitution::resetValue(Node value)
371		{
372	1	if (Trace.isOn("synth-stream-concrete"))
373		{
374		std::stringstream ss;
375		TermDbSygus::toStreamSygus(ss, value);
376		Trace("synth-stream-concrete")
377		<< " * Streaming concrete: registering value " << ss.str() << "\n";
378		}
379	1	d_last = Node::null();
380	1	d_value = value;
381		// reset permutation util
382	1	d_stream_permutations.reset(value);
383		// reset combination utils
384	1	d_curr_ind = 0;
385	1	d_comb_state_class.clear();
386	1	Trace("synth-stream-concrete") << " ..combining vars :";
387	2	for (const std::pair<const unsigned, std::vector<Node>>& p : d_var_classes)
388		{
389		// ignore classes without variables being permuted
390	1	unsigned perm_var_class_sz = d_stream_permutations.getVarClassSize(p.first);
391	1	if (perm_var_class_sz == 0)
392		{
393		continue;
394		}
395	3	d_comb_state_class.push_back(CombinationState(
396	2	p.second.size(), perm_var_class_sz, p.first, p.second));
397	1	if (Trace.isOn("synth-stream-concrete"))
398		{
399		Trace("synth-stream-concrete")
400		<< " " << p.first << " -> " << perm_var_class_sz << " from [ ";
401		for (const Node& var : p.second)
402		{
403		std::stringstream ss;
404		TermDbSygus::toStreamSygus(ss, var);
405		Trace("synth-stream-concrete") << " " << ss.str();
406		}
407		Trace("synth-stream-concrete") << " ]";
408		}
409		}
410	1	Trace("synth-stream-concrete") << "\n";
411	1	}
412
413	3	Node EnumStreamSubstitution::getNext()
414		{
415	3	if (Trace.isOn("synth-stream-concrete"))
416		{
417		std::stringstream ss;
418		TermDbSygus::toStreamSygus(ss, d_value);
419		Trace("synth-stream-concrete")
420		<< " ..streaming next combination of " << ss.str() << "\n";
421		}
422	3	unsigned n_classes = d_comb_state_class.size();
423		// intial case
424	3	if (d_last.isNull())
425		{
426	1	d_last = d_stream_permutations.getNext();
427		}
428		else
429		{
430	2	bool new_comb = false;
431	6	while (!new_comb && d_curr_ind < n_classes)
432		{
433	2	if (d_comb_state_class[d_curr_ind].getNextCombination())
434		{
435	1	new_comb = true;
436	2	Trace("synth-stream-concrete-debug2")
437	1	<< " ....class " << d_curr_ind << " has new comb\n";
438	1	d_curr_ind = 0;
439		}
440		else
441		{
442	2	Trace("synth-stream-concrete-debug2")
443	1	<< " ....class " << d_curr_ind << " reset\n";
444	1	d_comb_state_class[d_curr_ind].reset();
445	1	d_curr_ind++;
446		}
447		}
448		// no new combination
449	2	if (!new_comb)
450		{
451	2	Trace("synth-stream-concrete")
452		<< " ..no new comb, get next permutation\n ....total combs until "
453	1	"here : "
454	1	<< d_comb_values.size() << "\n";
455	1	d_last = d_stream_permutations.getNext();
456		// exhausted permutations
457	1	if (d_last.isNull())
458		{
459	1	Trace("synth-stream-concrete") << " ..no new comb, return null\n";
460	1	return Node::null();
461		}
462		// reset combination classes for next permutation
463		d_curr_ind = 0;
464		for (unsigned i = 0, size = d_comb_state_class.size(); i < size; ++i)
465		{
466		d_comb_state_class[i].reset();
467		}
468		}
469		}
470	2	if (Trace.isOn("synth-stream-concrete-debug"))
471		{
472		std::stringstream ss;
473		TermDbSygus::toStreamSygus(ss, d_last);
474		Trace("synth-stream-concrete-debug")
475		<< " ..using base perm " << ss.str() << "\n";
476		}
477		// building substitution
478	4	std::vector<Node> domain_sub, range_sub;
479	4	for (unsigned i = 0, size = d_comb_state_class.size(); i < size; ++i)
480		{
481	4	Trace("synth-stream-concrete")
482	4	<< " ..comb for class " << d_comb_state_class[i].getSubclassId()
483	2	<< " is";
484	4	std::vector<Node> raw_sub;
485	2	d_comb_state_class[i].getLastComb(raw_sub);
486		// retrieve variables for substitution domain
487		const std::vector<Node>& domain_sub_class =
488		d_stream_permutations.getVarsClass(
489	2	d_comb_state_class[i].getSubclassId());
490	2	Assert(domain_sub_class.size() == raw_sub.size());
491		// build proper substitution based on variables types and constructors
492	4	for (unsigned j = 0, size_j = raw_sub.size(); j < size_j; ++j)
493		{
494	2	for (std::pair<const TypeNode, Node>& p :
495	2	d_var_tn_cons[domain_sub_class[j]])
496		{
497		// get constructor of type p.first from variable being permuted
498	2	domain_sub.push_back(p.second);
499		// get constructor of type p.first from variable to be permuted for
500	2	range_sub.push_back(d_var_tn_cons[raw_sub[j]][p.first]);
501	4	Trace("synth-stream-concrete-debug2")
502	2	<< "\n ....{ adding " << domain_sub.back() << " ["
503	4	<< domain_sub.back().getType() << "] -> " << range_sub.back()
504	2	<< " [" << range_sub.back().getType() << "] }";
505		}
506		}
507	2	Trace("synth-stream-concrete") << "\n";
508		}
509		Node comb_value = d_last.substitute(
510	4	domain_sub.begin(), domain_sub.end(), range_sub.begin(), range_sub.end());
511		// the new combination value should be fresh, modulo rewriting, by
512		// construction (unless it's equiv to a constant, e.g. true / false)
513		Node builtin_comb_value =
514	4	d_tds->sygusToBuiltin(comb_value, comb_value.getType());
515	2	if (options::sygusSymBreakDynamic())
516		{
517	2	builtin_comb_value =
518	4	d_tds->getExtRewriter()->extendedRewrite(builtin_comb_value);
519		}
520	2	if (Trace.isOn("synth-stream-concrete"))
521		{
522		std::stringstream ss;
523		TermDbSygus::toStreamSygus(ss, comb_value);
524		Trace("synth-stream-concrete")
525		<< " ....register new comb value " << ss.str()
526		<< " with rewritten form " << builtin_comb_value
527		<< (builtin_comb_value.isConst() ? " (isConst)" : "") << "\n";
528		}
529	4	if (!builtin_comb_value.isConst()
530	2	&& !d_comb_values.insert(builtin_comb_value).second)
531		{
532		if (Trace.isOn("synth-stream-concrete"))
533		{
534		std::stringstream ss, ss1;
535		TermDbSygus::toStreamSygus(ss, comb_value);
536		Trace("synth-stream-concrete")
537		<< " ..term " << ss.str() << " is REDUNDANT with " << builtin_comb_value
538		<< "\n ..excluding all other concretizations (had "
539		<< d_comb_values.size() << " already)\n\n";
540		}
541		return Node::null();
542		}
543	2	if (Trace.isOn("synth-stream-concrete"))
544		{
545		std::stringstream ss;
546		TermDbSygus::toStreamSygus(ss, comb_value);
547		Trace("synth-stream-concrete")
548		<< " ..return new comb " << ss.str() << "\n\n";
549		}
550	2	return comb_value;
551		}
552
553	1	EnumStreamSubstitution::CombinationState::CombinationState(
554	1	unsigned n, unsigned k, unsigned subclass_id, const std::vector<Node>& vars)
555	1	: d_n(n), d_k(k)
556		{
557	1	Assert(!vars.empty());
558	1	Assert(k <= n);
559	1	d_last_comb.resize(k);
560	1	std::iota(d_last_comb.begin(), d_last_comb.end(), 0);
561	1	d_vars = vars;
562	1	d_subclass_id = subclass_id;
563	1	}
564
565	4	const unsigned EnumStreamSubstitution::CombinationState::getSubclassId() const
566		{
567	4	return d_subclass_id;
568		}
569
570	1	void EnumStreamSubstitution::CombinationState::reset()
571		{
572	1	std::iota(d_last_comb.begin(), d_last_comb.end(), 0);
573	1	}
574
575	2	void EnumStreamSubstitution::CombinationState::getLastComb(
576		std::vector<Node>& vars)
577		{
578	4	for (unsigned i = 0, size = d_last_comb.size(); i < size; ++i)
579		{
580	2	if (Trace.isOn("synth-stream-concrete"))
581		{
582		std::stringstream ss;
583		TermDbSygus::toStreamSygus(ss, d_vars[d_last_comb[i]]);
584		Trace("synth-stream-concrete") << " " << ss.str();
585		}
586	2	vars.push_back(d_vars[d_last_comb[i]]);
587		}
588	2	}
589
590	2	bool EnumStreamSubstitution::CombinationState::getNextCombination()
591		{
592		// find what to increment
593	2	bool new_comb = false;
594	3	for (int i = d_k - 1; i >= 0; --i)
595		{
596	2	if (d_last_comb[i] < d_n - d_k + i)
597		{
598	1	unsigned j = d_last_comb[i] + 1;
599	3	while (static_cast<unsigned>(i) <= d_k - 1)
600		{
601	1	d_last_comb[i++] = j++;
602		}
603	1	new_comb = true;
604	1	break;
605		}
606		}
607	2	return new_comb;
608		}
609
610	1	void EnumStreamConcrete::initialize(Node e) { d_ess.initialize(e.getType()); }
611	1	void EnumStreamConcrete::addValue(Node v)
612		{
613	1	d_ess.resetValue(v);
614	1	d_currTerm = d_ess.getNext();
615	1	}
616	2	bool EnumStreamConcrete::increment()
617		{
618	2	d_currTerm = d_ess.getNext();
619	2	return !d_currTerm.isNull();
620		}
621	2	Node EnumStreamConcrete::getCurrent() { return d_currTerm; }
622		} // namespace quantifiers
623		} // namespace theory
624	28194	} // namespace cvc5